diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/control.ml | 2 | ||||
-rw-r--r-- | lib/feedback.ml | 6 | ||||
-rw-r--r-- | lib/feedback.mli | 2 | ||||
-rw-r--r-- | lib/flags.ml | 9 | ||||
-rw-r--r-- | lib/flags.mli | 4 | ||||
-rw-r--r-- | lib/remoteCounter.ml | 12 | ||||
-rw-r--r-- | lib/system.ml | 7 | ||||
-rw-r--r-- | lib/system.mli | 3 |
8 files changed, 27 insertions, 18 deletions
diff --git a/lib/control.ml b/lib/control.ml index 18176b843..cce9d3a9f 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -14,7 +14,7 @@ let steps = ref 0 let are_we_threading = lazy ( match !Flags.async_proofs_mode with - | Flags.APonParallel _ -> true + | Flags.APon -> true | _ -> false) let check_for_interrupt () = diff --git a/lib/feedback.ml b/lib/feedback.ml index 27ed44724..e01844a48 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -65,7 +65,7 @@ type feedback_content = | GlobDef of Loc.t * string * string * string | ErrorMsg of Loc.t * string | InProgress of int - | SlaveStatus of int * string + | SlaveStatus of string * string | ProcessingInMaster | Goals of Loc.t * string | FileLoaded of string * string @@ -90,7 +90,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) | "inprogress", [n] -> InProgress (to_int n) | "slavestatus", [ns] -> - let n, s = to_pair to_int to_string ns in + let n, s = to_pair to_string to_string ns in SlaveStatus(n,s) | "goals", [loc;s] -> Goals (to_loc loc, to_string s) | "fileloaded", [dirpath; filename] -> @@ -121,7 +121,7 @@ let of_feedback_content = function | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] | SlaveStatus(n,s) -> constructor "feedback_content" "slavestatus" - [of_pair of_int of_string (n,s)] + [of_pair of_string of_string (n,s)] | Goals (loc,s) -> constructor "feedback_content" "goals" [of_loc loc;of_string s] | FileLoaded(dirpath, filename) -> diff --git a/lib/feedback.mli b/lib/feedback.mli index b3c0c8896..7e7b57625 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -40,7 +40,7 @@ type feedback_content = | GlobDef of Loc.t * string * string * string | ErrorMsg of Loc.t * string | InProgress of int - | SlaveStatus of int * string + | SlaveStatus of string * string | ProcessingInMaster | Goals of Loc.t * string | FileLoaded of string * string diff --git a/lib/flags.ml b/lib/flags.ml index 92824c9f5..4b323f611 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -48,18 +48,19 @@ let batch_mode = ref false type compilation_mode = BuildVo | BuildVi | Vi2Vo let compilation_mode = ref BuildVo -type async_proofs = APoff | APonLazy | APonParallel of int +type async_proofs = APoff | APonLazy | APon let async_proofs_mode = ref APoff let async_proofs_n_workers = ref 1 let async_proofs_private_flags = ref None let async_proofs_always_delegate = ref false let async_proofs_never_reopen_branch = ref false let async_proofs_flags_for_workers = ref [] +let async_proofs_worker_id = ref "master" let async_proofs_is_worker () = - match !async_proofs_mode with - | APonParallel n -> n > 0 - | _ -> false + !async_proofs_worker_id <> "master" +let async_proofs_is_master () = + !async_proofs_mode = APon && !async_proofs_worker_id = "master" let debug = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 7f2b749b7..db1d8bcc4 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -15,14 +15,16 @@ val batch_mode : bool ref type compilation_mode = BuildVo | BuildVi | Vi2Vo val compilation_mode : compilation_mode ref -type async_proofs = APoff | APonLazy | APonParallel of int +type async_proofs = APoff | APonLazy | APon val async_proofs_mode : async_proofs ref val async_proofs_n_workers : int ref val async_proofs_private_flags : string option ref val async_proofs_is_worker : unit -> bool +val async_proofs_is_master : unit -> bool val async_proofs_always_delegate : bool ref val async_proofs_never_reopen_branch : bool ref val async_proofs_flags_for_workers : string list ref +val async_proofs_worker_id : string ref val debug : bool ref diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index bec46901f..72887b21a 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -24,18 +24,14 @@ let new_counter ~name a ~incr ~build = (* - slaves must use a remote counter getter, not this one! *) (* - in the main process there is a race condition between slave managers (that are threads) and the main thread, hence the mutex *) - (match !Flags.async_proofs_mode with - | Flags.APonParallel n when n > 0 -> - Errors.anomaly(Pp.str"Slave processes must install remote counters"); - | _ -> ()); + if Flags.async_proofs_is_worker () then + Errors.anomaly(Pp.str"Slave processes must install remote counters"); Mutex.lock m; let x = f () in Mutex.unlock m; build x in let getter = ref(mk_thsafe_getter (fun () -> !data := incr !!data; !!data)) in let installer f = - (match !Flags.async_proofs_mode with - | Flags.APoff | Flags.APonLazy | Flags.APonParallel 0 -> - Errors.anomaly(Pp.str"Only slave processes can install a remote counter") - | _ -> ()); + if not (Flags.async_proofs_is_worker ()) then + Errors.anomaly(Pp.str"Only slave processes can install a remote counter"); getter := f in (fun () -> !getter ()), installer diff --git a/lib/system.ml b/lib/system.ml index 4188eb2b4..59260fbf6 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -295,3 +295,10 @@ let with_time time f x = let msg2 = if time then "" else " (failure)" in msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e + +let process_id () = + if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id + else if Flags.async_proofs_is_master () then + Printf.sprintf "master:%d" (Thread.id (Thread.self ())) + else "master" + diff --git a/lib/system.mli b/lib/system.mli index 9cfb1456f..0569c7889 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -69,3 +69,6 @@ val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.std_ppcmds val with_time : bool -> ('a -> 'b) -> 'a -> 'b + +(** {6 Name of current process.} *) +val process_id : unit -> string |