David L. Rager
ABSTRACT
We have implemented parallelism primitives that permit an ACL2 programmer to parallelize execution of ACL2 functions. We (1) introduce logical definitions for these primitives, (2) explain the features of our extension, (3) give an evaluation strategy for our implementation, and (4) use the parallelism primitives in examples to show speedup.
- AMD. Introducing multi-core technology. On the Web, April 2006. http://multicore.amd.com/en/Technology/.Google Scholar
- Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, Inc., 1979.Google Scholar
- Richard P. Gabriel and John McCarthy. Queue-based multi-processing lisp. In Conference on LISP and Functional Programming, pages 25--44, 1984. Google ScholarDigital Library
- Jr. Henry G. Baker and Carl Hewitt. The incremental garbage collection of processes. In Symposium on Artificial Intelligence and Programming Languages, pages 55--59, 1977. Google ScholarDigital Library
- Jared Davis. Finite Set Theory based on Fully Ordered Lists. In Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004), November 2004.Google Scholar
- S. L. Peyton Jones. Parallel implementations of functional programming languages. The Computer Journal, 32(2): 175--186, 1989. Google ScholarDigital Library
- Guy L. Steele Jr. Common Lisp the Language. Digital Press, second edition, 1990. Google ScholarDigital Library
- Matt Kaufmann and J Strother Moore. Miscellaneous remarks about guards. On the Web, April 2006. http://www.cs.utexas.edu/users/moore/acl2/v2-9/GUARD-MISCELLANY.html.Google Scholar
- OpenMCL. The Ephemeral GC, April 2006. http://openmcl.clozure.com/Doc/The-Ephemeral-GC.html.Google Scholar
- Jr. Robert H. Halstead. Implementation of multilisp: Lisp on a microprocessor. In Conference on LISP and Functional Programming, pages 9--17, 1984. Google ScholarDigital Library
Index Terms
- Adding parallelism capabilities to ACL2
Recommendations
A parallelized theorem prover for a logic with parallel execution
ITP'13: Proceedings of the 4th international conference on Interactive Theorem ProvingIn order to take best advantage of modern multi-core systems, interactive theorem provers need to parallelize execution effectively. We describe our modification to a particular theorem prover, ACL2, to use parallel execution automatically in its proof ...
An optimizing compiler for FP*-a data-parallel dialect of FP
SPDP '91: Proceedings of the 1991 Third IEEE Symposium on Parallel and Distributed ProcessingThe authors present an overview of a compiler for the functional language FP* that generates programs suitable for execution on massively parallel architectures. Data-parallel programs are naturally expressed using FP* functionals, which map efficiently ...
Futhark: purely functional GPU-programming with nested parallelism and in-place array updates
PLDI 2017: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and ImplementationFuthark is a purely functional data-parallel array language that offers a machine-neutral programming model and an optimising compiler that generates OpenCL code for GPUs.
This paper presents the design and implementation of three key features of ...
Comments