Emmanuel Sifakis

Parallel architectures such as multiprocessors have become ubiquitous. In order to exploit these architectures, programmers must write parallel programs with shared memory. This is notoriously a very difficult task, since the programmer must clearly identify all race conditions and synchronizations required. To deal with race conditions there are two widely used approaches, called pessimistic and optimistic concurrency. The latter is easier to program, but it needs either special hardware or a software implementation which might introduce a lot of overhead. The former needs more effort from the programmer since a miss-use can lead to deadlocks. Moreover, bad practices in concurrency programming can also introduce specific security flaws.

The aim of this thesis is to propose some concrete solutions to overcome these problems. In particular, it will consider the pessimistic concurrency approach and propose some automated techniques to reduce the programming effort. Moreover, it will investigate on a recent and important topic, the detection of concurrency vulnerabilities. This work will rely on combinations of several code analysis techniques like static analysis, runtime analysis, and runtime property enforcement.