
; Naive Mutex for N procs (deadlock-free) (unsafe)

begin shared_data
    C  dd  0  ! as counter	
    X  dd  0
end shared_data

begin thread_code
req:  lock inc dword [C]
      cmp dword [C], 1
      je cs
rst:  mov dword [C], 0
      jmp req
cs:   inc dword [X] ; critical section
exit: mov dword [C], 0
done:  
end thread_code

begin init_code
    start_threads
end init_code

begin unsafe_prop
  eip[$t1] = done && eip[$t2] = done && $t1:X < 2
end unsafe_prop
