[PATCH bpf-next 0/1] A tool to verify the BPF memory model

[PATCH bpf-next 0/1] A tool to verify the BPF memory model

[Puranjay Mohan]

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

[PATCH bpf-next 1/1] selftests/bpf: fix implementation of smp_mb()

[Puranjay Mohan]

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

Fixes: 88d706ba7cc5 ("selftests/bpf: Introduce arena spin lock")
Signed-off-by: Puranjay Mohan <puranjay@kernel.org>
---
 tools/testing/selftests/bpf/bpf_atomic.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tools/testing/selftests/bpf/bpf_atomic.h b/tools/testing/selftests/bpf/bpf_atomic.h
index a9674e544322..c550e5711967 100644
--- a/tools/testing/selftests/bpf/bpf_atomic.h
+++ b/tools/testing/selftests/bpf/bpf_atomic.h
@@ -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

Re: [PATCH bpf-next 1/1] selftests/bpf: fix implementation of smp_mb()

[Yonghong Song]

On 7/10/25 10:54 AM, Puranjay Mohan wrote:
> 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

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:

   Acked-by: Yonghong Song <yonghong.song@linux.dev>
   

>
> Fixes: 88d706ba7cc5 ("selftests/bpf: Introduce arena spin lock")
> Signed-off-by: Puranjay Mohan <puranjay@kernel.org>
> ---
>   tools/testing/selftests/bpf/bpf_atomic.h | 2 +-
>   1 file changed, 1 insertion(+), 1 deletion(-)
>
> diff --git a/tools/testing/selftests/bpf/bpf_atomic.h b/tools/testing/selftests/bpf/bpf_atomic.h
> index a9674e544322..c550e5711967 100644
> --- a/tools/testing/selftests/bpf/bpf_atomic.h
> +++ b/tools/testing/selftests/bpf/bpf_atomic.h
> @@ -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); \
>   	})
>   

Re: [PATCH bpf-next 0/1] A tool to verify the BPF memory model

[patchwork-bot+netdevbpf]

Hello:

This patch was applied to bpf/bpf-next.git (master)
by Alexei Starovoitov <ast@kernel.org>:

On Thu, 10 Jul 2025 17:54:32 +0000 you wrote:
> 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.
> 
> [...]

Here is the summary with links:
  - [bpf-next,1/1] selftests/bpf: fix implementation of smp_mb()
    https://git.kernel.org/bpf/bpf-next/c/0769857a07b4

You are awesome, thank you!
-- 
Deet-doot-dot, I am a bot.
https://korg.docs.kernel.org/patchwork/pwbot.html