memorder.tex: Fix typos in description of litmus test C-ISA2+o-r+a-r+a-r+a-o

This is the only patch for the second half of Chapter Memory Ordering. Please take a look. Thanks.

Quoted 1 line

From 0e43c93660383b7560c55131754dbc4bfaf13052 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Mon, 5 Nov 2018 20:27:02 +0900
Subject: [PATCH] memorder: Fix line numbers by applying new scheme to C-ISA2+o-r+a-r+a-r+a-o

Line numbers referring to Listing 15.23 don't match the line counts in the snippet. Fix this by putting labels in the source of the litmus test and referring them by \lnref{} macros.

Reported-by Junchang Wang <[email protected]>

Signed-off-by Akira Yokosawa <[email protected]>

---

Quoted 3 lines · Junchang Wang

This is the only patch for the second half of Chapter Memory Ordering. Please take a look. Thanks.

Good catch!

While we are here, why not apply the new scheme for snippets to this litmus test? Labeling lines in the source code can prevent such mismatches.

For the new scheme to support litmus tests, please see commit log of 69a75a84d7c3 ("future/formalregress: Example of extraction of snippet from .litmus file")

Thanks. Akira

--

 .../formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus    | 22 ++++-----
 memorder/memorder.tex                              | 52 +++-------------------
 2 files changed, 19 insertions(+), 55 deletions(-)

CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus +12 -10

index 343fded..b899369 100644
@@ -1,15 +1,16 @@
 C C-ISA2+o-r+a-r+a-r+a-o
+//\begin[snippet][labelbase=ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole,commandchars=\\\@\$]
 {
 }
 
-{
-#include "api.h"
-}
-
+{				//\fcvexclude
+#include "api.h"		//\fcvexclude
+}				//\fcvexclude
+				//\fcvexclude
 P0(int *x0, int *x1)
 {
 	WRITE_ONCE(*x0, 2);
-	smp_store_release(x1, 2);
+	smp_store_release(x1, 2);	//\lnlbl[P0:rel]
 }
 
 

@@ -17,16 +18,16 @@ P1(int *x1, int *x2)
 {
 	int r2;
 
-	r2 = smp_load_acquire(x1);
-	smp_store_release(x2, 2);
+	r2 = smp_load_acquire(x1);	//\lnlbl[P1:acq]
+	smp_store_release(x2, 2);	//\lnlbl[P1:rel]
 }
 
 P2(int *x2, int *x3)
 {
 	int r2;
 
-	r2 = smp_load_acquire(x2);
-	smp_store_release(x3, 2);
+	r2 = smp_load_acquire(x2);	//\lnlbl[P2:acq]
+	smp_store_release(x3, 2);	//\lnlbl[P2:rel]
 }
 
 P3(int *x3, int *x0)

@@ -34,8 +35,9 @@ P3(int *x3, int *x0)
 	int r1;
 	int r2;
 
-	r1 = smp_load_acquire(x3);
+	r1 = smp_load_acquire(x3);	//\lnlbl[P3:acq]
 	r2 = READ_ONCE(*x0);
 }
 
+//\end[snippet]
 exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)

memorder/memorder.tex +7 -45

index 8e11e92..d92d1e5 100644
@@ -2841,49 +2841,7 @@ from the passage of time, so that no matter how many threads are
 involved, the corresponding \co{exists} clause cannot trigger.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}[\LstLineNo]
-C C-ISA2+o-r+a-r+a-r+a-o
-{
-}
-
-P0(int *x0, int *x1)
-{
-  WRITE_ONCE(*x0, 2);
-  smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x1);
-  smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x2);
-  smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
-  int r1;
-  int r2;
-
-  r1 = smp_load_acquire(x3);
-  r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/litmus/[email protected]}
 \caption{Long ISA2 Release-Acquire Chain}
 \label{lst:memorder:Long ISA2 Release-Acquire Chain}
 \end{listing}

@@ -2899,16 +2857,20 @@ shows a three-step release-acquire chain, but where \co{P3()}'s
 final access is a \co{READ_ONCE()} from \co{x0}, which is
 accessed via \co{WRITE_ONCE()} by \co{P0()}, forming a non-temporal
 load-to-store link between these two processes.
