Portable Implementation of Parallelism

The parallel algorithm described here does depend on a shared-memory model of computation, since multiple instances of Task A, together with at most one instance of Task B will be accessing the data structures of the permanent database simultaneously, as well as the list K of intermediate clauses. (See Section ?? below.) On the other hand, there is no reason to specify the program for a particular shared-memory multiprocessor.

To achieve both portability and ease of implementation, we used the approach described in [3] and the p4 system, which is the current version of the system described there. ¶4 provides a set of C macros and subroutines not only for the portable implementation of low-level primitives such as locks, but also the structures use of locks through monitors, and it includes a library of useful monitors. One particular p4 monitor, the askfor monitor, is in fact a dispatcher. It implements the model of a pool of processes operating on a shared pool of work units, which is ROO's basic design. The askfor monitor is the core of the main loop shown in Figure . In our case the work units are of two types

• generate resolvents or paramodulants for a given clause, demodulate them, and perform initial subsumption test (Task A)
• empty list K by performing final rewriting and subsumption test (Task B).

Task B has priority; whenever K is non-empty, the first process to ask for work is assigned Task B.

The askfor monitor as supplied in the p4 package has facilities for delaying processes when the pool of work becomes empty and stopping all processes when one of them signals that a proof has been found.

Since ROO is implemented in terms of p4, it is portable among shared-memory multiprocessors on which p4 is implemented. Currently these include the Sequent Symmetry and Balance, the Encore Multimax, and the BBN GP-1000 and TC-2000.