THEN parallelism

[xrchz]

The various tacticals (THEN, THENL, THEN1) could be made to parallelise evaluation of the tactics on multiple subgoals. (I think it's reasonable to treat tactics that aren't robust to such parallelism as buggy.)

[barakeel]

I have implemented parmap (parallel map) in tttTools using PolyML. Unfortunately, Metis is not robust to parallelism and return a Subscript error when run in parallel.

load "tttTools"; val it = (): unit fun f () = METIS_PROVE (map snd (DB.thms "arithmetic")) 1+1=2; val f = fn: unit -> thm f (); metis: r[+0+81]# val it = ⊢ 1 + 1 = 2: thm tttTools.parmap_err 2 f [(),()]; metis: metis: r[+0+81]# val it = [Exn Subscript, Res ⊢ 1 + 1 = 2]: thm tttTools.result list

[mn200]

Ha! That's good to know. I will check that I can reproduce this problem with Isabelle's Future module, and then start prepping for bad uses of references in the metis source code. — Thanks.

[mn200]

The problem does indeed arise when using the Isabelle concurrency library (which is not so surprising).

[mn200]

There is a problem with making THEN1 evaluate in parallel. Basically, when we write t1 >- t2 we want t2 to evaluate in parallel with the t3 we imagine will be dealing with the “other” subgoals arising.

I had thought we might be able to defer execution (in a future) of t2 so that it was happening in parallel with other things. Unfortunately, this wrecks one of the various ways in which t1 >- t2 is supposed to fail. In particular, it is supposed to fail if t2 doesn't prove the first subgoal resulting from applying t1. But if you defer t2, you have to succeed, perhaps inappropriately.

For example,

TRY (conj_tac >- ACCEPT_TAC TRUTH) ([], ``p /\ q``)

will do entirely the wrong thing: giving back ([([], ``q:bool``)], jf) where jf fails even if given a list containing a theorem stating q. Interactively this is not so bad with top-level >-s, because of constant validity checking, but if you have >- nested under things that are sensitive to failures, it all goes haywire.

It seems like we could alter the official definition of >- to have this ugly behaviour, or we could insist on a new THEN1-ish combinator. I can imagine a syntax like

 tac1 
 |- tac2a
 |>- tac2b
 |>- tac2c
 -| tac2rest

but note how this does away with the nice feature whereby prefixes of the text act as valid tactics. In the above, you have to quote the whole thing, including the tac2rest in order to get the right behaviour (and the concurrent execution). This recreates all the ugliness of THENL. In effect, you are writing tac1 THENL (tac2a::tac2b::tac2c::tac2rest*) where there are as many repetitions of tac2rest introduced as necessary.

I think the ugly >- failure behaviour might be better, along with a special-purpose forcedTHEN1 for those unusual situations where you want to put a possibly failing THEN1 under a failure-sensitive combinator.

[mn200]

Please let me know if you can think of a way to make execution of t2 happen in parallel with tactics coming later, while still keeping t1 >- t2 having type tactic.

[xrchz]

I'm not in favour of making t1 >- t2 succeed -- I don't think using THEN1 under a failure-sensitive combinator is an uncommon usage. Perhaps the new parallel THEN1 could be the one with the new name? (My opinion here is currently weak, since I'm not confident I understand what's going on..)

[mn200]

I expect that the non-nested occurrences greatly outnumber the nested ones, meaning that one would have to change fewer things to get the benefit of concurrency in existing code bases.

[mn200]

I've been testing a futures-based THEN1 on cakeml's compiler/parsing/proofs. The “sequential THEN1” (which reports failure early rather than when a justification function is applied) is needed in two places:

1. core HOL’s whileTheory
2. the preamble’s kill_asm_guard, a utility only used in pegSoundScript.sml

I have a table of elapsed (“wall clock”) time results for the two big theories

thy	#thds=1	#thds=4
pegSound	55s	41s
pegComplete	222s	138s

This is without parallelising THEN or THENL, so seems very promising.

[mn200]

I can build at selftest level 2 with the futures-based THEN1 on the branch concurrent-thens. The sTHEN1 variant was needed in ARM/arm6-verification/correctness/multScript.sml (see 262ed734722).

[mn200]

A naive handling of THEN further improves pegSound with 4 threads to 30s, and pegComplete to 121s. I say naive because what I'm playing with can cause large overheads on big splits, where I think I need to chunk workloads rather than create as many futures as there are branches in the proof.

[mn200]

A chunking strategy gets the times to (27s,30s,26s) and (110s,112s,111s) respectively. This looks like an improvement, but it still is a significant downgrade on the 8192-way split in the core distribution's real_topology script. (That runs in 10s with sequential THEN and more like 60s (!!) with concurrent THEN.)

[mn200]

Holmake --mt=8 on concurrent-thens (with some additional locking on computeLib that is not yet committed) on real_topology takes 94s for the whole file; on master (1fb7e0979a1), purely sequential HOL takes 119s. The script file is identical in both cases. If there really was an issue in October 2018, the chunking has made it go away.