Messages in this thread |  | | Date | Sun, 29 Jan 2023 20:43:05 -0800 | From | "Paul E. McKenney" <> | Subject | Re: [PATCH v2 2/2] tools/memory-model: Make ppo a subrelation of po |
| |
On Sun, Jan 29, 2023 at 09:18:24PM -0500, Alan Stern wrote: > On Sun, Jan 29, 2023 at 03:09:00PM -0800, Paul E. McKenney wrote: > > On Sun, Jan 29, 2023 at 01:43:53PM -0800, Boqun Feng wrote: > > > in lock.cat: > > > > > > (* Allow up to one unmatched LKW per location; more must deadlock *) > > > let UNMATCHED-LKW = LKW \ domain(critical) > > > empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks > > > > > > we rule out deadlocks from the execution candidates we care about. > > > > Thank you, Boqun! > > Actually that's only part of it. The other part is rather obscure: > > (* Generate all co relations, including LKW events but not UL *) > let co0 = co0 | ([IW] ; loc ; [LKW]) | > (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW]) > > Implicitly this says that any lock with no corresponding unlock must > come last in the coherence order, which implies the unmatched-locks rule > (since only one lock event can be last). By itself, the unmatched-locks > rule would not prevent P3 from executing before P1, provided P1 executes > both its lock and unlock.
And thank you, Alan, as well!
And RCU looks to operate in a similar manner:
------------------------------------------------------------------------
C rcudeadlock
{ }
P0(int *a, int *b) { rcu_read_lock(); WRITE_ONCE(*a, 1); synchronize_rcu(); WRITE_ONCE(*b, 1); rcu_read_unlock(); }
P1(int *a, int *b) { int r1; int r2;
r1 = READ_ONCE(*b); smp_mb(); r2 = READ_ONCE(*a); }
exists (1:r1=1 /\ 1:r2=0)
------------------------------------------------------------------------
$ herd7 -conf linux-kernel.cfg rcudeadlock.litmus Test rcudeadlock Allowed States 0 No Witnesses Positive: 0 Negative: 0 Condition exists (1:r1=1 /\ 1:r2=0) Observation rcudeadlock Never 0 0 Time rcudeadlock 0.00 Hash=4f7f336ad39d724d93b089133b00d1e2
------------------------------------------------------------------------
So good enough! ;-)
Thanx, Paul
|  |