Symbolic Predictive Analysis for Concurrent Programs

Tuesday, April 12, 2011 - 4:14pm


Wednesday, April 20, 2011
3:30 PM – 4:30 PM
Computer Science Conference Room, Harold Frank Hall Rm. 1132

HOST: Tevfik Bultan

SPEAKER: Chao Wang
Researcher, NEC Laboratories

Title: Symbolic Predictive Analysis for Concurrent Programs


Multi-core and multi-processor systems are becoming increasingly popular. However, our ability to effectively harness the power of parallelism is predicated upon advances in tools and algorithms for analyzing and verifying concurrent programs. Concurrent programs are notoriously difficult to write, and a key reason for this is the behavioral complexity resulting from the large number of interleavings of concurrent components. In this talk, I will introduce a symbolic predictive analysis for runtime detection of concurrency errors, by monitoring and subsequently analyzing the execution traces of a program. This analysis consists of two steps: First, we derive a symbolic predictive model using the trace information collected at run time as well as the program source code. What this model captures are not just the given traces, but all possible interleavings of events of these traces. Then, we use symbolic reasoning to check whether there are concurrency errors in any of these interleavings. This is done by capturing these interleavings and the error conditions using a suitable set of first-order logic formulas, and deciding these formulas using a Satisfiability Modulo Theory (SMT) solver. Although the primary focus is to reduce the verification cost associated with today’s dominating practice of explicit parallel programming, the predictive model and analysis techniques can be used to address other important issues such as performance and security.


Chao Wang is a research staff member at NEC Laboratories in Princeton, New Jersey. His current research is on the specification and verification of complex computer systems (hardware, software, and embedded systems). He has a PhD degree from University of Colorado at Boulder. His thesis won the 2004 ACM SIGDA Outstanding PhD Dissertation Award. He received a NEC Technology Commercialization Award in 2007, an ACM TODAES Best Journal Paper Award in 2008, and an ACM SIGSOFT Distinguished Paper Award in 2010.