-However, because \co{P0()}'s \co{smp_store_release()} (line~12)
+\begin{lineref}[ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole]
+However, because \co{P0()}'s \co{smp_store_release()} (line~\lnref{P0:rel})
 is cumulative, if \co{P3()}'s \co{READ_ONCE()} returns zero,
 this cumulativity will force the \co{READ_ONCE()} to be ordered
 before \co{P0()}'s \co{smp_store_release()}.
-In addition, the release-acquire chain (lines~12, 20, 21, 28, 29, and~37)
+In addition, the release-acquire chain
+(lines~\lnref{P0:rel}, \lnref{P1:acq}, \lnref{P1:rel}, \lnref{P2:acq},
+\lnref{P2:rel}, and~\lnref{P3:acq})
 forces \co{P3()}'s \co{READ_ONCE()} to be ordered after \co{P0()}'s
 \co{smp_store_release()}.
 Because \co{P3()}'s \co{READ_ONCE()} cannot be both before and after
 \co{P0()}'s \co{smp_store_release()}, either or both of two things must
 be true:
+\end{lineref}
 
 \begin{enumerate}
 \item	\co{P3()}'s \co{READ_ONCE()} came after \co{P0()}'s

Signature · 1 line

2.7.4

Quoted 22 lines · Akira Yokosawa

Quoted 1 line

From 0e43c93660383b7560c55131754dbc4bfaf13052 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Mon, 5 Nov 2018 20:27:02 +0900
Subject: [PATCH] memorder: Fix line numbers by applying new scheme to C-ISA2+o-r+a-r+a-r+a-o

Line numbers referring to Listing 15.23 don't match the line counts in the snippet. Fix this by putting labels in the source of the litmus test and referring them by \lnref{} macros.

Reported-by Junchang Wang <[email protected]>

Signed-off-by Akira Yokosawa <[email protected]>

---

Quoted 3 lines · Junchang Wang

This is the only patch for the second half of Chapter Memory Ordering. Please take a look. Thanks.

Good catch!

While we are here, why not apply the new scheme for snippets to this litmus test? Labeling lines in the source code can prevent such mismatches.

Quoted 3 lines

For the new scheme to support litmus tests, please see commit log of 69a75a84d7c3 ("future/formalregress: Example of extraction of snippet from .litmus file")

Indeed, good catch!!! And here I -thought- that I proof-read this stuff...

Junchang, does Akira's approach look good to you?

Thanx, Paul

Quoted 146 lines

Thanks. Akira

--

 .../formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus    | 22 ++++-----
 memorder/memorder.tex                              | 52 +++-------------------
 2 files changed, 19 insertions(+), 55 deletions(-)

CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus +12 -10

index 343fded..b899369 100644
@@ -1,15 +1,16 @@
 C C-ISA2+o-r+a-r+a-r+a-o
+//\begin[snippet][labelbase=ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole,commandchars=\\\@\$]
 {
 }
 
-{
-#include "api.h"
-}
-
+{                            //\fcvexclude
+#include "api.h"             //\fcvexclude
+}                            //\fcvexclude
+                             //\fcvexclude
 P0(int *x0, int *x1)
 {
      WRITE_ONCE(*x0, 2);
-     smp_store_release(x1, 2);
+     smp_store_release(x1, 2);       //\lnlbl[P0:rel]
 }
 
 

@@ -17,16 +18,16 @@ P1(int *x1, int *x2)
 {
      int r2;
 
-     r2 = smp_load_acquire(x1);
-     smp_store_release(x2, 2);
+     r2 = smp_load_acquire(x1);      //\lnlbl[P1:acq]
+     smp_store_release(x2, 2);       //\lnlbl[P1:rel]
 }
 
 P2(int *x2, int *x3)
 {
      int r2;
 
-     r2 = smp_load_acquire(x2);
-     smp_store_release(x3, 2);
+     r2 = smp_load_acquire(x2);      //\lnlbl[P2:acq]
+     smp_store_release(x3, 2);       //\lnlbl[P2:rel]
 }
 
 P3(int *x3, int *x0)

@@ -34,8 +35,9 @@ P3(int *x3, int *x0)
      int r1;
      int r2;
 
-     r1 = smp_load_acquire(x3);
+     r1 = smp_load_acquire(x3);      //\lnlbl[P3:acq]
      r2 = READ_ONCE(*x0);
 }
 
+//\end[snippet]
 exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)

memorder/memorder.tex +7 -46

