Effective Detection of Atomic-Set Serializability Violations in Multithreaded Programs

PhD Thesis Proposal Defence


Title: "Effective Detection of Atomic-Set Serializability Violations in Multithreaded 
Programs"

by

Mr. Zhifeng Lai


Abstract:

Today's concurrent programs are riddled with bugs that can cause multiple 
threads to access shared data and interleave in ways that do not correspond to 
any sequential executions. These concurrency bugs give rise to the problem of 
data-consistency errors, which can lead to drastic consequences (e.g., the 
Northeast Blackout of 2003). However, detecting concurrency bugs is difficult 
because these bugs are manifested only under very specific thread interleavings 
but the number of possible interleavings for a multithreaded program is often 
myriad.

This proposal presents program analysis techniques to automatically verify that 
a multithreaded program correctly uses synchronization primitives to guarantee 
atomic-set serializability, a data-consistency criterion recently proposed for 
better detection of concurrency bugs. Atomic-set serializability characterizes 
a wide range of concurrency bugs. In addition, previous experiences using this 
criterion show that it is less likely to have benign violations than the other 
criteria. This proposal addresses the following two problems on detecting 
atomic-set serializability violations: inadequate interleaving coverage and 
inadequate input coverage.

First, dynamic approaches are widely used to detect errors (e.g., malign data 
race) caused by concurrency bugs. Existing dynamic approaches for detecting 
such violations are based on runtime monitoring. Their effectiveness is 
restricted by the inadequate coverage of interleavings. To address this 
problem, this proposal presents a dynamic testing technique that uses 
information from profiled runs to control a thread scheduler to focus on 
interleavings that have high potential for exhibiting such violations.

Second, for a given set of tests, our testing technique partially alleviates 
the problem of inadequate coverage of thread interleaving. However, the input 
coverage of our testing technique is restricted to that of the given tests. To 
address this problem, this proposal presents a static checking technique to 
automatically detect atomic-set serializability violations. Existing static 
approaches for detecting such violations use path-sensitive analyses, which are 
usually not scalable for large programs. To address the scalability issue, this 
proposal presents a series of flow-insensitive analyses to detect such 
violations.


Date:  			Thursday, 15 April 2010

Time:           	10:00am - 12:00noon

Venue:          	Room 3401
 			lifts 17/18

Committee Members:      Dr. Shing-Chi Cheung (Supervisor)
 			Dr. Charles Zhang (Chairperson)
 			Dr. Jogesh Muppala
 			Dr. Sunghun Kim


**** ALL are Welcome ****