Add an LKMM test for the hazard-pointer publication protocol used by the lockdep conversion.
The test checks that a scan cannot miss a hazard-pointer publication while the reader still observes the pre-unpublish pointer. The smp_mb() pair provides the required ordering. This covers the resolved-publication case. The in-flight wildcard window of the wildcard-flip scan is covered by hazptr-wildcard-flip-escape.litmus. Verified with herd7: Never 0 3. Signed-off-by: Kunwu Chan <[email protected]> --- Documentation/litmus-tests/README | 13 ++++++ .../hazptr/hazptr-acquire-before-scan.litmus | 45 +++++++++++++++++++ 2 files changed, 58 insertions(+) create mode 100644 Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests/README index 4d4ec9c6f2cc..c2bf20fa4092 100644 --- a/Documentation/litmus-tests/README +++ b/Documentation/litmus-tests/README @@ -97,3 +97,16 @@ SRCU-fastpath-scan-before-anchor.litmus period, violating the SRCU grace-period guarantee. See SRCU-fastpath-anchor-before-scan.litmus for the opposite ordering. + + +hazptr (/hazptr directory) +-------------------------- + +hazptr-acquire-before-scan.litmus + Test the resolved-publication ordering between hazard-pointer + publication and the scan. + +hazptr-wildcard-flip-escape.litmus + Test the in-flight wildcard window of the single-pass wildcard-flip + scan: a straggling acquire that published the old wildcard after + the final walk cannot still load the unpublished object. diff --git a/Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus b/Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus new file mode 100644 index 000000000000..6dc13830c07c --- /dev/null +++ b/Documentation/litmus-tests/hazptr/hazptr-acquire-before-scan.litmus @@ -0,0 +1,45 @@ +C hazptr-acquire-before-scan + +(* + * Result: Never + * + * The reclaimer unpublishes the pointer, executes smp_mb(), then + * scans the hazard-pointer slot. The reader publishes the + * protected address, executes smp_mb(), then loads the pointer. + * + * The smp_mb() pair forbids the reclaimer from missing the + * publication while the reader still observes the pre-unpublish + * pointer. + * + * This is the publication protocol used by the lockdep + * is_dynamic_key()/lockdep_unregister_key() conversion. + * + * This models the resolved-publication case. The in-flight + * wildcard window of the wildcard-flip scan is covered by + * hazptr-wildcard-flip-escape.litmus. + *) + +{ +int ptr = 1; +int hp = 0; +} + +P0(int *ptr, int *hp) +{ + int r0; + + WRITE_ONCE(*ptr, 0); /* Unpublish. */ + smp_mb(); + r0 = READ_ONCE(*hp); /* Scan. */ +} + +P1(int *ptr, int *hp) +{ + int r0; + + WRITE_ONCE(*hp, 1); /* Publish. */ + smp_mb(); + r0 = READ_ONCE(*ptr); /* Load pointer. */ +} + +exists (0:r0=0 /\ 1:r0=1) -- 2.43.0
