The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 03/10/2013 01:42 PM, Enrico Tassi wrote:
> To exploit parallel hardware in OCaml you need some machinery to handle
> a pool of already running workers and have an efficient way to transmit
> a prover state back and forth.  The machinery in question must be
> efficient enough to support the granularity of parallelism one wants.
> The more fine grained it is, the more efficient the machinery must be.
>
> If I understand well your use case, you want to delegate to slave
> processes small jobs.  IMO it the most difficult case.
>    

No, I don't think my jobs qualify as small, compared to the time for a 
UNIX fork().  A majority of my subgoals require a second or more to 
prove.  Some take minutes.  So, even an approach based on fork()ing for 
each subtask could work quite well, I expect.  I would expect to see 
almost perfect improvement in running time, i.e. N cores divides running 
time by N.

> My plan is to begin parallelizing proofs, then sub proofs (assuming the
> proof language lets you easily identify independent chunks) and finally,
> only if the machinery turns out to be fast enough, tactics.
> I'm sorry, but I'm not going to give it a try soon.
>    

Well, my use case of the "parallel semicolon" would only appear as the 
top-level tactic for a theorem, so perhaps my scenario fits into your 
"sub proofs" case.

I'll be watching your work in this direction with great interest.  
Thanks for pursuing it!