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

[Vincent St-Amour]

Reminder: Thomas Wahl will be giving a talk on Thursday at 2:00.

Vincent



At Wed, 29 May 2013 10:23:13 -0400,
Vincent St-Amour wrote:
> 
> 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.
> 
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar