
; A Linux Spinlock Implementation (safe version)

; x86-TSO : A Rigorous and Usable Programmer's Model for x86 Multiprocessors
; Sewell et al., CACM 2010

begin shared_data
    Lock    dd  1
end shared_data

begin thread_code
acquire: lock dec dword [Lock]
         jns cs
spin:    cmp dword [Lock], 0
	 jle spin
	 jmp acquire
cs:      ; critical section
exit:    mov dword [Lock], 1
         jmp acquire
end thread_code

begin init_code
    start_threads
end init_code

begin unsafe_prop
  eip[$t1] = cs && eip[$t2] = cs
end unsafe_prop
