ARMv8 memory ordering

In the ARM Architecture Reference Manual issue D.a (ARM DDI 0487D.a) section K11.3.1 "Acquiring a lock" has the following example code:

AArch32 
Px
        PLDW[R1]                     ; preload into cache in unique state
Loop
        LDAEX R5, [R1]               ; read lock with acquire
        CMP R5, #0                   ; check if 0
        STREXEQ R5, R0, [R1]         ; attempt to store new value
        CMPEQ R5, #0                 ; test if store suceeded
        BNE Loop                     ; retry if not

        ; loads and stores in the critical region can now be performed

My question is I can not find documentation  in Chapter E2 "The AArch32 Application Level Memory Model" that would prevent a speculative store after the BNE from being accelerated before the STREXEQ causing the store to be observed by another observer before the lock is acquired.

Version A.j of the manual contained the following statement: "Speculative writes by an observer cannot be observed by another observer." Which would preclude this from happening but I can find no equivalent statement in the latest manual.

  • A speculative write that is program-order-after a conditional branch is not propagated to other threads before the conditional branch is resolved. The PE may speculate into the critical region, but the speculation is rendered invalid once it is known that the branch has been resolved in the favour of a direction leading away from the critical region.

    Edit: The above is applicable to a load-store control dependency.

More questions in this forum