Resource Protection Using Atomics: Patterns and Verification

A. Amighi, Stefan Blom, Marieke Huisman

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

    4 Citations (Scopus)
    19 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