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@xxxxxxxxx>
> 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@xxxxxxxxx>
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
>
