diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2013-12-20 17:57:45 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-05 16:55:58 +0100 |
commit | 49692186bc73ff26fc008ca7cc58620a76bbd582 (patch) | |
tree | 6fb84813cbafe616e3174678c0e39d4974122200 /lib/remoteCounter.ml | |
parent | 738440cdf663f5d2cb4d8e4f186b1accb9dac81d (diff) |
Paral-ITP: cleanup of command line flags and more conservative default
-async-proofs off
the system behaves as in 8.4
-async-proofs lazy
proofs are delayed (when possible) but never processed in parallel
-async-proofs on
proofs are processed in parallel (when possible). The number of
workers is 1, can be changed with -async-proofs-j. Extra options to
the worker process can be given with -async-proofs-worker-flags.
The default for batch compilation used to be "lazy", now it is "off".
The "lazy" default was there to test the machinery, but it makes very
little sense in a batch scenario. If you process things sequentially,
you'd better do them immediately instead of accumulating everything in
memory until the end of the file and only then force all lazy computations.
The default for -ideslave was and still is "on". It becomes dynamically
"lazy" on a per task (proof) basis if the worker dies badly.
Note that by passing "-async-proofs on" to coqc one can produce a .vo
exploiting multiple workers. But this is rarely profitable given
that master-to-worker communication is inefficient (i.e. it really
depends on the size of proofs v.s. size of system state).
Diffstat (limited to 'lib/remoteCounter.ml')
-rw-r--r-- | lib/remoteCounter.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/lib/remoteCounter.ml b/lib/remoteCounter.ml index 1983d2722..e0e2d5cbc 100644 --- a/lib/remoteCounter.ml +++ b/lib/remoteCounter.ml @@ -16,14 +16,18 @@ let new_counter 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 *) - if !Flags.coq_slave_mode > 0 then - Errors.anomaly(Pp.str"Slave processes must install remote counters"); + (match !Flags.async_proofs_mode with + | Flags.APonParallel n when n > 0 -> + 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 = - if !Flags.coq_slave_mode < 1 then + (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") - else getter := f in + | _ -> ()); + getter := f in (fun () -> !getter ()), installer |