A Parallel Version of the Boyer-Moore Prover
COMPUTATIONAL LOGIC INC AUSTIN TX
Pagination or Media Count:
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.
- Computer Programming and Software