From: Andrea Parri <parri.andrea@gmail.com>
To: "Paul E. McKenney" <paulmck@kernel.org>
Cc: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
kernel-team@meta.com, mingo@kernel.org,
stern@rowland.harvard.edu, will@kernel.org, peterz@infradead.org,
boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com,
j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com
Subject: Re: [PATCH memory-model scripts 01/31] tools/memory-model: Document locking corner cases
Date: Wed, 22 Mar 2023 09:59:38 +0100 [thread overview]
Message-ID: <ZBrDeoCIs1wmNBeF@andrea> (raw)
In-Reply-To: <20230321010549.51296-1-paulmck@kernel.org>
> create mode 100644 Documentation/litmus-tests/locking/DCL-broken.litmus
> create mode 100644 Documentation/litmus-tests/locking/DCL-fixed.litmus
> create mode 100644 Documentation/litmus-tests/locking/RM-broken.litmus
> create mode 100644 Documentation/litmus-tests/locking/RM-fixed.litmus
Unfortunately none of them were liked by klitmus7/gcc, the diff below
works for me but please double check.
Andrea
diff --git a/Documentation/litmus-tests/locking/DCL-broken.litmus b/Documentation/litmus-tests/locking/DCL-broken.litmus
index cfaa25ff82b1e..bfb7ba4316d69 100644
--- a/Documentation/litmus-tests/locking/DCL-broken.litmus
+++ b/Documentation/litmus-tests/locking/DCL-broken.litmus
@@ -10,10 +10,9 @@ C DCL-broken
{
int flag;
int data;
- int lck;
}
-P0(int *flag, int *data, int *lck)
+P0(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -32,7 +31,7 @@ P0(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-P1(int *flag, int *data, int *lck)
+P1(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -51,5 +50,5 @@ P1(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
+locations [flag;data;0:r0;0:r1;1:r0;1:r1]
exists (0:r2=0 \/ 1:r2=0)
diff --git a/Documentation/litmus-tests/locking/DCL-fixed.litmus b/Documentation/litmus-tests/locking/DCL-fixed.litmus
index 579d6c246f167..d1b60bcb0c8f3 100644
--- a/Documentation/litmus-tests/locking/DCL-fixed.litmus
+++ b/Documentation/litmus-tests/locking/DCL-fixed.litmus
@@ -11,10 +11,9 @@ C DCL-fixed
{
int flag;
int data;
- int lck;
}
-P0(int *flag, int *data, int *lck)
+P0(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -33,7 +32,7 @@ P0(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-P1(int *flag, int *data, int *lck)
+P1(int *flag, int *data, spinlock_t *lck)
{
int r0;
int r1;
@@ -52,5 +51,5 @@ P1(int *flag, int *data, int *lck)
r2 = READ_ONCE(*data);
}
-locations [flag;data;lck;0:r0;0:r1;1:r0;1:r1]
+locations [flag;data;0:r0;0:r1;1:r0;1:r1]
exists (0:r2=0 \/ 1:r2=0)
diff --git a/Documentation/litmus-tests/locking/RM-broken.litmus b/Documentation/litmus-tests/locking/RM-broken.litmus
index c586ae4b547de..b7ef30cedfe51 100644
--- a/Documentation/litmus-tests/locking/RM-broken.litmus
+++ b/Documentation/litmus-tests/locking/RM-broken.litmus
@@ -9,12 +9,11 @@ C RM-broken
*)
{
- int lck;
int x;
- int y;
+ atomic_t y;
}
-P0(int *x, int *y, int *lck)
+P0(int *x, atomic_t *y, spinlock_t *lck)
{
int r2;
@@ -24,7 +23,7 @@ P0(int *x, int *y, int *lck)
spin_unlock(lck);
}
-P1(int *x, int *y, int *lck)
+P1(int *x, atomic_t *y, spinlock_t *lck)
{
int r0;
int r1;
@@ -37,6 +36,6 @@ P1(int *x, int *y, int *lck)
spin_unlock(lck);
}
-locations [x;lck;0:r2;1:r0;1:r1;1:r2]
-filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+locations [x;0:r2;1:r0;1:r1;1:r2]
+filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)
diff --git a/Documentation/litmus-tests/locking/RM-fixed.litmus b/Documentation/litmus-tests/locking/RM-fixed.litmus
index 672856736b42e..b628175596160 100644
--- a/Documentation/litmus-tests/locking/RM-fixed.litmus
+++ b/Documentation/litmus-tests/locking/RM-fixed.litmus
@@ -9,12 +9,11 @@ C RM-fixed
*)
{
- int lck;
int x;
- int y;
+ atomic_t y;
}
-P0(int *x, int *y, int *lck)
+P0(int *x, atomic_t *y, spinlock_t *lck)
{
int r2;
@@ -24,7 +23,7 @@ P0(int *x, int *y, int *lck)
spin_unlock(lck);
}
-P1(int *x, int *y, int *lck)
+P1(int *x, atomic_t *y, spinlock_t *lck)
{
int r0;
int r1;
@@ -37,6 +36,6 @@ P1(int *x, int *y, int *lck)
spin_unlock(lck);
}
-locations [x;lck;0:r2;1:r0;1:r1;1:r2]
-filter (y=2 /\ 1:r0=0 /\ 1:r1=1)
+locations [x;0:r2;1:r0;1:r1;1:r2]
+filter (1:r0=0 /\ 1:r1=1)
exists (1:r2=1)
next prev parent reply other threads:[~2023-03-22 8:59 UTC|newest]
Thread overview: 39+ messages / expand[flat|nested] mbox.gz Atom feed top
2023-03-21 1:05 [PATCH memory-model 0/31] LKMM scripting updates for v6.4 Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 01/31] tools/memory-model: Document locking corner cases Paul E. McKenney
2023-03-22 8:59 ` Andrea Parri [this message]
2023-03-22 19:14 ` Paul E. McKenney
2023-03-23 1:42 ` Andrea Parri
2023-03-23 2:52 ` Akira Yokosawa
2023-03-23 18:52 ` Paul E. McKenney
2023-03-23 23:30 ` Akira Yokosawa
2023-03-23 23:49 ` Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 02/31] tools/memory-model: Make judgelitmus.sh note timeouts Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 03/31] tools/memory-model: Make cmplitmushist.sh " Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 04/31] tools/memory-model: Make judgelitmus.sh identify bad macros Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 05/31] tools/memory-model: Make judgelitmus.sh detect hard deadlocks Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 06/31] tools/memory-model: Fix paulmck email address on pre-existing scripts Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 07/31] tools/memory-model: Update parseargs.sh for hardware verification Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 08/31] tools/memory-model: Make judgelitmus.sh handle hardware verifications Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 09/31] tools/memory-model: Add simpletest.sh to check locking, RCU, and SRCU Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 10/31] tools/memory-model: Fix checkalllitmus.sh comment Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 11/31] tools/memory-model: Hardware checking for check{,all}litmus.sh Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 12/31] tools/memory-model: Make judgelitmus.sh ransack .litmus.out files Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 13/31] tools/memory-model: Split runlitmus.sh out of checklitmus.sh Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 14/31] tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 15/31] tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 16/31] tools/memory-model: Keep assembly-language litmus tests Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 17/31] tools/memory-model: Allow herd to deduce CPU type Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 18/31] tools/memory-model: Make runlitmus.sh check for jingle errors Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 19/31] tools/memory-model: Add -v flag to jingle7 runs Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 20/31] tools/memory-model: Implement --hw support for checkghlitmus.sh Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 21/31] tools/memory-model: Fix scripting --jobs argument Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 22/31] tools/memory-model: Make checkghlitmus.sh use mselect7 Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 23/31] tools/memory-model: Make history-check scripts " Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 24/31] tools/memory-model: Add "--" to parseargs.sh for additional arguments Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 25/31] tools/memory-model: Repair parseargs.sh header comment Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 26/31] tools/memory-model: Add checktheselitmus.sh to run specified litmus tests Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 27/31] tools/memory-model: Add data-race capabilities to judgelitmus.sh Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 28/31] tools/memory-model: Make judgelitmus.sh handle scripted Result: tag Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 29/31] tools/memory-model: Use "-unroll 0" to keep --hw runs finite Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 30/31] tools/memory-model: Use "grep -E" instead of "egrep" Paul E. McKenney
2023-03-21 1:05 ` [PATCH memory-model scripts 31/31] tools/memory-model: Document LKMM test procedure Paul E. McKenney
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=ZBrDeoCIs1wmNBeF@andrea \
--to=parri.andrea@gmail.com \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=j.alglave@ucl.ac.uk \
--cc=kernel-team@meta.com \
--cc=linux-arch@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=luc.maranget@inria.fr \
--cc=mingo@kernel.org \
--cc=npiggin@gmail.com \
--cc=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=stern@rowland.harvard.edu \
--cc=will@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.