diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-24 11:41:04 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-26 14:53:08 +0100 |
| commit | e6556db92d4c4fe9ba38f26b89f805095d2b2638 (patch) | |
| tree | f1af54e0c0db922b571ffed6ec03f11df92d1e67 | |
| parent | d002d775f76ddab45983354022a0f8c59b1af313 (diff) | |
STM: backup/restore remote counters
| -rw-r--r-- | toplevel/stm.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index e73774c97..9b07b4fcd 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -1595,9 +1595,9 @@ let join () = jab (VCS.get_branch_pos VCS.Branch.master); VCS.print () -type tasks = Slaves.tasks -let dump x = Slaves.dump x -let check_task name tasks i = +type tasks = Slaves.tasks * RemoteCounter.remote_counters_status +let dump x = Slaves.dump x, RemoteCounter.backup () +let check_task name (tasks,_) i = let vcs = VCS.backup () in try let rc = Future.purify (Slaves.check_task name tasks) i in @@ -1605,11 +1605,12 @@ let check_task name tasks i = VCS.restore vcs; rc with e when Errors.noncritical e -> VCS.restore vcs; false -let info_tasks tasks = Slaves.info_tasks tasks -let finish_tasks name u d p tasks = +let info_tasks (tasks,_) = Slaves.info_tasks tasks +let finish_tasks name u d p (t,rcbackup as tasks) = + RemoteCounter.restore rcbackup; let finish_task (_,_,i) = let vcs = VCS.backup () in - Future.purify (Slaves.finish_task name u d p tasks) i; + Future.purify (Slaves.finish_task name u d p t) i; Pp.pperr_flush (); VCS.restore vcs in try List.iter finish_task (info_tasks tasks) |