TY - GEN
T1 - Using abstract interpretation to correct synchronization faults
AU - Ferrara, Pietro
AU - Tripp, Omer
AU - Liu, Peng
AU - Koskinen, Eric
N1 - Publisher Copyright:
© Springer International Publishing AG 2017.
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85010664782&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85010664782&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-52234-0_11
DO - 10.1007/978-3-319-52234-0_11
M3 - Conference contribution
AN - SCOPUS:85010664782
SN - 9783319522333
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 187
EP - 208
BT - Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings
A2 - Bouajjani, Ahmed
A2 - Monniaux, David
T2 - 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017
Y2 - 15 January 2017 through 17 January 2017
ER -