diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-10 04:12:11 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-11 11:59:07 +0100 |
commit | a758aac39aa330911f5f589ab3cae1bebed1e9ce (patch) | |
tree | 17e8e7c41a194a8ac3d17c9fa922da1177e574d4 /stm | |
parent | a77f3a3e076e273af35ad520cae2eef0e3552811 (diff) |
[stm] Move process_id to Spawned.
This brings us one step closer to actually moving all STM flags to
`stm`.
Diffstat (limited to 'stm')
-rw-r--r-- | stm/asyncTaskQueue.ml | 4 | ||||
-rw-r--r-- | stm/spawned.ml | 6 | ||||
-rw-r--r-- | stm/spawned.mli | 2 | ||||
-rw-r--r-- | stm/stm.ml | 6 |
4 files changed, 13 insertions, 5 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index cd22a7183..28c16a656 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -10,7 +10,7 @@ open CErrors open Pp open Util -let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp +let stm_pr_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else () @@ -295,7 +295,7 @@ module Make(T : Task) () = struct let slave_handshake () = Pool.worker_handshake (Option.get !slave_ic) (Option.get !slave_oc) - let pp_pid pp = Pp.(str (System.process_id () ^ " ") ++ pp) + let pp_pid pp = Pp.(str (Spawned.process_id () ^ " ") ++ pp) let debug_with_pid = Feedback.(function | { contents = Message(Debug, loc, pp) } as fb -> diff --git a/stm/spawned.ml b/stm/spawned.ml index 6ab096abf..fb5708f3a 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -73,3 +73,9 @@ let get_channels () = Printf.eprintf "Fatal error: ideslave communication channels not set.\n"; exit 1 | Some(ic, oc) -> ic, oc + +let process_id () = + Printf.sprintf "%d:%s:%d" (Unix.getpid ()) + (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id + else "master") + (Thread.id (Thread.self ())) diff --git a/stm/spawned.mli b/stm/spawned.mli index c3cf4d67b..7f463c6a6 100644 --- a/stm/spawned.mli +++ b/stm/spawned.mli @@ -20,3 +20,5 @@ val init_channels : unit -> unit (* Once initialized, these are the channels to talk with our master *) val get_channels : unit -> CThread.thread_ic * out_channel +(** {6 Name of current process.} *) +val process_id : unit -> string diff --git a/stm/stm.ml b/stm/stm.ml index 8aa832da8..877263096 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -10,8 +10,8 @@ (* let stm_debug () = !Flags.debug *) let stm_debug () = !Flags.stm_debug -let stm_pr_err s = Format.eprintf "%s] %s\n%!" (System.process_id ()) s -let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (System.process_id ()) Pp.pp_with pp +let stm_pr_err s = Format.eprintf "%s] %s\n%!" (Spawned.process_id ()) s +let stm_pp_err pp = Format.eprintf "%s] @[%a@]\n%!" (Spawned.process_id ()) Pp.pp_with pp let stm_prerr_endline s = if stm_debug () then begin stm_pr_err (s ()) end else () let stm_pperr_endline s = if stm_debug () then begin stm_pp_err (s ()) end else () @@ -355,7 +355,7 @@ end = struct (* {{{ *) if stm_debug () then Flags.we_are_parsing := false; let fname = - "stm_" ^ Str.global_replace (Str.regexp " ") "_" (System.process_id ()) in + "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in let string_of_transaction = function | Cmd { cast = t } | Fork (t, _,_,_) -> (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR") |