|title:||Encoding Deadlock-Free Monitors in the VerCors Verification Tool|
|topics:||Logics and semantics|
When reasoning about concurrent programs, one important property is the absence of deadlocks. For locks, it is well-understood how to achieve this, by imposing an order on the locks. However, for monitors (i.e. the wait and notify constructs) it is less clear how this can be achieved.
Jafar Hamin and Bart Jacobs have proposed a technique to prove the absence of deadlocks for programs using monitors. Their technique uses the notion of obligations: a thread has an obligation if it still has to notify a waiting thread, and a program is only correct if all obligations are fulfilled. Their verification technique is encoded in the VeriFast program verifier. In this project, you are asked to investigate how to encode their verification technique for the VerCors program verifier, which is being developed in the FMT group.
The project would consist of the following steps:
- understand the technique as proposed by Hamin and Jacobs
- investigate how to encode this in the VerCors verifier
- implement the encoding
- validate the encoding on several examples
- Final paper (Digital version available here)