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.

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 Monniaux CNRS, VERIMAG
16:00
30m
Talk
Using Abstract Interpretation to Correct Synchronization Faults
VMCAI
Pietro Ferrara IBM Research, Omer Tripp IBM Thomas J. Watson Research Center, Peng Liu Purdue University, Eric Koskinen Yale University
16:30
30m
Talk
Detecting All High-Level Dataraces in an RTOS Kernel.
VMCAI
Suvam Mukherjee Indian Institute of Science, Arunkumar S Indian Institute of Science, Deepak D'Souza
17:00
30m
Talk
Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions
VMCAI
Raphaël Monat Ecole Normale Supérieure de Lyon, Antoine Miné UPMC, France