On 2019-06-30, Andrea Parri <andrea.pa...@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
