Re: [PATCH v7 6/6] rcu/segcblist: Add additional comments to explain smp_mb()

[Alan Stern <stern@rowland.harvard.edu>]

On Sun, Oct 18, 2020 at 01:45:31PM -0700, Joel Fernandes wrote:
> Hi,
> Thanks Alan for your replies.

You're welcome.

> > > C rcubarrier+ctrldep
> > >
> > > (*
> > >  * Result: Never
> > >  *
> > >  * This litmus test shows that rcu_barrier (P1) prematurely
> > >  * returning by reading len 0 can cause issues if P0 does
> > >  * NOT have a smb_mb() after WRITE_ONCE(len, 1).
> > >  * mod_data == 2 means module was unloaded (so data is garbage).
> > >  *)
> > >
> > > { int len = 0; int enq = 0; }
> > >
> > > P0(int *len, int *mod_data, int *enq)
> > > {
> > >       int r0;
> > >
> > >       WRITE_ONCE(*len, 1);
> > >       smp_mb();               /* Needed! */
> > >       WRITE_ONCE(*enq, 1);
> > >
> > >       r0 = READ_ONCE(*mod_data);
> > > }
> > >
> > > P1(int *len, int *mod_data, int *enq)
> > > {
> > >       int r0;
> > >       int r1;
> > >
> > >       r1 = READ_ONCE(*enq);
> > >
> > >       // barrier Just for test purpose ("exists" clause) to force the..
> > >       // ..rcu_barrier() to see enq before len
> > >       smp_mb();
> > >       r0 = READ_ONCE(*len);
> > >
> > >       // implicit memory barrier due to conditional */
> > >       if (r0 == 0)
> > >               WRITE_ONCE(*mod_data, 2);
> > > }
> > >
> > > // Did P0 read garbage?
> > > exists (0:r0=2 /\ 1:r0=0 /\ 1:r1=1)
> >
> > Is this exists clause really what you meant?  Not only can it not be
> > satisfied, it couldn't even be satisfied if you left out the 0:r0=2
> > part.  And smp_mb() is stronger than neessary to enforce this.
> 
> This is indeed what I meant.
> 
> Maybe the exists clause can be simplified, but I just wanted to
> enforce that P1 saw P0's write to enq before seeing anything else.
> 
> Per my test, if you remove the smp_mb() in P0, the test will fail.
> 
> What I wanted to show was P0() seeing mod_data == 2 is bad and should
> never happen (as that implies rcu_barrier() saw len == 0 when it
> should not have). Maybe you can point out what is my test missing?

That's a little tricky, since I don't understand what the test is trying 
to say.

For example, you could change the exists clause to omit "/\ 1:r1=1".  
Maybe that's not a meaningful thing to do... but then it could be 
satisfied simply by having P1 run to completion before P0 starts.

Or you could leave the exists clause as it is and remove the smp_mb() 
from P0.  As you said, that version of the test would also fail since P0 
could then reorder its two writes.

> > However, some memory barrier is needed.  If the smp_mb() in P1 were
> > omitted then P1 would be free to reorder its reads, and the exists
> > clause could be satisfied as follows:
> >
> >         P0                      P1
> >         ------------------------------------------
> >                                 Read len = 0
> >         Write len = 1
> >         smp_mb();
> >         Write enq = 1
> >                                 Read enq = 1
> >                                 Write mod_data = 2
> >         Read mod_data = 2
> 
> Right, so I think I got it right then. I want to show that the control
> dependency in P1 provides the needed ordering. The extra smp_mb() I
> added was just so that I could force P1 to see P0's enqueue.

Yes, it's quite correct that because of the control dependency, P1 
cannot write mod_data before it reads the value of len.

Alan Stern