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@xxxxxxxxx>
> > ---
> > 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
> > --
