From 5d3f5c210aad8d73b007936e65694c401e66c7d0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 28 Nov 2014 18:41:43 +0100 Subject: STM: if a-p-always-delegate fetch states from parked worker on edit-at If the async-proofs-always-delegate is passed, workers are killed only when the proof they computed is obsolete. If one jumps back to a state that was computed by the worker (and not the master) instead of (re)computing such state in the master ask the worker to send it back. --- stm/vcs.mli | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'stm/vcs.mli') diff --git a/stm/vcs.mli b/stm/vcs.mli index 6c3571a08..7241ae461 100644 --- a/stm/vcs.mli +++ b/stm/vcs.mli @@ -79,11 +79,11 @@ module type S = sig (* read only dag *) module Dag : Dag.S with type node = id - val dag : ('kind,'diff,'info) t -> ('diff,'info,id) Dag.t + val dag : ('kind,'diff,'info) t -> ('diff,'info,id * id) Dag.t - val create_cluster : ('k,'e,'i) t -> id list -> id -> ('k,'e,'i) t - val cluster_of : ('k,'e,'i) t -> id -> id Dag.Cluster.t option - val delete_cluster : ('k,'e,'i) t -> id Dag.Cluster.t -> ('k,'e,'i) t + val create_cluster : ('k,'e,'i) t -> id list -> (id * id) -> ('k,'e,'i) t + val cluster_of : ('k,'e,'i) t -> id -> (id * id) Dag.Cluster.t option + val delete_cluster : ('k,'e,'i) t -> (id * id) Dag.Cluster.t -> ('k,'e,'i) t end -- cgit v1.2.3