* [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests
@ 2020-11-14 4:51 Akira Yokosawa
2020-11-14 4:54 ` [PATCH perfbook 1/2] CodeSamples/formal/litmus: Remove redundant initialization Akira Yokosawa
` (2 more replies)
0 siblings, 3 replies; 10+ messages in thread
From: Akira Yokosawa @ 2020-11-14 4:51 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
Hi Paul,
This patch set is what I mentioned the other day in response to
your LKMM patch for 5.11.
klitmus7 doesn't need most of type info in litmus-test init blocks.
While there are some cases where klitmus7 requires type info of variables
to be watched (via the "exists", "locations", or "filter" directive),
as long as the watched variables are of type "int", extra type info
in the init block is not required.
Litmus tests under CodeSamples/formal/ should keep compatible with
klitmus7 after this patch set is applied.
Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
under CodeSamples/formal/litmus/.
Patch 2/2 further reduce line counts of litmus tests by using "{}"
as empty init blocks.
It also adds/removes empty lines for those code snippets to have
consistent looks.
Similar changes to patch 1/2 can be made in the RCU litmus tests
presented in Section 12.3.2. They are not touched in this patch set.
May be in a follow-up patch.
Thanks, Akira
*NOTE*:
There are cases where litmus tests for herd7 can not be
made compatible with (current) klitmus7, though.
One such example is when a variable of a type other than the "int"
or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
directive.
Current klitmus7 has no idea of the way to obtain the value of such a
variable.
As for herd7, all the variables are treated as if they were "int" or
"int *" regardless of the type specified in the litmus tests, there
is no such problem.
--
Akira Yokosawa (2):
CodeSamples/formal/litmus: Remove redundant initializations
CodeSamples/formal: Use '{}' for empty init blocks in litmus tests
CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 5 ++---
CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 5 ++---
CodeSamples/formal/herd/C-Lock1.litmus | 5 +++--
CodeSamples/formal/herd/C-Lock2.litmus | 5 +++--
.../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
.../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
.../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus | 3 +--
.../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 5 ++---
CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 5 ++---
...B+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 7 ++-----
.../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 5 ++---
.../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 5 ++---
.../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 5 ++---
.../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 6 ++----
.../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 5 ++---
.../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus | 5 ++---
.../formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus | 5 ++---
.../formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 4 ++--
.../formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus | 4 ++--
CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus | 4 ++--
.../formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus | 7 +++----
CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus | 6 +++---
CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus | 8 ++------
CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus | 7 ++-----
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 8 ++------
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus | 7 +------
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus | 7 +------
CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 8 ++------
CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus | 6 +++---
.../formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 4 +---
.../formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 6 +-----
CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus | 6 +-----
CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus | 3 +--
.../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 6 ++----
CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 6 ++----
.../formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 4 ++--
CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus | 4 ++--
.../formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 4 ++--
CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 4 ++--
CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 6 +-----
CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-cmpxchg.litmus | 4 ++--
memorder/memorder.tex | 8 ++------
73 files changed, 124 insertions(+), 217 deletions(-)
--
2.17.1
^ permalink raw reply [flat|nested] 10+ messages in thread
* [PATCH perfbook 1/2] CodeSamples/formal/litmus: Remove redundant initialization
2020-11-14 4:51 [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests Akira Yokosawa
@ 2020-11-14 4:54 ` Akira Yokosawa
2020-11-14 4:56 ` [PATCH perfbook 2/2] CodeSamples/formal: Use '{}' for empty init blocks in litmus tests Akira Yokosawa
2020-11-15 20:42 ` [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of " Paul E. McKenney
2 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2020-11-14 4:54 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 40b6085963f79b50b2d326cad2b37692a7e89880 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 8 Nov 2020 07:33:29 +0900
Subject: [PATCH perfbook 1/2] CodeSamples/formal/litmus: Remove redundant initialization
In C Flavor litmus tests, global variables of type "int" need
initialization only when they aren't 0.
This is true not only for herd7 but also for klitmus7/litmus7.
Declaration of plain "int" or "int *" can also be removed.
We can also remove "&" in the right hand side of initialization.
Finally, to reduce line counts of snippets, use "{}" when
init blocks are empty.
For consistency, put an empty line above initialization blocks and
remove extra blank lines in other parts of litmus tests.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus | 5 ++---
.../formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus | 7 +++----
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 4 ++--
.../formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 6 +-----
CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus | 6 +-----
.../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 6 ++----
CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 6 ++----
CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 6 +-----
memorder/memorder.tex | 8 ++------
10 files changed, 18 insertions(+), 40 deletions(-)
diff --git a/CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus
index 833dc9cf..017c782b 100644
--- a/CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus
+++ b/CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus
@@ -1,8 +1,7 @@
C C-CCIRIW+o+o+o-o+o-o
//\begin[snippet][labelbase=ln:formal:C-CCIRIW+o+o+o-o+o-o:whole,commandchars=\@\[\]]
-{
-int x = 0;
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus b/CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus
index 48bf94e3..aa1c3cd0 100644
--- a/CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus
@@ -1,9 +1,9 @@
C C-LB+o-data-o+o-data-o+o-data-o
//\begin[snippet][labelbase=ln:formal:C-LB+o-data-o+o-data-o+o-data-o:whole,commandchars=\@\[\]]
+
{
-int x0=0;
-int x1=1;
-int x2=2;
+x1=1;
+x2=2;
}
{ //\fcvexclude
@@ -18,7 +18,6 @@ P0(int *x0, int *x1)
WRITE_ONCE(*x1, r2);
}
-
P1(int *x1, int *x2)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
index 63a86562..865943e5 100644
--- a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
@@ -2,8 +2,8 @@ C C-MP+o-wmb-o+o-ad-o
//\begin[snippet][][labelbase=ln:formal:C-MP+o-wmb-o+o-addr-o:whole,commandchars=\@\[\]]
{
-int y=1; (* \lnlbl[init:y] *)
-int *x1 = &y; (* \lnlbl[init:x1] *)
+y=1; (* \lnlbl[init:y] *)
+x1=y; (* \lnlbl[init:x1] *)
}
{ //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
index e9b91e87..11171cd5 100644
--- a/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
@@ -2,8 +2,8 @@ C C-S+o-wmb-o+o-addr-o
//\begin[snippet][labelbase=ln:formal:C-S+o-wmb-o+o-addr-o:whole,commandchars=\@\[\]]
{
-int y=1;
-int *x1 = &y;
+y=1;
+x1=y;
}
{ //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
index d664136b..a6d99b6f 100644
--- a/CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
+++ b/CodeSamples/formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus
@@ -1,11 +1,7 @@
C C-W+RWC+o-mb-o+a-o+o-mb-o
//\begin[snippet][labelbase=ln:formal:C-W+RWC+o-mb-o+a-o+o-mb-o:whole,commandchars=\@\[\]]
-{
-int x = 0;
-int y = 0;
-int z = 0;
-}
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus
index 17f300e1..53ae7bdc 100644
--- a/CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus
+++ b/CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus
@@ -1,11 +1,7 @@
C C-W+RWC+o-r+a-o+o-mb-o
//\begin[snippet][labelbase=ln:formal:C-W+RWC+o-r+a-o+o-mb-o:whole,commandchars=\@\[\]]
-{
-int x = 0;
-int y = 0;
-int z = 0;
-}
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
index 3525e033..1310bd7f 100644
--- a/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus
@@ -1,10 +1,8 @@
C C-WWC+o+o-data-o+o-addr-o
{
-int a = 0;
-int b = 0;
-int *x = &a;
-int *y = &b;
+x=a;
+y=b;
}
{
diff --git a/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus b/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
index 0d16b2f7..dbfc8044 100644
--- a/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus
@@ -1,10 +1,8 @@
C C-WWC+o+o-r+o-addr-o
{
-int a = 0;
-int b = 0;
-int *x = &a;
-int *y = &b;
+x=a;
+y=b;
}
{
diff --git a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
index 2115bcf1..747f777f 100644
--- a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
+++ b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus
@@ -1,11 +1,7 @@
C C-Z6.2+o-r+a-o+o-mb-o
//\begin[snippet][labelbase=ln:formal:C-Z6.2+o-r+a-o+o-mb-o:whole,commandchars=\@\[\]]
-{
-int x = 0;
-int y = 0;
-int z = 0;
-}
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/memorder/memorder.tex b/memorder/memorder.tex
index 44e1d14d..5118241e 100644
--- a/memorder/memorder.tex
+++ b/memorder/memorder.tex
@@ -1216,26 +1216,22 @@ Therefore, on older versions of Linux,
C C-MP+o-wmb-o+ld-addr-o
{
-int y=1;
-int *x1 = &y;
+y=1;
+x1=y;
}
P0(int* x0, int** x1) {
-
WRITE_ONCE(*x0, 2);
smp_wmb();
WRITE_ONCE(*x1, x0);
-
}
P1(int** x1) {
-
int *r2;
int r3;
r2 = lockless_dereference(*x1); // Obsolete @lnlbl[deref]
r3 = READ_ONCE(*r2); @lnlbl[read]
-
}
exists (1:r2=x0 /\ 1:r3=1)
--
2.17.1
^ permalink raw reply related [flat|nested] 10+ messages in thread
* [PATCH perfbook 2/2] CodeSamples/formal: Use '{}' for empty init blocks in litmus tests
2020-11-14 4:51 [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests Akira Yokosawa
2020-11-14 4:54 ` [PATCH perfbook 1/2] CodeSamples/formal/litmus: Remove redundant initialization Akira Yokosawa
@ 2020-11-14 4:56 ` Akira Yokosawa
2020-11-15 20:42 ` [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of " Paul E. McKenney
2 siblings, 0 replies; 10+ messages in thread
From: Akira Yokosawa @ 2020-11-14 4:56 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 7bd6d1eccdfd70b6d0ff1c04a080875215173615 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Sun, 8 Nov 2020 08:18:51 +0900
Subject: [PATCH perfbook 2/2] CodeSamples/formal: Use '{}' for empty init blocks in litmus tests
Also remove or add empty lines for consistency.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 5 ++---
CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 5 ++---
CodeSamples/formal/herd/C-Lock1.litmus | 5 +++--
CodeSamples/formal/herd/C-Lock2.litmus | 5 +++--
.../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
.../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
.../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
.../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
.../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus | 3 +--
.../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 5 ++---
CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 5 ++---
...B+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 7 ++-----
.../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 5 ++---
.../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 5 ++---
.../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 5 ++---
.../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 6 ++----
.../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 5 ++---
.../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus | 5 ++---
.../formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus | 5 ++---
.../formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 4 ++--
.../formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus | 4 ++--
CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus | 6 +++---
CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus | 8 ++------
CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus | 7 ++-----
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 4 ----
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus | 7 +------
CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus | 7 +------
CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 4 ----
CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus | 6 +++---
.../formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 4 +---
CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus | 4 ++--
CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus | 3 +--
.../formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 4 ++--
CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus | 4 ++--
.../formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 4 ++--
CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 4 ++--
CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 5 ++---
CodeSamples/formal/litmus/C-cmpxchg.litmus | 4 ++--
65 files changed, 106 insertions(+), 177 deletions(-)
diff --git a/CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus b/CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus
index ba0b4799..bb2c94ef 100644
--- a/CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus
+++ b/CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus
@@ -1,7 +1,7 @@
C C-LB+o-rl-rul-o+o-rl-rul-o
//\begin[snippet][labelbase=ln:formal:C-LB+o-rl-rul-o+o-rl-rul-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -11,7 +11,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
WRITE_ONCE(*x1, 1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
uintptr_t r1 = READ_ONCE(*x1);
diff --git a/CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus b/CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus
index 8551ecaa..7ac2a2ab 100644
--- a/CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus
@@ -1,7 +1,7 @@
C C-LB+rl-o-o-rul+rl-o-o-rul
//\begin[snippet][labelbase=ln:formal:C-LB+rl-o-o-rul+rl-o-o-rul:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -11,7 +11,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
rcu_read_unlock();
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
diff --git a/CodeSamples/formal/herd/C-Lock1.litmus b/CodeSamples/formal/herd/C-Lock1.litmus
index 5a1065d5..b66d83f4 100644
--- a/CodeSamples/formal/herd/C-Lock1.litmus
+++ b/CodeSamples/formal/herd/C-Lock1.litmus
@@ -1,7 +1,7 @@
C Lock1
//\begin[snippet][labelbase=ln:formal:C-Lock1:whole,commandchars=\\\[\]]
-{
-}
+
+{}
P0(int *x, spinlock_t *sp)
{
@@ -19,5 +19,6 @@ P1(int *x, spinlock_t *sp)
r1 = READ_ONCE(*x);
spin_unlock(sp);
}
+
//\end[snippet]
exists (1:r1=1)
diff --git a/CodeSamples/formal/herd/C-Lock2.litmus b/CodeSamples/formal/herd/C-Lock2.litmus
index dc28b24e..00210cb9 100644
--- a/CodeSamples/formal/herd/C-Lock2.litmus
+++ b/CodeSamples/formal/herd/C-Lock2.litmus
@@ -1,7 +1,7 @@
C Lock2
//\begin[snippet][labelbase=ln:formal:C-Lock2:whole,commandchars=\\\[\]]
-{
-}
+
+{}
P0(int *x, spinlock_t *sp1)
{
@@ -19,5 +19,6 @@ P1(int *x, spinlock_t *sp2) // Buggy!
r1 = READ_ONCE(*x);
spin_unlock(sp2);
}
+
//\end[snippet]
exists (1:r1=1)
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
index 7175ca89..f4ad486e 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
index 46fd9ad8..5ac9058b 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
index 3fdddbb2..cb989ab1 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
index a7f9ec55..d6dddac8 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus
index fc2117e2..e19d6cc6 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u
-{
-}
+{}
P0(spinlock_t *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
index f087f9cb..6bf22c64 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
index d9712c85..d9887d6d 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
index 22e8dd54..a075434c 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
index 17e640dc..7c9bca43 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus
index 9208eaad..a1d4e965 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u
-{
-}
+{}
P0(spinlock_t *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
index 19b70691..efe6925b 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
index c22f6a45..376bf88f 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
index 98ded7ea..984a2c4d 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
index 5f376fa2..59064811 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus
index 90ea057f..7d5b881b 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u+l-o-o-u
-{
-}
+{}
P0(spinlock_t *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
index 3e9e0236..456a3055 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus
@@ -1,8 +1,7 @@
C C-SB+l-o-o-u+l-o-o-u-C
// \begin[snippet][labelbase=ln:future:formalregress:C-SB+l-o-o-u+l-o-o-u-C:whole,commandchars=\%\[\]]
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus
index 1e2dd5be..c0703a49 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u-CE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
index 30a7fe71..5d19c0c7 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u-X
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus
index 28a0f83b..3e9c461c 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u-XE
-{
-}
+{}
P0(int *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus
index c16d8f95..8307b389 100644
--- a/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus
+++ b/CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus
@@ -1,7 +1,6 @@
C C-SB+l-o-o-u+l-o-o-u
-{
-}
+{}
P0(spinlock_t *sl, int *x0, int *x1)
{
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus
index 1a9625e8..1a9de656 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+i-rl-o-o-rul
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+i-rl-o-o-rul:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus
index 8681c847..8ae8db2c 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+o-o
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+o-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus
index 18595f4c..02bb51a7 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x1, uintptr_t *x2)
{
WRITE_ONCE(*x1, 2);
@@ -18,7 +17,6 @@ P1(uintptr_t *x1, uintptr_t *x2)
uintptr_t r2 = READ_ONCE(*x2);
}
-
P2(uintptr_t *x2, uintptr_t *x3)
{
rcu_read_lock();
@@ -27,7 +25,6 @@ P2(uintptr_t *x2, uintptr_t *x3)
rcu_read_unlock();
}
-
P3(uintptr_t *x0, uintptr_t *x3)
{
rcu_read_lock();
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus
index aa3a49fa..f48bf45e 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+o-rcusync-o
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+o-rcusync-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus
index 503dcf80..0542443e 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+o-rl-o-rul
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+o-rl-o-rul:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus
index 054e2e7a..69413916 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+o-rl-rul-o
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+o-rl-rul-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus
index 8c87d429..329a12f5 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x1, uintptr_t *x2)
{
rcu_read_lock();
@@ -19,7 +18,6 @@ P1(uintptr_t *x1, uintptr_t *x2)
rcu_read_unlock();
}
-
P2(uintptr_t *x2, uintptr_t *x0)
{
rcu_read_lock();
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus
index 5190ddf6..984d75a3 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+rl-o-o-rul
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+rl-o-o-rul:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus
index a39baf3a..10ce89a3 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus
@@ -1,7 +1,7 @@
C C-SB+o-rcusync-o+rl-o-rul-o
//\begin[snippet][labelbase=ln:formal:C-SB+o-rcusync-o+rl-o-rul-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
P0(uintptr_t *x0, uintptr_t *x1)
{
@@ -10,7 +10,6 @@ P0(uintptr_t *x0, uintptr_t *x1)
uintptr_t r2 = READ_ONCE(*x1);
}
-
P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
diff --git a/CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus
index 1d75e5e6..43fd622c 100644
--- a/CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus
+++ b/CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus
@@ -1,7 +1,7 @@
C C-2+2W+o-o+o-o
//\begin[snippet][labelbase=ln:formal:C-2+2W+o-o+o-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -13,7 +13,6 @@ P0(int *x0, int *x1)
WRITE_ONCE(*x1, 2);
}
-
P1(int *x0, int *x1)
{
WRITE_ONCE(*x1, 1);
diff --git a/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus b/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
index 8d17a1d2..bea2b9a6 100644
--- a/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
+++ b/CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus
@@ -1,7 +1,7 @@
C C-2+2W+o-wmb-o+o-wmb-o
//\begin[snippet][labelbase=ln:formal:C-2+2W+o-wmb-o+o-wmb-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -14,7 +14,6 @@ P0(int *x0, int *x1)
WRITE_ONCE(*x1, 2);
}
-
P1(int *x0, int *x1)
{
WRITE_ONCE(*x1, 1);
diff --git a/CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus b/CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus
index 962d1cea..b8f9cba7 100644
--- a/CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus
+++ b/CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus
@@ -1,7 +1,7 @@
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=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -13,7 +13,6 @@ P0(int *x0, int *x1)
smp_store_release(x1, 2); //\lnlbl[P0:rel]
}
-
P1(int *x1, int *x2)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus b/CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus
index c8e2f130..16f01665 100644
--- a/CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus
@@ -1,7 +1,7 @@
C C-LB+a-o+o-data-o+o-data-o
//\begin[snippet][labelbase=ln:formal:C-LB+a-o+o-data-o+o-data-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -15,7 +15,6 @@ P0(int *x0, int *x1)
WRITE_ONCE(*x1, 2);
}
-
P1(int *x1, int *x2)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus b/CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus
index c582dfd1..1012d225 100644
--- a/CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus
+++ b/CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus
@@ -1,7 +1,7 @@
C C-LB+a-r+a-r+a-r+a-r
//\begin[snippet][labelbase=ln:formal:C-LB+a-r+a-r+a-r+a-r:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -15,7 +15,6 @@ P0(int *x0, int *x1)
smp_store_release(x1, 2);
}
-
P1(int *x1, int *x2)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus b/CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
index a026e2d9..dcceca18 100644
--- a/CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus
@@ -1,6 +1,6 @@
C C-LB+cmpxchg-ctrl-o+o-ctrl-o
-{
-}
+
+{}
{
#include "api.h"
diff --git a/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus
index e97b879a..280c3c33 100644
--- a/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus
@@ -1,6 +1,6 @@
C C-LB+o-cge-o+o-cge-o+dstb
-{
-}
+
+{}
{
#include "api.h"
diff --git a/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus
index 14539b97..653fb485 100644
--- a/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus
@@ -1,6 +1,6 @@
C C-LB+o-cge-o+o-cge-o
-{
-}
+
+{}
{
#include "api.h"
diff --git a/CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus b/CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus
index f8a7406c..5c41c972 100644
--- a/CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus
@@ -1,7 +1,7 @@
C C-LB+o-cgt-o+o-cgt-o
//\begin[snippet][labelbase=ln:formal:C-LB+o-cgt-o+o-cgt-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus
index f40bb067..61da889d 100644
--- a/CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus
@@ -1,7 +1,7 @@
C C-LB+o-o+o-o
//\begin[snippet][labelbase=ln:formal:C-LB+o-o+o-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -15,7 +15,6 @@ P0(int *x0, int *x1)
WRITE_ONCE(*x0, 2);
}
-
P1(int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus b/CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus
index ac5faa81..d1f24f18 100644
--- a/CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus
@@ -1,7 +1,7 @@
C C-LB+o-r+a-o
//\begin[snippet][labelbase=ln:formal:C-LB+o-r+a-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -15,7 +15,6 @@ P0(int *x0, int *x1)
smp_store_release(x0, 2);
}
-
P1(int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus b/CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus
index 6eede7c4..7825a87f 100644
--- a/CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus
@@ -1,7 +1,7 @@
C C-LB+o-r+o-ctrl-o
//\begin[snippet][labelbase=ln:formal:C-LB+o-r+o-ctrl-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -15,7 +15,6 @@ P0(int *x0, int *x1)
smp_store_release(x0, 2);
}
-
P1(int *x0, int *x1)
{
int r2;
@@ -24,5 +23,6 @@ P1(int *x0, int *x1)
if (r2 >= 0) //\lnlbl[if]
WRITE_ONCE(*x1, 2); //\lnlbl[st]
}
+
//\end[snippet]
exists (1:r2=2 /\ 0:r2=2)
diff --git a/CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus b/CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus
index 543256e2..cb3060ba 100644
--- a/CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus
+++ b/CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus
@@ -1,7 +1,7 @@
C C-LB+o-r+o-data-o
//\begin[snippet][labelbase=ln:formal:C-LB+o-r+o-data-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -15,7 +15,6 @@ P0(int *x0, int *x1)
smp_store_release(x0, 2);
}
-
P1(int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus
index 65da9ea2..dff95bf2 100644
--- a/CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus
+++ b/CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus
@@ -1,28 +1,24 @@
C C-MP+o-o+o-rmb-o
//\begin[snippet][labelbase=ln:formal:C-MP+o-o+o-rmb-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
} //\fcvexclude
//\fcvexclude
P0(int* x0, int* x1) {
-
WRITE_ONCE(*x0, 2);
WRITE_ONCE(*x1, 2);
-
}
P1(int* x0, int* x1) {
-
int r2;
int r3;
r2 = READ_ONCE(*x1);
smp_rmb();
r3 = READ_ONCE(*x0);
-
}
//\end[snippet]
diff --git a/CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus b/CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus
index b08ad06b..28cb9e2a 100644
--- a/CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus
+++ b/CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus
@@ -1,17 +1,15 @@
C C-MP+o-r+o-ctrl-o
//\begin[snippet][labelbase=ln:formal:C-MP+o-r+o-ctrl-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
} //\fcvexclude
//\fcvexclude
P0(int* x0, int* x1) {
-
WRITE_ONCE(*x0, 2);
smp_store_release(x1, 2);
-
}
P1(int* x0, int* x1) {
@@ -21,7 +19,6 @@ P1(int* x0, int* x1) {
r2 = READ_ONCE(*x1); //\lnlbl[ld1]
if (r2 >= 0)
r3 = READ_ONCE(*x0); //\lnlbl[ld2]
-
}
//\end[snippet]
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
index 865943e5..bb62bd17 100644
--- a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus
@@ -11,21 +11,17 @@ x1=y; (* \lnlbl[init:x1] *)
} //\fcvexclude
//\fcvexclude
P0(int* x0, int** x1) {
-
WRITE_ONCE(*x0, 2); //\lnlbl[P0:x0]
smp_wmb(); //\lnlbl[P0:wmb]
WRITE_ONCE(*x1, x0); //\lnlbl[P0:x1]
-
}
P1(int** x1) {
-
int *r2;
int r3;
r2 = READ_ONCE(*x1); //\lnlbl[P1:x1]
r3 = READ_ONCE(*r2); //\lnlbl[P1:ref]
-
}
//\end[snippet]
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus
index 469ba780..6c566314 100644
--- a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus
@@ -1,29 +1,24 @@
C C-MP+o-wmb-o+o-o
//\begin[snippet][labelbase=ln:formal:C-MP+o-wmb-o+o-o:whole,commandchars=\@\[\]]
-{
-}
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
} //\fcvexclude
//\fcvexclude
P0(int* x0, int* x1) {
-
WRITE_ONCE(*x0, 2);
smp_wmb();
WRITE_ONCE(*x1, 2);
-
}
P1(int* x0, int* x1) {
-
int r2;
int r3;
r2 = READ_ONCE(*x1);
r3 = READ_ONCE(*x0);
-
}
//\end[snippet]
diff --git a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus
index 5b5bf45a..60d379d6 100644
--- a/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus
+++ b/CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus
@@ -1,30 +1,25 @@
C C-MP+o-wmb-o+o-rmb-o
//\begin[snippet][labelbase=ln:formal:C-MP+o-wmb-o+o-rmb-o:whole,commandchars=\@\[\]]
-{
-}
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
} //\fcvexclude
//\fcvexclude
P0(int* x0, int* x1) {
-
WRITE_ONCE(*x0, 2);
smp_wmb();
WRITE_ONCE(*x1, 2);
-
}
P1(int* x0, int* x1) {
-
int r2;
int r3;
r2 = READ_ONCE(*x1);
smp_rmb(); //\lnlbl[rmb]
r3 = READ_ONCE(*x0);
-
}
//\end[snippet]
diff --git a/CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus
index a84573a6..c48622a6 100644
--- a/CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus
+++ b/CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus
@@ -1,7 +1,7 @@
C C-MP-OMCA+o-o-o+o-rmb-o
//\begin[snippet][labelbase=ln:formal:C-MP-OMCA+o-o-o+o-rmb-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus
index 7e9a5bba..e4e15b01 100644
--- a/CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus
+++ b/CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus
@@ -1,7 +1,7 @@
C C-R+o-wmb-o+o-mb-o
//\begin[snippet][labelbase=ln:formal:C-R+o-wmb-o+o-mb-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -14,7 +14,6 @@ P0(int *x0, int *x1)
WRITE_ONCE(*x1, 1);
}
-
P1(int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus b/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
index 11171cd5..3bbcc4f1 100644
--- a/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
+++ b/CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus
@@ -11,20 +11,16 @@ x1=y;
} //\fcvexclude
//\fcvexclude
P0(int* x0, int** x1) {
-
WRITE_ONCE(*x0, 2); //\lnlbl[P0:x0]
smp_wmb();
WRITE_ONCE(*x1, x0);
-
}
P1(int** x1) {
-
int *r2;
r2 = READ_ONCE(*x1); //\lnlbl[P1:x1]
WRITE_ONCE(*r2, 3); //\lnlbl[P1:r2]
-
}
//\end[snippet]
diff --git a/CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus b/CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus
index 0357306b..4922680c 100644
--- a/CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus
+++ b/CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus
@@ -1,7 +1,7 @@
C C-SB+o-mb-o+o-mb-o
//\begin[snippet][labelbase=ln:formal:C-SB+o-mb-o+o-mb-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -16,7 +16,6 @@ P0(int *x0, int *x1)
r2 = READ_ONCE(*x1); //\lnlbl[P0:ld]
}
-
P1(int *x0, int *x1)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus b/CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus
index 85022aea..fabcb5d5 100644
--- a/CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus
+++ b/CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus
@@ -1,7 +1,7 @@
C C-SB+o-o+o-o
//\begin[snippet][labelbase=ln:formal:C-SB+o-o+o-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -15,7 +15,6 @@ P0(int *x0, int *x1)
r2 = READ_ONCE(*x1); //\lnlbl[ld0]
}
-
P1(int *x0, int *x1)
{
int r2;
@@ -23,5 +22,6 @@ P1(int *x0, int *x1)
WRITE_ONCE(*x1, 2); //\lnlbl[st1]
r2 = READ_ONCE(*x0); //\lnlbl[ld1]
}
+
//\end[snippet]
exists (1:r2=0 /\ 0:r2=0)
diff --git a/CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus b/CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
index e1502963..8076c0c6 100644
--- a/CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
+++ b/CodeSamples/formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus
@@ -1,7 +1,6 @@
C C-SB-OMCA+o-o-rmb-o+o-o-rmb-o
-{
-}
+{}
{
#include "api.h"
@@ -18,7 +17,6 @@ P0(int *x0, int *x1)
r2 = READ_ONCE(*x1);
}
-
P1(int *x0, int *x1)
{
int r1;
diff --git a/CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus b/CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus
index 88225dde..b0960253 100644
--- a/CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus
+++ b/CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus
@@ -1,7 +1,7 @@
C C-WRC+o+o-data-o+o-rmb-o
//\begin[snippet][labelbase=ln:formal:C-WRC+o+o-data-o+o-rmb-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus b/CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus
index 4cd69b8f..a1f000b8 100644
--- a/CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus
+++ b/CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus
@@ -1,8 +1,7 @@
C C-WRC+o+o-r+a-o
//\begin[snippet][labelbase=ln:formal:C-WRC+o+o-r+a-o:whole,commandchars=\@\[\]]
-{
-}
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
index 015bcd0f..81c0a96a 100644
--- a/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus
@@ -1,6 +1,6 @@
C C-WWC+o-cge-o+o-cge-o+o+dstb
-{
-}
+
+{}
{
#include "api.h"
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus
index 3fcd502c..1c15a01a 100644
--- a/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus
@@ -1,6 +1,6 @@
C C-WWC+o-cge-o+o-cge-o+o
-{
-}
+
+{}
{
#include "api.h"
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
index 989d99fe..aada09f5 100644
--- a/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus
@@ -1,6 +1,6 @@
C C-WWC+o-cgt-o+o-cgt-o+o+dstb
-{
-}
+
+{}
{
#include "api.h"
diff --git a/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus
index 9003fdce..1fd2db6f 100644
--- a/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus
+++ b/CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus
@@ -1,7 +1,7 @@
C C-WWC+o-cgt-o+o-cgt-o+o
//\begin[snippet][labelbase=ln:formal:C-WWC+o-cgt-o+o-cgt-o+o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
diff --git a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus
index dc89015d..db90e958 100644
--- a/CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus
+++ b/CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus
@@ -1,7 +1,7 @@
C C-Z6.2+o-r+a-r+a-r+a-o
//\begin[snippet][labelbase=ln:formal:C-Z6.2+o-r+a-r+a-r+a-o:whole,commandchars=\@\[\]]
-{
-}
+
+{}
{ //\fcvexclude
#include "api.h" //\fcvexclude
@@ -13,7 +13,6 @@ P0(int *x0, int *x1)
smp_store_release(x1, 2);
}
-
P1(int *x1, int *x2)
{
int r2;
diff --git a/CodeSamples/formal/litmus/C-cmpxchg.litmus b/CodeSamples/formal/litmus/C-cmpxchg.litmus
index 9579d4a7..aba438bd 100644
--- a/CodeSamples/formal/litmus/C-cmpxchg.litmus
+++ b/CodeSamples/formal/litmus/C-cmpxchg.litmus
@@ -1,6 +1,6 @@
C C-cmpxchg
-{
-}
+
+{}
{
#include "api.h"
--
2.17.1
^ permalink raw reply related [flat|nested] 10+ messages in thread
* Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests
2020-11-14 4:51 [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests Akira Yokosawa
2020-11-14 4:54 ` [PATCH perfbook 1/2] CodeSamples/formal/litmus: Remove redundant initialization Akira Yokosawa
2020-11-14 4:56 ` [PATCH perfbook 2/2] CodeSamples/formal: Use '{}' for empty init blocks in litmus tests Akira Yokosawa
@ 2020-11-15 20:42 ` Paul E. McKenney
2020-11-15 22:25 ` Akira Yokosawa
2 siblings, 1 reply; 10+ messages in thread
From: Paul E. McKenney @ 2020-11-15 20:42 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
> Hi Paul,
>
> This patch set is what I mentioned the other day in response to
> your LKMM patch for 5.11.
> klitmus7 doesn't need most of type info in litmus-test init blocks.
>
> While there are some cases where klitmus7 requires type info of variables
> to be watched (via the "exists", "locations", or "filter" directive),
> as long as the watched variables are of type "int", extra type info
> in the init block is not required.
>
> Litmus tests under CodeSamples/formal/ should keep compatible with
> klitmus7 after this patch set is applied.
>
> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
> under CodeSamples/formal/litmus/.
>
> Patch 2/2 further reduce line counts of litmus tests by using "{}"
> as empty init blocks.
> It also adds/removes empty lines for those code snippets to have
> consistent looks.
>
> Similar changes to patch 1/2 can be made in the RCU litmus tests
> presented in Section 12.3.2. They are not touched in this patch set.
>
> May be in a follow-up patch.
Queued and pushed, thank you very much!
> Thanks, Akira
>
> *NOTE*:
>
> There are cases where litmus tests for herd7 can not be
> made compatible with (current) klitmus7, though.
>
> One such example is when a variable of a type other than the "int"
> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
> directive.
> Current klitmus7 has no idea of the way to obtain the value of such a
> variable.
Good to know! Do we have litmus tests that have problems with this?
> As for herd7, all the variables are treated as if they were "int" or
> "int *" regardless of the type specified in the litmus tests, there
> is no such problem.
Indeed, herd7 lets you get away with quite a bit. ;-)
Thanx, Paul
> --
> Akira Yokosawa (2):
> CodeSamples/formal/litmus: Remove redundant initializations
> CodeSamples/formal: Use '{}' for empty init blocks in litmus tests
>
> CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 5 ++---
> CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 5 ++---
> CodeSamples/formal/herd/C-Lock1.litmus | 5 +++--
> CodeSamples/formal/herd/C-Lock2.litmus | 5 +++--
> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus | 3 +--
> .../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 5 ++---
> CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 5 ++---
> ...B+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 7 ++-----
> .../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 5 ++---
> .../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 5 ++---
> .../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 5 ++---
> .../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 6 ++----
> .../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 5 ++---
> .../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus | 5 ++---
> .../formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus | 5 ++---
> .../formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 4 ++--
> .../formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus | 4 ++--
> CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus | 4 ++--
> CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus | 4 ++--
> .../formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus | 7 +++----
> CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus | 6 +++---
> CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus | 8 ++------
> CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus | 7 ++-----
> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 8 ++------
> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus | 7 +------
> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus | 7 +------
> CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 4 ++--
> CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 8 ++------
> CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus | 6 +++---
> .../formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 4 +---
> .../formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 6 +-----
> CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus | 6 +-----
> CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus | 4 ++--
> CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus | 3 +--
> .../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 6 ++----
> CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 6 ++----
> .../formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 4 ++--
> CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus | 4 ++--
> .../formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 4 ++--
> CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 4 ++--
> CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 6 +-----
> CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 5 ++---
> CodeSamples/formal/litmus/C-cmpxchg.litmus | 4 ++--
> memorder/memorder.tex | 8 ++------
> 73 files changed, 124 insertions(+), 217 deletions(-)
>
> --
> 2.17.1
>
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests
2020-11-15 20:42 ` [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of " Paul E. McKenney
@ 2020-11-15 22:25 ` Akira Yokosawa
2020-11-21 1:14 ` Paul E. McKenney
0 siblings, 1 reply; 10+ messages in thread
From: Akira Yokosawa @ 2020-11-15 22:25 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote:
> On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
>> Hi Paul,
>>
>> This patch set is what I mentioned the other day in response to
>> your LKMM patch for 5.11.
>> klitmus7 doesn't need most of type info in litmus-test init blocks.
>>
>> While there are some cases where klitmus7 requires type info of variables
>> to be watched (via the "exists", "locations", or "filter" directive),
>> as long as the watched variables are of type "int", extra type info
>> in the init block is not required.
>>
>> Litmus tests under CodeSamples/formal/ should keep compatible with
>> klitmus7 after this patch set is applied.
>>
>> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
>> under CodeSamples/formal/litmus/.
>>
>> Patch 2/2 further reduce line counts of litmus tests by using "{}"
>> as empty init blocks.
>> It also adds/removes empty lines for those code snippets to have
>> consistent looks.
>>
>> Similar changes to patch 1/2 can be made in the RCU litmus tests
>> presented in Section 12.3.2. They are not touched in this patch set.
>>
>> May be in a follow-up patch.
>
> Queued and pushed, thank you very much!
>
>> Thanks, Akira
>>
>> *NOTE*:
>>
>> There are cases where litmus tests for herd7 can not be
>> made compatible with (current) klitmus7, though.
>>
>> One such example is when a variable of a type other than the "int"
>> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
>> directive.
>> Current klitmus7 has no idea of the way to obtain the value of such a
>> variable.
>
> Good to know! Do we have litmus tests that have problems with this?
One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus
---
C Lock1-for-herd7
(*
* Example test incompatible with klitmus7
*
* klitmus7 cannot access spinlock_t variable.
*)
{}
P0(int *x, spinlock_t *sp)
{
spin_lock(sp);
WRITE_ONCE(*x, 1);
WRITE_ONCE(*x, 0);
spin_unlock(sp);
}
P1(int *x, spinlock_t *sp)
{
int r1;
spin_lock(sp);
r1 = READ_ONCE(*x);
spin_unlock(sp);
}
locations [sp] (* incompatible with klitmus7 *)
exists (1:r1=1)
---
klitmus7 can't convert this to a kernel module:
---
$ klitmus7 -o temp C-Lock1-for-herd7.litmus
File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t
---
Actually, herd7/LKMM does complain of this one:
---
Test Lock1-for-herd7 Allowed
States 1
1:r1=0; sp=0;
No
Witnesses
Positive: 0 Negative: 2
Flag lock-final <---
Condition exists (1:r1=1)
Observation Lock1-for-herd7 Never 0 2
Time Lock1-for-herd7 0.01
Hash=5d10e6c355cec0c36f354abf175adc54
---
Comment at line 57 of lock.cat says:
---
(* The final value of a spinlock should not be tested *)
flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
---
Thanks, Akira
>
>> As for herd7, all the variables are treated as if they were "int" or
>> "int *" regardless of the type specified in the litmus tests, there
>> is no such problem.
>
> Indeed, herd7 lets you get away with quite a bit. ;-)
>
> Thanx, Paul
>
>> --
>> Akira Yokosawa (2):
>> CodeSamples/formal/litmus: Remove redundant initializations
>> CodeSamples/formal: Use '{}' for empty init blocks in litmus tests
>>
>> CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 5 ++---
>> CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 5 ++---
>> CodeSamples/formal/herd/C-Lock1.litmus | 5 +++--
>> CodeSamples/formal/herd/C-Lock2.litmus | 5 +++--
>> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
>> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
>> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
>> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
>> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
>> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
>> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
>> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
>> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
>> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
>> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
>> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
>> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
>> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
>> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
>> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus | 3 +--
>> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
>> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus | 3 +--
>> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
>> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus | 3 +--
>> .../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 5 ++---
>> CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 5 ++---
>> ...B+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 7 ++-----
>> .../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 5 ++---
>> .../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 5 ++---
>> .../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 5 ++---
>> .../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 6 ++----
>> .../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 5 ++---
>> .../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus | 5 ++---
>> .../formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus | 5 ++---
>> .../formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 4 ++--
>> .../formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus | 4 ++--
>> CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus | 4 ++--
>> CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus | 4 ++--
>> .../formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus | 7 +++----
>> CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus | 6 +++---
>> CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus | 8 ++------
>> CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus | 7 ++-----
>> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 8 ++------
>> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus | 7 +------
>> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus | 7 +------
>> CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 4 ++--
>> CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 8 ++------
>> CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus | 6 +++---
>> .../formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 4 +---
>> .../formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 6 +-----
>> CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus | 6 +-----
>> CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus | 4 ++--
>> CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus | 3 +--
>> .../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 6 ++----
>> CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 6 ++----
>> .../formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 4 ++--
>> CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus | 4 ++--
>> .../formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 4 ++--
>> CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 4 ++--
>> CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 6 +-----
>> CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 5 ++---
>> CodeSamples/formal/litmus/C-cmpxchg.litmus | 4 ++--
>> memorder/memorder.tex | 8 ++------
>> 73 files changed, 124 insertions(+), 217 deletions(-)
>>
>> --
>> 2.17.1
>>
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests
2020-11-15 22:25 ` Akira Yokosawa
@ 2020-11-21 1:14 ` Paul E. McKenney
2020-11-21 2:51 ` Akira Yokosawa
0 siblings, 1 reply; 10+ messages in thread
From: Paul E. McKenney @ 2020-11-21 1:14 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Mon, Nov 16, 2020 at 07:25:09AM +0900, Akira Yokosawa wrote:
> On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote:
> > On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
> >> Hi Paul,
> >>
> >> This patch set is what I mentioned the other day in response to
> >> your LKMM patch for 5.11.
> >> klitmus7 doesn't need most of type info in litmus-test init blocks.
> >>
> >> While there are some cases where klitmus7 requires type info of variables
> >> to be watched (via the "exists", "locations", or "filter" directive),
> >> as long as the watched variables are of type "int", extra type info
> >> in the init block is not required.
> >>
> >> Litmus tests under CodeSamples/formal/ should keep compatible with
> >> klitmus7 after this patch set is applied.
> >>
> >> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
> >> under CodeSamples/formal/litmus/.
> >>
> >> Patch 2/2 further reduce line counts of litmus tests by using "{}"
> >> as empty init blocks.
> >> It also adds/removes empty lines for those code snippets to have
> >> consistent looks.
> >>
> >> Similar changes to patch 1/2 can be made in the RCU litmus tests
> >> presented in Section 12.3.2. They are not touched in this patch set.
> >>
> >> May be in a follow-up patch.
> >
> > Queued and pushed, thank you very much!
> >
> >> Thanks, Akira
> >>
> >> *NOTE*:
> >>
> >> There are cases where litmus tests for herd7 can not be
> >> made compatible with (current) klitmus7, though.
> >>
> >> One such example is when a variable of a type other than the "int"
> >> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
> >> directive.
> >> Current klitmus7 has no idea of the way to obtain the value of such a
> >> variable.
> >
> > Good to know! Do we have litmus tests that have problems with this?
>
> One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus
So there is not currently such a litmus test in perfbook, but one could
easily be created, correct?
Or am I still confused? ;-)
Thanx, Paul
> ---
> C Lock1-for-herd7
>
> (*
> * Example test incompatible with klitmus7
> *
> * klitmus7 cannot access spinlock_t variable.
> *)
>
> {}
>
> P0(int *x, spinlock_t *sp)
> {
> spin_lock(sp);
> WRITE_ONCE(*x, 1);
> WRITE_ONCE(*x, 0);
> spin_unlock(sp);
> }
>
> P1(int *x, spinlock_t *sp)
> {
> int r1;
>
> spin_lock(sp);
> r1 = READ_ONCE(*x);
> spin_unlock(sp);
> }
>
> locations [sp] (* incompatible with klitmus7 *)
> exists (1:r1=1)
> ---
>
> klitmus7 can't convert this to a kernel module:
>
> ---
> $ klitmus7 -o temp C-Lock1-for-herd7.litmus
> File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t
> ---
>
> Actually, herd7/LKMM does complain of this one:
>
> ---
> Test Lock1-for-herd7 Allowed
> States 1
> 1:r1=0; sp=0;
> No
> Witnesses
> Positive: 0 Negative: 2
> Flag lock-final <---
> Condition exists (1:r1=1)
> Observation Lock1-for-herd7 Never 0 2
> Time Lock1-for-herd7 0.01
> Hash=5d10e6c355cec0c36f354abf175adc54
> ---
>
> Comment at line 57 of lock.cat says:
>
> ---
> (* The final value of a spinlock should not be tested *)
> flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> ---
>
> Thanks, Akira
>
> >
> >> As for herd7, all the variables are treated as if they were "int" or
> >> "int *" regardless of the type specified in the litmus tests, there
> >> is no such problem.
> >
> > Indeed, herd7 lets you get away with quite a bit. ;-)
> >
> > Thanx, Paul
> >
> >> --
> >> Akira Yokosawa (2):
> >> CodeSamples/formal/litmus: Remove redundant initializations
> >> CodeSamples/formal: Use '{}' for empty init blocks in litmus tests
> >>
> >> CodeSamples/formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 5 ++---
> >> CodeSamples/formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 5 ++---
> >> CodeSamples/formal/herd/C-Lock1.litmus | 5 +++--
> >> CodeSamples/formal/herd/C-Lock2.litmus | 5 +++--
> >> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> ...C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> .../C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> .../herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> .../formal/herd/C-SB+l-o-o-u+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-C.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-CE.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-X.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u-XE.litmus | 3 +--
> >> CodeSamples/formal/herd/C-SB+l-o-o-u+l-o-o-u.litmus | 3 +--
> >> .../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 5 ++---
> >> CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 5 ++---
> >> ...B+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 7 ++-----
> >> .../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 5 ++---
> >> .../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 5 ++---
> >> .../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 5 ++---
> >> .../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 6 ++----
> >> .../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 5 ++---
> >> .../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-2+2W+o-o+o-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-2+2W+o-wmb-o+o-wmb-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-CCIRIW+o+o+o-o+o-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-ISA2+o-r+a-r+a-r+a-o.litmus | 5 ++---
> >> .../formal/litmus/C-LB+a-o+o-data-o+o-data-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-LB+a-r+a-r+a-r+a-r.litmus | 5 ++---
> >> .../formal/litmus/C-LB+cmpxchg-ctrl-o+o-ctrl-o.litmus | 4 ++--
> >> .../formal/litmus/C-LB+o-cge-o+o-cge-o+dstb.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-LB+o-cge-o+o-cge-o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-LB+o-cgt-o+o-cgt-o.litmus | 4 ++--
> >> .../formal/litmus/C-LB+o-data-o+o-data-o+o-data-o.litmus | 7 +++----
> >> CodeSamples/formal/litmus/C-LB+o-o+o-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-LB+o-r+a-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-LB+o-r+o-ctrl-o.litmus | 6 +++---
> >> CodeSamples/formal/litmus/C-LB+o-r+o-data-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-MP+o-o+o-rmb-o.litmus | 8 ++------
> >> CodeSamples/formal/litmus/C-MP+o-r+o-ctrl-o.litmus | 7 ++-----
> >> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-addr-o.litmus | 8 ++------
> >> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-o.litmus | 7 +------
> >> CodeSamples/formal/litmus/C-MP+o-wmb-o+o-rmb-o.litmus | 7 +------
> >> CodeSamples/formal/litmus/C-MP-OMCA+o-o-o+o-rmb-o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-R+o-wmb-o+o-mb-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-S+o-wmb-o+o-addr-o.litmus | 8 ++------
> >> CodeSamples/formal/litmus/C-SB+o-mb-o+o-mb-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-SB+o-o+o-o.litmus | 6 +++---
> >> .../formal/litmus/C-SB-OMCA+o-o-rmb-o+o-o-rmb-o.litmus | 4 +---
> >> .../formal/litmus/C-W+RWC+o-mb-o+a-o+o-mb-o.litmus | 6 +-----
> >> CodeSamples/formal/litmus/C-W+RWC+o-r+a-o+o-mb-o.litmus | 6 +-----
> >> CodeSamples/formal/litmus/C-WRC+o+o-data-o+o-rmb-o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-WRC+o+o-r+a-o.litmus | 3 +--
> >> .../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 6 ++----
> >> CodeSamples/formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 6 ++----
> >> .../formal/litmus/C-WWC+o-cge-o+o-cge-o+o+dstb.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-WWC+o-cge-o+o-cge-o+o.litmus | 4 ++--
> >> .../formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o+dstb.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-WWC+o-cgt-o+o-cgt-o+o.litmus | 4 ++--
> >> CodeSamples/formal/litmus/C-Z6.2+o-r+a-o+o-mb-o.litmus | 6 +-----
> >> CodeSamples/formal/litmus/C-Z6.2+o-r+a-r+a-r+a-o.litmus | 5 ++---
> >> CodeSamples/formal/litmus/C-cmpxchg.litmus | 4 ++--
> >> memorder/memorder.tex | 8 ++------
> >> 73 files changed, 124 insertions(+), 217 deletions(-)
> >>
> >> --
> >> 2.17.1
> >>
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests
2020-11-21 1:14 ` Paul E. McKenney
@ 2020-11-21 2:51 ` Akira Yokosawa
2020-11-21 3:47 ` Paul E. McKenney
0 siblings, 1 reply; 10+ messages in thread
From: Akira Yokosawa @ 2020-11-21 2:51 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, Akira Yokosawa
On Fri, 20 Nov 2020 17:14:10 -0800, Paul E. McKenney wrote:
> On Mon, Nov 16, 2020 at 07:25:09AM +0900, Akira Yokosawa wrote:
>> On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote:
>>> On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
>>>> Hi Paul,
>>>>
>>>> This patch set is what I mentioned the other day in response to
>>>> your LKMM patch for 5.11.
>>>> klitmus7 doesn't need most of type info in litmus-test init blocks.
>>>>
>>>> While there are some cases where klitmus7 requires type info of variables
>>>> to be watched (via the "exists", "locations", or "filter" directive),
>>>> as long as the watched variables are of type "int", extra type info
>>>> in the init block is not required.
>>>>
>>>> Litmus tests under CodeSamples/formal/ should keep compatible with
>>>> klitmus7 after this patch set is applied.
>>>>
>>>> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
>>>> under CodeSamples/formal/litmus/.
>>>>
>>>> Patch 2/2 further reduce line counts of litmus tests by using "{}"
>>>> as empty init blocks.
>>>> It also adds/removes empty lines for those code snippets to have
>>>> consistent looks.
>>>>
>>>> Similar changes to patch 1/2 can be made in the RCU litmus tests
>>>> presented in Section 12.3.2. They are not touched in this patch set.
>>>>
>>>> May be in a follow-up patch.
>>>
>>> Queued and pushed, thank you very much!
>>>
>>>> Thanks, Akira
>>>>
>>>> *NOTE*:
>>>>
>>>> There are cases where litmus tests for herd7 can not be
>>>> made compatible with (current) klitmus7, though.
>>>>
>>>> One such example is when a variable of a type other than the "int"
>>>> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
>>>> directive.
>>>> Current klitmus7 has no idea of the way to obtain the value of such a
>>>> variable.
>>>
>>> Good to know! Do we have litmus tests that have problems with this?
>>
>> One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus
>
> So there is not currently such a litmus test in perfbook, but one could
> easily be created, correct?
You are right!
Thanks, Akira
PS.
I'm preparing a patch series to add an index framework in perfbook.
My plan is to add a specific make target for the time being to have such
index pages printed.
As you should know, the hard part is to embed a *lot* of index annotations
in .tex source files.
I'm thinking of splitting indexes into a general one and API index.
By API, I mean functions such as smp_mb(), READ_ONCE(), etc.
API index can have kernel API, perfbook specific API, C11 API, and GCC API.
As for words/terms, if you can provide me a wish list you'd like to see in
the general index, I'm willing to add such annotations.
My starting point of the general index is the Glossary.
Thoughts?
>
> Or am I still confused? ;-)
>
> Thanx, Paul
>
>> ---
>> C Lock1-for-herd7
>>
>> (*
>> * Example test incompatible with klitmus7
>> *
>> * klitmus7 cannot access spinlock_t variable.
>> *)
>>
>> {}
>>
>> P0(int *x, spinlock_t *sp)
>> {
>> spin_lock(sp);
>> WRITE_ONCE(*x, 1);
>> WRITE_ONCE(*x, 0);
>> spin_unlock(sp);
>> }
>>
>> P1(int *x, spinlock_t *sp)
>> {
>> int r1;
>>
>> spin_lock(sp);
>> r1 = READ_ONCE(*x);
>> spin_unlock(sp);
>> }
>>
>> locations [sp] (* incompatible with klitmus7 *)
>> exists (1:r1=1)
>> ---
>>
>> klitmus7 can't convert this to a kernel module:
>>
>> ---
>> $ klitmus7 -o temp C-Lock1-for-herd7.litmus
>> File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t
>> ---
>>
>> Actually, herd7/LKMM does complain of this one:
>>
>> ---
>> Test Lock1-for-herd7 Allowed
>> States 1
>> 1:r1=0; sp=0;
>> No
>> Witnesses
>> Positive: 0 Negative: 2
>> Flag lock-final <---
>> Condition exists (1:r1=1)
>> Observation Lock1-for-herd7 Never 0 2
>> Time Lock1-for-herd7 0.01
>> Hash=5d10e6c355cec0c36f354abf175adc54
>> ---
>>
>> Comment at line 57 of lock.cat says:
>>
>> ---
>> (* The final value of a spinlock should not be tested *)
>> flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
>> ---
>>
>> Thanks, Akira
>>
[...]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests
2020-11-21 2:51 ` Akira Yokosawa
@ 2020-11-21 3:47 ` Paul E. McKenney
2020-11-21 4:14 ` Index in Perfbook (was Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests) Akira Yokosawa
0 siblings, 1 reply; 10+ messages in thread
From: Paul E. McKenney @ 2020-11-21 3:47 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sat, Nov 21, 2020 at 11:51:11AM +0900, Akira Yokosawa wrote:
> On Fri, 20 Nov 2020 17:14:10 -0800, Paul E. McKenney wrote:
> > On Mon, Nov 16, 2020 at 07:25:09AM +0900, Akira Yokosawa wrote:
> >> On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote:
> >>> On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
> >>>> Hi Paul,
> >>>>
> >>>> This patch set is what I mentioned the other day in response to
> >>>> your LKMM patch for 5.11.
> >>>> klitmus7 doesn't need most of type info in litmus-test init blocks.
> >>>>
> >>>> While there are some cases where klitmus7 requires type info of variables
> >>>> to be watched (via the "exists", "locations", or "filter" directive),
> >>>> as long as the watched variables are of type "int", extra type info
> >>>> in the init block is not required.
> >>>>
> >>>> Litmus tests under CodeSamples/formal/ should keep compatible with
> >>>> klitmus7 after this patch set is applied.
> >>>>
> >>>> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
> >>>> under CodeSamples/formal/litmus/.
> >>>>
> >>>> Patch 2/2 further reduce line counts of litmus tests by using "{}"
> >>>> as empty init blocks.
> >>>> It also adds/removes empty lines for those code snippets to have
> >>>> consistent looks.
> >>>>
> >>>> Similar changes to patch 1/2 can be made in the RCU litmus tests
> >>>> presented in Section 12.3.2. They are not touched in this patch set.
> >>>>
> >>>> May be in a follow-up patch.
> >>>
> >>> Queued and pushed, thank you very much!
> >>>
> >>>> Thanks, Akira
> >>>>
> >>>> *NOTE*:
> >>>>
> >>>> There are cases where litmus tests for herd7 can not be
> >>>> made compatible with (current) klitmus7, though.
> >>>>
> >>>> One such example is when a variable of a type other than the "int"
> >>>> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
> >>>> directive.
> >>>> Current klitmus7 has no idea of the way to obtain the value of such a
> >>>> variable.
> >>>
> >>> Good to know! Do we have litmus tests that have problems with this?
> >>
> >> One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus
> >
> > So there is not currently such a litmus test in perfbook, but one could
> > easily be created, correct?
>
> You are right!
>
> Thanks, Akira
>
> PS.
>
> I'm preparing a patch series to add an index framework in perfbook.
> My plan is to add a specific make target for the time being to have such
> index pages printed.
> As you should know, the hard part is to embed a *lot* of index annotations
> in .tex source files.
Quite right, it is a big job!
> I'm thinking of splitting indexes into a general one and API index.
> By API, I mean functions such as smp_mb(), READ_ONCE(), etc.
>
> API index can have kernel API, perfbook specific API, C11 API, and GCC API.
The upside is that the individual indexes are smaller and perhaps
more manageable. The downside is that a reader who has no idea
what the function call is might have to look it up in four (or maybe
even five) indexes. Especially if the API is a historic API that
is no longer used.
I have no idea what the right answer is. One approach would be to
have all of the APIs appear both in their respective categories and
in the general index. Not sure that this would be any better, though.
> As for words/terms, if you can provide me a wish list you'd like to see in
> the general index, I'm willing to add such annotations.
> My starting point of the general index is the Glossary.
The glossary is a good starting point. People mentioned in the text is
another. Not sure whether or not those quoted in the epigraphs should
be included or not. Names of algorithms should be included, also names
of data structures and of famous problems (for example, the Dining
Philosopher's problem, mazes, and so on).
I am sure that I am missing quite a few categories, but at least a
start! ;-)
Thanx, Paul
> Thoughts?
>
> >
> > Or am I still confused? ;-)
> >
> > Thanx, Paul
> >
> >> ---
> >> C Lock1-for-herd7
> >>
> >> (*
> >> * Example test incompatible with klitmus7
> >> *
> >> * klitmus7 cannot access spinlock_t variable.
> >> *)
> >>
> >> {}
> >>
> >> P0(int *x, spinlock_t *sp)
> >> {
> >> spin_lock(sp);
> >> WRITE_ONCE(*x, 1);
> >> WRITE_ONCE(*x, 0);
> >> spin_unlock(sp);
> >> }
> >>
> >> P1(int *x, spinlock_t *sp)
> >> {
> >> int r1;
> >>
> >> spin_lock(sp);
> >> r1 = READ_ONCE(*x);
> >> spin_unlock(sp);
> >> }
> >>
> >> locations [sp] (* incompatible with klitmus7 *)
> >> exists (1:r1=1)
> >> ---
> >>
> >> klitmus7 can't convert this to a kernel module:
> >>
> >> ---
> >> $ klitmus7 -o temp C-Lock1-for-herd7.litmus
> >> File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t
> >> ---
> >>
> >> Actually, herd7/LKMM does complain of this one:
> >>
> >> ---
> >> Test Lock1-for-herd7 Allowed
> >> States 1
> >> 1:r1=0; sp=0;
> >> No
> >> Witnesses
> >> Positive: 0 Negative: 2
> >> Flag lock-final <---
> >> Condition exists (1:r1=1)
> >> Observation Lock1-for-herd7 Never 0 2
> >> Time Lock1-for-herd7 0.01
> >> Hash=5d10e6c355cec0c36f354abf175adc54
> >> ---
> >>
> >> Comment at line 57 of lock.cat says:
> >>
> >> ---
> >> (* The final value of a spinlock should not be tested *)
> >> flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> >> ---
> >>
> >> Thanks, Akira
> >>
>
> [...]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Index in Perfbook (was Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests)
2020-11-21 3:47 ` Paul E. McKenney
@ 2020-11-21 4:14 ` Akira Yokosawa
2020-11-22 3:52 ` Paul E. McKenney
0 siblings, 1 reply; 10+ messages in thread
From: Akira Yokosawa @ 2020-11-21 4:14 UTC (permalink / raw)
To: paulmck; +Cc: perfbook, Akira Yokosawa
On Fri, 20 Nov 2020 19:47:14 -0800, Paul E. McKenney wrote:
> On Sat, Nov 21, 2020 at 11:51:11AM +0900, Akira Yokosawa wrote:
>> On Fri, 20 Nov 2020 17:14:10 -0800, Paul E. McKenney wrote:
>>> On Mon, Nov 16, 2020 at 07:25:09AM +0900, Akira Yokosawa wrote:
>>>> On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote:
>>>>> On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
>>>>>> Hi Paul,
>>>>>>
>>>>>> This patch set is what I mentioned the other day in response to
>>>>>> your LKMM patch for 5.11.
>>>>>> klitmus7 doesn't need most of type info in litmus-test init blocks.
>>>>>>
>>>>>> While there are some cases where klitmus7 requires type info of variables
>>>>>> to be watched (via the "exists", "locations", or "filter" directive),
>>>>>> as long as the watched variables are of type "int", extra type info
>>>>>> in the init block is not required.
>>>>>>
>>>>>> Litmus tests under CodeSamples/formal/ should keep compatible with
>>>>>> klitmus7 after this patch set is applied.
>>>>>>
>>>>>> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
>>>>>> under CodeSamples/formal/litmus/.
>>>>>>
>>>>>> Patch 2/2 further reduce line counts of litmus tests by using "{}"
>>>>>> as empty init blocks.
>>>>>> It also adds/removes empty lines for those code snippets to have
>>>>>> consistent looks.
>>>>>>
>>>>>> Similar changes to patch 1/2 can be made in the RCU litmus tests
>>>>>> presented in Section 12.3.2. They are not touched in this patch set.
>>>>>>
>>>>>> May be in a follow-up patch.
>>>>>
>>>>> Queued and pushed, thank you very much!
>>>>>
>>>>>> Thanks, Akira
>>>>>>
>>>>>> *NOTE*:
>>>>>>
>>>>>> There are cases where litmus tests for herd7 can not be
>>>>>> made compatible with (current) klitmus7, though.
>>>>>>
>>>>>> One such example is when a variable of a type other than the "int"
>>>>>> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
>>>>>> directive.
>>>>>> Current klitmus7 has no idea of the way to obtain the value of such a
>>>>>> variable.
>>>>>
>>>>> Good to know! Do we have litmus tests that have problems with this?
>>>>
>>>> One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus
>>>
>>> So there is not currently such a litmus test in perfbook, but one could
>>> easily be created, correct?
>>
>> You are right!
>>
>> Thanks, Akira
>>
>> PS.
>>
>> I'm preparing a patch series to add an index framework in perfbook.
>> My plan is to add a specific make target for the time being to have such
>> index pages printed.
>> As you should know, the hard part is to embed a *lot* of index annotations
>> in .tex source files.
>
> Quite right, it is a big job!
>
>> I'm thinking of splitting indexes into a general one and API index.
>> By API, I mean functions such as smp_mb(), READ_ONCE(), etc.
>>
>> API index can have kernel API, perfbook specific API, C11 API, and GCC API.
>
> The upside is that the individual indexes are smaller and perhaps
> more manageable. The downside is that a reader who has no idea
> what the function call is might have to look it up in four (or maybe
> even five) indexes. Especially if the API is a historic API that
> is no longer used.
>
> I have no idea what the right answer is. One approach would be to
> have all of the APIs appear both in their respective categories and
> in the general index. Not sure that this would be any better, though.
My idea is to merge all the APIs into a single API Index.
Category of each API can be shown there like:
__atomic_load() (GCC), <pages>
ACCESS_ONCE() (kernel, historic), <pages>
atomic_inc() (kernel), <pages>
atomic_load() (C11), <pages>
fork() (POSIX), <pages>
smp_mb() (kernel), <pages>
smp_read_barrier_depends() (kernel, historic), <pages>
Give or take the appearance of annotations. For example we can use
"G" for "GCC", "C" for "C11", "k" for "kernel", "k,h" for "kernel, historic",
etc.
>
>> As for words/terms, if you can provide me a wish list you'd like to see in
>> the general index, I'm willing to add such annotations.
>> My starting point of the general index is the Glossary.
>
> The glossary is a good starting point. People mentioned in the text is
> another. Not sure whether or not those quoted in the epigraphs should
> be included or not.
Ah, I missed people's names.
> Names of algorithms should be included, also names
> of data structures and of famous problems (for example, the Dining
> Philosopher's problem, mazes, and so on).
>
> I am sure that I am missing quite a few categories, but at least a
> start! ;-)
Let me see how it can be done.
I'll submit a [NOT PULL] request when it is ready as PoC.
Thanks, Akira
>
> Thanx, Paul
>
>> Thoughts?
>>
>>>
>>> Or am I still confused? ;-)
>>>
>>> Thanx, Paul
>>>
>>>> ---
>>>> C Lock1-for-herd7
>>>>
>>>> (*
>>>> * Example test incompatible with klitmus7
>>>> *
>>>> * klitmus7 cannot access spinlock_t variable.
>>>> *)
>>>>
>>>> {}
>>>>
>>>> P0(int *x, spinlock_t *sp)
>>>> {
>>>> spin_lock(sp);
>>>> WRITE_ONCE(*x, 1);
>>>> WRITE_ONCE(*x, 0);
>>>> spin_unlock(sp);
>>>> }
>>>>
>>>> P1(int *x, spinlock_t *sp)
>>>> {
>>>> int r1;
>>>>
>>>> spin_lock(sp);
>>>> r1 = READ_ONCE(*x);
>>>> spin_unlock(sp);
>>>> }
>>>>
>>>> locations [sp] (* incompatible with klitmus7 *)
>>>> exists (1:r1=1)
>>>> ---
>>>>
>>>> klitmus7 can't convert this to a kernel module:
>>>>
>>>> ---
>>>> $ klitmus7 -o temp C-Lock1-for-herd7.litmus
>>>> File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t
>>>> ---
>>>>
>>>> Actually, herd7/LKMM does complain of this one:
>>>>
>>>> ---
>>>> Test Lock1-for-herd7 Allowed
>>>> States 1
>>>> 1:r1=0; sp=0;
>>>> No
>>>> Witnesses
>>>> Positive: 0 Negative: 2
>>>> Flag lock-final <---
>>>> Condition exists (1:r1=1)
>>>> Observation Lock1-for-herd7 Never 0 2
>>>> Time Lock1-for-herd7 0.01
>>>> Hash=5d10e6c355cec0c36f354abf175adc54
>>>> ---
>>>>
>>>> Comment at line 57 of lock.cat says:
>>>>
>>>> ---
>>>> (* The final value of a spinlock should not be tested *)
>>>> flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
>>>> ---
>>>>
>>>> Thanks, Akira
>>>>
>>
>> [...]
^ permalink raw reply [flat|nested] 10+ messages in thread
* Re: Index in Perfbook (was Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests)
2020-11-21 4:14 ` Index in Perfbook (was Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests) Akira Yokosawa
@ 2020-11-22 3:52 ` Paul E. McKenney
0 siblings, 0 replies; 10+ messages in thread
From: Paul E. McKenney @ 2020-11-22 3:52 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook
On Sat, Nov 21, 2020 at 01:14:59PM +0900, Akira Yokosawa wrote:
> On Fri, 20 Nov 2020 19:47:14 -0800, Paul E. McKenney wrote:
> > On Sat, Nov 21, 2020 at 11:51:11AM +0900, Akira Yokosawa wrote:
> >> On Fri, 20 Nov 2020 17:14:10 -0800, Paul E. McKenney wrote:
> >>> On Mon, Nov 16, 2020 at 07:25:09AM +0900, Akira Yokosawa wrote:
> >>>> On Sun, 15 Nov 2020 12:42:44 -0800, Paul E. McKenney wrote:
> >>>>> On Sat, Nov 14, 2020 at 01:51:01PM +0900, Akira Yokosawa wrote:
> >>>>>> Hi Paul,
> >>>>>>
> >>>>>> This patch set is what I mentioned the other day in response to
> >>>>>> your LKMM patch for 5.11.
> >>>>>> klitmus7 doesn't need most of type info in litmus-test init blocks.
> >>>>>>
> >>>>>> While there are some cases where klitmus7 requires type info of variables
> >>>>>> to be watched (via the "exists", "locations", or "filter" directive),
> >>>>>> as long as the watched variables are of type "int", extra type info
> >>>>>> in the init block is not required.
> >>>>>>
> >>>>>> Litmus tests under CodeSamples/formal/ should keep compatible with
> >>>>>> klitmus7 after this patch set is applied.
> >>>>>>
> >>>>>> Patch 1/2 removes initialization to 0 and type info of "int" or "int *"
> >>>>>> under CodeSamples/formal/litmus/.
> >>>>>>
> >>>>>> Patch 2/2 further reduce line counts of litmus tests by using "{}"
> >>>>>> as empty init blocks.
> >>>>>> It also adds/removes empty lines for those code snippets to have
> >>>>>> consistent looks.
> >>>>>>
> >>>>>> Similar changes to patch 1/2 can be made in the RCU litmus tests
> >>>>>> presented in Section 12.3.2. They are not touched in this patch set.
> >>>>>>
> >>>>>> May be in a follow-up patch.
> >>>>>
> >>>>> Queued and pushed, thank you very much!
> >>>>>
> >>>>>> Thanks, Akira
> >>>>>>
> >>>>>> *NOTE*:
> >>>>>>
> >>>>>> There are cases where litmus tests for herd7 can not be
> >>>>>> made compatible with (current) klitmus7, though.
> >>>>>>
> >>>>>> One such example is when a variable of a type other than the "int"
> >>>>>> or "int *" (such as "spinlock_t") is specified in the "locations" or "filter"
> >>>>>> directive.
> >>>>>> Current klitmus7 has no idea of the way to obtain the value of such a
> >>>>>> variable.
> >>>>>
> >>>>> Good to know! Do we have litmus tests that have problems with this?
> >>>>
> >>>> One such litmus test can be made up based on CodeSamples/formal/herd/C-Lock1.litmus
> >>>
> >>> So there is not currently such a litmus test in perfbook, but one could
> >>> easily be created, correct?
> >>
> >> You are right!
> >>
> >> Thanks, Akira
> >>
> >> PS.
> >>
> >> I'm preparing a patch series to add an index framework in perfbook.
> >> My plan is to add a specific make target for the time being to have such
> >> index pages printed.
> >> As you should know, the hard part is to embed a *lot* of index annotations
> >> in .tex source files.
> >
> > Quite right, it is a big job!
> >
> >> I'm thinking of splitting indexes into a general one and API index.
> >> By API, I mean functions such as smp_mb(), READ_ONCE(), etc.
> >>
> >> API index can have kernel API, perfbook specific API, C11 API, and GCC API.
> >
> > The upside is that the individual indexes are smaller and perhaps
> > more manageable. The downside is that a reader who has no idea
> > what the function call is might have to look it up in four (or maybe
> > even five) indexes. Especially if the API is a historic API that
> > is no longer used.
> >
> > I have no idea what the right answer is. One approach would be to
> > have all of the APIs appear both in their respective categories and
> > in the general index. Not sure that this would be any better, though.
>
> My idea is to merge all the APIs into a single API Index.
> Category of each API can be shown there like:
>
> __atomic_load() (GCC), <pages>
> ACCESS_ONCE() (kernel, historic), <pages>
> atomic_inc() (kernel), <pages>
> atomic_load() (C11), <pages>
> fork() (POSIX), <pages>
> smp_mb() (kernel), <pages>
> smp_read_barrier_depends() (kernel, historic), <pages>
>
> Give or take the appearance of annotations. For example we can use
> "G" for "GCC", "C" for "C11", "k" for "kernel", "k,h" for "kernel, historic",
> etc.
Ah, that does make more sense, thank you for clarifying!
> >> As for words/terms, if you can provide me a wish list you'd like to see in
> >> the general index, I'm willing to add such annotations.
> >> My starting point of the general index is the Glossary.
> >
> > The glossary is a good starting point. People mentioned in the text is
> > another. Not sure whether or not those quoted in the epigraphs should
> > be included or not.
>
> Ah, I missed people's names.
>
> > Names of algorithms should be included, also names
> > of data structures and of famous problems (for example, the Dining
> > Philosopher's problem, mazes, and so on).
> >
> > I am sure that I am missing quite a few categories, but at least a
> > start! ;-)
>
> Let me see how it can be done.
>
> I'll submit a [NOT PULL] request when it is ready as PoC.
Sounds very good!
Thanx, Paul
> Thanks, Akira
>
> >
> > Thanx, Paul
> >
> >> Thoughts?
> >>
> >>>
> >>> Or am I still confused? ;-)
> >>>
> >>> Thanx, Paul
> >>>
> >>>> ---
> >>>> C Lock1-for-herd7
> >>>>
> >>>> (*
> >>>> * Example test incompatible with klitmus7
> >>>> *
> >>>> * klitmus7 cannot access spinlock_t variable.
> >>>> *)
> >>>>
> >>>> {}
> >>>>
> >>>> P0(int *x, spinlock_t *sp)
> >>>> {
> >>>> spin_lock(sp);
> >>>> WRITE_ONCE(*x, 1);
> >>>> WRITE_ONCE(*x, 0);
> >>>> spin_unlock(sp);
> >>>> }
> >>>>
> >>>> P1(int *x, spinlock_t *sp)
> >>>> {
> >>>> int r1;
> >>>>
> >>>> spin_lock(sp);
> >>>> r1 = READ_ONCE(*x);
> >>>> spin_unlock(sp);
> >>>> }
> >>>>
> >>>> locations [sp] (* incompatible with klitmus7 *)
> >>>> exists (1:r1=1)
> >>>> ---
> >>>>
> >>>> klitmus7 can't convert this to a kernel module:
> >>>>
> >>>> ---
> >>>> $ klitmus7 -o temp C-Lock1-for-herd7.litmus
> >>>> File "C-Lock1-for-herd7.litmus" Parameter sp, type mismatch int vs. spinlock_t
> >>>> ---
> >>>>
> >>>> Actually, herd7/LKMM does complain of this one:
> >>>>
> >>>> ---
> >>>> Test Lock1-for-herd7 Allowed
> >>>> States 1
> >>>> 1:r1=0; sp=0;
> >>>> No
> >>>> Witnesses
> >>>> Positive: 0 Negative: 2
> >>>> Flag lock-final <---
> >>>> Condition exists (1:r1=1)
> >>>> Observation Lock1-for-herd7 Never 0 2
> >>>> Time Lock1-for-herd7 0.01
> >>>> Hash=5d10e6c355cec0c36f354abf175adc54
> >>>> ---
> >>>>
> >>>> Comment at line 57 of lock.cat says:
> >>>>
> >>>> ---
> >>>> (* The final value of a spinlock should not be tested *)
> >>>> flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
> >>>> ---
> >>>>
> >>>> Thanks, Akira
> >>>>
> >>
> >> [...]
^ permalink raw reply [flat|nested] 10+ messages in thread
end of thread, other threads:[~2020-11-22 3:52 UTC | newest]
Thread overview: 10+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-11-14 4:51 [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests Akira Yokosawa
2020-11-14 4:54 ` [PATCH perfbook 1/2] CodeSamples/formal/litmus: Remove redundant initialization Akira Yokosawa
2020-11-14 4:56 ` [PATCH perfbook 2/2] CodeSamples/formal: Use '{}' for empty init blocks in litmus tests Akira Yokosawa
2020-11-15 20:42 ` [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of " Paul E. McKenney
2020-11-15 22:25 ` Akira Yokosawa
2020-11-21 1:14 ` Paul E. McKenney
2020-11-21 2:51 ` Akira Yokosawa
2020-11-21 3:47 ` Paul E. McKenney
2020-11-21 4:14 ` Index in Perfbook (was Re: [PATCH perfbook 0/2] CodeSamples/formal: Cleanup of init blocks in litmus tests) Akira Yokosawa
2020-11-22 3:52 ` Paul E. McKenney
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.