CUBA: Interprocedural Context-UnBounded Analysis of Concurrent Programs
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 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 25mTalk | 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 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 FerlesUT Austin, Jacob Van GeffenUT Austin, Isil DilligUT Austin, Yannis SmaragdakisUniversity of Athens Media Attached | ||
15:15 25mTalk | 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 |