* [PATCH] memorder: Make RCU litmus tests klitmus7 ready
@ 2019-01-23 15:28 Akira Yokosawa
2019-01-24 0:06 ` Paul E. McKenney
0 siblings, 1 reply; 2+ messages in thread
From: Akira Yokosawa @ 2019-01-23 15:28 UTC (permalink / raw)
To: Paul E. McKenney; +Cc: perfbook, Akira Yokosawa
From 81058687119c2bac703bc669d826c8466c517cda Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@gmail.com>
Date: Wed, 23 Jan 2019 21:35:28 +0900
Subject: [PATCH] memorder: Make RCU litmus tests klitmus7 ready
Use uintptr_t, which is available for kernel modules, instead of
intptr_t.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
---
Hi Paul,
You've added C-SB+o-rcusync-o+rl-o-o-rul to KLITMUS_READY in the
Makefile under CodeSamples/formal/herd in commit 74b1eae67cc7
("memorder: Start section on RCU detailed semantics.").
However, "make cross-klitmus; cd klitmus; make" ends up in errors
starting from:
CodeSamples/formal/herd/klitmus/litmus043.c:286:3: error: unknown type name 'intptr_t'
intptr_t *x1;
^
[...]
IIUC, intptr_t is not available for kernel modules. Using uintptr_t
instead looks like a solution.
Thanks, Akira
--
.../formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 8 ++++----
.../formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 8 ++++----
.../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 8 ++++----
CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 8 ++++----
...+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 16 ++++++++--------
.../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 8 ++++----
.../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 8 ++++----
.../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 8 ++++----
.../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 12 ++++++------
.../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 8 ++++----
.../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 8 ++++----
CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus | 8 ++++----
12 files changed, 54 insertions(+), 54 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 f53ffac..ba0b479 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
@@ -3,18 +3,18 @@ C C-LB+o-rl-rul-o+o-rl-rul-o
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
- intptr_t r1 = READ_ONCE(*x0);
+ uintptr_t r1 = READ_ONCE(*x0);
rcu_read_lock();
rcu_read_unlock();
WRITE_ONCE(*x1, 1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
- intptr_t r1 = READ_ONCE(*x1);
+ uintptr_t r1 = READ_ONCE(*x1);
rcu_read_lock();
rcu_read_unlock();
WRITE_ONCE(*x0, 1);
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 829e82d..8551eca 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
@@ -3,19 +3,19 @@ C C-LB+rl-o-o-rul+rl-o-o-rul
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
- intptr_t r1 = READ_ONCE(*x0);
+ uintptr_t r1 = READ_ONCE(*x0);
WRITE_ONCE(*x1, 1);
rcu_read_unlock();
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
- intptr_t r1 = READ_ONCE(*x1);
+ uintptr_t r1 = READ_ONCE(*x1);
WRITE_ONCE(*x0, 1);
rcu_read_unlock();
}
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 2422abe..1a9625e 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
@@ -3,18 +3,18 @@ C C-SB+o-rcusync-o+i-rl-o-o-rul
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
WRITE_ONCE(*x1, 2);
rcu_read_unlock();
}
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 4c471c4..8681c84 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
@@ -3,18 +3,18 @@ C C-SB+o-rcusync-o+o-o
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
}
//\end[snippet]
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 78eed5e..18595f4 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
@@ -3,36 +3,36 @@ C C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x1, intptr_t *x2)
+P1(uintptr_t *x1, uintptr_t *x2)
{
WRITE_ONCE(*x1, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x2);
+ uintptr_t r2 = READ_ONCE(*x2);
}
-P2(intptr_t *x2, intptr_t *x3)
+P2(uintptr_t *x2, uintptr_t *x3)
{
rcu_read_lock();
WRITE_ONCE(*x2, 2);
- intptr_t r2 = READ_ONCE(*x3);
+ uintptr_t r2 = READ_ONCE(*x3);
rcu_read_unlock();
}
-P3(intptr_t *x0, intptr_t *x3)
+P3(uintptr_t *x0, uintptr_t *x3)
{
rcu_read_lock();
WRITE_ONCE(*x3, 2);
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
rcu_read_unlock();
}
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 e43188b..aa3a49f 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
@@ -3,19 +3,19 @@ C C-SB+o-rcusync-o+o-rcusync-o
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
}
//\end[snippet]
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 a4e3aa9..503dcf8 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
@@ -3,19 +3,19 @@ C C-SB+o-rcusync-o+o-rl-o-rul
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
rcu_read_lock();
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
rcu_read_unlock();
}
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 7998036..054e2e7 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
@@ -3,20 +3,20 @@ C C-SB+o-rcusync-o+o-rl-rul-o
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x1, 2);
rcu_read_lock();
rcu_read_unlock();
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
}
//\end[snippet]
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 4905ea5..8c87d42 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
@@ -3,28 +3,28 @@ C C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x1, intptr_t *x2)
+P1(uintptr_t *x1, uintptr_t *x2)
{
rcu_read_lock();
WRITE_ONCE(*x1, 2);
- intptr_t r2 = READ_ONCE(*x2);
+ uintptr_t r2 = READ_ONCE(*x2);
rcu_read_unlock();
}
-P2(intptr_t *x2, intptr_t *x0)
+P2(uintptr_t *x2, uintptr_t *x0)
{
rcu_read_lock();
WRITE_ONCE(*x2, 2);
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
rcu_read_unlock();
}
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 4be12dd..5190ddf 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
@@ -3,19 +3,19 @@ C C-SB+o-rcusync-o+rl-o-o-rul
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
WRITE_ONCE(*x1, 2);
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
rcu_read_unlock();
}
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 356a61e..a39baf3 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
@@ -3,20 +3,20 @@ C C-SB+o-rcusync-o+rl-o-rul-o
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
WRITE_ONCE(*x1, 2);
rcu_read_unlock();
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
}
//\end[snippet]
diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
index 356a61e..a39baf3 100644
--- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
+++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
@@ -3,20 +3,20 @@ C C-SB+o-rcusync-o+rl-o-rul-o
{
}
-P0(intptr_t *x0, intptr_t *x1)
+P0(uintptr_t *x0, uintptr_t *x1)
{
WRITE_ONCE(*x0, 2);
synchronize_rcu();
- intptr_t r2 = READ_ONCE(*x1);
+ uintptr_t r2 = READ_ONCE(*x1);
}
-P1(intptr_t *x0, intptr_t *x1)
+P1(uintptr_t *x0, uintptr_t *x1)
{
rcu_read_lock();
WRITE_ONCE(*x1, 2);
rcu_read_unlock();
- intptr_t r2 = READ_ONCE(*x0);
+ uintptr_t r2 = READ_ONCE(*x0);
}
//\end[snippet]
--
2.7.4
^ permalink raw reply related [flat|nested] 2+ messages in thread
* Re: [PATCH] memorder: Make RCU litmus tests klitmus7 ready
2019-01-23 15:28 [PATCH] memorder: Make RCU litmus tests klitmus7 ready Akira Yokosawa
@ 2019-01-24 0:06 ` Paul E. McKenney
0 siblings, 0 replies; 2+ messages in thread
From: Paul E. McKenney @ 2019-01-24 0:06 UTC (permalink / raw)
To: Akira Yokosawa; +Cc: perfbook, Akira Yokosawa
On Thu, Jan 24, 2019 at 12:28:04AM +0900, Akira Yokosawa wrote:
> >From 81058687119c2bac703bc669d826c8466c517cda Mon Sep 17 00:00:00 2001
> From: Akira Yokosawa <akiyks@gmail.com>
> Date: Wed, 23 Jan 2019 21:35:28 +0900
> Subject: [PATCH] memorder: Make RCU litmus tests klitmus7 ready
>
> Use uintptr_t, which is available for kernel modules, instead of
> intptr_t.
>
> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Good catch, queued and pushed!
I guess my strategy of just picking the shortest name was not so
inspired. ;-)
Thanx, Paul
> ---
> Hi Paul,
>
> You've added C-SB+o-rcusync-o+rl-o-o-rul to KLITMUS_READY in the
> Makefile under CodeSamples/formal/herd in commit 74b1eae67cc7
> ("memorder: Start section on RCU detailed semantics.").
> However, "make cross-klitmus; cd klitmus; make" ends up in errors
> starting from:
>
> CodeSamples/formal/herd/klitmus/litmus043.c:286:3: error: unknown type name 'intptr_t'
> intptr_t *x1;
> ^
> [...]
>
> IIUC, intptr_t is not available for kernel modules. Using uintptr_t
> instead looks like a solution.
>
> Thanks, Akira
> --
> .../formal/herd/C-LB+o-rl-rul-o+o-rl-rul-o.litmus | 8 ++++----
> .../formal/herd/C-LB+rl-o-o-rul+rl-o-o-rul.litmus | 8 ++++----
> .../formal/herd/C-SB+o-rcusync-o+i-rl-o-o-rul.litmus | 8 ++++----
> CodeSamples/formal/herd/C-SB+o-rcusync-o+o-o.litmus | 8 ++++----
> ...+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 16 ++++++++--------
> .../formal/herd/C-SB+o-rcusync-o+o-rcusync-o.litmus | 8 ++++----
> .../formal/herd/C-SB+o-rcusync-o+o-rl-o-rul.litmus | 8 ++++----
> .../formal/herd/C-SB+o-rcusync-o+o-rl-rul-o.litmus | 8 ++++----
> .../herd/C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul.litmus | 12 ++++++------
> .../formal/herd/C-SB+o-rcusync-o+rl-o-o-rul.litmus | 8 ++++----
> .../formal/herd/C-SB+o-rcusync-o+rl-o-rul-o.litmus | 8 ++++----
> CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus | 8 ++++----
> 12 files changed, 54 insertions(+), 54 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 f53ffac..ba0b479 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
> @@ -3,18 +3,18 @@ C C-LB+o-rl-rul-o+o-rl-rul-o
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> - intptr_t r1 = READ_ONCE(*x0);
> + uintptr_t r1 = READ_ONCE(*x0);
> rcu_read_lock();
> rcu_read_unlock();
> WRITE_ONCE(*x1, 1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> - intptr_t r1 = READ_ONCE(*x1);
> + uintptr_t r1 = READ_ONCE(*x1);
> rcu_read_lock();
> rcu_read_unlock();
> WRITE_ONCE(*x0, 1);
> 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 829e82d..8551eca 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
> @@ -3,19 +3,19 @@ C C-LB+rl-o-o-rul+rl-o-o-rul
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> rcu_read_lock();
> - intptr_t r1 = READ_ONCE(*x0);
> + uintptr_t r1 = READ_ONCE(*x0);
> WRITE_ONCE(*x1, 1);
> rcu_read_unlock();
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> rcu_read_lock();
> - intptr_t r1 = READ_ONCE(*x1);
> + uintptr_t r1 = READ_ONCE(*x1);
> WRITE_ONCE(*x0, 1);
> rcu_read_unlock();
> }
> 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 2422abe..1a9625e 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
> @@ -3,18 +3,18 @@ C C-SB+o-rcusync-o+i-rl-o-o-rul
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> rcu_read_lock();
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> WRITE_ONCE(*x1, 2);
> rcu_read_unlock();
> }
> 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 4c471c4..8681c84 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
> @@ -3,18 +3,18 @@ C C-SB+o-rcusync-o+o-o
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x1, 2);
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> }
>
> //\end[snippet]
> 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 78eed5e..18595f4 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
> @@ -3,36 +3,36 @@ C C-SB+o-rcusync-o+o-rcusync-o+rl-o-o-rul+rl-o-o-rul
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x1, intptr_t *x2)
> +P1(uintptr_t *x1, uintptr_t *x2)
> {
> WRITE_ONCE(*x1, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x2);
> + uintptr_t r2 = READ_ONCE(*x2);
> }
>
>
> -P2(intptr_t *x2, intptr_t *x3)
> +P2(uintptr_t *x2, uintptr_t *x3)
> {
> rcu_read_lock();
> WRITE_ONCE(*x2, 2);
> - intptr_t r2 = READ_ONCE(*x3);
> + uintptr_t r2 = READ_ONCE(*x3);
> rcu_read_unlock();
> }
>
>
> -P3(intptr_t *x0, intptr_t *x3)
> +P3(uintptr_t *x0, uintptr_t *x3)
> {
> rcu_read_lock();
> WRITE_ONCE(*x3, 2);
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> rcu_read_unlock();
> }
>
> 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 e43188b..aa3a49f 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
> @@ -3,19 +3,19 @@ C C-SB+o-rcusync-o+o-rcusync-o
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x1, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> }
>
> //\end[snippet]
> 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 a4e3aa9..503dcf8 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
> @@ -3,19 +3,19 @@ C C-SB+o-rcusync-o+o-rl-o-rul
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x1, 2);
> rcu_read_lock();
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> rcu_read_unlock();
> }
>
> 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 7998036..054e2e7 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
> @@ -3,20 +3,20 @@ C C-SB+o-rcusync-o+o-rl-rul-o
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x1, 2);
> rcu_read_lock();
> rcu_read_unlock();
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> }
>
> //\end[snippet]
> 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 4905ea5..8c87d42 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
> @@ -3,28 +3,28 @@ C C-SB+o-rcusync-o+rl-o-o-rul+rl-o-o-rul
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x1, intptr_t *x2)
> +P1(uintptr_t *x1, uintptr_t *x2)
> {
> rcu_read_lock();
> WRITE_ONCE(*x1, 2);
> - intptr_t r2 = READ_ONCE(*x2);
> + uintptr_t r2 = READ_ONCE(*x2);
> rcu_read_unlock();
> }
>
>
> -P2(intptr_t *x2, intptr_t *x0)
> +P2(uintptr_t *x2, uintptr_t *x0)
> {
> rcu_read_lock();
> WRITE_ONCE(*x2, 2);
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> rcu_read_unlock();
> }
>
> 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 4be12dd..5190ddf 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
> @@ -3,19 +3,19 @@ C C-SB+o-rcusync-o+rl-o-o-rul
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> rcu_read_lock();
> WRITE_ONCE(*x1, 2);
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> rcu_read_unlock();
> }
>
> 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 356a61e..a39baf3 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
> @@ -3,20 +3,20 @@ C C-SB+o-rcusync-o+rl-o-rul-o
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> rcu_read_lock();
> WRITE_ONCE(*x1, 2);
> rcu_read_unlock();
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> }
>
> //\end[snippet]
> diff --git a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> index 356a61e..a39baf3 100644
> --- a/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> +++ b/CodeSamples/formal/herd/C-SB+o-rcusync-o+rl-rul-o.litmus
> @@ -3,20 +3,20 @@ C C-SB+o-rcusync-o+rl-o-rul-o
> {
> }
>
> -P0(intptr_t *x0, intptr_t *x1)
> +P0(uintptr_t *x0, uintptr_t *x1)
> {
> WRITE_ONCE(*x0, 2);
> synchronize_rcu();
> - intptr_t r2 = READ_ONCE(*x1);
> + uintptr_t r2 = READ_ONCE(*x1);
> }
>
>
> -P1(intptr_t *x0, intptr_t *x1)
> +P1(uintptr_t *x0, uintptr_t *x1)
> {
> rcu_read_lock();
> WRITE_ONCE(*x1, 2);
> rcu_read_unlock();
> - intptr_t r2 = READ_ONCE(*x0);
> + uintptr_t r2 = READ_ONCE(*x0);
> }
>
> //\end[snippet]
> --
> 2.7.4
>
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2019-01-24 0:06 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2019-01-23 15:28 [PATCH] memorder: Make RCU litmus tests klitmus7 ready Akira Yokosawa
2019-01-24 0:06 ` 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.