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

We present a static analysis by abstract interpretation of numeric properties in multi-threaded programs. The analysis is sound (assuming a sequentially consistent memory), parameterized by a choice of abstract domains and, in order to scale up, it is modular, in that it iterates over each thread individually (possibly several times) instead of iterating over their product. We build on previous work that formalized rely-guarantee verification methods as a concrete, fixpoint-based semantics, and then apply classic numeric abstractions to abstract independently thread states and thread interference. This results in a flexible algorithm allowing a wide range of precision versus cost trade-offs, and able to infer even flow-sensitive and relational thread interference. We implemented our method in an analyzer prototype for a simple language and experimented it on several classic mutual exclusion algorithms for two or more threads. Our prototype is instantiated with the polyhedra domain and employs simple control partitioning to distinguish critical sections from surrounding code. It currently relates the variables of all threads using polyhedra, which limits its scalability in the number of variables. Nevertheless, preliminary experiments show that modularity enables scaling to a large number of thread instances, provided that the total number of variables stays small.

Tue 17 Jan

VMCAI-2017-papers
16:00 - 17:30: VMCAI - Concurrency 2 at Amphitheater 44
Chair(s): David MonniauxCNRS, VERIMAG
VMCAI-2017-papers16:00 - 16:30
Talk
Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University
VMCAI-2017-papers16:30 - 17:00
Talk
Suvam MukherjeeIndian Institute of Science, Arunkumar SIndian Institute of Science, Deepak D'Souza
VMCAI-2017-papers17:00 - 17:30
Talk
Raphaël MonatEcole Normale Supérieure de Lyon, Antoine MinéUPMC, France