[Pl-seminar] 6/6: Thomas Wahl, Symmetry-aware predicate abstraction for shared-variable concurrent programs

[Vincent St-Amour]

NEU Programming Languages Seminar presents

Thomas Wahl
Northeastern University

Thursday, 6/6
2:00-3:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Symmetry-aware predicate abstraction for shared-variable concurrent programs

Predicate abstraction is a key enabling technology for applying
finite-state exploration tools to programs written in mainstream
languages. It has been used successfully for debugging sequential
system-level C code, in projects such as SLAM at Microsoft. Despite this
success, there is little evidence of fruitful applications of predicate
abstraction to shared-variable concurrent software. We attribute this
gap to the lack of abstraction strategies that permit a scalable
analysis of the resulting multi-threaded Boolean programs.

In this talk I will describe a symmetry-aware predicate abstraction 
strategy: it takes into account the replicated structure of C programs 
that consist of many threads executing the same procedure, and generates
a Boolean program template whose multi-threaded execution soundly 
overapproximates the concurrent C program. State explosion during model 
checking parallel instantiations of this template can now be absorbed by 
exploiting symmetry.

In the second part I will report on efforts to extend the symmetry-aware 
method to the parametric formulation of the problem, where the number of 
executing threads is left unspecified. It turns out that the abstract 
concurrent programs obtained lack a key property that would have made 
existing infinite-state verification technology applicable. Worse, I 
discuss the somewhat surprising fact that simple program location 
reachability is in fact undecidable for these programs, despite the 
recursion-freeness and the finite-domain variables. I describe a 
low-cost, sound and precise solution to this problem, enabling the full 
parameterized verification of programs such as the ticket busy-wait lock 
algorithm, the default locking mechanism used in recent versions of the 
Linux kernel.