Make critical sections safe in the presence of exceptions

We introduce the `with_lock` combinator that locks a mutex in an atomic fashion.
This ensures that exceptions thrown by signals will not leave the system in a
deadlocked state.

2 files changed, 4 insertions, 4 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 23d089fb6b..247b139798 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -112,8 +112,8 @@ let create_delegate ?(blocking=true) ~name fix_exn =
     if not blocking then (fun () -> raise (NotReady name)), ignore else
     let lock = Mutex.create () in
     let cond = Condition.create () in
-    (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock),
-    (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in
+    (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.wait cond lock)),
+    (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.broadcast cond)) in
   let ck = create ~name ~fix_exn (Delegated wait) in
   ck, assignment signal ck
 
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml
index 5e1150146e..9ea751eef9 100644
--- a/lib/remoteCounter.ml
+++ b/lib/remoteCounter.ml
@@ -28,10 +28,10 @@ let new_counter ~name a ~incr ~build =
          managers (that are threads) and the main thread, hence the mutex *)
     if Flags.async_proofs_is_worker () then
       CErrors.anomaly(Pp.str"Slave processes must install remote counters.");
-    Mutex.lock m; let x = f () in Mutex.unlock m;
+    let x = CThread.with_lock m ~scope:f in
     build x in
   let mk_thsafe_remote_getter f () =
-    Mutex.lock m; let x = f () in Mutex.unlock m; x in
+    CThread.with_lock m ~scope:f in
   let getter = ref(mk_thsafe_local_getter (fun () -> !data := incr !!data; !!data)) in
   let installer f =
     if not (Flags.async_proofs_is_worker ()) then