index 8e11e92..d92d1e5 100644
@@ -2841,49 +2841,7 @@ from the passage of time, so that no matter how many threads are
 involved, the corresponding \co{exists} clause cannot trigger.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}[\LstLineNo]
-C C-ISA2+o-r+a-r+a-r+a-o
-{
-}
-
-P0(int *x0, int *x1)
-{
-  WRITE_ONCE(*x0, 2);
-  smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x1);
-  smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x2);
-  smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
-  int r1;
-  int r2;
-
-  r1 = smp_load_acquire(x3);
-  r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/litmus/[email protected]}
 \caption{Long ISA2 Release-Acquire Chain}
 \label{lst:memorder:Long ISA2 Release-Acquire Chain}
 \end{listing}

@@ -2899,16 +2857,20 @@ shows a three-step release-acquire chain, but where \co{P3()}'s
 final access is a \co{READ_ONCE()} from \co{x0}, which is
 accessed via \co{WRITE_ONCE()} by \co{P0()}, forming a non-temporal
 load-to-store link between these two processes.
-However, because \co{P0()}'s \co{smp_store_release()} (line~12)
+\begin{lineref}[ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole]
+However, because \co{P0()}'s \co{smp_store_release()} (line~\lnref{P0:rel})
 is cumulative, if \co{P3()}'s \co{READ_ONCE()} returns zero,
 this cumulativity will force the \co{READ_ONCE()} to be ordered
 before \co{P0()}'s \co{smp_store_release()}.
-In addition, the release-acquire chain (lines~12, 20, 21, 28, 29, and~37)
+In addition, the release-acquire chain
+(lines~\lnref{P0:rel}, \lnref{P1:acq}, \lnref{P1:rel}, \lnref{P2:acq},
+\lnref{P2:rel}, and~\lnref{P3:acq})
 forces \co{P3()}'s \co{READ_ONCE()} to be ordered after \co{P0()}'s
 \co{smp_store_release()}.
 Because \co{P3()}'s \co{READ_ONCE()} cannot be both before and after
 \co{P0()}'s \co{smp_store_release()}, either or both of two things must
 be true:
+\end{lineref}
 
 \begin{enumerate}
 \item        \co{P3()}'s \co{READ_ONCE()} came after \co{P0()}'s
--

2.7.4

Quoted 30 lines · Paul E. McKenney

Quoted 17 lines · Akira Yokosawa

Quoted 1 line

From 0e43c93660383b7560c55131754dbc4bfaf13052 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Mon, 5 Nov 2018 20:27:02 +0900
Subject: [PATCH] memorder: Fix line numbers by applying new scheme to C-ISA2+o-r+a-r+a-r+a-o

Line numbers referring to Listing 15.23 don't match the line counts in the snippet. Fix this by putting labels in the source of the litmus test and referring them by \lnref{} macros.

Reported-by Junchang Wang <[email protected]>

Signed-off-by Akira Yokosawa <[email protected]>

---

Quoted 3 lines · Junchang Wang

This is the only patch for the second half of Chapter Memory Ordering. Please take a look. Thanks.

Quoted 8 lines

Good catch!

While we are here, why not apply the new scheme for snippets to this litmus test? Labeling lines in the source code can prevent such mismatches.

For the new scheme to support litmus tests, please see commit log of 69a75a84d7c3 ("future/formalregress: Example of extraction of snippet from .litmus file")

Indeed, good catch!!! And here I -thought- that I proof-read this stuff...

Quoted 1 line

Junchang, does Akira's approach look good to you?

Hi Paul,

Sorry for the late response. The new scheme is the right approach in comparison to hard-coding line numbers; Akira's approach looks good to me.

@Akira Yokosawa Thanks a lot for pointing me to the right scheme, which looks nice. I believe we programmers tend to hard-coding line numbers/variables at the very beginning of drafting/coding; that's a nice tradeoff between efficiency and portability :-) . I can help check and apply the new scheme in reading through other chapters.

Thanks,
--Junchang

Quoted 149 lines

Thanx, Paul

Quoted 146 lines

Thanks. Akira

--

 .../formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus    | 22 ++++-----
 memorder/memorder.tex                              | 52 +++-------------------
 2 files changed, 19 insertions(+), 55 deletions(-)

CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus +12 -10

index 343fded..b899369 100644
@@ -1,15 +1,16 @@
 C C-ISA2+o-r+a-r+a-r+a-o
