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
|14:00 - 14:25|
|14:25 - 14:50|
|14:50 - 15:15|
Kostas FerlesUT Austin, Jacob Van GeffenUT Austin, Isil DilligUT Austin, Yannis SmaragdakisUniversity of AthensMedia Attached
|15:15 - 15:40|
Yu-Fang Chen, Matthias HeizmannUniversity of Freiburg, Germany, Ondrej LengalBrno 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 SciencesMedia Attached