aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-09-14 11:40:15 +0200
committerPierre-Marie Pédrot2016-09-14 11:40:15 +0200
commit5e4dc9a1896a1dff832089be20cd43f4f4776869 (patch)
treef8661480501f26b7d3dd46e064c1a6084991a280 /stm
parent93a03345830047310d975d5de3742fa58a0a224b (diff)
parent3e794be5f02ed438cdc5a351d09bdfb54c0be01a (diff)
Merge branch 'v8.6'
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml16
-rw-r--r--stm/stm.ml8
2 files changed, 20 insertions, 4 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 49b51b1715..fa6422cdc5 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -298,10 +298,24 @@ module Make(T : Task) = struct
let slave_handshake () =
Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc)
+ let pp_pid pp =
+ (* Breaking all abstraction barriers... very nice *)
+ let get_xml pp = match Richpp.repr pp with
+ | Xml_datatype.Element("_", [], xml) -> xml
+ | _ -> assert false in
+ Richpp.richpp_of_xml (Xml_datatype.Element("_", [],
+ get_xml (Richpp.richpp_of_pp Pp.(str (System.process_id ()^ " "))) @
+ get_xml pp))
+
+ let debug_with_pid = Feedback.(function
+ | { contents = Message(Debug, loc, pp) } as fb ->
+ { fb with contents = Message(Debug,loc,pp_pid pp) }
+ | x -> x)
+
let main_loop () =
(* We pass feedback to master *)
let slave_feeder oc fb =
- Marshal.to_channel oc (RespFeedback fb) []; flush oc in
+ Marshal.to_channel oc (RespFeedback (debug_with_pid fb)) []; flush oc in
Feedback.add_feeder (fun x -> slave_feeder (Option.get !slave_oc) x);
Feedback.set_logger Feedback.feedback_logger;
(* We ask master to allocate universe identifiers *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 482bbe4c2a..3964e6b5c3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -37,10 +37,12 @@ let state_computed, state_computed_hook = Hook.make
let state_ready, state_ready_hook = Hook.make
~default:(fun state_id -> ()) ()
-let forward_feedback, forward_feedback_hook = Hook.make
- ~default:(function
+let forward_feedback, forward_feedback_hook =
+ let m = Mutex.create () in
+ Hook.make ~default:(function
| { id = id; route; contents } ->
- feedback ~id:id ~route contents) ()
+ try Mutex.lock m; feedback ~id:id ~route contents; Mutex.unlock m
+ with e -> Mutex.unlock m; raise e) ()
let parse_error, parse_error_hook = Hook.make
~default:(fun id loc msg ->