Using abstract interpretation to correct synchronization faults

Abstract

We describe a novel use of abstract interpretation in which the abstract domain informs a runtime system to correct synchronization failures. To this end, we first introduce a novel synchronization paradigm, dubbed corrective synchronization, that is a generalization of existing approaches to ensuring serializability. Specifically, the correctness of multi-threaded execution need not be enforced by previous methods that either reduce parallelism (pessimistic) or roll back illegal thread interleavings (optimistic); instead inadmissible states can be altered into admissible ones. In this way, the effects of inadmissible interleavings can be compensated for by modifying the program state as a transaction completes, while accounting for the behavior of concurrent transactions. We have proved that corrective synchronization is serializable and give conditions under which progress is ensured. Next, we describe an abstract interpretation that is able to compute these valid serializable post-states w.r.t. a transaction’s entry state by computing an under-approximation of the serializable intermediate (or final) states as the fixpoint solution over an inter-procedural control-flow graph. These abstract states inform a runtime system that is able to perform state correction dynamically. We have instantiated this setup to clients of a Java-like Concurrent Map data structure to ensure safe composition of map operations. Finally, we report early encouraging results that the approach competes with or out-performs previous pessimistic or optimistic approaches.