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

From: Andrea Parri <parri.andrea@gmail.com>
To: Petr Mladek <pmladek@suse.com>
Cc: Sergey Senozhatsky <sergey.senozhatsky@gmail.com>,
	Sergey Senozhatsky <sergey.senozhatsky.work@gmail.com>,
	Steven Rostedt <rostedt@goodmis.org>,
	Brendan Higgins <brendanhiggins@google.com>,
	Peter Zijlstra <peterz@infradead.org>,
	John Ogness <john.ogness@linutronix.de>,
	Thomas Gleixner <tglx@linutronix.de>,
	Linus Torvalds <torvalds@linux-foundation.org>,
	Greg Kroah-Hartman <gregkh@linuxfoundation.org>,
	linux-kernel@vger.kernel.org
Subject: Re: numlist_push() barriers Re: [RFC PATCH v4 1/9] printk-rb: add a new printk ringbuffer implementation
Date: Mon, 26 Aug 2019 18:01:13 +0200	[thread overview]
Message-ID: <20190826160113.GA2062@andrea> (raw)
In-Reply-To: <20190826141058.y6idkqpjqkpbv5s7@pathway.suse.cz>

> > 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)