Thesis Topic Details

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.

This is also a PhD topic.