On Parallelizing ACL2
David Rager, May 4, 2005
Abstract
What does it mean to parallelize ACL2? What attempts have been made in
the past? What's so hard about it? What's a long term vision for
parallelization/distribution of work for ACL2? What are the recent
developments? These questions and more, will I/we be answering during
our ACL2 meeting today.
Put more concretely, with the help of many, I've designed and
implemented a construct called "parallelize" that you can wrap around a
function call. This construct evaluates the arguments to the function
call in parallel and then applys that main function to the results of
calculating those arguments. While this construct is new, and thus
unfamiliar, its goal is to be a high level addition to the language and
provide parallelism without requiring the user to think too hard.
Handouts
- Examples and results of using the parallelize construct:
- Implementation of the parallelize construct in mostly raw lisp: