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

Explicit signaling between threads is a perennial cause of bugs in concurrent programs. While there are several run-time techniques to automatically notify threads upon the availability of some shared resource, such techniques are not widely-adopted due to their run-time overhead. This paper proposes a new solution based on static analysis for automatically generating a performant explicit-signal program from its corresponding \emph{implicit-signal} implementation. The key idea is to generate verification conditions that allow us to minimize the number of required signals and unnecessary context switches, while guaranteeing semantic equivalence between the source and target programs. We have implemented our method in a tool called Expresso and evaluate it on challenging benchmarks from prior papers and open-source software. Expresso-generated code significantly outperforms past automatic signaling mechanisms (avg. 1.56x speedup) and closely matches the performance of hand-optimized explicit-signal code.

Wed 20 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

14:00 - 15:40: Concurrency and TerminationPLDI Research Papers at Grand Ballroom AB
Chair(s): Iulian NeamtiuNew Jersey Institute of Technology
14:00 - 14:25
Talk
Static Serializability Analysis for Causal Consistency
PLDI Research Papers
Lucas BrutschyETH Zurich, Dimitar DimitrovETH Zurich, Switzerland, Peter MüllerETH Zurich, Martin VechevETH Zürich
14:25 - 14:50
Talk
CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs
PLDI Research Papers
Peizun LiuNortheastern University, USA, Thomas WahlNortheastern University
Media Attached
14:50 - 15:15
Talk
Symbolic Reasoning for Automatic Signal Placement
PLDI Research Papers
Kostas FerlesUT Austin, Jacob Van GeffenUT Austin, Isil DilligUT Austin, Yannis SmaragdakisUniversity of Athens
Media Attached
15:15 - 15:40
Talk
Advanced Automata-Based Algorithms for Program Termination Checking
PLDI Research Papers
Yu-Fang Chen, Matthias HeizmannUniversity of Freiburg, Germany, Ondřej LengálBrno University of Technology , Yong LiInstitute of Software, Chinese Academy of Sciences, Ming-Hsien TsaiAcademia Sinica, Taiwan, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences
Media Attached