A history of BlockingQueues

M. Zaharieva, Marieke Huisman, Stefan Blom

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

17 Downloads (Pure)

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 combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.
Original languageUndefined
Title of host publicationProceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012)
EditorsG.J. Pace, A.P. Ravn
Place of PublicationLondon
PublisherEPTCS
Pages31-35
Number of pages5
DOIs
Publication statusPublished - 19 Sep 2012

Publication series

NameElectronic Proceedings in Theoretical Computer Science
PublisherEPTCS
Volume94
ISSN (Print)2075-2180
ISSN (Electronic)2075-2180

Keywords

  • EWI-22671
  • METIS-296167
  • IR-83448
  • CR-D.2.4

Cite this

Zaharieva, M., Huisman, M., & Blom, S. (2012). A history of BlockingQueues. In G. J. Pace, & A. P. Ravn (Eds.), Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012) (pp. 31-35). (Electronic Proceedings in Theoretical Computer Science; Vol. 94). London: EPTCS. https://doi.org/10.4204/EPTCS.94.4
Zaharieva, M. ; Huisman, Marieke ; Blom, Stefan. / A history of BlockingQueues. Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012). editor / G.J. Pace ; A.P. Ravn. London : EPTCS, 2012. pp. 31-35 (Electronic Proceedings in Theoretical Computer Science).
@inproceedings{3ade4cea2cdb44ad927ba97aea3cbcb7,
title = "A history of BlockingQueues",
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 combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.",
keywords = "EWI-22671, METIS-296167, IR-83448, CR-D.2.4",
author = "M. Zaharieva and Marieke Huisman and Stefan Blom",
note = "10.4204/EPTCS.94.4",
year = "2012",
month = "9",
day = "19",
doi = "10.4204/EPTCS.94.4",
language = "Undefined",
series = "Electronic Proceedings in Theoretical Computer Science",
publisher = "EPTCS",
pages = "31--35",
editor = "G.J. Pace and A.P. Ravn",
booktitle = "Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012)",

}

Zaharieva, M, Huisman, M & Blom, S 2012, A history of BlockingQueues. in GJ Pace & AP Ravn (eds), Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012). Electronic Proceedings in Theoretical Computer Science, vol. 94, EPTCS, London, pp. 31-35. https://doi.org/10.4204/EPTCS.94.4

A history of BlockingQueues. / Zaharieva, M.; Huisman, Marieke; Blom, Stefan.

Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012). ed. / G.J. Pace; A.P. Ravn. London : EPTCS, 2012. p. 31-35 (Electronic Proceedings in Theoretical Computer Science; Vol. 94).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

TY - GEN

T1 - A history of BlockingQueues

AU - Zaharieva, M.

AU - Huisman, Marieke

AU - Blom, Stefan

N1 - 10.4204/EPTCS.94.4

PY - 2012/9/19

Y1 - 2012/9/19

N2 - 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 combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.

AB - 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 combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.

KW - EWI-22671

KW - METIS-296167

KW - IR-83448

KW - CR-D.2.4

U2 - 10.4204/EPTCS.94.4

DO - 10.4204/EPTCS.94.4

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 31

EP - 35

BT - Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012)

A2 - Pace, G.J.

A2 - Ravn, A.P.

PB - EPTCS

CY - London

ER -

Zaharieva M, Huisman M, Blom S. A history of BlockingQueues. In Pace GJ, Ravn AP, editors, Proceedings Sixth Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS 2012). London: EPTCS. 2012. p. 31-35. (Electronic Proceedings in Theoretical Computer Science). https://doi.org/10.4204/EPTCS.94.4