On 5/18/2024 2:31 AM, Alan Stern wrote:
On Thu, May 16, 2024 at 10:44:05AM +0200, Hernan Ponce de Leon wrote:
On 5/16/2024 10:31 AM, Jonas Oberhauser wrote:
Am 5/16/2024 um 3:43 AM schrieb Alan Stern:
Hernan and Jonas:
Can you explain more fully the changes you want to make to herd7 and/or
the LKMM? The goal is to make the memory barriers currently implicit in
RMW operations explicit, but I couldn't understand how you propose to do
this.
Are you going to change herd7 somehow, and if so, how? It seems like
you should want to provide sufficient information so that the .bell
and .cat files can implement the appropriate memory barriers associated
with each RMW operation. What additional information is needed? And
how (explained in English, not by quoting source code) will the .bell
and .cat files make use of this information?
Alan
I don't know whether herd7 needs to be changed. Probably, herd7 does the
following:
- if a tag called Mb appears on an rmw instruction (by instruction I
mean things like xchg(), atomic_inc_return_relaxed()), replace it with
one of those things:
* full mb ; once (the rmw) ; full mb, if a value returning
(successful) rmw
* once (the rmw) otherwise
- everything else gets translated 1:1 into some internal representation
This is my understanding from reading the source code of CSem.ml in herd7's
repo.
Also, this is exactly what dartagnan is currently doing.
What I'm proposing is:
1. remove this transpilation step,
2. and instead allow the Mb tag to actually appear on RMW instructions
3. change the cat file to explicitly define the behavior of the Mb tag
on RMW instructions
These are the exact 3 things I changed in dartagnan for testing what Jonas
proposed.
I am not sure if further changes are needed for herd7.
I implemented these changes in herd7 and they seem enough.
I opened a PRs for discussion
https://github.com/herd/herdtools7/pull/865
Okay, good. This answers the first part of what I asked. What about
the second part? That is, how will the changes to the .def, .bell, and
.cat files achieve your goals?
At least the cat model needs to be updated. If I remove the fences from
herd7, but keep the current model, these 4 tests fail.
--- Summary:
!!! Result changed:
./litmus/manual/locked/SUW+or-ow+l-ow-or.litmus.out.new
!!! Result changed:
./litmus/manual/atomic/C-PaulEMcKenney-SB+adat-o+adat-o.litmus.out.new
!!! Result changed: ./litmus/manual/atomic/C-atomic-01.litmus.out.new
!!! Result changed: ./litmus/manual/atomic/C-atomic-02.litmus.out.new
Using this patch I get the correct results
diff --git a/tools/memory-model/linux-kernel.cat
b/tools/memory-model/linux-kernel.cat
index adf3c4f41229..7e4787cdbd66 100644
--- a/tools/memory-model/linux-kernel.cat
+++ b/tools/memory-model/linux-kernel.cat
@@ -34,6 +34,12 @@ let R4rmb = R \ Noreturn (* Reads for which rmb
works *)
let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb]
let wmb = [W] ; fencerel(Wmb) ; [W]
let mb = ([M] ; fencerel(Mb) ; [M]) |
+ (* everything across a full barrier RMW is ordered. This
includes up to one event inside the RMW. *)
+ ([M] ; po ; [RMW & Mb] ; po ; [M]) |
+ (* full barrier RMW writes are ordered with everything behind
the RMW *)
+ ([W & RMW & Mb] ; po ; [M]) |
+ (* full barrier RMW reads are ordered with everything before the
RMW *)
+ ([M] ; po ; [R & RMW & Mb]) |
([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |
Hernan
Alan