+//\begin[snippet][labelbase=ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole,commandchars=\\\@\$]
 {
 }
 
-{
-#include "api.h"
-}
-
+{                            //\fcvexclude
+#include "api.h"             //\fcvexclude
+}                            //\fcvexclude
+                             //\fcvexclude
 P0(int *x0, int *x1)
 {
      WRITE_ONCE(*x0, 2);
-     smp_store_release(x1, 2);
+     smp_store_release(x1, 2);       //\lnlbl[P0:rel]
 }
 
 

@@ -17,16 +18,16 @@ P1(int *x1, int *x2)
 {
      int r2;
 
-     r2 = smp_load_acquire(x1);
-     smp_store_release(x2, 2);
+     r2 = smp_load_acquire(x1);      //\lnlbl[P1:acq]
+     smp_store_release(x2, 2);       //\lnlbl[P1:rel]
 }
 
 P2(int *x2, int *x3)
 {
      int r2;
 
-     r2 = smp_load_acquire(x2);
-     smp_store_release(x3, 2);
+     r2 = smp_load_acquire(x2);      //\lnlbl[P2:acq]
+     smp_store_release(x3, 2);       //\lnlbl[P2:rel]
 }
 
 P3(int *x3, int *x0)

@@ -34,8 +35,9 @@ P3(int *x3, int *x0)
      int r1;
      int r2;
 
-     r1 = smp_load_acquire(x3);
+     r1 = smp_load_acquire(x3);      //\lnlbl[P3:acq]
      r2 = READ_ONCE(*x0);
 }
 
+//\end[snippet]
 exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)

memorder/memorder.tex +7 -46

index 8e11e92..d92d1e5 100644
@@ -2841,49 +2841,7 @@ from the passage of time, so that no matter how many threads are
 involved, the corresponding \co{exists} clause cannot trigger.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}[\LstLineNo]
-C C-ISA2+o-r+a-r+a-r+a-o
-{
-}
-
-P0(int *x0, int *x1)
-{
-  WRITE_ONCE(*x0, 2);
-  smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x1);
-  smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x2);
-  smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
-  int r1;
-  int r2;
-
-  r1 = smp_load_acquire(x3);
-  r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/litmus/[email protected]}
 \caption{Long ISA2 Release-Acquire Chain}
 \label{lst:memorder:Long ISA2 Release-Acquire Chain}
 \end{listing}

@@ -2899,16 +2857,20 @@ shows a three-step release-acquire chain, but where \co{P3()}'s
 final access is a \co{READ_ONCE()} from \co{x0}, which is
 accessed via \co{WRITE_ONCE()} by \co{P0()}, forming a non-temporal
 load-to-store link between these two processes.
-However, because \co{P0()}'s \co{smp_store_release()} (line~12)
+\begin{lineref}[ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole]
+However, because \co{P0()}'s \co{smp_store_release()} (line~\lnref{P0:rel})
 is cumulative, if \co{P3()}'s \co{READ_ONCE()} returns zero,
 this cumulativity will force the \co{READ_ONCE()} to be ordered
 before \co{P0()}'s \co{smp_store_release()}.
-In addition, the release-acquire chain (lines~12, 20, 21, 28, 29, and~37)
+In addition, the release-acquire chain
+(lines~\lnref{P0:rel}, \lnref{P1:acq}, \lnref{P1:rel}, \lnref{P2:acq},
+\lnref{P2:rel}, and~\lnref{P3:acq})
 forces \co{P3()}'s \co{READ_ONCE()} to be ordered after \co{P0()}'s
 \co{smp_store_release()}.
 Because \co{P3()}'s \co{READ_ONCE()} cannot be both before and after
 \co{P0()}'s \co{smp_store_release()}, either or both of two things must
 be true:
+\end{lineref}
 
 \begin{enumerate}
 \item        \co{P3()}'s \co{READ_ONCE()} came after \co{P0()}'s
--

2.7.4

Quoted 35 lines · Junchang Wang

Quoted 24 lines · Paul E. McKenney

Quoted 22 lines · Akira Yokosawa

Quoted 1 line

From 0e43c93660383b7560c55131754dbc4bfaf13052 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Mon, 5 Nov 2018 20:27:02 +0900
Subject: [PATCH] memorder: Fix line numbers by applying new scheme to C-ISA2+o-r+a-r+a-r+a-o

