Adding parallelism capabilities to ACL2

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. Categories and Subject Descriptors D.1 [Programming Techniques]: Concurrent Programming—parallel programming; D.2.4 [Software Engineering]: Software/Program Verification—correctness proofs, formal methods; D.3.2 [Programming Languages]: Language Classifications—applicative (functional) languages General Terms verification, performance Keywords parallel ACL2, functional language, plet, pcall, pand, por, granularity

• Type: Conference
• Year: 2006
• Where: ACL2
• Authors: David L. Rager
• Keywords: ACL2 2006, ACL2 Programmer, Computational Linguistics, Concurrent Programming—parallel Programming, Parallelism Primitives