Resource Protection Using Atomics: Patterns and Verification

A. Amighi, Stefan Blom, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)
14 Downloads (Pure)

Abstract

For the verification of concurrent programs, it is essential to be able to show that synchronisation mechanisms are implemented correctly. A common way to implement such sychronisers is by using atomic operations. This paper identifies what different synchronisation patterns can be implemented by using atomic read, write and compare-and-set operation. Additionally, this paper proposes also a specification of these operations in Java’s AtomicInteger class, and shows how different synchronisation mechanisms can be built and verified using atomic integer as the synchronisation primitive. The specifications for the methods in the AtomicInteger class are derived from the classical concurrent separation logic rule for atomic operations. A main characteristic of our specification is its ease of use. To verify an implementation of a synchronisation mechanism, the user only has to specify (1) what are the different roles of the threads participating in the synchronisation, (2) what are the legal state transitions in the synchroniser, and (3) what share of the resource invariant can be obtained in a certain state, given the role of the current thread. The approach is illustrated on several synchronisation mechanisms. For all implementations, we provide a machine-checked proof that the implementations correctly implement the synchroniser.
Original languageUndefined
Title of host publicationProceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014
EditorsJacques Garrigue
Place of PublicationBerlin
PublisherSpringer
Pages255-274
Number of pages20
ISBN (Print)978-3-319-12735-4
DOIs
Publication statusPublished - Nov 2014

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume8858
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • EWI-25323
  • Permissions
  • atomics
  • Separation Logic
  • IR-94051
  • Verification
  • Specification
  • Concurrency
  • METIS-309668
  • Java volatiles

Cite this

Amighi, A., Blom, S., & Huisman, M. (2014). Resource Protection Using Atomics: Patterns and Verification. In J. Garrigue (Ed.), Proceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 (pp. 255-274). (Lecture Notes in Computer Science; Vol. 8858). Berlin: Springer. https://doi.org/10.1007/978-3-319-12736-1_14
Amighi, A. ; Blom, Stefan ; Huisman, Marieke. / Resource Protection Using Atomics: Patterns and Verification. Proceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014. editor / Jacques Garrigue. Berlin : Springer, 2014. pp. 255-274 (Lecture Notes in Computer Science).
@inproceedings{fb6681d7dc884d26a46463b257c33bcd,
title = "Resource Protection Using Atomics: Patterns and Verification",
abstract = "For the verification of concurrent programs, it is essential to be able to show that synchronisation mechanisms are implemented correctly. A common way to implement such sychronisers is by using atomic operations. This paper identifies what different synchronisation patterns can be implemented by using atomic read, write and compare-and-set operation. Additionally, this paper proposes also a specification of these operations in Java’s AtomicInteger class, and shows how different synchronisation mechanisms can be built and verified using atomic integer as the synchronisation primitive. The specifications for the methods in the AtomicInteger class are derived from the classical concurrent separation logic rule for atomic operations. A main characteristic of our specification is its ease of use. To verify an implementation of a synchronisation mechanism, the user only has to specify (1) what are the different roles of the threads participating in the synchronisation, (2) what are the legal state transitions in the synchroniser, and (3) what share of the resource invariant can be obtained in a certain state, given the role of the current thread. The approach is illustrated on several synchronisation mechanisms. For all implementations, we provide a machine-checked proof that the implementations correctly implement the synchroniser.",
keywords = "EWI-25323, Permissions, atomics, Separation Logic, IR-94051, Verification, Specification, Concurrency, METIS-309668, Java volatiles",
author = "A. Amighi and Stefan Blom and Marieke Huisman",
note = "eemcs-eprint-25323",
year = "2014",
month = "11",
doi = "10.1007/978-3-319-12736-1_14",
language = "Undefined",
isbn = "978-3-319-12735-4",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "255--274",
editor = "Jacques Garrigue",
booktitle = "Proceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014",

}

Amighi, A, Blom, S & Huisman, M 2014, Resource Protection Using Atomics: Patterns and Verification. in J Garrigue (ed.), Proceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014. Lecture Notes in Computer Science, vol. 8858, Springer, Berlin, pp. 255-274. https://doi.org/10.1007/978-3-319-12736-1_14

Resource Protection Using Atomics: Patterns and Verification. / Amighi, A.; Blom, Stefan; Huisman, Marieke.

Proceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014. ed. / Jacques Garrigue. Berlin : Springer, 2014. p. 255-274 (Lecture Notes in Computer Science; Vol. 8858).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Resource Protection Using Atomics: Patterns and Verification

AU - Amighi, A.

AU - Blom, Stefan

AU - Huisman, Marieke

N1 - eemcs-eprint-25323

PY - 2014/11

Y1 - 2014/11

N2 - For the verification of concurrent programs, it is essential to be able to show that synchronisation mechanisms are implemented correctly. A common way to implement such sychronisers is by using atomic operations. This paper identifies what different synchronisation patterns can be implemented by using atomic read, write and compare-and-set operation. Additionally, this paper proposes also a specification of these operations in Java’s AtomicInteger class, and shows how different synchronisation mechanisms can be built and verified using atomic integer as the synchronisation primitive. The specifications for the methods in the AtomicInteger class are derived from the classical concurrent separation logic rule for atomic operations. A main characteristic of our specification is its ease of use. To verify an implementation of a synchronisation mechanism, the user only has to specify (1) what are the different roles of the threads participating in the synchronisation, (2) what are the legal state transitions in the synchroniser, and (3) what share of the resource invariant can be obtained in a certain state, given the role of the current thread. The approach is illustrated on several synchronisation mechanisms. For all implementations, we provide a machine-checked proof that the implementations correctly implement the synchroniser.

AB - For the verification of concurrent programs, it is essential to be able to show that synchronisation mechanisms are implemented correctly. A common way to implement such sychronisers is by using atomic operations. This paper identifies what different synchronisation patterns can be implemented by using atomic read, write and compare-and-set operation. Additionally, this paper proposes also a specification of these operations in Java’s AtomicInteger class, and shows how different synchronisation mechanisms can be built and verified using atomic integer as the synchronisation primitive. The specifications for the methods in the AtomicInteger class are derived from the classical concurrent separation logic rule for atomic operations. A main characteristic of our specification is its ease of use. To verify an implementation of a synchronisation mechanism, the user only has to specify (1) what are the different roles of the threads participating in the synchronisation, (2) what are the legal state transitions in the synchroniser, and (3) what share of the resource invariant can be obtained in a certain state, given the role of the current thread. The approach is illustrated on several synchronisation mechanisms. For all implementations, we provide a machine-checked proof that the implementations correctly implement the synchroniser.

KW - EWI-25323

KW - Permissions

KW - atomics

KW - Separation Logic

KW - IR-94051

KW - Verification

KW - Specification

KW - Concurrency

KW - METIS-309668

KW - Java volatiles

U2 - 10.1007/978-3-319-12736-1_14

DO - 10.1007/978-3-319-12736-1_14

M3 - Conference contribution

SN - 978-3-319-12735-4

T3 - Lecture Notes in Computer Science

SP - 255

EP - 274

BT - Proceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014

A2 - Garrigue, Jacques

PB - Springer

CY - Berlin

ER -

Amighi A, Blom S, Huisman M. Resource Protection Using Atomics: Patterns and Verification. In Garrigue J, editor, Proceedings of the 12th Asian Symposium on Programming Languages and Systems, APLAS 2014. Berlin: Springer. 2014. p. 255-274. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-12736-1_14