Preemption Sealing for Efficient Concurrency Testing

Thomas Ball

Microsoft Research

2nd March, 13:00–14:30

CS conference room, FAB 086-01

Abstract

The choice of where a thread scheduling algorithm preempts one thread in order to execute another is essential to reveal concurrency errors such as atomicity violations, livelocks, and deadlocks. We present a scheduling strategy called preemption sealing that controlsw here and when a scheduler is disabled from preempting threads during program execution. We demonstrate that this strategy is effective in addressing two key problems in testing industrial-scale concurrent programs: (1) tolerating existing errors in order to find more errors, and (2) compositional testing of layered, concurrent systems. We evaluate the effectiveness of preemption sealing,implemented in the CHESS tool, http://research.microsoft.com/chess/, for these two scenarios on newly released concurrency libraries for Microsoft's .NET framework.

This is Joint work with Sebastian Burckhardt (MSR), Katherine E. Coons (UT Austin),Madanlal Musuvathi (MSR), and Shaz Qadeer (MSR).

Biography

Tom Ball manages the Software Reliability Research group at MSR. His research interests are in how combinations of static and dynamic program analysis, model checking and theorem proving techniques can help improve the correctness and reliability of programs.

Tom attended Cornell University (B.A. 1987), and the University of Wisconsin-Madison (Ph.D. 1993). From 1993–1999, he was at Bell Labs in Naperville, IL in the (now defunct) Software Production Research Department.

Host

Fei Xie