Research on SMP Parallel Computing

Parallelizing an Interactive Theorem Prover: Functional Programming and Proofs with ACL2

Multi-core systems have become commonplace, however, theorem provers often do not take advantage of the additional computing resources in an interactive setting. Our research explores automatically using these additional resources to lessen the delay between when users submit conjectures to the theorem prover and when they receive feedback from the prover that is useful in discovering how to successfully complete the proof of a particular theorem.

We have developed mechanisms to permit applicative programs to execute in parallel while simultaneously preparing these programs for verification by a semi-automatic reasoning system. We have also created a parallel version of an automated theorem prover, with management of user interaction issues, such as output and how inherently single-threaded, user-level proof features can be configured for use with parallel computation. Finally, we have investigated the types of proofs that are amenable to parallel execution. This investigation yields the result that almost all proof attempts that require a non-trivial amount of time can benefit from parallel execution. Proof attempts executed in parallel almost always provide the aforementioned feedback sooner than if they executed serially, and their execution time is often significantly reduced.

Dissertation Defense

There are two tarballs available, upon request, that make up the supporting evidence for the dissertation. The first tarball contains:

The second tarball contains the above, plus all of the raw data, logs, and latex and excel files that constitute the "results."

I am trying to avoid being in the business of distributing old versions of ACL2 or CCL. As such, these tarballs are not available for download, but if a reader has good reason, I can send them a tarball.

Parallelism Library for ACL2

One of ACL2's strengths lies in its ability to execute industrial models efficiently. ACL2 provides the capability to execute models in parallel. This capability can increase the speed of explicit calls to simulators written in ACL2, and it can also decrease the time required for proofs that make heavy use of the evaluation of ground terms. The parallelism primitives allow for limiting parallel evaluation (spawning of so-called ``threads'') depending on resource availability. Specifically, the primitives allow specification of a size condition to control the granularity under which parallelism is limited. If you use the parallelism primitives in recursive functions, you get data-dependent parallelism of the program's execution.

Our API consists of the ACL2 primitives plet, pargs, pand, and por, which all accept an optional granularity condition. 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.

ACL2 Parallelism Documentation

Papers and Related Downloads

Integration of our library as a build option for ACL2 is done, It's still considered experimental, but it should work for you (and please let me know if it doesn't). The following command is an example of how to use CCL to build ACL2 with the parallelism library enabled:
make PREFIX=ccl- LISP=/your-ccl-directory/ccl-1.3/ccl/scripts/ccl64 ACL2_PAR=p

Here are some bibtex entries for the above papers.

Parallelism Library for CCL and SBCL

A side-effect of our ACL2 efforts is that our four parallelism primitives also function in raw LISP, namely CCL and SBCL. In an effort to gain user feedback and exposure to more interesting programs, a raw LISP version of the parallelism library is available below. For simplicity's sake, the file is intended to be load'ed into the LISP read eval print loop.

parallel.lsp

Please see the ACL2 Documentation for an explanation of how to use the parallelism primitives.


Home

Valid XHTML 1.1!