diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-11-27 15:09:52 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-11-27 15:12:06 +0100 |
| commit | afcc125f8ebafe4b35c61591c803e86b67cc5887 (patch) | |
| tree | e21486f5cc4ca15731c1d1426ceaebb7388cadb0 | |
| parent | f8968fb29a3fc4032622e4ebfb68be75d1c97c58 (diff) | |
Reduction: every n iterations a slaves process checks for interruption
I chose n to be 10000 iterations. It might be big, but a slave, to check
for a termination request, has to pass the ball to the thread that
sends "regularly" Ticks to the master process. Thread.yield is a
system call, so we have to do it very rarely.
| -rw-r--r-- | kernel/reduction.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 194b223bb..40b8bd4cc 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -244,6 +244,9 @@ let in_whnf (t,stk) = | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true | FLOCKED -> assert false +let steps = ref 0 + + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv @@ -251,6 +254,11 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *) and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = Util.check_for_interrupt (); + incr steps; + if !steps = 10000 && !Flags.coq_slave_mode > 0 then begin + Thread.yield (); + steps := 0; + end; (* First head reduce both terms *) let rec whd_both (t1,stk1) (t2,stk2) = let st1' = whd_stack (snd infos) t1 stk1 in |