* [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. @ 2022-10-11 3:17 Patrick Yingxi Pan 2022-10-11 8:37 ` Akira Yokosawa 0 siblings, 1 reply; 9+ messages in thread From: Patrick Yingxi Pan @ 2022-10-11 3:17 UTC (permalink / raw) To: perfbook 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 -- ^ permalink raw reply related [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 3:17 [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied Patrick Yingxi Pan @ 2022-10-11 8:37 ` Akira Yokosawa 2022-10-11 8:58 ` Paul E. McKenney 0 siblings, 1 reply; 9+ messages in thread From: Akira Yokosawa @ 2022-10-11 8:37 UTC (permalink / raw) To: Patrick Yingxi Pan; +Cc: Paul E. McKenney, perfbook, 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 > -- ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 8:37 ` Akira Yokosawa @ 2022-10-11 8:58 ` Paul E. McKenney 2022-10-11 9:21 ` Akira Yokosawa 0 siblings, 1 reply; 9+ messages in thread From: Paul E. McKenney @ 2022-10-11 8:58 UTC (permalink / raw) To: Akira Yokosawa; +Cc: Patrick Yingxi Pan, perfbook 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 > > -- ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 8:58 ` Paul E. McKenney @ 2022-10-11 9:21 ` Akira Yokosawa 2022-10-11 9:48 ` Paul E. McKenney 0 siblings, 1 reply; 9+ messages in thread From: Akira Yokosawa @ 2022-10-11 9:21 UTC (permalink / raw) To: Paul E. McKenney; +Cc: Patrick Yingxi Pan, perfbook, 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 >>> -- ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 9:21 ` Akira Yokosawa @ 2022-10-11 9:48 ` Paul E. McKenney 2022-10-11 10:41 ` Akira Yokosawa 0 siblings, 1 reply; 9+ messages in thread From: Paul E. McKenney @ 2022-10-11 9:48 UTC (permalink / raw) To: Akira Yokosawa; +Cc: Patrick Yingxi Pan, perfbook 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 9:48 ` Paul E. McKenney @ 2022-10-11 10:41 ` Akira Yokosawa 2022-10-11 12:13 ` Akira Yokosawa 0 siblings, 1 reply; 9+ messages in thread From: Akira Yokosawa @ 2022-10-11 10:41 UTC (permalink / raw) To: Paul E. McKenney; +Cc: Patrick Yingxi Pan, perfbook 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 10:41 ` Akira Yokosawa @ 2022-10-11 12:13 ` Akira Yokosawa 2022-10-11 15:04 ` Akira Yokosawa 0 siblings, 1 reply; 9+ messages in thread From: Akira Yokosawa @ 2022-10-11 12:13 UTC (permalink / raw) To: Paul E. McKenney; +Cc: Patrick Yingxi Pan, perfbook 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 12:13 ` Akira Yokosawa @ 2022-10-11 15:04 ` Akira Yokosawa 2022-10-12 2:26 ` Patrick Yingxi Pan 0 siblings, 1 reply; 9+ messages in thread From: Akira Yokosawa @ 2022-10-11 15:04 UTC (permalink / raw) To: Paul E. McKenney; +Cc: Patrick Yingxi Pan, perfbook, 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
* Re: [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied. 2022-10-11 15:04 ` Akira Yokosawa @ 2022-10-12 2:26 ` Patrick Yingxi Pan 0 siblings, 0 replies; 9+ messages in thread From: Patrick Yingxi Pan @ 2022-10-12 2:26 UTC (permalink / raw) To: Akira Yokosawa; +Cc: Paul E. McKenney, perfbook 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 ^ permalink raw reply [flat|nested] 9+ messages in thread
end of thread, other threads:[~2022-10-12 2:26 UTC | newest] Thread overview: 9+ messages (download: mbox.gz follow: Atom feed -- links below jump to the message on this page -- 2022-10-11 3:17 [PATCH] memorder.tex: the exists clause in Listing 15.35 should never be satisfied Patrick Yingxi Pan 2022-10-11 8:37 ` Akira Yokosawa 2022-10-11 8:58 ` Paul E. McKenney 2022-10-11 9:21 ` Akira Yokosawa 2022-10-11 9:48 ` Paul E. McKenney 2022-10-11 10:41 ` Akira Yokosawa 2022-10-11 12:13 ` Akira Yokosawa 2022-10-11 15:04 ` Akira Yokosawa 2022-10-12 2:26 ` Patrick Yingxi Pan
This is an external index of several public inboxes, see mirroring instructions on how to clone and mirror all data and code used by this external index.