Index Insertions

To ensure that an index is well-formed at all times during insertions, we make an assumption about the underlying hardware, and use a simple technique for manipulating pointers while making the insertion.

We assume that storing a pointer in memory is an atomic operation. In particular, when accessing a pointer that may be being updated by another process, a process gets either the old pointer or the new pointer, not some bits from the old one and others from the new one.

The data structures for the indices are linked lists and trees. The trees are implemented as linked lists of subtrees, so we can limit the presentation to linked lists. Suppose we have a doubly-linked list [A,B,C,D], and suppose we wish to insert node Xbetween nodes B and C. See Figure ??.

 

Figure: During Insertion of X

9#9

We simply make sure that node X is well-formed, including the pointers to C and D and data of X (e.g., a subtree), before making B's ``next'' pointer and C's ``previous'' pointer point to X. Another process traversing the list while the update is occurring might visit node X, and it might not.

We now show that it does not matter whether the other process visits node X. Insertion into an index means that a clause becomes a candidate for an operation. Visiting node X corresponds to finding clause say C_x. For each type of index, we show that the nondeterminism of visiting X causes redundancy or optimization rather than incompleteness (failure to perform a required operation).

Clash-index.

A clause, say C_x, (the given clause) is inserted into Clash-index at the beginning of a Task A when it moves from Set-of-support to Have-been-given. The clause C_x must be available via indexing to complete inferences in that and all subsequent instances of Task A. Previous instances of Task A that are still executing at the time of the insert can then find C_x via the Clash-index. We prevent the use of C_x by those previous instances of Task A with the following technique. Each given clause is given a unique sequence number, starting with 0. This can be accomplished, because the beginnings of instances of Task A are serialized (at the highest level by the monitor). When an instance of Task A is using Clash-index to complete inferences, it rejects clauses with sequence numbers greater than that of the given clause. All rejected clauses have been inserted into Clash-index since the start of this instance of Task A, and need not be used to complete inferences. Such clauses would not be found through Clash-index an analogous sequential execution.

All-index.

A clause is inserted into All-index when it is kept by Task B. (There is no analog of the Clash-index sequence number for All-index.) Four operations make use of All-index: forward subsumption, back subsumption, back demodulation, and unit conflict.

Forward subsumption.

Just one instance of Task B can be executing at a given time, and Task B makes the second (and final) forward subsumption test, so the decision to keep a clause (inserting it into Set-of-support and All-index) is serialized. If all forward subsumption tests were performed by Task B, then forward subsumption would clearly be correct. Forward subsumption tests performed by Task A can be viewed as an optimization, because they can be performed in parallel and any clause subsumed in Task A will also be subsumed in Task B³. In particular, it does not matter if a clause newly inserted into All-index is found by Task A forward subsumption.

Back subsumption.

We assume that whenever back subsumption is in use, forward subsumption is also in use. Clauses are enqueued for back subsumption (Task C) in Task B after being inserted into all-index. We show that back subsumption with a clause C is unaffected by any clause, say C_x, that is inserted into All-index while back subsumption is occurring with clause C. Since C is inserted into All-index before C_x is inserted, C does not subsume C_x; otherwise, forward subsumption would have caused C_x to be deleted. Therefore, back subsumption on C does not find C_x by indexing.

Back demodulation.

The argument for the correctness of back demodulation is similar to that for back subsumption. A newly-kept clause C_x cannot be back demodulated by C, because C became a demodulator before the final demodulation of C_x by by Task B.

Unit conflict.

Task B performs the unit conflict test. Therefore, All-index cannot be updated at the same time the unit conflict occurs.

Demod-index.

We assume that back demodulation is in effect; otherwise, no demodulators are inserted into Demod-index after initialization. The argument for the correctness of the operation of Demod-index is similar to that for forward subsumption with All-index. In analogy with forward subsumption, Task B performs a second (and final) demodulation of potentially new clauses. A newly-kept clause that becomes a new demodulator is inserted into Demod-index by Task B, so that the any final demodulations and insertion into Demod-index are serialized. Any demodulation done by Task A can be viewed as an optimization.