Messages in this thread | | | Date | Wed, 8 May 2024 03:17:15 +0200 | From | Andrea Parri <> | Subject | Re: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg |
| |
> > Don't the annotations in linux-kernel.def and linux-kernel.bell (like > > "noreturn") already make this explicit? > > Not that I'm aware. All I can see there is that according to .bell RMW don't > have an mb mode, but according to .def they do. > > How this mb disappears between parsing the code (.def) and interpreting it > (.bell) is totally implicit. Including how noreturn affects this > disappeareance.
IIRC, that's more or less implicit ;-) in the herd macros of the .def file; for example,
(noreturn)
- atomic_add(V,X) { __atomic_op(X,+,V); }
Generates a pair of R*[noreturn] and W*[once] events
(w/ return)
- atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
Generates a pair of R*[once] and W*[once] events
- atomic_add_return_acquire(V,X) __atomic_op_return{acquire}(X,+,V)
Generates a pair of R*[acquire] and W*[once] events
- atomic_add_return_release(V,X) __atomic_op_return{acquire}(X,+,V)
Generates a pair of R*[once] and W*[release] events
- atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
Generates a pair of R*[once] and W*[once] events plus two F[mb] events
(possibly failing)
- atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W)
Generates a pair of R*[once] and W*[once] events if successful; a single R*[once] event otherwise.
- atomic_cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W)
Generates a pair of R*[acquire] and W*[once] events if successful; a single R*[once] event otherwise.
- atomic_cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W)
Generates a pair of R*[once] and W*[release] events if successful; a single R*[once] event otherwise.
- atomic_cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W)
Generates a pair of R*[once] and W*[once] events plus two F[mb] events if successful; a single R*[once] event otherwise.
The line
instructions RMW[{'once,'acquire,'release}]
in the .bell file seems to be effectively redundant (perhaps a LISA backward -compatibility?): consider
$ cat rmw.litmus C rmw {} P0(atomic_t *x) { int r0;
r0 = atomic_inc_return_release(x); }
exists (x=1)
Some experiments:
- Upon removing 'release from "(instructions) RMW"
$ herd7 -conf linux-kernel.cfg rmw.litmus Test rmw Allowed States 1 [x]=1; Ok Witnesses Positive: 1 Negative: 0 Condition exists ([x]=1) Observation rmw Always 1 0 Time rmw 0.00 Hash=3a2dd354c250206d993d31f05f3f595c
- Upon restoring 'release in RMW and removing it from W
$ herd7 -conf linux-kernel.cfg rmw.litmus Test rmw Allowed States 1 [x]=1; Ok Witnesses Positive: 1 Negative: 0 Condition exists ([x]=1) Observation rmw Always 1 0 Time rmw 0.00 Hash=3a2dd354c250206d993d31f05f3f595c
- Upon removing 'release from both W and RMW
$ herd7 -conf linux-kernel.cfg rmw.litmus (herd complains... ) File "./linux-kernel.bell", line 76, characters 32-39: unbound var: Release
But I'd have to defer to Luc/Jade about herd internals and/or recommended style on this matter.
Andrea
| |