• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
      • Set-waterfall-parallelism
      • Parallel-programming
      • Set-waterfall-printing
      • Unsupported-parallelism-features
      • Set-total-parallelism-work-limit
      • Set-parallel-execution
      • Set-total-parallelism-work-limit-error
      • Compiling-ACL2p
      • Waterfall-parallelism-for-book-certification
      • Cpu-core-count
      • Set-waterfall-parallelism-hacks-enabled
      • Parallel-proof
      • Non-parallel-book
      • Parallel
      • Without-waterfall-parallelism
      • Set-waterfall-parallelism-hacks-enabled!
      • With-waterfall-parallelism
      • Parallelism-build
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Parallelism

Waterfall-parallelism-for-book-certification

For ACL2(p): using waterfall parallelism during book certification

This documentation topic relates to the experimental extension of ACL2 supporting parallel execution and proof; see parallelism.

There are books whose certification can be sped up significantly by using waterfall parallelism. (See parallelism, including the caveat in its "IMPORTANT NOTE".) One such example in the ACL2 community books is models/jvm/m5/apprentice.lisp, which is typically excluded from regressions because of how long it takes to certify. In order to use waterfall parallelism during certification of a book <book-name>.lisp using `make' (see books-certification and see books-certification-classic), we recommend creating a file <book-name>.acl2 that includes the following forms.

#+acl2-par
(set-waterfall-parallelism t)

(certify-book <book-name> ? t) ; other arguments may be preferable

Note that there are books that will not certify when waterfall-parallelism is enabled. See file acl2-customization-files/README for more information, including how to certify essentially all books using waterfall parallelism.