AArch64 broken_spinlock_ur10 { uint32_t lock = 0; uint64_t obj = 0; uint64_t ptr = obj; 0:X0 = lock; 0:X10 = ptr; 0:X11 = obj; 1:X0 = lock; 1:X10 = ptr; } P0 | P1 ; MOV X1, #0 | enq: ; STR X1, [X10] | LDAXR W1, [X0] ; DMB SY | ADD W2, W1, #16, LSL #12 ; | STXR W3, W2, [X0] ; (* spin_unlock_wait(&lock); *) | CBZ W3, enqed ; chk: | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBZ W3, enqed ; B.EQ chked | LDAXR W1, [X0] ; LDR W1, [X0] | ADD W2, W1, #16, LSL #12 ; AND W2, W1, #0xffff | STXR W3, W2, [X0] ; CMP W2, W1, LSR #16 | CBNZ W3, end ; B.EQ chked | enqed: ; LDR W1, [X0] | EOR W2, W1, W1, ROR #16 ; AND W2, W1, #0xffff | CBZ W2, outl ; CMP W2, W1, LSR #16 | spinl: ; B.NE end | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; (* smp_mb(); obj = 1; *) | CBZ W2, outl ; chked: | LDAXRH W3, [X0] ; DMB SY | ; MOV X0, #1 | EOR W2, W3, W1, LSR #16 ; STR X0, [X11] | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBZ W2, outl ; | LDAXRH W3, [X0] ; | EOR W2, W3, W1, LSR #16 ; | CBNZ W2, end ; | outl: ; | ; | (* if (ptr) BUG_ON( *ptr ); *) ; | LDR X0, [X10] ; | MOV X1, #0 ; | CBZ X0, end ; | LDR X1, [X0] ; | ; end: | end: ; ~exists (1:X1=1)