Re: [PATCH printk v3 09/14] printk: Wait for all reserved records with pr_flush()

[Petr Mladek]

On Mon 2024-02-05 14:39:03, John Ogness wrote:
> On 2024-01-31, Petr Mladek <pmladek@xxxxxxxx> wrote:
> >> +	last_finalized_seq = desc_last_finalized_seq(rb);
> >> +
> >> +	/*
> >> +	 * @head_id is loaded after @last_finalized_seq to ensure that it is
> >> +	 * at or beyond @last_finalized_seq.

Maybe we could do it the following way. I would slightly update the
above comment:

	 * @head_id is loaded after @last_finalized_seq to ensure that
	 * it points to the record with @last_finalized_seq or newer.

I have got it even from the previous record but I had to think about
it a  bit. You always wanted to make a difference between the IDs
and sequence numbers.

Anyway, this comment makes the safety kind of obvious.

@head_id always have to be updated when the related record is reserved.
And all other CPUs have to see it so that they have to bump @head_id
for a newer record.

And @last_finalized_seq points to an already finalized record.
If a record is finalized then other CPUs must be able to
read valid data.

Maybe, we should add the two above paragraphs into the human
readable part of the comment as well. They describe some
basics of the design. Everything would blow up when
neither of them is true.

My motivation is that a good human friendly description
helps to understand what the code does and that it is
"obviously" correct.

I agree that the below precise description is useful.
But people should need it only when they want to prove
or revisit the human friendly claim.

> >> +	 *
> >> +	 * Memory barrier involvement:
> >> +	 *
> >> +	 * If desc_last_finalized_seq:A reads from
> >> +	 * desc_update_last_finalized:A, then
> >> +	 * prb_next_reserve_seq:A reads from desc_reserve:D.
> >> +	 *
> >> +	 * Relies on:
> >> +	 *
> >> +	 * RELEASE from desc_reserve:D to desc_update_last_finalized:A
> >> +	 *    matching
> >> +	 * ACQUIRE from desc_last_finalized_seq:A to prb_next_reserve_seq:A
> >> +	 *
> >> +	 * Note: desc_reserve:D and desc_update_last_finalized:A can be
> >> +	 *       different CPUs. However, the desc_update_last_finalized:A CPU
> >> +	 *       (which performs the release) must have previously seen
> >> +	 *       desc_read:C, which implies desc_reserve:D can be seen.
> >
> > The most tricky part is desc_reserve:D. It is a supper complicated
> > barrier which guarantees many things. But I think that there are
> > many more write barriers before the allocated descriptor reaches
> > finalized state. So that it should be easier to prove the correctness
> > here by other easier barriers.
> 
> Yes, desc_reserve:D provides memory barriers for several orderings. But
> it is _not_ providing a memory barrier for this ordering. It only marks
> where @head_id is stored.
> 
> The only memory barriers involved here are desc_update_last_finalized:A
> and its counterpart desc_last_finalized_seq:A.
> 
> CPU0                                 CPU1
> ====                                 ====
> store(head_id)
> store_release(last_finalized_seq)    load_acquire(last_finalized_seq)
>                                      load(head_id)
> 
> > To make it clear. I am all for keeping the above precise description
> > as is. I just think about adding one more human friendly note which
> > might help future generations to understand the correctness an easier
> > way.  Something like:
> >
> > 	* Note: The above description might be hard to follow because
> > 	*	desc_reserve:D is a multi-purpose barrier. But this is
> > 	*	just the first barrier which makes sure that @head_id
> > 	*	is updated before the reserved descriptor gets finalized
> > 	*	and updates @last_finalized_seq.
> > 	*
> > 	*	There are more release barriers in between, especially,
> > 	*	desc_reserve:F and desc_update_last_finalized:A. Also these make
> > 	*	sure that the desc_last_finalized_seq:A acquire barrier allows
> > 	*	to read @head_id related to @last_finalized_seq or newer.
> 
> Non-global memory barriers must operate on the same memory. In this
> case, the acquire/release memory barriers are operating on
> @last_finalized_seq. The other ordered memory load in this situation is
> for @head_id, so it makes sense to specify the store of @head_id as the
> start of the release block.

I am a bit confused by the "non-global memory barrier" here. I would
expect that acquire()/release() variants provide global barriers.
They are used to implement locking.

Anyway, I am fine with keeping this precise description as is
if we make the correctness more "obvious" from the human friendly
part of the comment.

I am sorry for all the nitpicking. I want to make sure that
the entire comment is correct including the precise part.
This was not easy so I thought about ways to make it easier.
Sigh.

Anyway, I do not want to block the patchset much longer
because of this formal things.

> > BTW: It came to my mind whether the logic might be more
> >      straightforward if we store desc_ring->next_finalized_seq instead
> >      of @last_finalized_seq.
> 
> I thought about this as well. But I felt like the meaning was a bit
> confusing. Also @head_id points to the latest reserved descriptor, so it
> makes the code a bit easier to follow when creating a diff based on the
> latest finalized descriptor.

Fair enough.

Best Regards,
Petr