From: "Paul E. McKenney" <paulmck@linux.ibm.com>
To: Akira Yokosawa <akys@qa2.so-net.ne.jp>
Cc: perfbook@vger.kernel.org, Akira Yokosawa <akiyks@gmail.com>
Subject: Re: [PATCH] memorder: Make RCU litmus tests klitmus7 ready
Date: Wed, 23 Jan 2019 16:06:17 -0800 [thread overview]
Message-ID: <20190124000617.GN4240@linux.ibm.com> (raw)
In-Reply-To: <f1838444-907a-7c73-bf54-205c30708633@qa2.so-net.ne.jp>
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
>
prev parent reply other threads:[~2019-01-24 0:06 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-01-23 15:28 [PATCH] memorder: Make RCU litmus tests klitmus7 ready Akira Yokosawa
2019-01-24 0:06 ` Paul E. McKenney [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20190124000617.GN4240@linux.ibm.com \
--to=paulmck@linux.ibm.com \
--cc=akiyks@gmail.com \
--cc=akys@qa2.so-net.ne.jp \
--cc=perfbook@vger.kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
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.