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. 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
