On Parallelizing ACL2

David Rager, May 4, 2005


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.