aboutsummaryrefslogtreecommitdiff
path: root/stm/workerPool.ml
diff options
context:
space:
mode:
authorLasse Blaauwbroek2021-04-01 09:18:00 +0200
committerLasse Blaauwbroek2021-04-09 21:05:43 +0200
commit520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9 (patch)
tree965f41e71b205511685060a215fbaa228390be4c /stm/workerPool.ml
parent1a64b1560ce88855a76e2faa14cec2864de2f37c (diff)
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.
Diffstat (limited to 'stm/workerPool.ml')
-rw-r--r--stm/workerPool.ml7
1 files changed, 1 insertions, 6 deletions
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index 45c92c3748..fef9300377 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -72,12 +72,7 @@ let worker_handshake slave_ic slave_oc =
exit 1
let locking { lock; pool = p } f =
- try
- Mutex.lock lock;
- let x = f p in
- Mutex.unlock lock;
- x
- with e -> Mutex.unlock lock; raise e
+ CThread.with_lock lock ~scope:(fun () -> f p)
let rec create_worker extra pool priority id =
let cancel = ref false in