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 PMA, we have developed a basic theory about how to analyse such software (we're certainly not the first; there's lots of existing theory and even commercial tools). Now, the challenge is to turn this into 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.
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.
Some Related Publications
- "Refactoring and Active Object Languages", V. Stolz et al., 2020.
- "Shared Variables in Go: A semantic analysis of the Go memory model", S. Valle, Master thesis, 2016.
- "Operational Semantics of a Weak Memory Model with Channel Synchronization", Daniel Schnetzer Fava et al., 2018.
- "Automated Refactoring of Rust Programs", P.O. Ringdal, Master thesis, 2020.
- Ka I Pun, Martin Steffen, Volker Stolz:
Deadlock checking by a behavioral effect system for lock handling
. J. Log. Algebr. Program. 81(3): 331-354 (2012) - "Deadlock Checking by Data Race Detection", UIO Technical Report 421 (2012)