On Tue, Oct 11, 2022 at 06:21:16PM +0900, Akira Yokosawa wrote: > On Tue, 11 Oct 2022 01:58:25 -0700, Paul E. McKenney wrote: > > On Tue, Oct 11, 2022 at 05:37:55PM +0900, Akira Yokosawa wrote: > >> [+CC: Paul] > >> > >> Hi, > >> > >> On Tue, 11 Oct 2022 11:17:25 +0800, Patrick Yingxi Pan wrote: > >>> Hello! > >>> > >>> According to the context and my understanding of locking primitives, I > >>> suppose the 'exists' clause in the litmus test shouldn't be satisfied. > >> > >> I agree with you in that section 15.4.2.2 is described as if the > >> result were "Never". > >> > >> However, if you run herd7 on the litmus test, you'll get: > >> > >> ------------------------------------------------ > >> Test Lock-outside-across Allowed > >> States 4 > >> 0:r1=0; 1:r1=0; > >> 0:r1=0; 1:r1=1; > >> 0:r1=1; 1:r1=0; > >> 0:r1=1; 1:r1=1; > >> Ok > >> Witnesses > >> Positive: 2 Negative: 12 > >> Condition exists (0:r1=0 /\ 1:r1=0) > >> Observation Lock-outside-across Sometimes 2 12 <-- > >> Time Lock-outside-across 0.02 > >> Hash=06337358bba3d1ed44db8ea81cf1d236 > >> ------------------------------------------------ > >> > >> That said, I'm not in the position of deciding LKMM is right or not. > > > > Thank you for checking, Akira! > > > > This is the following litmus test? > > > > CodeSamples/formal/herd/C-Lock-outside-across.litmus > > Yes, it is. Strange. This is what I get from it on the -rcu dev branch as well as on v6.0 and v5.19: $ herd7 -conf linux-kernel.cfg /home/git/perfbook/CodeSamples/formal/herd/C-Lock-outside-across.litmus Test Lock-outside-across Allowed States 3 0:r1=0; 1:r1=1; 0:r1=1; 1:r1=0; 0:r1=1; 1:r1=1; No Witnesses Positive: 0 Negative: 3 Condition exists (0:r1=0 /\ 1:r1=0) Observation Lock-outside-across Never 0 3 Time Lock-outside-across 0.01 Hash=06337358bba3d1ed44db8ea81cf1d236 Am I running a bad version of herd7 or something? $ herd7 -version 7.56+02~dev, Rev: c375ecc537da22070913496ad2043ae501c7ab78 Thanx, Paul
