Re: [RFC PATCH v2 1/2] printk-rb: add a new printk ringbuffer implementation

[John Ogness <john.ogness@linutronix.de>]

On 2019-06-30, Andrea Parri <andrea.parri@amarulasolutions.com> wrote:
>> The significant events for 2 contexts that are accessing the same
>> addresses of a descriptor are:
>> 
>> P0(struct desc *d0)
>> {
>>         // adding a new descriptor d0
>> 
>>         WRITE_ONCE(d0->next, EOL);               // C
>>         WRITE_ONCE(d0->seq, X);                  // D
>>         cmpxchg_release(newest, Y, indexof(d0)); // E
>> }
>> 
>> P1(struct desc *d1)
>> {
>>         // adding a new descriptor d1 that comes after d0
>> 
>>         struct desc *d0;
>>         int r0, r1;
>> 
>>         r0 = READ_ONCE(newest);                 // A
>>         d0 = &array[r0];
>>         r1 = READ_ONCE(d0->seq);                // B
>>         WRITE_ONCE(d0->next, Z);                // F
>> }
>> 
>> d0 is the same address for P0 and P1. (The values of EOL, X, Y, Z are
>> unrelated and irrelevant.)
>
>   (1) If A reads from E, then B reads from D (or from another store
>       to ->seq, not reported in the snippet, which overwrites D)
>
>   (2) If A reads from E, then F overwrites C
>
> This, IIUC, for the informal descriptions of the (intended) guarantees.
> Back to the pairings in question: AFAICT,
>
>   (a) For (1), we rely on the pairing:
>
>         RELEASE from D to E  (matching)  ADDRESS DEP. from A to B
>
>   (b) For (2), we rely on the pairing:
>
>         RELEASE from C to E  (matching)  ADDRESS DEP. from A to F
>
> Does this make sense?

Yes. This is what I needed to see.

> IMO (and assuming that what I wrote above makes some sense), (a-b) and
> (1-2) above, together with the associated annotations of the code/ops,
> provide all the desired and necessary information to document MB5.
>
> For readability purposes, it could be nice to also keep the snippet you
> provided above (but let me stress, again, that such a snippet should be
> integrated with additional information as suggested above).
>
> As to "where to insert the memory barrier documentation", I really have
> no suggestion ATM.  I guess someone would split it (say, before A and E)
> while others could prefer to keep it within a same inline comment.

Thank you. This is the level of formalization I've been looking for. I
will rework the comments (and naming) and post a v3. It is probably best
for you to wait until then to look at this again. (And after going
through such formal processes, even _I_ am having difficulties
understanding what some of my memory barriers are supposed to be
synchronizing.)

John Ogness