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

Puranjay Mohan (1):
selftests/bpf: fix implementation of smp_mb()

 tools/testing/selftests/bpf/bpf_atomic.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

2.47.1

As BPF doesn't include any barrier instructions, smp_mb() is implemented by doing a dummy value returning atomic operation. Such an operation acts a full barrier as enforced by LKMM and also by the work in progress BPF memory model.

If the returned value is not used, clang[1] can optimize the value returning atomic instruction in to a normal atomic instruction which provides no ordering guarantees.

Mark the variable as volatile so the above optimization is never performed and smp_mb() works as expected.

[1] https://godbolt.org/z/qzze7bG6z

---
 tools/testing/selftests/bpf/bpf_atomic.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

index a9674e544322..c550e5711967 100644
@@ -61,7 +61,7 @@ extern bool CONFIG_X86_64 __kconfig __weak;
 
 #define smp_mb()                                 \
 	({                                       \
-		unsigned long __val;             \
+		volatile unsigned long __val;    \
 		__sync_fetch_and_add(&__val, 0); \
 	})
 

2.47.1

You are using llvm19 in the above godbolt run.
But from llvm20, instead of 'lock ...' insn, 'atomic_fetch_or' will be generated so barrier semantics will be preserved.

Since CI is using llvm20, so we should not have any problem. But for llvm19 or lower, the patch does fix a problem for arm64 etc. So in case that maintainer agrees with this patch, my ACK is below: