diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-24 11:40:32 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
commit | d002d775f76ddab45983354022a0f8c59b1af313 (patch) | |
tree | c60111f1a613cd9e86bd666ac501fb0986a9a3d5 /lib | |
parent | 2145e0274482017dc8e16c8ee774bc422be930e1 (diff) |
remoteCounter: backup/restore
When you resume the compilation of a .vi file, you want to
avoid collisions on fresh names.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/remoteCounter.ml | 22 | ||||
-rw-r--r-- | lib/remoteCounter.mli | 11 |
2 files changed, 29 insertions, 4 deletions
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index e0e2d5cbc..bec46901f 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -9,8 +9,16 @@ type 'a getter = unit -> 'a type 'a installer = ('a getter) -> unit -let new_counter a ~incr ~build = - let data = ref a in +type remote_counters_status = (string * Obj.t) list + +let counters : remote_counters_status ref = ref [] + +let (!!) x = !(!x) + +let new_counter ~name a ~incr ~build = + assert(not (List.mem_assoc name !counters)); + let data = ref (ref a) in + counters := (name, Obj.repr data) :: !counters; let m = Mutex.create () in let mk_thsafe_getter f () = (* - slaves must use a remote counter getter, not this one! *) @@ -22,7 +30,7 @@ let new_counter a ~incr ~build = | _ -> ()); 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 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 -> @@ -31,3 +39,11 @@ let new_counter a ~incr ~build = getter := f in (fun () -> !getter ()), installer +let backup () = !counters + +let restore l = + List.iter (fun (name, data) -> + assert(List.mem_assoc name !counters); + let dataref = Obj.obj (List.assoc name !counters) in + !dataref := !!(Obj.obj data)) + l diff --git a/lib/remoteCounter.mli b/lib/remoteCounter.mli index f17f1be3c..5a47ba663 100644 --- a/lib/remoteCounter.mli +++ b/lib/remoteCounter.mli @@ -6,9 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Remote counters are *global* counters for fresh ids. In the master/slave + * scenario, the slave installs a getter that asks the master for a fresh + * value. In the scenario of a slave that runs after the death of the master + * on some marshalled data, a backup of all counters status should be taken and + * restored to avoid reusing ids. *) + type 'a getter = unit -> 'a type 'a installer = ('a getter) -> unit -val new_counter : +val new_counter : name:string -> 'a -> incr:('a -> 'a) -> build:('a -> 'b) -> 'b getter * 'b installer +type remote_counters_status +val backup : unit -> remote_counters_status +val restore : remote_counters_status -> unit |