Line numbers referring to Listing 15.23 don't match the line counts in the snippet. Fix this by putting labels in the source of the litmus test and referring them by \lnref{} macros.

Reported-by Junchang Wang <[email protected]>

Signed-off-by Akira Yokosawa <[email protected]>

---

Quoted 3 lines · Junchang Wang

This is the only patch for the second half of Chapter Memory Ordering. Please take a look. Thanks.

Good catch!

While we are here, why not apply the new scheme for snippets to this litmus test? Labeling lines in the source code can prevent such mismatches.

Quoted 7 lines

Quoted 3 lines

For the new scheme to support litmus tests, please see commit log of 69a75a84d7c3 ("future/formalregress: Example of extraction of snippet from .litmus file")

Indeed, good catch!!! And here I -thought- that I proof-read this stuff...

Junchang, does Akira's approach look good to you?

Hi Paul,

Quoted 3 lines

Sorry for the late response. The new scheme is the right approach in comparison to hard-coding line numbers; Akira's approach looks good to me.

Very good! Unless you tell me otherwise, I will add your:

Acked-by Junchang Wang <[email protected]>

This would indicate your approval of Akira's patch.

Thanx, Paul

Quoted 161 lines

@Akira Yokosawa Thanks a lot for pointing me to the right scheme, which looks nice. I believe we programmers tend to hard-coding line numbers/variables at the very beginning of drafting/coding; that's a nice tradeoff between efficiency and portability :-) . I can help check and apply the new scheme in reading through other chapters.

Thanks,
--Junchang

Quoted 149 lines

Thanx, Paul

Quoted 146 lines

Thanks. Akira

--

 .../formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus    | 22 ++++-----
 memorder/memorder.tex                              | 52 +++-------------------
 2 files changed, 19 insertions(+), 55 deletions(-)

CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus +12 -10

index 343fded..b899369 100644
@@ -1,15 +1,16 @@
 C C-ISA2+o-r+a-r+a-r+a-o
+//\begin[snippet][labelbase=ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole,commandchars=\\\@\$]
 {
 }
 
-{
-#include "api.h"
-}
-
+{                            //\fcvexclude
+#include "api.h"             //\fcvexclude
+}                            //\fcvexclude
+                             //\fcvexclude
 P0(int *x0, int *x1)
 {
      WRITE_ONCE(*x0, 2);
-     smp_store_release(x1, 2);
+     smp_store_release(x1, 2);       //\lnlbl[P0:rel]
 }
 
 

@@ -17,16 +18,16 @@ P1(int *x1, int *x2)
 {
      int r2;
 
-     r2 = smp_load_acquire(x1);
-     smp_store_release(x2, 2);
+     r2 = smp_load_acquire(x1);      //\lnlbl[P1:acq]
+     smp_store_release(x2, 2);       //\lnlbl[P1:rel]
 }
 
 P2(int *x2, int *x3)
 {
      int r2;
 
-     r2 = smp_load_acquire(x2);
-     smp_store_release(x3, 2);
+     r2 = smp_load_acquire(x2);      //\lnlbl[P2:acq]
+     smp_store_release(x3, 2);       //\lnlbl[P2:rel]
 }
 
 P3(int *x3, int *x0)

@@ -34,8 +35,9 @@ P3(int *x3, int *x0)
      int r1;
      int r2;
 
-     r1 = smp_load_acquire(x3);
+     r1 = smp_load_acquire(x3);      //\lnlbl[P3:acq]
      r2 = READ_ONCE(*x0);
 }
 
+//\end[snippet]
 exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)

memorder/memorder.tex +7 -46

index 8e11e92..d92d1e5 100644
@@ -2841,49 +2841,7 @@ from the passage of time, so that no matter how many threads are
 involved, the corresponding \co{exists} clause cannot trigger.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}[\LstLineNo]
-C C-ISA2+o-r+a-r+a-r+a-o
-{
-}
-
-P0(int *x0, int *x1)
-{
-  WRITE_ONCE(*x0, 2);
-  smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x1);
-  smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x2);
-  smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
-  int r1;
-  int r2;
-
-  r1 = smp_load_acquire(x3);
-  r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/litmus/[email protected]}
 \caption{Long ISA2 Release-Acquire Chain}
 \label{lst:memorder:Long ISA2 Release-Acquire Chain}
 \end{listing}

