Jeroen Meijer - Formal Specification of LinkedBlockingQueue Using Concurrent Separation Logic

author:Jeroen Meijer
title:Formal Specification of LinkedBlockingQueue Using Concurrent Separation Logic
committee:prof.dr. M. Huisman
graduation date:June 2011 (mark: 9)


Proving the correctness of multi-threaded programs is a challenge. To meet this challenge Hurlin recently designed a method based on separation logic to specify concurrent Java-like programs with fork, join and re-entrant locks. In this study we evaluate the usability of Hurlin’s method. This is done by developing a formal specification for Java’s library class LinkedBlockingQueue and arguing why LinkedBlockingQueue respects this specification. In our project we also inspect the Java Synchronizer Framework. We conclude that Hurlin’s program logic is very useful for specifying a Java library class, however we need to introduce some additional language constructs in order to be able to specify LinkedBlockingQueue’s safety properties. We are able to specify if threads have permission to change the head and tail of the queue. To be able to specify the blocking properties of LinkedBlockingQueue we need to introduce a new specification formula spec lock to specify which Lock protects a ConditionObject in Java’s Synchronizer Framework.