> > 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) > > Which r0 the above exists rule refers to, please? > Do both P0 and P1 define r0 by purpose?
"1:r0" is the value returned by the above READ_ONCE(*y), following the convention [thread number]:[local variable]; but yes, I could probably have saved you this question by picking a different name, ;-) sorry. > > > 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; > > Do you have any explanation how r0=x; x=2; could happen, please? I should have remarked: the states listed here lose their significance when there is a data race: "data race" is LKMM's way of saying "I give up, I'm unable to list all the reachable states; your call...". ;-) This example is "complicated", e.g., by the tearing of the plain read, tearing which is envisaged/modelled by the LKMM: however, this tearing doesn't explain the "1:r0=x; x=2;" state by itself, AFAICT. Said this, I'm not sure how I copied this output... For completeness, I report the full/intended test at the bottom of my email. > > Does the ommited READ_ONCE allows to do r0 = (*y) twice > before and after *r0 = 1? > Or the two operations P1 can be called in any order? > > I am sorry if it obvious. Feel free to ask me to re-read Paul's > articles on LWN more times or point me to another resources. > > > > > 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 > > So, it might be even worse. Do I get it correctly? Worse than I was hoping..., definitely! ;-) Andrea --- C S+ponarelease+addrnana { 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 = *y; *r0 = 1; } exists (1:r0=x /\ x=2)