Wed 20 Jun 2018 14:25 - 14:50 at Grand Ballroom AB - Concurrency and Termination Chair(s): Iulian Neamtiu

A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch ``most bugs'' in practice. The question whether the technique can also prove the absence of bugs at least in some cases has remained largely open.

In this paper we introduce a broad verification methodology for resource-parameterized programs that observes how changes to the resource parameter affect the behavior of the program. Applied to the context-unbounded analysis problem (CUBA), the methodology results in partial verification techniques for procedural concurrent programs. Our solutions may not terminate, but are able to both refute and prove context-unbounded safety for concurrent recursive threads. We demonstrate the effectiveness of our method using a variety of examples, the safe of which cannot be proved safe by earlier, context-bounded methods.

Wed 20 Jun

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:40
Concurrency and TerminationPLDI Research Papers at Grand Ballroom AB
Chair(s): Iulian Neamtiu New Jersey Institute of Technology
14:00
25m
Talk
Static Serializability Analysis for Causal Consistency
PLDI Research Papers
Lucas Brutschy ETH Zurich, Dimitar Dimitrov ETH Zurich, Switzerland, Peter Müller ETH Zurich, Martin Vechev ETH Zürich
14:25
25m
Talk
CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs
PLDI Research Papers
Peizun Liu Northeastern University, USA, Thomas Wahl Northeastern University
Media Attached
14:50
25m
Talk
Symbolic Reasoning for Automatic Signal Placement
PLDI Research Papers
Kostas Ferles UT Austin, Jacob Van Geffen UT Austin, Isil Dillig UT Austin, Yannis Smaragdakis University of Athens
Media Attached
15:15
25m
Talk
Advanced Automata-Based Algorithms for Program Termination Checking
PLDI Research Papers
Yu-Fang Chen , Matthias Heizmann University of Freiburg, Germany, Ondřej Lengál Brno University of Technology , Yong Li Institute of Software, Chinese Academy of Sciences, Ming-Hsien Tsai Academia Sinica, Taiwan, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences
Media Attached