Re: numlist_push() barriers Re: [RFC PATCH v4 1/9] printk-rb: add a new printk ringbuffer implementation

[Petr Mladek]

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