123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121typestate=|Unlocked(* can be locked *)|Locked(* is locked; threads may be waiting *)|Poisonedofexn(* disabled due to exception in critical section *)exceptionPoisonedofexntypet={id:Trace.id;mutex:Mutex.t;mutablestate:state;(* Owned by [t.mutex] *)waiters:[`Take|`Errorofexn]Waiters.t;(* Owned by [t.mutex] *)}(* Invariant: t.state <> Locked -> is_empty t.waiters *)(* When [t.state = Unlocked], [t] owns the user resource that [t] protects.
[mutex t R] means [t] is a share of a reference to a mutex with an invariant R.
[locked t] means the holder has the ability to unlock [t]. *)(* {R} t = create () {mutex t R} *)letcreate()=letid=Trace.mint_id()inTrace.create_objidMutex;{id;mutex=Mutex.create();state=Unlocked;(* Takes ownership of R *)waiters=Waiters.create();}(* {mutex t R * locked t * R} unlock t {mutex t R}
If [t] is in an invalid state, it raises an exception and nothing changes. *)letunlockt=Mutex.lockt.mutex;(* We now have ownership of [t.state] and [t.waiters]. *)Trace.putt.id;matcht.statewith|Unlocked->Mutex.unlockt.mutex;letex=Sys_error"Eio.Mutex.unlock: already unlocked!"int.state<-Poisonedex;raiseex|Locked->beginmatchWaiters.wake_onet.waiters`Takewith|`Ok->()(* We transferred [locked t * R] to a waiter; [t] remains [Locked]. *)|`Queue_empty->t.state<-Unlocked(* The state now owns R. *)end;Mutex.unlockt.mutex|Poisonedex->Mutex.unlockt.mutex;raise(Poisonedex)(* {mutex t R} lock t {mutex t R * locked t * R} *)letlockt=Mutex.lockt.mutex;matcht.statewith|Locked->Trace.try_gett.id;beginmatchWaiters.await~mutex:(Somet.mutex)"Mutex.lock"t.waiterswith|`Errorex->Trace.gett.id;raiseex(* Poisoned; stop waiting *)|`Take->(* The unlocker didn't change the state, so it's still Locked, as required.
{locked t * R} *)Trace.gett.idend|Unlocked->Trace.gett.id;t.state<-Locked;(* We transfer R from the state to our caller. *)(* {locked t * R} *)Mutex.unlockt.mutex|Poisonedex->Mutex.unlockt.mutex;raise(Poisonedex)(* {mutex t R} v = try_lock t { mutex t R * if v then locked t * R else [] } *)lettry_lockt=Mutex.lockt.mutex;matcht.statewith|Locked->Trace.try_gett.id;Mutex.unlockt.mutex;false|Unlocked->Trace.gett.id;t.state<-Locked;(* We transfer R from the state to our caller. *)Mutex.unlockt.mutex;(* {locked t * R} *)true|Poisonedex->Mutex.unlockt.mutex;raise(Poisonedex)(* {mutex t R * locked t} poison t ex {mutex t R} *)letpoisontex=Mutex.lockt.mutex;t.state<-Poisonedex;Waiters.wake_allt.waiters(`Error(Poisonedex));Mutex.unlockt.mutex(* {locked t * R} fn () {locked t * R} ->
{mutex t R} use_ro t fn {mutex t R} *)letuse_rotfn=lockt;(* {mutex t R * locked t * R} *)matchfn()with|x->unlockt;x|exceptionex->unlockt;raiseex(* {locked t * R} v = match fn () with _ -> true | exception _ -> false {locked t * if v then R else []} ->
{mutex t R} use_rw ~protect t fn {mutex t R} *)letuse_rw~protecttfn=lockt;(* {mutex t R * locked t * R} *)matchifprotectthenCancel.protectfnelsefn()with|x->unlockt;x|exceptionex->(* {mutex t R * locked t} *)poisontex;raiseex