Does a store-release followed by a load-acquire guarantee visibility of pagination offsets on AArch64 without extra barriers?

Resolution

Yes. On AArch64, a store-release (STLR) followed by a load-acquire (LDAR) on the same memory location guarantees that the consumer thread will see the updated pagination offset, provided the offset was written before the store-release in program order. No additional DMB or DSB barriers are required for this specific synchronization pattern in normal memory.

Technical Explanation

AArch64 utilizes a weakly ordered memory model, but STLR and LDAR provide one-way barriers that create a "synchronizes-with" relationship:

• Store-Release (STLR): Ensures all memory accesses (loads or stores) appearing before the STLR in program order are observed by other observers before the STLR itself becomes visible.
• Load-Acquire (LDAR): Ensures all memory accesses appearing after the LDAR in program order are observed only after the LDAR has completed.

When the consumer's LDAR reads the value written by the producer's STLR, the architecture guarantees that the preceding write to the pagination offset is visible to the consumer. This prevents the consumer from observing a stale offset while seeing a "ready" flag.

Implementation Requirements

1. Memory Type: This guarantee applies to Normal Memory. If the offset or flag resides in Device Memory, different ordering rules apply, and explicit barriers (like DSB) may be necessary depending on the specific device attribute.
2. Atomic Primitives: Use language-level atomics (e.g., std::atomic in C++ with memory_order_release and memory_order_acquire) to ensure the compiler does not reorder the instructions before they reach the hardware.
3. Matching Locations: The LDAR must target the same memory address as the STLR to establish the synchronization edge.

Verification Steps

To verify the implementation, perform the following checks:

• Assembly Audit: Inspect the generated assembly to confirm the compiler is emitting STLR and LDAR instructions rather than standard STR/LDR paired with DMB.
• Stress Testing: Use a tool like litmus-test or herd to simulate the memory pattern and ensure no stale reads occur under high contention.

Diagnostic Detail Required: Are the pagination offset and readiness flag located in the same cache line or mapped to different memory attributes (e.g., one in Normal and one in Device memory)?