On Wed, Dec 12, 2018 at 04:32:50PM -0500, Alan Stern wrote:
> On Wed, 12 Dec 2018, Paul E. McKenney wrote:
>
> > OK. How about this one?
> >
> > P0 P1 P2 P3
> > Wa=2 rcu_read_lock() Wc=2 Wd=2
> > memb Wb=2 Rd=0 synchronize_rcu();
> > Rb=0 Rc=0 Ra=0
> > rcu_read_unlock()
> >
> > The model should say that it is allowed. Taking a look...
> >
> > P0 P1 P2 P3
> > Rd=0
> > Wd=2
> > synchronize_rcu();
> > Ra=0
> > Wa=2
> > membs
> > rcu_read_lock()
> > [m01]
> > Rc=0
> > Wc=2
> > [m02] [m03]
> > membe
> > Rb=0
> > Wb=2
> > rcu_read_unlock()
> >
> > Looks allowed to me. If the synchronization of P1 and P2 were
> > interchanged, it should be forbidden:
> >
> > P0 P1 P2 P3
> > Wa=2 Wb=2 rcu_read_lock() Wd=2
> > memb Rc=0 Wc=2 synchronize_rcu();
> > Rb=0 Rd=0 Ra=0
> > rcu_read_unlock()
> >
> > Taking a look...
> >
> > P0 P1 P2 P3
> > rcu_read_lock()
> > Rd=0
> > Wa=2 Wb=2 Wd=2
> > membs synchronize_rcu();
> > [m01]
> > Rc=0
> > Wc=2
> > rcu_read_unlock()
> > [m02] Ra=0 [Forbidden?]
> > membe
> > Rb=0
For one thing, Wb=2 needs to be down here, apologies! Which then ...
> Have you tried writing these as real litmus tests and running them
> through herd?
That comes later, but yes, I will do that.
> > I believe that this ordering forbids the cycle:
> >
> > Wa=1 > membs -> [m01] -> Rc=0 -> Wc=2 -> rcu_read_unlock() ->
> > return from synchronize_rcu() -> Ra
> >
> > Does this make sense, or am I missing something?
>
> It's hard to tell. What you have written here isn't justified by the
> litmus test source code, since the position of m01 in P1's program
> order is undetermined. How do you justify m01 -> Rc, for example?
... justifies Rc=0 following [m01].
> Write it this way instead, using the relations defined in the
> sys_membarrier patch for linux-kernel.cat:
>
> memb ->memb-gp memb ->rcu-link Rc ->memb-rscsi Rc ->rcu-link
>
> rcu_read_unlock ->rcu-rscsi rcu_read_lock ->rcu-link
>
> synchronize_rcu ->rcu-gp synchronize_rcu ->rcu-link memb
>
> Recall that:
>
> memb-gp is the identity relation on sys_membarrier events,
>
> rcu-link includes (po? ; fre ; po),
>
> memb-rscsi is the identity relation on all events,
>
> rcu-rscsi links unlocks to their corresponding locks, and
>
> rcu-gp is the identity relation on synchronize_rcu events.
>
> These facts justify the cycle above.
>
> Leaving off the final rcu-link step, the sequence matches the
> definition of rcu-fence (the relations are memb-gp, memb-rscsi,
> rcu-rscsi, rcu-gp with rcu-links in between). Therefore the cycle is
> forbidden.
Understood, but that would be using the model to check the model. ;-)
Thanx, Paul
