Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 2017
Tue 17 Jan 2017 16:00 - 16:30 at Amphitheater 44 - Concurrency 2 Chair(s): David Monniaux

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.

Conference Day
Tue 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30
Concurrency 2VMCAI at Amphitheater 44
Chair(s): David MonniauxCNRS, VERIMAG
Using Abstract Interpretation to Correct Synchronization Faults
Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University
Detecting All High-Level Dataraces in an RTOS Kernel.
Suvam MukherjeeIndian Institute of Science, Arunkumar SIndian Institute of Science, Deepak D'Souza
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
Raphaël MonatEcole Normale Supérieure de Lyon, Antoine MinéUPMC, France