Concurrent Refinement in Nuprl
by Roderick Moten
Cornell University Ph.D. Thesis
This dissertation reports on the design, implementation, and analysis of the first parallel interactive theorem prover, called the MP refiner. The MP refiner is a shared memory multi-processor implementation of the inference engine of Nuprl. The inference engine of Nuprl is called the refiner. The MP refiner is implemented in the functional programming language Standard ML and is compatible with the refiner of Nuprl 4.1. Parallelism is provided in the MP refiner using an extension to the runtime system of the SML/NJ compiler for Standard ML. The MP refiner provides AND-parallelism and OR-parallelism expressed in terms of concurrent tactics. Concurrent tactics are created using the new tacticals PTHEN and PORELSLEL. The process of evaluating concurrent tactics is called concurrent refinement.
The MP refiner is a collection of threads operating as sequential refiners running on separate processors. Concurrent tactics exploit parallelism by spawning tactics to be evaluated by other refiner threads simultaneously. Tests conducted with the MP refiner running on a four processor Sparc shared-memory multi-processor reveal that concurrent refinement can significantly decrease the elapsed time of constructing proofs interactively. The concurrent tactics constructed with course-grain tactics gave speedups slightly less than two.
On the other hand,the concurrent tactics using fine-grain tactics gave speedups close to three. The granularity of a tactic depends on the amount of primitive inferences it invokes. The poor speedups of concurrent tactics constructed with course-grain tactics resulted from bus contention between the multiple processors caused by the memory management of SML/NJ. The design of the MP refiner is based on a rigorous mathematical description of the refiner. The mathematical description includes a model of concurrent refinement. In addition, this disseration presents the first complete rigorous presentation of the Nuprl second order substitution algorithm and the first thorough description of the various components that make up the refiner.
bibTex ref: Mot97