Electrical Engineering and Computer Science

ACAL Seminar

A Randomized Algorithm for Concurrency Testing

Madan Musuvathi

Microsoft Research
Thursday, October 08, 2009
12:00pm - 1:30pm
1005 EECS

Add to Google Calendar
Seminar in conjunction with Software

About the Event

Concurrent programming is known to be error prone and concurrency bugs are notorious for hiding in rare thread schedules. The goal of concurrency testing is to effectively identify these buggy schedules from the exponentially many possible schedules.

In this talk, I will present a randomized algorithm that is extremely effective in finding concurrency bugs. The algorithm uses random choices to schedule the threads and guarantees a reasonably-large probability of finding bugs in every run of the program. Repeated independent runs can reduce the chance of missing errors to any desired bound. The guarantees of the algorithm depend on the "depth" of the bug, a new classification for concurrency bugs. Under this classification, many concurrency bugs seen in practice, including ordering violations, deadlocks, and atomicity violations, have a small depth --- mostly 1 or 2. Given a program that creates at most n threads and executes at most k synchronization operations, the randomized algorithm finds a bug of depth d with a probability at least 1/(n.k^{d-1}) in every run of the program.

The theoretical bound above is very efficient for bugs of small depths --- it is inverse polynomial both in the number of threads and in the number of synchronizations. In practice, the algorithm performs far greater than this worst-case bound, finding bugs in well-tested programs well within the first hundred runs. The algorithm scales to large programs and has found previously unknown bugs in many Microsoft products, including SQL Server, Internet Explorer, Office Communicator, and open-source programs such as Firefox, PBZip2, and Splash benchmarks.

In this talk, I will describe the theory behind this algorithm and its relationship to the Dimension Theory of Partial-Orders. I will also describe its implementation and the practical challenges in scaling this algorithm to large-scale programs.


Madan Musuvathi is a Researcher at Microsoft Research. He is interested in building analysis tools that scale to large programs. His research interests include program analysis, operating systems, verification, and model checking. He received his Ph.D. from Stanford University in 2004.

Additional Information

Contact: Lauri Johnson

Phone: 734-763-4921

Email: lkjohns@eecs.umich.edu

Sponsor: Satish Narayanasamy

Open to: Public