Back to University of Twente portal
| author: | Jeroen Meijer |
| title: | Formal Specification of LinkedBlockingQueue Using Concurrent Separation Logic |
| keywords: | |
| topics: | |
| committee: | Marieke Huisman |
| started: | February 2011 |
| end: | June 2011 |
Abstract
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.