A Parallel Version of the Boyer-Moore Prover
Abstract
The idea of this system is to use idle processors to in crease the speed of NQTHM. There were many design considerations, including: No shared file system; Easy to kill jobs on a given host; Easy to prevent job assignment on a given host; Robust; and Nicer user interface. The system will be used to process an NQTHM event list in parallel, with a given granularity. Given a granularity of n, then the first job will process the first n PROVE-LEMMAs. Each subsequent job will process n PROVE-LEMMAs. Since an arbitrary subsequence of PROVE-LEMMAs may require a previous definition, each will process all previous definitions. A subsequence of PROVE-LEMMAs may also require PROVE-LEMMAs from a previous subsequences, treating each PROVE-LEMMA as an ADD-AXIOM. This system allows the user to run a job on multiple machines in parallel. The issue of machine use has been discussed at Computational Logic and a preliminary policy adopted. It is the policy at Computational Logic to allow users to run parallel jobs using the dispatcher. Spawned jobs are to be run at the default (nice) priority level, and it is OK for any user to kick spawned parallel jobs off the local machine if he wishes (without feeling bad about it!).
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1989
- Accession Number
- ADA207190
Entities
People
- Matt Kaufmann
- Matt Wilding