diff options
| author | Pierre-Marie Pédrot | 2016-09-14 11:40:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-14 11:40:15 +0200 |
| commit | 5e4dc9a1896a1dff832089be20cd43f4f4776869 (patch) | |
| tree | f8661480501f26b7d3dd46e064c1a6084991a280 /stm | |
| parent | 93a03345830047310d975d5de3742fa58a0a224b (diff) | |
| parent | 3e794be5f02ed438cdc5a351d09bdfb54c0be01a (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/asyncTaskQueue.ml | 16 | ||||
| -rw-r--r-- | stm/stm.ml | 8 |
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 -> |
