Formal Specification of LinkedBlockingQueue Using Concurrent Separation Logic

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 Link-edBlockingQueue 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 in-troduce some additional language constructs in order to be able to specify LinkedBlockingQueue’s safety proper-ties. 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. 1