Managing the Shared Database

In this section we present some of the implementation details of ROO, including updating the clause set and its indices and management of memory. Careful management of updates is critical for three reasons. (1) The database is shared by all processes, (2) updates occur often, and (3) we wish to minimize locking the database or parts of the database. Memory management is important, because the shared database can grow to be very large, and because much memory (new inferences) can be associated with individual processes.

All processes have access to to the shared database, which contains (among other things) of the following data.

The pool of work to be done.

The pool constists of Tasks A (inference), B (insertions into the shared database), C (back subsumption), and D (back demodulation). Use of the pool is covered in Section ??.

Permanent clauses.

A permanent clause occurs in exactly one of the sets Axioms, Set-of-support, Have-been-given, Demodulators, and Inactive. A permanent clause (the given clause) moves from Set-of-support to Have-been-given at the beginning of Task A, and a permanent clause is moved to Inactive if it is deleted by back subsumption or back demodulation. A single lock serializes movement of all permanent clauses.

Indices.

The indices are used to find clauses based on unification properties. There are three indices: All-index, Clash-index, and Demod-index. All-index refers to all clauses except those in Inactive, and it is used to locate clauses for the forward subsumption, back subsumption, and unit conflict operations and to locate terms for back demodulation. Clash-index refers to clauses in Axioms and Have-been-given, and it is used by Task A to complete inferences initiated with the given clause. Demod-index is used to locate clauses in Demodulators when demodulating clauses. Each index has a lock for serializing updates.

Process data.

This is an array, indexed by processor identifier, of collections of data. The data for each process (which is available to all other processes) contains a lock and a list for memory balancing (see Section ), the time at which the process finished its most recent Task (see Section ??), and statistics for the process.

Available nodes.

See Section ??.

Set of index nodes to be deleted.

See Section ??.