Add a three-process litmus test for the in-flight wildcard window of the single-pass wildcard-flip scan.
P0 models hazptr_synchronize(): it unpublishes the object and enqueues the waiter after its memory barrier. P1 models the scan kthread: it picks up the waiter, flips the wildcard, and performs the final hazard-pointer walk. P2 models a straggling hazptr_acquire(): it reads and publishes the old wildcard, then loads the object after its publication barrier. The forbidden outcome is that the final walk misses the straggler's slot while the straggler still loads the unpublished object. Verified with herd7 (linux-kernel.cfg): Never 0 13. Signed-off-by: Kunwu Chan <[email protected]> --- .../hazptr/hazptr-wildcard-flip-escape.litmus | 46 +++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 Documentation/litmus-tests/hazptr/hazptr-wildcard-flip-escape.litmus diff --git a/Documentation/litmus-tests/hazptr/hazptr-wildcard-flip-escape.litmus b/Documentation/litmus-tests/hazptr/hazptr-wildcard-flip-escape.litmus new file mode 100644 index 000000000000..de467bb82d20 --- /dev/null +++ b/Documentation/litmus-tests/hazptr/hazptr-wildcard-flip-escape.litmus @@ -0,0 +1,46 @@ +C hazptr-wildcard-flip-escape + +(* + * Result: Never + * + * Check that a straggling acquire which published the old + * wildcard after the final walk cannot still load the + * unpublished object. + *) + +{ + int ptr = 3; + int hp = 0; + int wildcard = 1; + int enq = 0; +} + +P0(int *ptr, int *enq) +{ + WRITE_ONCE(*ptr, 0); + smp_mb(); + smp_store_release(enq, 1); +} + +P1(int *enq, int *wildcard, int *hp) +{ + int r1; + int r2; + + r1 = smp_load_acquire(enq); + WRITE_ONCE(*wildcard, 2); + r2 = READ_ONCE(*hp); +} + +P2(int *wildcard, int *hp, int *ptr) +{ + int r0; + int r3; + + r0 = READ_ONCE(*wildcard); + WRITE_ONCE(*hp, r0); + smp_mb(); + r3 = READ_ONCE(*ptr); +} + +exists (1:r1=1 /\ 1:r2=0 /\ 2:r3=3) -- 2.43.0
