tjh.dev
Merge branch 'a-tool-to-verify-the-bpf-memory-model'
Puranjay Mohan says:
====================
A tool to verify the BPF memory model
I am building a tool called blitmus[1] that converts memory model litmus
tests written in C into BPF programs that run in parallel to verify that the
JITs are enforcing the memory model correctly.
With this tool I was able to find a bug in the implementation of the smp_mb()
in the selftests.
Using the following litmus test:
C SB+fencembonceonces
(*
* Result: Never
*
* This litmus test demonstrates that full memory barriers suffice to
* order the store-buffering pattern, where each process writes to the
* variable that the preceding process reads. (Locking and RCU can also
* suffice, but not much else.)
*)
{}
P0(int *x, int *y)
{
int r0;
WRITE_ONCE(*x, 1);
smp_mb();
r0 = READ_ONCE(*y);
}
P1(int *x, int *y)
{
int r0;
WRITE_ONCE(*y, 1);
smp_mb();
r0 = READ_ONCE(*x);
}
exists (0:r0=0 /\ 1:r0=0)
Running the generated program on an ARMv8 machine:
With the current implementation of smp_mb():
[root@fedora blitmus]# ./sb_fencembonceonces
Starting litmus test with configuration:
Test: SB+fencembonceonces
Iterations: 4100
Test SB+fencembonceonces Allowed
Histogram (4 states)
4545 *>0:r0=0; 1:r0=0;
20403742 :>0:r0=0; 1:r0=1;
20591700 :>0:r0=1; 1:r0=0;
13 :>0:r0=1; 1:r0=1;
Ok
Witnesses
Positive: 4545, Negative: 40995455
Condition exists (0:r0=0 /\ 1:r0=0) is validated
Observation SB+fencembonceonces Sometimes 4545 40995455
Time SB+fencembonceonces 8.33
Thu Jul 10 16:56:41 UTC
Positive witnesses mean that smp_mb() is not working as
expected and not providing any ordering.
After applying the patch to fix smp_mb():
[root@fedora blitmus]# ./sb_fencembonceonces
Starting litmus test with configuration:
Test: SB+fencembonceonces
Iterations: 4100
Test SB+fencembonceonces Allowed
Histogram (3 states)
19657569 :>0:r0=0; 1:r0=1;
20227574 :>0:r0=1; 1:r0=0;
1114857 :>0:r0=1; 1:r0=1;
No
Witnesses
Positive: 0, Negative: 41000000
Condition exists (0:r0=0 /\ 1:r0=0) is NOT validated
Observation SB+fencembonceonces Never 0 41000000
Time SB+fencembonceonces 9.58
Thu Jul 10 16:56:10 UTC
0 positive witnesses mean that invalid behaviour is not seen and smp_mb()
is ordering the operations properly.
I hope to improve this tool more and use it to fuzz the JITs of ARMv8,
RISC-V, and Power and see what other bugs can be exposed.
[1] https://github.com/puranjaymohan/blitmus
====================
Link: https://patch.msgid.link/20250710175434.18829-1-puranjay@kernel.org
Signed-off-by: Alexei Starovoitov <ast@kernel.org>