• 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
          • Parallelism-tutorial
          • Granularity
          • Pand
          • Deflock
          • Parallelism-at-the-top-level
          • Spec-mv-let
          • Error-triples-and-parallelism
          • Por
          • Pargs
          • Early-termination
          • With-output-lock
          • Plet
          • Parallelism-performance
          • Parallel-execution
        • 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

Parallel-programming

Parallel programming in ACL2(p)

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

One of ACL2's strengths lies in its ability to execute industrial models efficiently. The ACL2 source code provides an experimental parallel execution capability that can increase the speed of explicit evaluation, including simulator runs using such models, and it can also decrease the time required for proofs that make heavy use of the evaluation of ground terms.

The parallelism primitives are plet, pargs, pand, por, and spec-mv-let. Pand and por terminate early when an argument is found to evaluate to nil or non-nil, respectively, thus potentially improving on the efficiency of lazy evaluation. Spec-mv-let is a modification of mv-let that supports speculative and parallel execution.

Of the above five parallelism primitives, all but spec-mv-let allow for limiting parallel execution (spawning of so-called ``threads'') depending on resource availability. Specifically, the primitives allow specification of a size condition to control the granularity under which threads are allowed to spawn. You can use such granularity declarations in recursively-defined functions to implement data-dependent parallelism in their execution.

We recommend that in order to learn to use the parallelism primitives, you begin by reading examples: see parallelism-tutorial. That section will direct you to further documentation topics.

In addition to providing parallel programming primitives, ACL2(p) also provides the ability to execute the main ACL2 proof process in parallel. See set-waterfall-parallelism for further details.

Disclaimer. The parallelism primitives have been designed for executing purely functional code, but some ACL2 functions do interesting things ``under the hood'' in order to achieve their effects. For example, hons primitives such as hons-wash may not have the intended effect when executed under the parallelism primitives.

Subtopics

Parallelism-tutorial
A tutorial on how to use the parallelism library.
Granularity
Limit the amount of parallelism
Pand
Parallel, Boolean version of and
Deflock
Define a wrapper macro that provides mutual exclusion in ACL2(p)
Parallelism-at-the-top-level
Parallel execution in the ACL2 top-level loop
Spec-mv-let
Modification of mv-let supporting speculative and parallel execution
Error-triples-and-parallelism
How to avoid error triples in ACL2(p)
Por
Parallel, Boolean version of or
Pargs
Parallel evaluation of arguments in a function call
Early-termination
Early termination for pand and por.
With-output-lock
Provides a mutual-exclusion mechanism for performing output in parallel
Plet
Parallel version of let
Parallelism-performance
Performance issues for parallel execution
Parallel-execution
For ACL2(p): configure parallel execution