Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



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



[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Index of Archives]     [Linux NFS]     [Linux NILFS]     [Linux USB Devel]     [Video for Linux]     [Linux Audio Users]     [Yosemite News]     [Linux Kernel]     [Linux SCSI]

  Powered by Linux