A History of BlockingQueues
Marina Zaharieva-Stojanovski, Marieke Huisman, Stefan Blom

TL;DR
This paper introduces a formal, history-based specification method for concurrent data structures, demonstrated on Java's BlockingQueue, enhancing modularity and correctness verification.
Contribution
It proposes a novel history-based specification approach using JML and separation logic, improving the stability and modularity of concurrent data structure specifications.
Findings
Successfully specified BlockingQueue behaviour
Ensured correct inheritance of specifications
Applicable to other concurrent data structures
Abstract
This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object's state, we specify it in terms of the object's state history. A history is defined as a list of state updates, which at all points can be related to the actual object's state. We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
