On Wed, Oct 12, 2022 at 10:26:15AM +0800, Patrick Yingxi Pan wrote: > Nice to know! Never imagined my patch could be more helpful like this. > Thanks guys for the scrutiny! I have queued and pushed this commit, thank you both! Good catch on the herd7 bug!!! Thanx, Paul > Thanx, Patrick > > On Tue, Oct 11, 2022 at 11:04 PM Akira Yokosawa <akiyks@xxxxxxxxx> wrote: > > > > 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
