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 JunDisplayed 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 25mTalk | 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 25mTalk | CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs PLDI Research Papers Media Attached | ||
14:50 25mTalk | Symbolic Reasoning for Automatic Signal Placement PLDI Research Papers Kostas Ferles UT Austin, Jacob Van Geffen UT Austin, Işıl Dillig UT Austin, Yannis Smaragdakis University of Athens Media Attached | ||
15:15 25mTalk | 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 |