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, 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



[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