Using abstract interpretation to correct synchronization faults

Pietro Ferrara, Omer Tripp, Peng Liu, Eric Koskinen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Proceedings
EditorsAhmed Bouajjani, David Monniaux
Pages187-208
Number of pages22
DOIs
StatePublished - 2017
Event18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 - Paris, France
Duration: 15 Jan 201717 Jan 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10145 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017
Country/TerritoryFrance
CityParis
Period15/01/1717/01/17

Fingerprint

Dive into the research topics of 'Using abstract interpretation to correct synchronization faults'. Together they form a unique fingerprint.

Cite this