On Tue, 11 Oct 2022 21:13:58 +0900, Akira Yokosawa wrote: > On Tue, 11 Oct 2022 19:41:56 +0900, Akira Yokosawa wrote: >> On Tue, 11 Oct 2022 02:48:22 -0700, Paul E. McKenney wrote: >>> 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? >> Ah, you are right! >> I got the Sometimes result from herd7 of herdtools7's current master. >> >> I'll try bisecting herdtools7. > And the bisection points to a very recent commit. > I have opened an issue at https://github.com/herd/herdtools7/issues/433. And Luc has just merged the fix. Now the result reads: --------------------------------------------- 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 --------------------------------------------- $ herd7 -version 7.56+02~dev, Rev: 5a20233c2d0b9ab59b7670a930d2a1bf98de6744 Thanks, Akira > > It looks like Patrick noticed the typo at the best timing. No? ;-) > > Thanks, Akira > >> >> Sorry for the noise. >> >> Thanks, Akira >> >>> >>> $ herd7 -version >>> 7.56+02~dev, Rev: c375ecc537da22070913496ad2043ae501c7ab78 >>> >>> Thanx, Paul
