lkml.org 
[lkml]   [2024]   [May]   [8]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [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

\
 
 \ /
  Last update: 2024-05-08 03:17    [W:0.066 / U:1.664 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site