Sign in
android-kvm
/
linux
/
ea52d698c1ed0c4555656de0dd1f7ac5866f89e1
/
.
/
tools
/
memory-model
/
litmus-tests
/
MP+wmbonceonce+rmbonceonce.litmus
blob: 604ad41ea0c2be5e255ee8c93daa5d6e38b1bdc6 [
file
] [
log
] [
blame
]
C MP
+
wmbonceonce
+
rmbonceonce
{}
P0
(
int
*
x
,
int
*
y
)
{
WRITE_ONCE
(*
x
,
1
);
smp_wmb
();
WRITE_ONCE
(*
y
,
1
);
}
P1
(
int
*
x
,
int
*
y
)
{
int
r0
;
int
r1
;
r0
=
READ_ONCE
(*
y
);
smp_rmb
();
r1
=
READ_ONCE
(*
x
);
}
exists
(
1
:
r0
=
1
/
\
1
:
r1
=
0
)