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

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

[Patrick Yingxi Pan]

Hello!

According to the context and my understanding of locking primitives, I
suppose the 'exists' clause in the litmus test shouldn't be satisfied.

Signed-off-by: Patrick Pan <pyxchina92929@gmail.com>
---
 memorder/memorder.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/memorder/memorder.tex b/memorder/memorder.tex
index a0a87d0a..9c1846d0 100644
--- a/memorder/memorder.tex
+++ b/memorder/memorder.tex
@@ -3452,7 +3452,7 @@ following subsequent critical sections?
 This question can be answered for the Linux kernel by referring to
 \cref{lst:memorder:Accesses Outside of Critical Sections}
 (\path{C-Lock-outside-across.litmus}).
-Running this litmus test yields the \co{Sometimes} result,
+Running this litmus test yields the \co{Never} result,
 which means that accesses in code leading up to a prior critical section
 is also visible to the current CPU or thread holding that same lock.
 Similarly, code that is placed after a subsequent critical section

base-commit: 7f12a9358e220f3d0c3a0880d01bc283113d7a5b
--

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

[Akira Yokosawa]

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

        Thanks, Akira

> 
> Signed-off-by: Patrick Pan <pyxchina92929@gmail.com>
> ---
>  memorder/memorder.tex | 2 +-
>  1 file changed, 1 insertion(+), 1 deletion(-)
> 
> diff --git a/memorder/memorder.tex b/memorder/memorder.tex
> index a0a87d0a..9c1846d0 100644
> --- a/memorder/memorder.tex
> +++ b/memorder/memorder.tex
> @@ -3452,7 +3452,7 @@ following subsequent critical sections?
>  This question can be answered for the Linux kernel by referring to
>  \cref{lst:memorder:Accesses Outside of Critical Sections}
>  (\path{C-Lock-outside-across.litmus}).
> -Running this litmus test yields the \co{Sometimes} result,
> +Running this litmus test yields the \co{Never} result,
>  which means that accesses in code leading up to a prior critical section
>  is also visible to the current CPU or thread holding that same lock.
>  Similarly, code that is placed after a subsequent critical section
> 
> base-commit: 7f12a9358e220f3d0c3a0880d01bc283113d7a5b
> --

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

[Paul E. McKenney]

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

							Thanx, Paul

> > Signed-off-by: Patrick Pan <pyxchina92929@gmail.com>
> > ---
> >  memorder/memorder.tex | 2 +-
> >  1 file changed, 1 insertion(+), 1 deletion(-)
> > 
> > diff --git a/memorder/memorder.tex b/memorder/memorder.tex
> > index a0a87d0a..9c1846d0 100644
> > --- a/memorder/memorder.tex
> > +++ b/memorder/memorder.tex
> > @@ -3452,7 +3452,7 @@ following subsequent critical sections?
> >  This question can be answered for the Linux kernel by referring to
> >  \cref{lst:memorder:Accesses Outside of Critical Sections}
> >  (\path{C-Lock-outside-across.litmus}).
> > -Running this litmus test yields the \co{Sometimes} result,
> > +Running this litmus test yields the \co{Never} result,
> >  which means that accesses in code leading up to a prior critical section
> >  is also visible to the current CPU or thread holding that same lock.
> >  Similarly, code that is placed after a subsequent critical section
> > 
> > base-commit: 7f12a9358e220f3d0c3a0880d01bc283113d7a5b
> > --

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

[Akira Yokosawa]

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.

        Thanks, Akira

> 
> 							Thanx, Paul
> 
>>> Signed-off-by: Patrick Pan <pyxchina92929@gmail.com>
>>> ---
>>>  memorder/memorder.tex | 2 +-
>>>  1 file changed, 1 insertion(+), 1 deletion(-)
>>>
>>> diff --git a/memorder/memorder.tex b/memorder/memorder.tex
>>> index a0a87d0a..9c1846d0 100644
>>> --- a/memorder/memorder.tex
>>> +++ b/memorder/memorder.tex
>>> @@ -3452,7 +3452,7 @@ following subsequent critical sections?
>>>  This question can be answered for the Linux kernel by referring to
>>>  \cref{lst:memorder:Accesses Outside of Critical Sections}
>>>  (\path{C-Lock-outside-across.litmus}).
>>> -Running this litmus test yields the \co{Sometimes} result,
>>> +Running this litmus test yields the \co{Never} result,
>>>  which means that accesses in code leading up to a prior critical section
>>>  is also visible to the current CPU or thread holding that same lock.
>>>  Similarly, code that is placed after a subsequent critical section
>>>
>>> base-commit: 7f12a9358e220f3d0c3a0880d01bc283113d7a5b
>>> --

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

[Paul E. McKenney]

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?

$ herd7 -version
7.56+02~dev, Rev: c375ecc537da22070913496ad2043ae501c7ab78

							Thanx, Paul

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

[Akira Yokosawa]

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

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

[Akira Yokosawa]

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

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

[Akira Yokosawa]

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

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

[Patrick Yingxi Pan]

Nice to know! Never imagined my patch could be more helpful like this.
Thanks guys for the scrutiny!

            Thanx, Patrick

On Tue, Oct 11, 2022 at 11:04 PM Akira Yokosawa <akiyks@gmail.com> 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