Update snippets of litmus tests

index 0dc806e..6084f12 100644
@@ -2,20 +2,24 @@ C C-RCU-remove
 //\begin[snippet][labelbase=ln:formal:C-RCU-remove:whole,commandchars=\\\@\$]
 
 {
-	int *z=1; (* \lnlbl[tail:2] *)
-	int *y=2; (* \lnlbl[tail:1] *)
+	int z=1; (* \lnlbl[tail:2] *)
+	int y=2; (* \lnlbl[tail:1] *)
 	int *x=y; (* \lnlbl[head] *)
+	int * 1:r1; (* \fcvexclude *)
 }
 
-P0(int *x, int *y, int *z)		//\lnlbl[P0start]
+P0(int **x, int *y, int *z)		//\lnlbl[P0start]
 {
 	rcu_assign_pointer(*x, z);	//\lnlbl[assignnewtail]
 	synchronize_rcu();		//\lnlbl[sync]
 	WRITE_ONCE(*y, 0);		//\lnlbl[free]
 }					//\lnlbl[P0end]
 
-P1(int *x, int *y, int *z)		//\lnlbl[P1start]
+P1(int **x, int *y, int *z)		//\lnlbl[P1start]
 {
+	int *r1;
+	int r2;
+
 	rcu_read_lock();		//\lnlbl[rl]
 	r1 = rcu_dereference(*x);	//\lnlbl[rderef]
 	r2 = READ_ONCE(*r1);		//\lnlbl[read]

@@ -23,5 +27,5 @@ P1(int *x, int *y, int *z)		//\lnlbl[P1start]
 }					//\lnlbl[P1end]
 
 //\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [0:r1; 1:r1; x; y; z]
+locations [1:r1; x; y; z]
 exists (1:r2=0)

index bf88ee4..f0080c1 100644
@@ -8,16 +8,26 @@ C C-RomanPenyaev-list-rcu-rr
 	int *w=x;
 	int *v=w;			(* \lnlbl[listhead] *)
 	int *c=w;			(* \lnlbl[rrcache] *)
+	int * 0:r1;			(* \fcvexclude *)
+	int * 0:r2;			(* \fcvexclude *)
+	int * 0:r3;			(* \fcvexclude *)
+	int * 0:r4;			(* \fcvexclude *)
+	int * 1:r1;			(* \fcvexclude *)
 }
 
-P0(int *c, int *v)			//\lnlbl[P0start]
+P0(int **c, int **v)			//\lnlbl[P0start]
 {
+	int *r1;
+	int *r2;
+	int *r3;
+	int *r4;
+
 	rcu_read_lock();		//\lnlbl[rl1]
 	r1 = READ_ONCE(*c);		//\lnlbl[rdcache]
 	if (r1 == 0) {			//\lnlbl[rdckcache]
 		r1 = READ_ONCE(*v);	//\lnlbl[rdinitcache]
 	}
-	r2 = rcu_dereference(*r1);	//\lnlbl[rdnext]
+	r2 = rcu_dereference(*(int **)r1);//\lnlbl[rdnext]
 	smp_store_release(c, r2);	//\lnlbl[rdupdcache]
 	rcu_read_unlock();		//\lnlbl[rul1]
 	rcu_read_lock();		//\lnlbl[rl2]

@@ -25,17 +35,19 @@ P0(int *c, int *v)			//\lnlbl[P0start]
 	if (r3 == 0) {
 		r3 = READ_ONCE(*v);
 	}
-	r4 = rcu_dereference(*r3);
+	r4 = rcu_dereference(*(int **)r3);
 	smp_store_release(c, r4);
 	rcu_read_unlock();		//\lnlbl[rul2]
 }					//\lnlbl[P0end]
 
-P1(int *c, int *v, int *w, int *x, int *y)//\lnlbl[P1start]
+P1(int **c, int **v, int **w, int **x, int **y)//\lnlbl[P1start]
 {
+	int *r1;
+
 	rcu_assign_pointer(*w, y);	//\lnlbl[updremove]
 	synchronize_rcu();		//\lnlbl[updsync1]
 	r1 = READ_ONCE(*c);		//\lnlbl[updrdcache]
-	if (r1 == x) {			//\lnlbl[updckcache]
+	if ((int **)r1 == x) {		//\lnlbl[updckcache]
 		WRITE_ONCE(*c, 0);	//\lnlbl[updinitcache]
 		synchronize_rcu();	//\lnlbl[updsync2]
 	}

@@ -43,5 +55,5 @@ P1(int *c, int *v, int *w, int *x, int *y)//\lnlbl[P1start]
 }					//\lnlbl[P1end]
 
 //\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [0:r1; 1:r1; 1:r3; c; v; w; x; y]
+locations [1:r1; c; v; w; x; y]
 exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)

index 05a8e6d..e23148e 100644
@@ -49,6 +49,8 @@ ABSPERF_SHORT  := $(filter-out $(ABSPERF_LONG),$(ABSPERF_TEST))
 ABSPERF_OUT    = absperf.out absperf-all.out
 HERD7_TEST     := $(filter-out $(ABSPERF_TEST),$(HERD7_LITMUS))
 HERD7_OUT      := $(HERD7_TEST:%.litmus=%.out)
