> > + /*
> > + * bA:
> > + *
> > + * Setup the node to be a list terminator: next_id == id.
> > + */
> > + WRITE_ONCE(n->next_id, id);
>
> Do we need WRITE_ONCE() here?
> Both "n" and "id" are given as parameters and do not change.
> The assigment must be done before "id" is set as nl->head_id.
> The ordering is enforced by cmpxchg_release().
(Disclaimer: this is still a very much debated issue...)
According to the LKMM, this question boils down to the question:
Is there "ordering"/synchronization between the above access and
the "matching accesses" bF and aA' to the same location?
Again according to the LKMM's analysis, such synchronization is provided
by the RELEASE -> "reads-from" -> ADDR relation. (Encoding address dep.
in litmus tests is kind of tricky but possible, e.g., for the pattern in
question, we could write/model as follows:
C S+ponarelease+addroncena
{
int *y = &a;
}
P0(int *x, int **y, int *a)
{
int *r0;
*x = 2;
r0 = cmpxchg_release(y, a, x);
}
P1(int *x, int **y)
{
int *r0;
r0 = READ_ONCE(*y);
*r0 = 1;
}
exists (1:r0=x /\ x=2)
Then
$ herd7 -conf linux-kernel.cfg S+ponarelease+addroncena
Test S+ponarelease+addroncena Allowed
States 2
1:r0=a; x=2;
1:r0=x; x=1;
No
Witnesses
Positive: 0 Negative: 2
Condition exists (1:r0=x /\ x=2)
Observation S+ponarelease+addroncena Never 0 2
Time S+ponarelease+addroncena 0.01
Hash=7eaf7b5e95419a3c352d7fd50b9cd0d5
that is, the test is not racy and the "exists" clause is not satisfiable
in the LKMM. Notice that _if the READ_ONCE(*y) in P1 were replaced by a
plain read, then we would obtain:
Test S+ponarelease+addrnana Allowed
States 2
1:r0=x; x=1;
1:r0=x; x=2;
Ok
Witnesses
Positive: 1 Negative: 1
Flag data-race [ <-- the LKMM warns about a data-race ]
Condition exists (1:r0=x /\ x=2)
Observation S+ponarelease+addrnana Sometimes 1 1
Time S+ponarelease+addrnana 0.00
Hash=a61acf2e8e51c2129d33ddf5e4c76a49
N.B. This analysis generally depends on the assumption that every marked
access (e.g., the cmpxchg_release() called out above and the READ_ONCE()
heading the address dependencies) are _single-copy atomic, an assumption
which has been recently shown to _not be valid in such generality:
https://lkml.kernel.org/r/20190821103200.kpufwtviqhpbuv2n@willie-the-truck
(Bug in the LKMM? or in the Linux implementation of these primitives? or
in the compiler? your blame here...)
[...]
> > + /*
> > + * bD:
> > + *
> > + * Set @seq to +1 of @seq from the previous head.
> > + *
> > + * Memory barrier involvement:
> > + *
> > + * If bB reads from bE, then bC->aA reads from bD.
> > + *
> > + * Relies on:
> > + *
> > + * RELEASE from bD to bE
> > + * matching
> > + * ADDRESS DEP. from bB to bC->aA
> > + */
> > + WRITE_ONCE(n->seq, seq + 1);
>
> Do we really need WRITE_ONCE() here?
> It is the same problem as with setting n->next_id above.
Same considerations as above would apply here.
Andrea
