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
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 | 28 +++--
tools/memory-model/linux-kernel.cat | 9 ++
tools/memory-model/linux-kernel.def | 176 +++++++++++++--------------
3 files changed, 115 insertions(+), 98 deletions(-)
--
2.34.1