Re: [PATCH RESEND bpf-next 1/1] powerpc64/bpf: Add jit support for load_acquire and store_release

[<puranjay@kernel.org>]

Puranjay Mohan <puranjay@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