@@ -2899,16 +2857,20 @@ shows a three-step release-acquire chain, but where \co{P3()}'s
 final access is a \co{READ_ONCE()} from \co{x0}, which is
 accessed via \co{WRITE_ONCE()} by \co{P0()}, forming a non-temporal
 load-to-store link between these two processes.
-However, because \co{P0()}'s \co{smp_store_release()} (line~12)
+\begin{lineref}[ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole]
+However, because \co{P0()}'s \co{smp_store_release()} (line~\lnref{P0:rel})
 is cumulative, if \co{P3()}'s \co{READ_ONCE()} returns zero,
 this cumulativity will force the \co{READ_ONCE()} to be ordered
 before \co{P0()}'s \co{smp_store_release()}.
-In addition, the release-acquire chain (lines~12, 20, 21, 28, 29, and~37)
+In addition, the release-acquire chain
+(lines~\lnref{P0:rel}, \lnref{P1:acq}, \lnref{P1:rel}, \lnref{P2:acq},
+\lnref{P2:rel}, and~\lnref{P3:acq})
 forces \co{P3()}'s \co{READ_ONCE()} to be ordered after \co{P0()}'s
 \co{smp_store_release()}.
 Because \co{P3()}'s \co{READ_ONCE()} cannot be both before and after
 \co{P0()}'s \co{smp_store_release()}, either or both of two things must
 be true:
+\end{lineref}
 
 \begin{enumerate}
 \item        \co{P3()}'s \co{READ_ONCE()} came after \co{P0()}'s
--

2.7.4

Quoted 41 lines · Paul E. McKenney

Quoted 38 lines · Junchang Wang

Quoted 24 lines · Paul E. McKenney

Quoted 22 lines · Akira Yokosawa

Quoted 1 line

From 0e43c93660383b7560c55131754dbc4bfaf13052 Mon Sep 17 00:00:00 2001

From: Akira Yokosawa <[email protected]>
Date: Mon, 5 Nov 2018 20:27:02 +0900
Subject: [PATCH] memorder: Fix line numbers by applying new scheme to C-ISA2+o-r+a-r+a-r+a-o

Line numbers referring to Listing 15.23 don't match the line counts in the snippet. Fix this by putting labels in the source of the litmus test and referring them by \lnref{} macros.

Reported-by Junchang Wang <[email protected]>

Signed-off-by Akira Yokosawa <[email protected]>

---

Quoted 3 lines · Junchang Wang

This is the only patch for the second half of Chapter Memory Ordering. Please take a look. Thanks.

Good catch!

While we are here, why not apply the new scheme for snippets to this litmus test? Labeling lines in the source code can prevent such mismatches.

Quoted 7 lines

Quoted 3 lines

For the new scheme to support litmus tests, please see commit log of 69a75a84d7c3 ("future/formalregress: Example of extraction of snippet from .litmus file")

Indeed, good catch!!! And here I -thought- that I proof-read this stuff...

Junchang, does Akira's approach look good to you?

Hi Paul,

Sorry for the late response. The new scheme is the right approach in comparison to hard-coding line numbers; Akira's approach looks good to me.

Quoted 3 lines

Very good! Unless you tell me otherwise, I will add your:

Acked-by Junchang Wang <[email protected]>

Got it. Thanks a lot.

--Junchang

Quoted 166 lines

This would indicate your approval of Akira's patch.

Thanx, Paul

Quoted 161 lines

@Akira Yokosawa Thanks a lot for pointing me to the right scheme, which looks nice. I believe we programmers tend to hard-coding line numbers/variables at the very beginning of drafting/coding; that's a nice tradeoff between efficiency and portability :-) . I can help check and apply the new scheme in reading through other chapters.

Thanks,
--Junchang

Quoted 149 lines

Thanx, Paul

Quoted 146 lines

Thanks. Akira

--

 .../formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus    | 22 ++++-----
 memorder/memorder.tex                              | 52 +++-------------------
 2 files changed, 19 insertions(+), 55 deletions(-)

CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus +12 -10

index 343fded..b899369 100644
@@ -1,15 +1,16 @@
 C C-ISA2+o-r+a-r+a-r+a-o
+//\begin[snippet][labelbase=ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole,commandchars=\\\@\$]
 {
 }
 
