tools/memory-model/linux-kernel.bell | 26 ++-- tools/memory-model/linux-kernel.cat | 10 ++ tools/memory-model/linux-kernel.def | 176 +++++++++++++-------------- 3 files changed, 115 insertions(+), 97 deletions(-)
Currently, the effect of several tag on operations is defined only in
the herd7 tool's OCaml code as syntax transformations, while the effect
of all other tags is defined in tools/memory-model.
This asymmetry means that two seemingly analogous definitions in
tools/memory-model behave quite differently because the generated
representation is sometimes modified by hardcoded behavior in herd7.
It also makes it hard to see that the behavior of the formalization
matches the intuition described in explanation.txt without delving into
the implementation of herd7.
Furthermore, this hardcoded behavior is hard to maintain inside herd7 and
other tools implementing WMM, and has caused several bugs and confusions
with the tool maintainers, e.g.:
https://github.com/MPI-SWS/genmc/issues/22
https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904
https://github.com/hernanponcedeleon/Dat3M/issues/254
It also means that potential future extensions of LKMM with new tags may
not work without changing internals of the herd7 tool.
In this patch series, we first emulate the effect of herd7 transformations
in tools/memory-model through explicit rules in .cat and .bell files that
reference the transformed tags.
These transformations do not have any immediate effect with the current
herd7 implementation, because they apply after the syntax transformations
have already modified those tags.
In a second step, we then distinguish between syntactic tags (that are
placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the
read and write of an xchg_acquire() operation) and sets of events (that
would be defined after the (emulated) transformations, e.g., an Acquire
set that includes only on the read of the xchg_acquire(), but "has been
removed" from the write).
This second step is incompatible with the current herd7 implementation,
since herd7 uses hardcoded tag names to decide what to do with LKMM;
therefore, the newly introduced syntactic tags will be ignored or
processed incorrectly by herd7.
Have fun,
jonas
Changes since v1:
- addressed several spelling/style issues pointed out by Alan
- simplified the definition of Marked accesses based on a
suggestion by Alan
Jonas Oberhauser (4):
tools/memory-model: Legitimize current use of tags in LKMM macros
tools/memory-model: Define applicable tags on operation in tools/...
tools/memory-model: Define effect of Mb tags on RMWs in tools/...
tools/memory-model: Distinguish between syntactic and semantic tags
tools/memory-model/linux-kernel.bell | 26 ++--
tools/memory-model/linux-kernel.cat | 10 ++
tools/memory-model/linux-kernel.def | 176 +++++++++++++--------------
3 files changed, 115 insertions(+), 97 deletions(-)
--
2.34.1
On Tue, Jun 04, 2024 at 05:29:18PM +0200, Jonas Oberhauser wrote: > Currently, the effect of several tag on operations is defined only in > the herd7 tool's OCaml code as syntax transformations, while the effect > of all other tags is defined in tools/memory-model. > This asymmetry means that two seemingly analogous definitions in > tools/memory-model behave quite differently because the generated > representation is sometimes modified by hardcoded behavior in herd7. > > It also makes it hard to see that the behavior of the formalization > matches the intuition described in explanation.txt without delving into > the implementation of herd7. > > Furthermore, this hardcoded behavior is hard to maintain inside herd7 and > other tools implementing WMM, and has caused several bugs and confusions > with the tool maintainers, e.g.: > > https://github.com/MPI-SWS/genmc/issues/22 > https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904 > https://github.com/hernanponcedeleon/Dat3M/issues/254 > > It also means that potential future extensions of LKMM with new tags may > not work without changing internals of the herd7 tool. > > In this patch series, we first emulate the effect of herd7 transformations > in tools/memory-model through explicit rules in .cat and .bell files that > reference the transformed tags. > These transformations do not have any immediate effect with the current > herd7 implementation, because they apply after the syntax transformations > have already modified those tags. > > In a second step, we then distinguish between syntactic tags (that are > placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the > read and write of an xchg_acquire() operation) and sets of events (that > would be defined after the (emulated) transformations, e.g., an Acquire > set that includes only on the read of the xchg_acquire(), but "has been > removed" from the write). > > This second step is incompatible with the current herd7 implementation, > since herd7 uses hardcoded tag names to decide what to do with LKMM; > therefore, the newly introduced syntactic tags will be ignored or > processed incorrectly by herd7. The patches look good to me. Just to clarify: Your first step encompasses patches 1 - 3, and the second step is patch 4. The first three patches can be applied now, but the last one needs to wait until herd7 has been updated. Is this all correct? Alan
Am 6/4/2024 um 7:56 PM schrieb Alan Stern: > On Tue, Jun 04, 2024 at 05:29:18PM +0200, Jonas Oberhauser wrote: >> Currently, the effect of several tag on operations is defined only in >> the herd7 tool's OCaml code as syntax transformations, while the effect >> of all other tags is defined in tools/memory-model. >> This asymmetry means that two seemingly analogous definitions in >> tools/memory-model behave quite differently because the generated >> representation is sometimes modified by hardcoded behavior in herd7. >> >> It also makes it hard to see that the behavior of the formalization >> matches the intuition described in explanation.txt without delving into >> the implementation of herd7. >> >> Furthermore, this hardcoded behavior is hard to maintain inside herd7 and >> other tools implementing WMM, and has caused several bugs and confusions >> with the tool maintainers, e.g.: >> >> https://github.com/MPI-SWS/genmc/issues/22 >> https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904 >> https://github.com/hernanponcedeleon/Dat3M/issues/254 >> >> It also means that potential future extensions of LKMM with new tags may >> not work without changing internals of the herd7 tool. >> >> In this patch series, we first emulate the effect of herd7 transformations >> in tools/memory-model through explicit rules in .cat and .bell files that >> reference the transformed tags. >> These transformations do not have any immediate effect with the current >> herd7 implementation, because they apply after the syntax transformations >> have already modified those tags. >> >> In a second step, we then distinguish between syntactic tags (that are >> placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the >> read and write of an xchg_acquire() operation) and sets of events (that >> would be defined after the (emulated) transformations, e.g., an Acquire >> set that includes only on the read of the xchg_acquire(), but "has been >> removed" from the write). >> >> This second step is incompatible with the current herd7 implementation, >> since herd7 uses hardcoded tag names to decide what to do with LKMM; >> therefore, the newly introduced syntactic tags will be ignored or >> processed incorrectly by herd7. > > The patches look good to me. > > Just to clarify: Your first step encompasses patches 1 - 3, and the > second step is patch 4. The first three patches can be applied now, but > the last one needs to wait until herd7 has been updated. Is this all > correct? Exactly.
On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: > > > Am 6/4/2024 um 7:56 PM schrieb Alan Stern: > > Just to clarify: Your first step encompasses patches 1 - 3, and the > > second step is patch 4. The first three patches can be applied now, but > > the last one needs to wait until herd7 has been updated. Is this all > > correct? > > Exactly. With regard to patch 4, how much thought have you and Hernan given to backward compatibility? Once herd7 is changed, old memory model files will no longer work correctly. To avoid being so disruptive, perhaps the changes to herd7 should be under control of a new command-line or config-file switch. If the switch is enabled, the new simplified code gets used; otherwise herd7 would continue to use its old built-in rules for special tags. Alan
Am 6/8/2024 um 3:00 AM schrieb Alan Stern: > On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: >> >> >> Am 6/4/2024 um 7:56 PM schrieb Alan Stern: >>> Just to clarify: Your first step encompasses patches 1 - 3, and the >>> second step is patch 4. The first three patches can be applied now, but >>> the last one needs to wait until herd7 has been updated. Is this all >>> correct? >> >> Exactly. > > With regard to patch 4, how much thought have you and Hernan given to > backward compatibility? Once herd7 is changed, old memory model files > will no longer work correctly. Yes, Akira pointed this out too. My thought back then was to update herd now, and wait with the fourth patch for a while until most people who run the LKMM would have upgraded. However... > To avoid being so disruptive, perhaps the changes to herd7 should be > under control of a new command-line or config-file switch. If the > switch is enabled, the new simplified code gets used; otherwise herd7 > would continue to use its old built-in rules for special tags ... I like that idea a lot better actually. I think it needs to be placed into the files, or people will get strange, silent results. But then I think we need to make sure that there's no internal behaviors left. I don't want to introduce more flags in the future to turn off other internal behavior. jonas
On 6/8/2024 3:00 AM, Alan Stern wrote: > On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: >> >> >> Am 6/4/2024 um 7:56 PM schrieb Alan Stern: >>> Just to clarify: Your first step encompasses patches 1 - 3, and the >>> second step is patch 4. The first three patches can be applied now, but >>> the last one needs to wait until herd7 has been updated. Is this all >>> correct? >> >> Exactly. > > With regard to patch 4, how much thought have you and Hernan given to > backward compatibility? Once herd7 is changed, old memory model files > will no longer work correctly. > Honestly, I did not think much about this (at least until Akira mentioned in my PR). My hope was that changes to the model could be back-ported to previous kernel versions. However that would not work for existing out-of-tree files. My question is: is compatibility with out-of-tree files really a requirement? I would argue that if people are using outdated models, they may get wrong results anyway. This is because some of the changes done to lkmm during the last few years change the expected result for some litmus tests. Hernan
On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
> On 6/8/2024 3:00 AM, Alan Stern wrote:
>> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
>>>
>>>
>>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
>>>> Just to clarify: Your first step encompasses patches 1 - 3, and the
>>>> second step is patch 4. The first three patches can be applied now,
>>>> but
>>>> the last one needs to wait until herd7 has been updated. Is this all
>>>> correct?
>>>
>>> Exactly.
>>
>> With regard to patch 4, how much thought have you and Hernan given to
>> backward compatibility? Once herd7 is changed, old memory model files
>> will no longer work correctly.
>>
>
> Honestly, I did not think much about this (at least until Akira
> mentioned in my PR). My hope was that changes to the model could be
> back-ported to previous kernel versions. However that would not work for
> existing out-of-tree files.
>
> My question is: is compatibility with out-of-tree files really a
> requirement? I would argue that if people are using outdated models,
> they may get wrong results anyway. This is because some of the changes
> done to lkmm during the last few years change the expected result for
> some litmus tests.
>
> Hernan
I pushed some new changes to the code for backward compatibility [1].
The series also needs the patch at the bottom to properly deal with the
ordering of failing CAses and non-returning operations. With it, all
litmus tests return the correct result (the script needs to pass option
-lkmm-legacy false to herd).
Implementation-wise, there are two things that I would like to have:
- atomic_add_unless implementation is treated different than the rest
and it is one of the few remaining cases where memory orderings are
hardcoded [2]. I would like to define it in the .def file as
atomic_add_unless(X,V,U) __atomic_add_unless{ONCE}(X,V,U)
- "deref" and "lderef" instructions seems to add a "rb_dep" fence. None
of the model files (.cat, .def, .bell) refers to "rb_dep" so this looks
useless to me. However, I never checked the details of these
dereferencing instruction so I might be missing something. Maybe Paul
can clarify.
Hernan
[1] https://github.com/herd/herdtools7/pull/865
[2] https://github.com/herd/herdtools7/issues/868
diff --git a/tools/memory-model/linux-kernel.def
b/tools/memory-model/linux-kernel.def
index 001366ff3fb4..5a40c2cad39b 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -32,10 +32,10 @@ xchg(X,V) __xchg{MB}(X,V)
xchg_relaxed(X,V) __xchg{ONCE}(X,V)
xchg_release(X,V) __xchg{RELEASE}(X,V)
xchg_acquire(X,V) __xchg{ACQUIRE}(X,V)
-cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W)
-cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W)
-cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W)
-cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W)
+cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
+cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
+cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
+cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)
// Spinlocks
spin_lock(X) { __lock(X); }
@@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
atomic_read_acquire(X) smp_load_acquire(X)
atomic_set_release(X,V) { smp_store_release(X,V); }
-atomic_add(V,X) { __atomic_op(X,+,V); }
-atomic_sub(V,X) { __atomic_op(X,-,V); }
-atomic_and(V,X) { __atomic_op(X,&,V); }
-atomic_or(V,X) { __atomic_op(X,|,V); }
-atomic_xor(V,X) { __atomic_op(X,^,V); }
-atomic_inc(X) { __atomic_op(X,+,1); }
-atomic_dec(X) { __atomic_op(X,-,1); }
-atomic_andnot(V,X) { __atomic_op(X,&~,V); }
+atomic_add(V,X) { __atomic_op{NORETURN}(X,+,V); }
+atomic_sub(V,X) { __atomic_op{NORETURN}(X,-,V); }
+atomic_and(V,X) { __atomic_op{NORETURN}(X,&,V); }
+atomic_or(V,X) { __atomic_op{NORETURN}(X,|,V); }
+atomic_xor(V,X) { __atomic_op{NORETURN}(X,^,V); }
+atomic_inc(X) { __atomic_op{NORETURN}(X,+,1); }
+atomic_dec(X) { __atomic_op{NORETURN}(X,-,1); }
+atomic_andnot(V,X) { __atomic_op{NORETURN}(X,&~,V); }
atomic_add_return(V,X) __atomic_op_return{MB}(X,+,V)
atomic_add_return_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V)
@@ -127,10 +127,10 @@ atomic_xchg(X,V) __xchg{MB}(X,V)
atomic_xchg_relaxed(X,V) __xchg{ONCE}(X,V)
atomic_xchg_release(X,V) __xchg{RELEASE}(X,V)
atomic_xchg_acquire(X,V) __xchg{ACQUIRE}(X,V)
-atomic_cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W)
-atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W)
-atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W)
-atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W)
+atomic_cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
+atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
+atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
+atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)
atomic_sub_and_test(V,X) __atomic_op_return{MB}(X,-,V) == 0
atomic_dec_and_test(X) __atomic_op_return{MB}(X,-,1) == 0
On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote:
> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
>> On 6/8/2024 3:00 AM, Alan Stern wrote:
>>> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
>>>>
>>>>
>>>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
>>>>> Just to clarify: Your first step encompasses patches 1 - 3, and the
>>>>> second step is patch 4. The first three patches can be applied
>>>>> now, but
>>>>> the last one needs to wait until herd7 has been updated. Is this all
>>>>> correct?
>>>>
>>>> Exactly.
>>>
>>> With regard to patch 4, how much thought have you and Hernan given to
>>> backward compatibility? Once herd7 is changed, old memory model files
>>> will no longer work correctly.
>>>
>>
>> Honestly, I did not think much about this (at least until Akira
>> mentioned in my PR). My hope was that changes to the model could be
>> back-ported to previous kernel versions. However that would not work
>> for existing out-of-tree files.
>>
>> My question is: is compatibility with out-of-tree files really a
>> requirement? I would argue that if people are using outdated models,
>> they may get wrong results anyway. This is because some of the changes
>> done to lkmm during the last few years change the expected result for
>> some litmus tests.
>>
>> Hernan
>
> I pushed some new changes to the code for backward compatibility [1].
> The series also needs the patch at the bottom to properly deal with the
> ordering of failing CAses and non-returning operations. With it, all
> litmus tests return the correct result (the script needs to pass option
> -lkmm-legacy false to herd).
I have been playing around with an alternative to this.
Rather than implementing this as an "option", I can implemented it as a
"model variant (*)" and add this to the model
flag ~empty (if "lkmmlatest" then 0 else _)
as new-lkmm-models-require-variant-lkmmlatest
If the user forgets to set the variant for the new model, herd7 will
flag the executions showing that something is off.
To be fully backward compatible, we would need to backport this to old
models
flag ~empty (if "lkmmlatest" then 1 else _)
as new-lkmm-models-require-variant-lkmmlatest
If the user (wrongly) sets the variant for an old model, the the
executions will be flagged.
Any thoughts?
Hernan
(*) This trick seems to be used for some arm models
https://github.com/herd/herdtools7/blob/master/herd/libdir/arm-models/mixed/ec.cat#L66C1-L67C67
>
> Implementation-wise, there are two things that I would like to have:
>
> - atomic_add_unless implementation is treated different than the rest
> and it is one of the few remaining cases where memory orderings are
> hardcoded [2]. I would like to define it in the .def file as
>
> atomic_add_unless(X,V,U) __atomic_add_unless{ONCE}(X,V,U)
>
> - "deref" and "lderef" instructions seems to add a "rb_dep" fence. None
> of the model files (.cat, .def, .bell) refers to "rb_dep" so this looks
> useless to me. However, I never checked the details of these
> dereferencing instruction so I might be missing something. Maybe Paul
> can clarify.
>
> Hernan
>
> [1] https://github.com/herd/herdtools7/pull/865
> [2] https://github.com/herd/herdtools7/issues/868
>
>
> diff --git a/tools/memory-model/linux-kernel.def
> b/tools/memory-model/linux-kernel.def
> index 001366ff3fb4..5a40c2cad39b 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -32,10 +32,10 @@ xchg(X,V) __xchg{MB}(X,V)
> xchg_relaxed(X,V) __xchg{ONCE}(X,V)
> xchg_release(X,V) __xchg{RELEASE}(X,V)
> xchg_acquire(X,V) __xchg{ACQUIRE}(X,V)
> -cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W)
> -cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W)
> -cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W)
> -cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W)
> +cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
> +cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
> +cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
> +cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)
>
> // Spinlocks
> spin_lock(X) { __lock(X); }
> @@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
> atomic_read_acquire(X) smp_load_acquire(X)
> atomic_set_release(X,V) { smp_store_release(X,V); }
>
> -atomic_add(V,X) { __atomic_op(X,+,V); }
> -atomic_sub(V,X) { __atomic_op(X,-,V); }
> -atomic_and(V,X) { __atomic_op(X,&,V); }
> -atomic_or(V,X) { __atomic_op(X,|,V); }
> -atomic_xor(V,X) { __atomic_op(X,^,V); }
> -atomic_inc(X) { __atomic_op(X,+,1); }
> -atomic_dec(X) { __atomic_op(X,-,1); }
> -atomic_andnot(V,X) { __atomic_op(X,&~,V); }
> +atomic_add(V,X) { __atomic_op{NORETURN}(X,+,V); }
> +atomic_sub(V,X) { __atomic_op{NORETURN}(X,-,V); }
> +atomic_and(V,X) { __atomic_op{NORETURN}(X,&,V); }
> +atomic_or(V,X) { __atomic_op{NORETURN}(X,|,V); }
> +atomic_xor(V,X) { __atomic_op{NORETURN}(X,^,V); }
> +atomic_inc(X) { __atomic_op{NORETURN}(X,+,1); }
> +atomic_dec(X) { __atomic_op{NORETURN}(X,-,1); }
> +atomic_andnot(V,X) { __atomic_op{NORETURN}(X,&~,V); }
>
> atomic_add_return(V,X) __atomic_op_return{MB}(X,+,V)
> atomic_add_return_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V)
> @@ -127,10 +127,10 @@ atomic_xchg(X,V) __xchg{MB}(X,V)
> atomic_xchg_relaxed(X,V) __xchg{ONCE}(X,V)
> atomic_xchg_release(X,V) __xchg{RELEASE}(X,V)
> atomic_xchg_acquire(X,V) __xchg{ACQUIRE}(X,V)
> -atomic_cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W)
> -atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W)
> -atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W)
> -atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W)
> +atomic_cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
> +atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
> +atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
> +atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)
>
> atomic_sub_and_test(V,X) __atomic_op_return{MB}(X,-,V) == 0
> atomic_dec_and_test(X) __atomic_op_return{MB}(X,-,1) == 0
Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon: > On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote: >> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote: >>> On 6/8/2024 3:00 AM, Alan Stern wrote: >>>> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: >>>>> >>>>> >>>>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern: >>>>>> Just to clarify: Your first step encompasses patches 1 - 3, and the >>>>>> second step is patch 4. The first three patches can be applied >>>>>> now, but >>>>>> the last one needs to wait until herd7 has been updated. Is this all >>>>>> correct? >>>>> >>>>> Exactly. >>>> >>>> With regard to patch 4, how much thought have you and Hernan given to >>>> backward compatibility? Once herd7 is changed, old memory model files >>>> will no longer work correctly. >>>> >>> >>> Honestly, I did not think much about this (at least until Akira >>> mentioned in my PR). My hope was that changes to the model could be >>> back-ported to previous kernel versions. However that would not work >>> for existing out-of-tree files. >>> >>> My question is: is compatibility with out-of-tree files really a >>> requirement? I would argue that if people are using outdated models, >>> they may get wrong results anyway. This is because some of the >>> changes done to lkmm during the last few years change the expected >>> result for some litmus tests. >>> >>> Hernan >> >> I pushed some new changes to the code for backward compatibility [1]. >> The series also needs the patch at the bottom to properly deal with >> the ordering of failing CAses and non-returning operations. With it, >> all litmus tests return the correct result (the script needs to pass >> option -lkmm-legacy false to herd). > > I have been playing around with an alternative to this. > > Rather than implementing this as an "option", I can implemented it as a > "model variant (*)" and add this to the model How exactly do these model variants get selected? I was thinking that another good approach could be to have a new generic C model which doesn't know anything about LKMM. I believe this would be specified in the header of the .litmus files? > flag ~empty (if "lkmmlatest" then 0 else _) > as new-lkmm-models-require-variant-lkmmlatest > > If the user forgets to set the variant for the new model, herd7 will > flag the executions showing that something is off. > > To be fully backward compatible, we would need to backport this to old > models > > flag ~empty (if "lkmmlatest" then 1 else _) > as new-lkmm-models-require-variant-lkmmlatest should this be then _ else 0 ? or what does the _ do here? I also don't think we can backport things to old models > If the user (wrongly) sets the variant for an old model, the the > executions will be flagged. > > Any thoughts? > > Hernan > > (*) This trick seems to be used for some arm models > > https://github.com/herd/herdtools7/blob/master/herd/libdir/arm-models/mixed/ec.cat#L66C1-L67C67
On 7/29/2024 4:45 PM, Jonas Oberhauser wrote: > > > Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon: >> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote: >>> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote: >>>> On 6/8/2024 3:00 AM, Alan Stern wrote: >>>>> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: >>>>>> >>>>>> >>>>>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern: >>>>>>> Just to clarify: Your first step encompasses patches 1 - 3, and the >>>>>>> second step is patch 4. The first three patches can be applied >>>>>>> now, but >>>>>>> the last one needs to wait until herd7 has been updated. Is this >>>>>>> all >>>>>>> correct? >>>>>> >>>>>> Exactly. >>>>> >>>>> With regard to patch 4, how much thought have you and Hernan given to >>>>> backward compatibility? Once herd7 is changed, old memory model files >>>>> will no longer work correctly. >>>>> >>>> >>>> Honestly, I did not think much about this (at least until Akira >>>> mentioned in my PR). My hope was that changes to the model could be >>>> back-ported to previous kernel versions. However that would not work >>>> for existing out-of-tree files. >>>> >>>> My question is: is compatibility with out-of-tree files really a >>>> requirement? I would argue that if people are using outdated models, >>>> they may get wrong results anyway. This is because some of the >>>> changes done to lkmm during the last few years change the expected >>>> result for some litmus tests. >>>> >>>> Hernan >>> >>> I pushed some new changes to the code for backward compatibility [1]. >>> The series also needs the patch at the bottom to properly deal with >>> the ordering of failing CAses and non-returning operations. With it, >>> all litmus tests return the correct result (the script needs to pass >>> option -lkmm-legacy false to herd). >> >> I have been playing around with an alternative to this. >> >> Rather than implementing this as an "option", I can implemented it as >> a "model variant (*)" and add this to the model > > How exactly do these model variants get selected? > > I was thinking that another good approach could be to have a new generic > C model which doesn't know anything about LKMM. I believe this would be > specified in the header of the .litmus files? > > >> flag ~empty (if "lkmmlatest" then 0 else _) >> as new-lkmm-models-require-variant-lkmmlatest >> >> If the user forgets to set the variant for the new model, herd7 will >> flag the executions showing that something is off. >> >> To be fully backward compatible, we would need to backport this to old >> models >> >> flag ~empty (if "lkmmlatest" then 1 else _) >> as new-lkmm-models-require-variant-lkmmlatest > > should this be then _ else 0 ? or what does the _ do here? Yes, my bad. > > I also don't think we can backport things to old models IIRC I have seen (non lkmm related) patches being backported to stable kernel versions. Why can't we do this for lkmm if backward compatibility is really a requirement? Otherwise I don't see a way of preventing developers to use old models with the new option (since I plan to keep the "old variant" as default, this would have to be done on purpose, but still). > >> If the user (wrongly) sets the variant for an old model, the the >> executions will be flagged. >> >> Any thoughts? >> >> Hernan >> >> (*) This trick seems to be used for some arm models >> >> https://github.com/herd/herdtools7/blob/master/herd/libdir/arm-models/mixed/ec.cat#L66C1-L67C67 >
Am 7/29/2024 um 5:19 PM schrieb Hernan Ponce de Leon: > On 7/29/2024 4:45 PM, Jonas Oberhauser wrote: >> >> >> Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon: >>> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote: >>>> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote: >>>>> On 6/8/2024 3:00 AM, Alan Stern wrote: >>>>>> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: >>>>>>> >>>>>>> >>>>>>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern: >>>>>>>> Just to clarify: Your first step encompasses patches 1 - 3, and the >>>>>>>> second step is patch 4. The first three patches can be applied >>>>>>>> now, but >>>>>>>> the last one needs to wait until herd7 has been updated. Is >>>>>>>> this all >>>>>>>> correct? >>>>>>> >>>>>>> Exactly. >>>>>> >>>>>> With regard to patch 4, how much thought have you and Hernan given to >>>>>> backward compatibility? Once herd7 is changed, old memory model >>>>>> files >>>>>> will no longer work correctly. >>>>>> >>>>> >>>>> Honestly, I did not think much about this (at least until Akira >>>>> mentioned in my PR). My hope was that changes to the model could be >>>>> back-ported to previous kernel versions. However that would not >>>>> work for existing out-of-tree files. >>>>> >>>>> My question is: is compatibility with out-of-tree files really a >>>>> requirement? I would argue that if people are using outdated >>>>> models, they may get wrong results anyway. This is because some of >>>>> the changes done to lkmm during the last few years change the >>>>> expected result for some litmus tests. >>>>> >>>>> Hernan >>>> >>>> I pushed some new changes to the code for backward compatibility >>>> [1]. The series also needs the patch at the bottom to properly deal >>>> with the ordering of failing CAses and non-returning operations. >>>> With it, all litmus tests return the correct result (the script >>>> needs to pass option -lkmm-legacy false to herd). >>> >>> I have been playing around with an alternative to this. >>> >>> Rather than implementing this as an "option", I can implemented it as >>> a "model variant (*)" and add this to the model >> >> How exactly do these model variants get selected? >> >> I was thinking that another good approach could be to have a new >> generic C model which doesn't know anything about LKMM. I believe this >> would be specified in the header of the .litmus files? >> >> >>> flag ~empty (if "lkmmlatest" then 0 else _) >>> as new-lkmm-models-require-variant-lkmmlatest >>> >>> If the user forgets to set the variant for the new model, herd7 will >>> flag the executions showing that something is off. >>> >>> To be fully backward compatible, we would need to backport this to >>> old models >>> >>> flag ~empty (if "lkmmlatest" then 1 else _) >>> as new-lkmm-models-require-variant-lkmmlatest >> >> should this be then _ else 0 ? or what does the _ do here? > > Yes, my bad. > >> >> I also don't think we can backport things to old models > > IIRC I have seen (non lkmm related) patches being backported to stable > kernel versions. Why can't we do this for lkmm if backward compatibility > is really a requirement? Otherwise I don't see a way of preventing > developers to use old models with the new option (since I plan to keep > the "old variant" as default, this would have to be done on purpose, but > still). I don't think this is a problem. If the old version is the default, and we define it in the .cfg file for the tree version of LKMM, then it will work correctly for both the old and new versions. People playing around with Memory Models should be careful enough not to intentionally break the model by passing bogus options. Of course, defining a new syntax identifier and putting it in all headers would be more robust. But it's more work and I would only do that if we really got rid of all the LKMM specifics. Have fun, jonas
On 7/29/2024 5:44 PM, Jonas Oberhauser wrote: > > > Am 7/29/2024 um 5:19 PM schrieb Hernan Ponce de Leon: >> On 7/29/2024 4:45 PM, Jonas Oberhauser wrote: >>> >>> >>> Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon: >>>> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote: >>>>> On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote: >>>>>> On 6/8/2024 3:00 AM, Alan Stern wrote: >>>>>>> On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: >>>>>>>> >>>>>>>> >>>>>>>> Am 6/4/2024 um 7:56 PM schrieb Alan Stern: >>>>>>>>> Just to clarify: Your first step encompasses patches 1 - 3, and >>>>>>>>> the >>>>>>>>> second step is patch 4. The first three patches can be applied >>>>>>>>> now, but >>>>>>>>> the last one needs to wait until herd7 has been updated. Is >>>>>>>>> this all >>>>>>>>> correct? >>>>>>>> >>>>>>>> Exactly. >>>>>>> >>>>>>> With regard to patch 4, how much thought have you and Hernan >>>>>>> given to >>>>>>> backward compatibility? Once herd7 is changed, old memory model >>>>>>> files >>>>>>> will no longer work correctly. >>>>>>> >>>>>> >>>>>> Honestly, I did not think much about this (at least until Akira >>>>>> mentioned in my PR). My hope was that changes to the model could >>>>>> be back-ported to previous kernel versions. However that would not >>>>>> work for existing out-of-tree files. >>>>>> >>>>>> My question is: is compatibility with out-of-tree files really a >>>>>> requirement? I would argue that if people are using outdated >>>>>> models, they may get wrong results anyway. This is because some of >>>>>> the changes done to lkmm during the last few years change the >>>>>> expected result for some litmus tests. >>>>>> >>>>>> Hernan >>>>> >>>>> I pushed some new changes to the code for backward compatibility >>>>> [1]. The series also needs the patch at the bottom to properly deal >>>>> with the ordering of failing CAses and non-returning operations. >>>>> With it, all litmus tests return the correct result (the script >>>>> needs to pass option -lkmm-legacy false to herd). >>>> >>>> I have been playing around with an alternative to this. >>>> >>>> Rather than implementing this as an "option", I can implemented it >>>> as a "model variant (*)" and add this to the model >>> >>> How exactly do these model variants get selected? >>> >>> I was thinking that another good approach could be to have a new >>> generic C model which doesn't know anything about LKMM. I believe >>> this would be specified in the header of the .litmus files? >>> >>> >>>> flag ~empty (if "lkmmlatest" then 0 else _) >>>> as new-lkmm-models-require-variant-lkmmlatest >>>> >>>> If the user forgets to set the variant for the new model, herd7 will >>>> flag the executions showing that something is off. >>>> >>>> To be fully backward compatible, we would need to backport this to >>>> old models >>>> >>>> flag ~empty (if "lkmmlatest" then 1 else _) >>>> as new-lkmm-models-require-variant-lkmmlatest >>> >>> should this be then _ else 0 ? or what does the _ do here? >> >> Yes, my bad. >> >>> >>> I also don't think we can backport things to old models >> >> IIRC I have seen (non lkmm related) patches being backported to stable >> kernel versions. Why can't we do this for lkmm if backward >> compatibility is really a requirement? Otherwise I don't see a way of >> preventing developers to use old models with the new option (since I >> plan to keep the "old variant" as default, this would have to be done >> on purpose, but still). > > I don't think this is a problem. If the old version is the default, and > we define it in the .cfg file for the tree version of LKMM, then it will > work correctly for both the old and new versions. People playing around > with Memory Models should be careful enough not to intentionally break > the model by passing bogus options. The same was true for my implementation using the lkmm-legacy option rather than the model variant, but this was still considered to break backward compatibility. https://github.com/herd/herdtools7/pull/865#issuecomment-2229930493 > > Of course, defining a new syntax identifier and putting it in all > headers would be more robust. But it's more work and I would only do > that if we really got rid of all the LKMM specifics. > > Have fun, > jonas
Am 7/29/2024 um 5:53 PM schrieb Hernan Ponce de Leon: > On 7/29/2024 5:44 PM, Jonas Oberhauser wrote: >> >> >> I don't think this is a problem. If the old version is the default, >> and we define it in the .cfg file for the tree version of LKMM, then >> it will work correctly for both the old and new versions. People >> playing around with Memory Models should be careful enough not to >> intentionally break the model by passing bogus options. > > The same was true for my implementation using the lkmm-legacy option Yeah, I'm fine with that one. (Although it may be better to have a version number as value instead of just a boolean flag, like -model-version=x_y_z - just in case this is not the last time). > rather than the model variant, but this was still considered to break > backward compatibility. > > https://github.com/herd/herdtools7/pull/865#issuecomment-2229930493 I think Akira is a bit overzealous here. What if a user accidentally puts -lkmm-legacy false and accidentally also adds the version number into the litmus test and/or model? The request can be fulfilled, by defining some relation in the bell file that has a magic name like version_x_y_z and checks that the x_y_z matches the -model-version=x_y_z provided as an argument. But I don't think we need to go that far. jonas
On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: > > > Am 6/4/2024 um 7:56 PM schrieb Alan Stern: > > On Tue, Jun 04, 2024 at 05:29:18PM +0200, Jonas Oberhauser wrote: > > > Currently, the effect of several tag on operations is defined only in > > > the herd7 tool's OCaml code as syntax transformations, while the effect > > > of all other tags is defined in tools/memory-model. > > > This asymmetry means that two seemingly analogous definitions in > > > tools/memory-model behave quite differently because the generated > > > representation is sometimes modified by hardcoded behavior in herd7. > > > > > > It also makes it hard to see that the behavior of the formalization > > > matches the intuition described in explanation.txt without delving into > > > the implementation of herd7. > > > > > > Furthermore, this hardcoded behavior is hard to maintain inside herd7 and > > > other tools implementing WMM, and has caused several bugs and confusions > > > with the tool maintainers, e.g.: > > > > > > https://github.com/MPI-SWS/genmc/issues/22 > > > https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904 > > > https://github.com/hernanponcedeleon/Dat3M/issues/254 > > > > > > It also means that potential future extensions of LKMM with new tags may > > > not work without changing internals of the herd7 tool. > > > > > > In this patch series, we first emulate the effect of herd7 transformations > > > in tools/memory-model through explicit rules in .cat and .bell files that > > > reference the transformed tags. > > > These transformations do not have any immediate effect with the current > > > herd7 implementation, because they apply after the syntax transformations > > > have already modified those tags. > > > > > > In a second step, we then distinguish between syntactic tags (that are > > > placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the > > > read and write of an xchg_acquire() operation) and sets of events (that > > > would be defined after the (emulated) transformations, e.g., an Acquire > > > set that includes only on the read of the xchg_acquire(), but "has been > > > removed" from the write). > > > > > > This second step is incompatible with the current herd7 implementation, > > > since herd7 uses hardcoded tag names to decide what to do with LKMM; > > > therefore, the newly introduced syntactic tags will be ignored or > > > processed incorrectly by herd7. > > > > The patches look good to me. > > > > Just to clarify: Your first step encompasses patches 1 - 3, and the > > second step is patch 4. The first three patches can be applied now, but > > the last one needs to wait until herd7 has been updated. Is this all > > correct? > > Exactly. Just to make sure that I am following along properly... My belief is that there will be a new version of this series. Please let me know if I am missing something. Thanx, Paul
Am 6/6/2024 um 6:37 PM schrieb Paul E. McKenney: > On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: >> >> >> Am 6/4/2024 um 7:56 PM schrieb Alan Stern: >>> On Tue, Jun 04, 2024 at 05:29:18PM +0200, Jonas Oberhauser wrote: >>>> Currently, the effect of several tag on operations is defined only in >>>> the herd7 tool's OCaml code as syntax transformations, while the effect >>>> of all other tags is defined in tools/memory-model. >>>> This asymmetry means that two seemingly analogous definitions in >>>> tools/memory-model behave quite differently because the generated >>>> representation is sometimes modified by hardcoded behavior in herd7. >>>> >>>> It also makes it hard to see that the behavior of the formalization >>>> matches the intuition described in explanation.txt without delving into >>>> the implementation of herd7. >>>> >>>> Furthermore, this hardcoded behavior is hard to maintain inside herd7 and >>>> other tools implementing WMM, and has caused several bugs and confusions >>>> with the tool maintainers, e.g.: >>>> >>>> https://github.com/MPI-SWS/genmc/issues/22 >>>> https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904 >>>> https://github.com/hernanponcedeleon/Dat3M/issues/254 >>>> >>>> It also means that potential future extensions of LKMM with new tags may >>>> not work without changing internals of the herd7 tool. >>>> >>>> In this patch series, we first emulate the effect of herd7 transformations >>>> in tools/memory-model through explicit rules in .cat and .bell files that >>>> reference the transformed tags. >>>> These transformations do not have any immediate effect with the current >>>> herd7 implementation, because they apply after the syntax transformations >>>> have already modified those tags. >>>> >>>> In a second step, we then distinguish between syntactic tags (that are >>>> placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the >>>> read and write of an xchg_acquire() operation) and sets of events (that >>>> would be defined after the (emulated) transformations, e.g., an Acquire >>>> set that includes only on the read of the xchg_acquire(), but "has been >>>> removed" from the write). >>>> >>>> This second step is incompatible with the current herd7 implementation, >>>> since herd7 uses hardcoded tag names to decide what to do with LKMM; >>>> therefore, the newly introduced syntactic tags will be ignored or >>>> processed incorrectly by herd7. >>> >>> The patches look good to me. >>> >>> Just to clarify: Your first step encompasses patches 1 - 3, and the >>> second step is patch 4. The first three patches can be applied now, but >>> the last one needs to wait until herd7 has been updated. Is this all >>> correct? >> >> Exactly. > > Just to make sure that I am following along properly... My belief is > that there will be a new version of this series. Please let me know if > I am missing something. At least one :)) Have fun, jonas
On Mon, Jun 10, 2024 at 10:04:26AM +0200, Jonas Oberhauser wrote: > > > Am 6/6/2024 um 6:37 PM schrieb Paul E. McKenney: > > On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote: > > > > > > > > > Am 6/4/2024 um 7:56 PM schrieb Alan Stern: > > > > On Tue, Jun 04, 2024 at 05:29:18PM +0200, Jonas Oberhauser wrote: > > > > > Currently, the effect of several tag on operations is defined only in > > > > > the herd7 tool's OCaml code as syntax transformations, while the effect > > > > > of all other tags is defined in tools/memory-model. > > > > > This asymmetry means that two seemingly analogous definitions in > > > > > tools/memory-model behave quite differently because the generated > > > > > representation is sometimes modified by hardcoded behavior in herd7. > > > > > > > > > > It also makes it hard to see that the behavior of the formalization > > > > > matches the intuition described in explanation.txt without delving into > > > > > the implementation of herd7. > > > > > > > > > > Furthermore, this hardcoded behavior is hard to maintain inside herd7 and > > > > > other tools implementing WMM, and has caused several bugs and confusions > > > > > with the tool maintainers, e.g.: > > > > > > > > > > https://github.com/MPI-SWS/genmc/issues/22 > > > > > https://github.com/herd/herdtools7/issues/384#issuecomment-1132859904 > > > > > https://github.com/hernanponcedeleon/Dat3M/issues/254 > > > > > > > > > > It also means that potential future extensions of LKMM with new tags may > > > > > not work without changing internals of the herd7 tool. > > > > > > > > > > In this patch series, we first emulate the effect of herd7 transformations > > > > > in tools/memory-model through explicit rules in .cat and .bell files that > > > > > reference the transformed tags. > > > > > These transformations do not have any immediate effect with the current > > > > > herd7 implementation, because they apply after the syntax transformations > > > > > have already modified those tags. > > > > > > > > > > In a second step, we then distinguish between syntactic tags (that are > > > > > placed by the programmer on operations, e.g., an 'ACQUIRE tag on both the > > > > > read and write of an xchg_acquire() operation) and sets of events (that > > > > > would be defined after the (emulated) transformations, e.g., an Acquire > > > > > set that includes only on the read of the xchg_acquire(), but "has been > > > > > removed" from the write). > > > > > > > > > > This second step is incompatible with the current herd7 implementation, > > > > > since herd7 uses hardcoded tag names to decide what to do with LKMM; > > > > > therefore, the newly introduced syntactic tags will be ignored or > > > > > processed incorrectly by herd7. > > > > > > > > The patches look good to me. > > > > > > > > Just to clarify: Your first step encompasses patches 1 - 3, and the > > > > second step is patch 4. The first three patches can be applied now, but > > > > the last one needs to wait until herd7 has been updated. Is this all > > > > correct? > > > > > > Exactly. > > > > Just to make sure that I am following along properly... My belief is > > that there will be a new version of this series. Please let me know if > > I am missing something. > > At least one :)) ;-) ;-) ;-) I will await a later version, then. Thanx, Paul
© 2016 - 2026 Red Hat, Inc.