Messages in this thread | | | Date | Mon, 26 Aug 2019 16:10:58 +0200 | From | Petr Mladek <> | Subject | Re: numlist_push() barriers Re: [RFC PATCH v4 1/9] printk-rb: add a new printk ringbuffer implementation |
| |
On Mon 2019-08-26 10:34:36, Andrea Parri wrote: > > > + /* > > > + * 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)
Which r0 the above exists rule refers to, please? Do both P0 and P1 define r0 by purpose?
> 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?
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?
Best Regards, Petr
| |