PARALLEL-PROOF

Major Section:  PARALLELISM

Here we document support for parallel proof in ACL2(p), an experimental extension of ACL2; also see parallelism, and for parallel programming in particular, see parallel-programming.

Some Related Topics

• ACL2P-KEY-CHECKPOINTS -- key checkpoints in ACL2(p)

• DEFAULT-TOTAL-PARALLELISM-WORK-LIMIT -- for ACL2(p): returns the default value for global total-parallelism-work-limit

• PARALLEL-PUSHING-OF-SUBGOALS-FOR-INDUCTION -- consequences of how parallelized proofs of subgoals are pushed for induction

• SET-TOTAL-PARALLELISM-WORK-LIMIT -- for ACL2(p): set thread limit for parallelism primitives

• SET-TOTAL-PARALLELISM-WORK-LIMIT-ERROR -- for ACL2(p): control the action taken when the thread limit is exceeded

• SET-WATERFALL-PARALLELISM -- for ACL2(p): configuring the parallel execution of the waterfall

• SET-WATERFALL-PARALLELISM-HACKS-ENABLED -- for ACL2(p): enable waterfall-parallelism hacks

• SET-WATERFALL-PARALLELISM-HACKS-ENABLED! -- for ACL2(p): enabling waterfall parallelism hacks

• SET-WATERFALL-PRINTING -- for ACL2(p): configuring the printing that occurs within the parallelized waterfall

• UNSUPPORTED-WATERFALL-PARALLELISM-FEATURES -- proof features not supported with waterfall-parallelism enabled

• WATERFALL-PARALLELISM -- for ACL2(p): configuring the parallel execution of the waterfall

• WATERFALL-PRINTING -- for ACL2(p): configuring the printing within the parallelized waterfall