AArch64 SPINLOCK { (* shared memory *) uint32_t spin_lock_unlocked = 0; uint32_t crit = 0; (* P0: *) 0:X0 = spin_lock_unlocked; uint32_t 0:X1 = 0; uint32_t 0:X2 = 0; uint32_t 0:X3 = 0; 0:X4 = crit; uint32_t 0:X5 = 90; uint32_t 0:X6 = 0; uint32_t 0:X20 = 0; (* P1: *) 1:X0 = spin_lock_unlocked; uint32_t 1:X1 = 0; uint32_t 1:X2 = 0; uint32_t 1:X3 = 0; 1:X4 = crit; uint32_t 1:X5 = 91; uint32_t 1:X6 = 0; uint32_t 1:X20 = 0; } P0 | P1 ; BL enq | BL enq ; STR W5, [X4] | STR W5, [X4] ; LDR W6, [X4] | LDR W6, [X4] ; CMP W5,W6 | CMP W5,W6 ; B.NE error | B.NE error ; BL unlock | BL unlock ; B exit | B exit ; (* * void spin_lock(unsigned int *lock) * * Take the lock pointed to by lock. It is an error to call this * function while holding the lock. *) enq: |enq: ; LDAXR W1, [X0] | LDAXR W1, [X0] ; ADD W2, W1, #16, LSL #12 | ADD W2, W1, #16, LSL #12 ; STXR W3, W2, [X0] | STXR W3, W2, [X0] ; CBNZ W3, enq | CBNZ W3, enq ; EOR W2, W1, W1, ROR #16 | EOR W2, W1, W1, ROR #16 ; CBZ W2, out | CBZ W2, out ; spin: |spin: ; LDAXRH W3, [X0] | LDAXRH W3, [X0] ; EOR W2, W3, W1, LSR #16 | EOR W2, W3, W1, LSR #16 ; CBNZ W2, spin | CBNZ W2, spin ; out: RET |out: RET ; (* * void spin_unlock(unsigned int *lock) * * Release the lock pointed to by lock. It is an error to call * this function without holding the lock. *) unlock: |unlock: ; LDRH W1, [X0] | LDRH W1, [X0] ; ADD W1, W1, #1 | ADD W1, W1, #1 ; STLRH W1, [X0] | STLRH W1, [X0] ; RET | RET ; error: MOV W20, #1 |error: MOV W20, #1 ; exit: |exit: ; forall (0:X20=0 /\ 1:X20=0)