-{
-#include "api.h"
-}
-
+{                            //\fcvexclude
+#include "api.h"             //\fcvexclude
+}                            //\fcvexclude
+                             //\fcvexclude
 P0(int *x0, int *x1)
 {
      WRITE_ONCE(*x0, 2);
-     smp_store_release(x1, 2);
+     smp_store_release(x1, 2);       //\lnlbl[P0:rel]
 }
 
 

@@ -17,16 +18,16 @@ P1(int *x1, int *x2)
 {
      int r2;
 
-     r2 = smp_load_acquire(x1);
-     smp_store_release(x2, 2);
+     r2 = smp_load_acquire(x1);      //\lnlbl[P1:acq]
+     smp_store_release(x2, 2);       //\lnlbl[P1:rel]
 }
 
 P2(int *x2, int *x3)
 {
      int r2;
 
-     r2 = smp_load_acquire(x2);
-     smp_store_release(x3, 2);
+     r2 = smp_load_acquire(x2);      //\lnlbl[P2:acq]
+     smp_store_release(x3, 2);       //\lnlbl[P2:rel]
 }
 
 P3(int *x3, int *x0)

@@ -34,8 +35,9 @@ P3(int *x3, int *x0)
      int r1;
      int r2;
 
-     r1 = smp_load_acquire(x3);
+     r1 = smp_load_acquire(x3);      //\lnlbl[P3:acq]
      r2 = READ_ONCE(*x0);
 }
 
+//\end[snippet]
 exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)

memorder/memorder.tex +7 -46

index 8e11e92..d92d1e5 100644
@@ -2841,49 +2841,7 @@ from the passage of time, so that no matter how many threads are
 involved, the corresponding \co{exists} clause cannot trigger.
 
 \begin{listing}[tbp]
-{ \scriptsize
-\begin{verbbox}[\LstLineNo]
-C C-ISA2+o-r+a-r+a-r+a-o
-{
-}
-
-P0(int *x0, int *x1)
-{
-  WRITE_ONCE(*x0, 2);
-  smp_store_release(x1, 2);
-}
-
-
-P1(int *x1, int *x2)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x1);
-  smp_store_release(x2, 2);
-}
-
-P2(int *x2, int *x3)
-{
-  int r2;
-
-  r2 = smp_load_acquire(x2);
-  smp_store_release(x3, 2);
-}
-
-P3(int *x3, int *x0)
-{
-  int r1;
-  int r2;
-
-  r1 = smp_load_acquire(x3);
-  r2 = READ_ONCE(*x0);
-}
-
-exists (1:r2=2 /\ 2:r2=2 /\ 3:r1=2 /\ 3:r2=0)
-\end{verbbox}
-}
-\centering
-\theverbbox
+\input{CodeSamples/formal/litmus/[email protected]}
 \caption{Long ISA2 Release-Acquire Chain}
 \label{lst:memorder:Long ISA2 Release-Acquire Chain}
 \end{listing}

@@ -2899,16 +2857,20 @@ shows a three-step release-acquire chain, but where \co{P3()}'s
 final access is a \co{READ_ONCE()} from \co{x0}, which is
 accessed via \co{WRITE_ONCE()} by \co{P0()}, forming a non-temporal
 load-to-store link between these two processes.
-However, because \co{P0()}'s \co{smp_store_release()} (line~12)
+\begin{lineref}[ln:formal:litmus:C-ISA2+o-r+a-r+a-r+a-o:whole]
+However, because \co{P0()}'s \co{smp_store_release()} (line~\lnref{P0:rel})
 is cumulative, if \co{P3()}'s \co{READ_ONCE()} returns zero,
 this cumulativity will force the \co{READ_ONCE()} to be ordered
 before \co{P0()}'s \co{smp_store_release()}.
-In addition, the release-acquire chain (lines~12, 20, 21, 28, 29, and~37)
+In addition, the release-acquire chain
+(lines~\lnref{P0:rel}, \lnref{P1:acq}, \lnref{P1:rel}, \lnref{P2:acq},
+\lnref{P2:rel}, and~\lnref{P3:acq})
 forces \co{P3()}'s \co{READ_ONCE()} to be ordered after \co{P0()}'s
 \co{smp_store_release()}.
 Because \co{P3()}'s \co{READ_ONCE()} cannot be both before and after
 \co{P0()}'s \co{smp_store_release()}, either or both of two things must
 be true:
+\end{lineref}
 
 \begin{enumerate}
 \item        \co{P3()}'s \co{READ_ONCE()} came after \co{P0()}'s
--

2.7.4