+KLITMUS_READY = C-RCU-remove C-RomanPenyaev-list-rcu-rr
+KLITMUS_TEST   := $(addsuffix .litmus,$(KLITMUS_READY))
 
 .PHONY: all clean litmus2herd run-herd7 run-absperf run-absperf-all cross-klitmus
 .PHONY: help

@@ -98,9 +100,9 @@ $(ABSPERF_OUT):
 
 cross-klitmus: klitmus.tar
 
-klitmus.tar: litmus2herd
+klitmus.tar: litmus2herd $(KLITMUS_TEST)
 	mkdir -p klitmus
-	klitmus7 -o klitmus $(LITMUS7_HERD_TEST)
+	klitmus7 -rcu yes -o klitmus $(LITMUS7_HERD_TEST) $(KLITMUS_TEST)
 	tar cf klitmus.tar ./klitmus
 
 help:

index 6084f12..33c410f 100644
@@ -26,6 +26,6 @@ P1(int **x, int *y, int *z)		//\lnlbl[P1start]
 	rcu_read_unlock();		//\lnlbl[rul]
 }					//\lnlbl[P1end]
 
-//\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [1:r1; x; y; z]
-exists (1:r2=0)
+//\end[snippet]
+locations [1:r1; x; y; z]	(* \lnlbl[locations_] *)
+exists (1:r2=0)			(* \lnlbl[exists_] *)

index f0080c1..1a197bd 100644
@@ -54,6 +54,6 @@ P1(int **c, int **v, int **w, int **x, int **y)//\lnlbl[P1start]
 	smp_store_release(x, 0);	//\lnlbl[updfree]
 }					//\lnlbl[P1end]
 
-//\end[snippet][locationslabel=locations_,existslabel=exists_]
-locations [1:r1; c; v; w; x; y]
-exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)
+//\end[snippet]
+locations [1:r1; c; v; w; x; y]			(* \lnlbl[locations_] *)
+exists (0:r1=0 \/ 0:r2=0 \/ 0:r3=0 \/ 0:r4=0)	(* \lnlbl[exists_] *)

index 32d8e52..3e9e023 100644
@@ -26,6 +26,6 @@ P1(int *sl, int *x0, int *x1)
 	smp_store_release(sl, 0);
 }
 
-//\end[snippet][filterlabel=filter_]
-filter (0:r2=0 /\ 1:r2=0)
+//\end[snippet]
+filter (0:r2=0 /\ 1:r2=0)	(* \lnlbl[filter_] *)
 exists (0:r1=0 /\ 1:r1=0)

73 lines not on this page · raw message

index 3fe79ce..517424b 100644
@@ -511,8 +511,8 @@ at the beginning of a litmus test.
 
 Similarly, several tokens such as \qco{exists}, \qco{filter},
 and~\qco{locations} indicate the end of litmus test's body.
-Once one of them appears in a litmus test, no comment is
-allowed to appear thereafter.  Those tokens keep the same meaning
+Once one of them appears in a litmus test, comments should be
+ocaml style (\qco{(* ... *)}). Those tokens keep the same meaning
 even when they appear in comments!
 
 The pair of characters \qco{\{} and \qco{\}} also have special

@@ -520,7 +520,7 @@ meaning in the C flavour tests. They are used to seperate portions
 in a litmus test.
 
 First pair of \qco{\{} and \qco{\}} encloses initialization part.
-Comments in this part should be of the form \qco{(* ... *)}.
+Comments in this part should also be in the ocaml form.
 
 You can't use \qco{\{} and \qco{\}} in comments in litmus tests, either.
 

@@ -544,7 +544,7 @@ P0(int *x}
 
 [...]
 
-exists (0:r1=0)  // comment after test body
+exists (0:r1=0)  // C++ style comment after test body
 \end{VerbatimN}
 \end{linelabel}
 

@@ -576,20 +576,11 @@ P1(int *x0, int *x1)
 	r2 = READ_ONCE(*x0);
 }
 
-//\end[snippet][existslabel=exists_]
-exists (1:r2=0 /\ 0:r2=0)
+//\end[snippet]
+exists (1:r2=0 /\ 0:r2=0)  (* \lnlbl[exists_] *)
 \end{VerbatimN}
 \end{linelabel}
 
-To support labeling lines after the test body, \co{\\end[snippet]}
-can have following options:
-
-\begin{VerbatimU}
-exsitslabel=<label of exists>
-filterlabel=<label of filter>
-locationslabel=<label of locations>
-\end{VerbatimU}
-
 Example above is converted to the following intermediate code
 by a script \path{utilities/reorder_ltms.pl}.\footnote{
 	Currently, only C flavour litmus tests are supported.

@@ -624,8 +615,8 @@ P1(int *x0, int *x1)
 	r2 = READ_ONCE(*x0);
 }
 
-exists (1:r2=0 /\ 0:r2=0)\lnlbl{exists_}
-//\end{snippet}[existslabel=exists_]
+exists (1:r2=0 /\ 0:r2=0)  \lnlbl{exists_}
+//\end{snippet}
 \end{VerbatimN}
 \end{linelabel}