Thesis Topic Details

Topic ID:
2924
Title:
Static Analysis for Detecting Concurrency Bugs in Concurrent C/C++ Programs
Supervisor:
Jingling Xue
Research Area:
Programming Languages
Associated Staff
Assessor:
Manuel Chakravarty
Topic Details
Status:
Active
Type:
R & D
Programs:
CS CE SE
Group Suitable:
Yes
Industrial:
Yes
Pre-requisites:
--
Description:
Concurrent programming is gaining significant prominence in the software industry, especially due to the advent of multicores. The future of programming is concurrent programming. However, concurrent programming is hard. Concurrency bugs, such as data races, deadlocks, livelocks, atomicity violations and serialisability violations, and concurrency-related security vulnerabilities, are hard to detect, reproduce, debug and fix. Most of these concurrent bugs are of high severity, causing hangs or crashes.


Static program analysis aims at finding such concurrency bugs in a program without actually executing
it. Unlike dynamic analysis, static analysis is capable of finding all bugs in a program. However,
Concurrent programs are difficult to analyse since the number of thread
interleavings increases exponentially with the number of threads.
In addition, concurrent C/C++ programs are harder to analyse than concurrent Java programs
due to non-lexically scoped locks, pointer arithmetic and type casting, to name just a few.


A number of academic and commercial static analysis tools are available for finding concurrency bugs in C/C++/Java programs. However, industry-strength practically-usable tools are few and far between. In general, the main obstacles in static analysis are long analysis times and excessive false-positive results. The situation is worse for multi-threaded programs due to arbitrary thread interleavings and more so for concurrent C/C++ programs.


In this collaborative project with Sun Microsystems Laboratories, Brisbane, we are looking for a highly motivated student to work on developing static analysis techniques for detecting concurrency bugs in concurrent C/C++ programs and integrating your techniques with Sun's Parfait open-source framework, which is built on top of the LLVM compilation infrastructure.


Paifait aims to achieve scalability and precision for millions of lines of code by applying a variety of techniques with varying costs and precision. This sequence of techniques starts with fast techniques first so that each latter one provides a refinement of the preceding one. In addition, Paifait relies on demand-driven techniques to ensure the techniques are parallelisable with further improved scalability on multicore processors.


The number of research issues are fairly open at this stage. Specifically, we intend to identify the correlations and constraints over locks and the memory locations protected by the locks. The problems for finding certain concurrency bugs can then be solved using
data-flow analysis, abstract interpretation and
some constraint solvers (e.g., SAT and linear programming).


This project will also develop your knowledge and skills in concurrent programming to prepare you to successfully transition to the future software industry.

Comments:
http://www.gotw.ca/publications/concurrency-ddj.htm

http://www.ddj.com/development-tools/193500967?cid=RSSfeed_DDJ_debugging
http://www.cse.unsw.edu.au/~jingling/saw08.pdf


This is also a PhD topic.

Past Student Reports
 
No Reports Available. Contact the supervisor for more information.

Check out all available reports in the CSE Thesis Report Library.

NOTE: only current CSE students can login to view and select reports to download.