Dec 01, 2010: Marieke Huisman: Verification of Concurrent Java Programs

December 01, 2010Verification of Concurrent Java Programs
Room: Zi 5126Marieke Huisman

Increasing performance demands, application complexity and explicit multi-core parallelism makes concurrency omnipresent in software applications. However, due to the complex interferences between threads in an application, concurrent software is also notoriously hard to get correct. Instead of spending large amounts of money to fix incorrect software, formal techniques are needed to reason about the behaviour of concurrent programs.
This talk describes how we developed a variant of permission-based separation logic that is particularly suited to reason about multithreaded Java programs with dynamic thread creation and termination, and reentrant locks. Non-trivial programming patterns (e.g. the iterator usage protocol, and lists with lock-coupling) can be verified with this logic.
In the last part of this talk, I will describe my ideas how this work will be continued within the ERC VerCors project. In particular, expressiveness of the logic will be extended, to specify and verify concurrent data structures. The verification logic will be parameterised over the locking policy, so that a high-level specification of the behaviour of a data structure can be reused for different implementations. The logic will also be parameterised with concurrency and synchronisation primitives, so that a logic for a different programming language can be defined as an instance of the general logic. Eventually, I hope to adapt the results, so that they can also be used in a distributed setting, where data consistency between the different sites has to be maintained.