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.
Sorry for the noise.
Thanks, Akira
>
> $ herd7 -version
> 7.56+02~dev, Rev: c375ecc537da22070913496ad2043ae501c7ab78
>
> Thanx, Paul
