In a nutshell

The task is to implement an analysis for concurrency bugs (like races or deadlocks).

Background & motivation

Writing bug-free, safe, software in a modern language like Java can be quite a challenge: apart from getting the business logic of what is to be implemented right, null-pointer accesses and other bugs get in our way.

For concurrent/multi-threaded software, we face yet another challenge: firstly, we need to figure out where to use concurrency primitives like locking to protect shared data. Design decision have a big influence on performance here—of course we could just use one “giant” lock to protect resources, but then we’d almost end up with a sequential application again.

More critically, we may accidentally introduce deadlocks or data-races, which will make our application get stuck or produce garbled results.

At PSY, we have developed a basic theory about how to analyse such software. See for instance “Behaviour Inference”, “Deadlock checking by a behavioral effect system for lock handling” (as tech reports), or “Deadlock Checking by Data Race Detection”. We’re certainly not the first or the only ones with such approaches; there’s lots of existing theory and academic or commercial tools.

Now, the challenge is to turn the theory a useable tool for Java (analysing synchronized blocks, or locking using java.util.concurrent) or for C-programs using the pthreads-API. Another alternative would be the Go language.

Problem setting

A prospective student would try to use an existing program analysis framework like Soot to

  • implement the analysis,
  • collect performance results on scalability,
  • run experiments on existing open-source software projects,
  • contribute to publications/conference submissions.