The current macros in linux-kernel.def reference instructions such as
__xchg{mb} or __cmpxchg{acquire}, which are invalid combinations of tags
and instructions according to the declarations in linux-kernel.bell.
This works with current herd7 because herd7 removes these tags anyways
and does not actually enforce validity of combinations at all.
If a future herd7 version no longer applies these hardcoded
transformations, then all currently invalid combinations will actually
appear on some instruction.
We therefore adjust the declarations to make the resulting combinations
valid, by adding the 'mb tag to the set of Accesses and allowing all
Accesses to appear on all read, write, and RMW instructions.
Signed-off-by: Jonas Oberhauser <[email protected]>
---
tools/memory-model/linux-kernel.bell | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
index ce068700939c..1b2444cdf8d1 100644
--- a/tools/memory-model/linux-kernel.bell
+++ b/tools/memory-model/linux-kernel.bell
@@ -16,10 +16,11 @@
enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||
'release (*smp_store_release*) ||
'acquire (*smp_load_acquire*) ||
- 'noreturn (* R of non-return RMW *)
-instructions R[{'once,'acquire,'noreturn}]
-instructions W[{'once,'release}]
-instructions RMW[{'once,'acquire,'release}]
+ 'noreturn (* R of non-return RMW *) ||
+ 'mb (*xchg(),compare_exchange(),...*)
+instructions R[Accesses]
+instructions W[Accesses]
+instructions RMW[Accesses]
enum Barriers = 'wmb (*smp_wmb*) ||
'rmb (*smp_rmb*) ||
--
2.34.1
On Mon, May 27, 2024 at 05:22:50PM +0200, Jonas Oberhauser wrote:
> The current macros in linux-kernel.def reference instructions such as
> __xchg{mb} or __cmpxchg{acquire}, which are invalid combinations of tags
> and instructions according to the declarations in linux-kernel.bell.
> This works with current herd7 because herd7 removes these tags anyways
> and does not actually enforce validity of combinations at all.
>
> If a future herd7 version no longer applies these hardcoded
> transformations, then all currently invalid combinations will actually
> appear on some instruction.
>
> We therefore adjust the declarations to make the resulting combinations
> valid, by adding the 'mb tag to the set of Accesses and allowing all
> Accesses to appear on all read, write, and RMW instructions.
>
> Signed-off-by: Jonas Oberhauser <[email protected]>
> ---
> tools/memory-model/linux-kernel.bell | 9 +++++----
> 1 file changed, 5 insertions(+), 4 deletions(-)
>
> diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell
> index ce068700939c..1b2444cdf8d1 100644
> --- a/tools/memory-model/linux-kernel.bell
> +++ b/tools/memory-model/linux-kernel.bell
> @@ -16,10 +16,11 @@
> enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||
> 'release (*smp_store_release*) ||
> 'acquire (*smp_load_acquire*) ||
> - 'noreturn (* R of non-return RMW *)
> -instructions R[{'once,'acquire,'noreturn}]
> -instructions W[{'once,'release}]
> -instructions RMW[{'once,'acquire,'release}]
> + 'noreturn (* R of non-return RMW *) ||
> + 'mb (*xchg(),compare_exchange(),...*)
It would be better to write cmpxchg() instead of compare_exchange().
Alan
> +instructions R[Accesses]
> +instructions W[Accesses]
> +instructions RMW[Accesses]
>
> enum Barriers = 'wmb (*smp_wmb*) ||
> 'rmb (*smp_rmb*) ||
> --
> 2.34.1
>