On Thu, Jul 17, 2025 at 08:56:45PM +0000, puran...@kernel.org wrote:
> Puranjay Mohan <puran...@kernel.org> writes:
>
> Somehow the cover letter for this patch was missed, adding it here:
>
> To test the functionality of these special instructions, a tool called
> blitmus[0] was used to convert the following baseline litmus test[1] to bpf
> programs:
>
> C MP+poonceonces
>
> (*
> * Result: Sometimes
> *
> * Can the counter-intuitive message-passing outcome be prevented with
> * no ordering at all?
> *)
>
> {}
>
> P0(int *buf, int *flag)
> {
> WRITE_ONCE(*buf, 1);
> WRITE_ONCE(*flag, 1);
> }
>
> P1(int *buf, int *flag)
> {
> int r0;
> int r1;
>
> r0 = READ_ONCE(*flag);
> r1 = READ_ONCE(*buf);
> }
>
> exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
>
> Running the generated bpf program shows that the bad outcome is possible on
> powerpc:
>
> [fedora@linux-kernel blitmus]$ sudo ./mp_poonceonces
> Starting litmus test with configuration:
> Test: MP+poonceonces
> Iterations: 4100
>
> Test MP+poonceonces Allowed
> Histogram (4 states)
> 21548375 :>1:r0=0; 1:r1=0;
> 301187 :>1:r0=0; 1:r1=1;
> 337147 *>1:r0=1; 1:r1=0;
> 18813291 :>1:r0=1; 1:r1=1;
> Ok
>
> Witnesses
> Positive: 337147, Negative: 40662853
> Condition exists (1:r0=1 /\ 1:r1=0) is validated
> Observation MP+poonceonces Sometimes 337147 40662853
> Time MP+poonceonces 13.48
>
> Thu Jul 17 18:12:51 UTC
>
> Now the second write and the first read is converted to store_release and
> load_acquire and it gives us the following litmus test[2]
>
> C MP+pooncerelease+poacquireonce
>
> (*
> * Result: Never
> *
> * This litmus test demonstrates that smp_store_release() and
> * smp_load_acquire() provide sufficient ordering for the message-passing
> * pattern.
> *)
>
> {}
>
> P0(int *buf, int *flag)
> {
> WRITE_ONCE(*buf, 1);
> smp_store_release(flag, 1);
> }
>
> P1(int *buf, int *flag)
> {
> int r0;
> int r1;
>
> r0 = smp_load_acquire(flag);
> r1 = READ_ONCE(*buf);
> }
>
> exists (1:r0=1 /\ 1:r1=0) (* Bad outcome. *)
>
>
> Running the generated bpf program shows that the bad outcome is *not* possible
> on powerpc with the implementation in this patch:
>
> [fedora@linux-kernel blitmus]$ sudo ./mp_pooncerelease_poacquireonce
> Starting litmus test with configuration:
> Test: MP+pooncerelease+poacquireonce
> Iterations: 4100
>
> Test MP+pooncerelease+poacquireonce Allowed
> Histogram (3 states)
> 21036021 :>1:r0=0; 1:r1=0;
> 14488694 :>1:r0=0; 1:r1=1;
> 5475285 :>1:r0=1; 1:r1=1;
> No
>
> Witnesses
> Positive: 0, Negative: 41000000
> Condition exists (1:r0=1 /\ 1:r1=0) is NOT validated
> Observation MP+pooncerelease+poacquireonce Never 0 41000000
> Time MP+pooncerelease+poacquireonce 13.74
>
> Thu Jul 17 18:13:40 UTC
>
> [0] https://github.com/puranjaymohan/blitmus
> [1]
> https://github.com/puranjaymohan/blitmus/blob/main/litmus_tests/MP%2Bpoonceonces.litmus
> [2]
> https://github.com/puranjaymohan/blitmus/blob/main/litmus_tests/MP%2Bpooncerelease%2Bpoacquireonce.litmus
Hi Puranjay,
Thanks for the patch. I applied the patch and tested it.
Before this patch:
# ./test_progs -a \
verifier_load_acquire,verifier_store_release,atomics
#11/1 atomics/add:OK
#11/2 atomics/sub:OK
#11/3 atomics/and:OK
#11/4 atomics/or:OK
#11/5 atomics/xor:OK
#11/6 atomics/cmpxchg:OK
#11/7 atomics/xchg:OK
#11 atomics:OK
#528/1 verifier_load_acquire/Clang version < 18, ENABLE_ATOMICS_TESTS not
defined, and/or JIT doesn't support load-acquire, use a dummy test:OK
#528 verifier_load_acquire:OK
#565/1 verifier_store_release/Clang version < 18, ENABLE_ATOMICS_TESTS not
defined, and/or JIT doesn't support store-release, use a dummy test:OK
#565 verifier_store_release:OK
Summary: 3/9 PASSED, 0 SKIPPED, 0 FAILED
After this patch:
# ./test_progs -a \
verifier_load_acquire,verifier_store_release,atomics
#11/1 atomics/add:OK
#11/2 atomics/sub:OK
#11/3 atomics/and:OK
#11/4 atomics/or:OK
#11/5 atomics/xor:OK
#11/6 atomics/cmpxchg:OK
#11/7 atomics/xchg:OK
#11 atomics:OK
#529/1 verifier_load_acquire/load-acquire, 8-bit:OK
#529/2 verifier_load_acquire/load-acquire, 8-bit @unpriv:OK
#529/3 verifier_load_acquire/load-acquire, 16-bit:OK
#529/4 verifier_load_acquire/load-acquire, 16-bit @unpriv:OK
#529/5 verifier_load_acquire/load-acquire, 32-bit:OK
#529/6 verifier_load_acquire/load-acquire, 32-bit @unpriv:OK
#529/7 verifier_load_acquire/load-acquire, 64-bit:OK
#529/8 verifier_load_acquire/load-acquire, 64-bit @unpriv:OK
#529/9 verifier_load_acquire/load-acquire with uninitialized src_reg:OK
#529/10 verifier_load_acquire/load-acquire with uninitialized src_reg
@unpriv:OK
#529/11 verifier_load_acquire/load-acquire with non-pointer src_reg:OK
#529/12 verifier_load_acquire/load-acquire with non-pointer src_reg @unpriv:OK
#529/13 verifier_load_acquire/misaligned load-acquire:OK
#529/14 verifier_load_acquire/misaligned load-acquire @unpriv:OK
#529/15 verifier_load_acquire/load-acquire from ctx pointer:OK
#529/16 verifier_load_acquire/load-acquire from ctx pointer @unpriv:OK
#529/17 verifier_load_acquire/load-acquire with invalid register R15:OK
#529/18 verifier_load_acquire/load-acquire with invalid register R15 @unpriv:OK
#529/19 verifier_load_acquire/load-acquire from pkt pointer:OK
#529/20 verifier_load_acquire/load-acquire from flow_keys pointer:OK
#529/21 verifier_load_acquire/load-acquire from sock pointer:OK
#529 verifier_load_acquire:OK
#566/1 verifier_store_release/store-release, 8-bit:OK
#566/2 verifier_store_release/store-release, 8-bit @unpriv:OK
#566/3 verifier_store_release/store-release, 16-bit:OK
#566/4 verifier_store_release/store-release, 16-bit @unpriv:OK
#566/5 verifier_store_release/store-release, 32-bit:OK
#566/6 verifier_store_release/store-release, 32-bit @unpriv:OK
#566/7 verifier_store_release/store-release, 64-bit:OK
#566/8 verifier_store_release/store-release, 64-bit @unpriv:OK
#566/9 verifier_store_release/store-release with uninitialized src_reg:OK
#566/10 verifier_store_release/store-release with uninitialized src_reg
@unpriv:OK
#566/11 verifier_store_release/store-release with uninitialized dst_reg:OK
#566/12 verifier_store_release/store-release with uninitialized dst_reg
@unpriv:OK
#566/13 verifier_store_release/store-release with non-pointer dst_reg:OK
#566/14 verifier_store_release/store-release with non-pointer dst_reg
@unpriv:OK
#566/15 verifier_store_release/misaligned store-release:OK
#566/16 verifier_store_release/misaligned store-release @unpriv:OK
#566/17 verifier_store_release/store-release to ctx pointer:OK
#566/18 verifier_store_release/store-release to ctx pointer @unpriv:OK
#566/19 verifier_store_release/store-release, leak pointer to stack:OK
#566/20 verifier_store_release/store-release, leak pointer to stack @unpriv:OK
#566/21 verifier_store_release/store-release, leak pointer to map:OK
#566/22 verifier_store_release/store-release, leak pointer to map @unpriv:OK
#566/23 verifier_store_release/store-release with invalid register R15:OK
#566/24 verifier_store_release/store-release with invalid register R15
@unpriv:OK
#566/25 verifier_store_release/store-release to pkt pointer:OK
#566/26 verifier_store_release/store-release to flow_keys pointer:OK
#566/27 verifier_store_release/store-release to sock pointer:OK
#566 verifier_store_release:OK
Summary: 3/55 PASSED, 0 SKIPPED, 0 FAILED
Tested-by: Saket Kumar Bhaskar <sk...@linux.ibm.com>
Regards,
Saket
