When a clause is moved into or from one of the sets of permanent clauses, it is usually inserted into deleted from one of the indices as well. Since movement into or from a clause set is very fast, all movements are serialized with respect to a single lock. Since updating an index must be serialized and can be expensive, each index has its own update lock.
All computation-intensive read access to the database is to obtain clauses via the indices; therefore our main strategy is to never deny read access to the indices or to a clause obtained via an index. In particular, an index can be read while it is locked (being updated) by another process, and a clause found by indexing can be used for inference, subsumption, or demodulation while it is being moved to another set (being deleted, for example) by another process. Therefore we must ensure that all indices and all clauses that can be obtained via the indices have sound (well-formed) data structures at all times during all updates.
The problem of deleting a clause while another process is using it is greatly simplified by the fact that clauses are deleted by moving them to the set Inactive rather than physically deallocating them. (The sequential theorem prover OTTER does this as well, so that deleted clauses can be printed if they occur in a proof. The memory cost for this is usually not high.) The creation of permanent clauses is not a problem2, because they are created (well-formed) before being inserted into a clause set.
The following subsections detail our approaches to the problem of maintaining soundness of the indices during updates. Aside from soundness of the data structures are questions of completeness and redundancy. A process may or may not find a particular clause via indexing, depending on the moment of update. Will the overall outcome of the two cases be the same? This question is also addressed in the following subsections.