Index Deletions

A clause is deleted from all indices when it is moved to the set Inactive by back subsumption in Task C or by back demodulation in Task D. The two main problems with deletions are (1) to keep the indices well-formed so that other processes can access them during deletions, and (2) to ensure that the overall algorithm is correct with respect to deletions.

The problem of maintaining well-formed data structures is more difficult for deletions than for insertions, because dangling references must be prevented. As with insertions, we can restrict the discussion to doubly linked lists. Consider the deletion of node Xfrom the list [A,B,X,C,D]. See Figure ??.

 

Figure: After Deletion of X

10#10

If process P₁is visiting node X while it is being deleted by process P₂, process P₁ must continue to have access to X after the deletion. Our technique is to have process P₂ remove X from the list by updating B's ``next'' and D's ``previous'' pointers, but to leave node X intact until a later time when it is safe to deallocate X. It is safe to deallocate X when all processes have finished the task that is executing at the time X is removed from the list. We implement this technique by storing X, along with a record of the time at which it was removed from the list, in a special set To-be-deleted. In addition, whenever a process, say n finishes a task, it records the time in time-finished-task[n]. Periodically (the beginning of Task B in our implementation) the members of To-be-deleted are polled to determine if any can be deallocated. Consider a pair <node,time> in To-be-deleted. Let n be the number of processes, and let min be 11#11 time-finished-task[i]. if time < min, it is safe to deallocate node, because all tasks that may have been using it have finished executing.

To show that the overall algorithm is correct with respect to deletions, we show that if the database is in a stable state, then no clause subsumes any other clause and no clause can be demodulated by any demodulator.

Consider a time at which all processes are executing Task A. The data base is in a stable state, because no updates are occurring. To see that no clause (ignoring the set Inactive) subsumed any other clause, assume, by way of contradiction, that clause Q_x subsumes clause Q_a. Clause Q_x must have entered the data base after Q_a and be strictly more general than Q_a; otherwise, Q_x would have been forward subsumed by Q_a. Therefore, Q_a must have been inserted into All-index before Task C starts back subsumption with Q_x. Therefore, back subsumption with Q_x finds and deletes Q_a.

The argument for demodulation is similar to that for subsumption.

Deletions delayed by parallelism can, however, cause redundancy in inference of clauses by Task A. A clause that would have been back demodulated or back subsumed in a sequential execution can be present and be used to complete an inference in an analogous parallel execution, because the new demodulator is enqueued for Task D or the subsuming clause is enqueued for Task C.