Effective Detection of Atomic-Set Serializability Violations in Multithreaded Programs

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering


PhD Thesis Defence


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

By

Mr. Zhifeng Lai


Abstract

Today’s multithreaded 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 thesis 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 thesis 
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 thesis proposes a dynamic predictive 
analysis technique that can infer potential violations from executions 
that are even violation-free, and an active randomized testing technique 
that can quickly confirm real violations reported by the dynamic 
predictive analysis technique.

Second, for a given set of tests, our dynamic predictive analysis 
technique and active randomized testing technique partially alleviate 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 thesis proposes an effective 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 thesis proposes a series 
of flow-insensitive analyses which scale to programs with thousands of 
lines of code.


Date:			Tuesday, 27 July 2010

Time:			10:00am – 12:00noon

Venue:			Room 3501
 			Lifts 25/26

Chairman:		Prof. Johnny Sin (ECE)

Committee Members:	Prof. Shing-Chi Cheung (Supervisor)
 			Prof. Lin Gu
 			Prof. Charles Zhang
                         Prof. Mitchell Tseng (IELM)
                         Prof. Michael Lyu (Comp. Sci. & Engg., CUHK)


**** ALL are Welcome ****