Verification of Shared-Reading Synchronisers

Afshin Amighi, Marieke Huisman, Stefan Blom

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

    71 Downloads (Pure)

    Abstract

    Synchronisation classes are an important building block for shared memory concurrent programs. Thus to reason about such programs, it is important to be able to verify the implementation of these synchronisation classes, considering atomic operations as the synchronisation primitives on which the implementations are built. For synchronisation classes controlling exclusive access to a shared resource, such as locks, a technique has been proposed to reason about their behaviour. This paper proposes a technique to verify implementations of both exclusive access and shared-reading synchronisers. We use permission-based Separation Logic to describe the behaviour of the main atomic operations and the basis for our technique is formed by a specification for class AtomicInteger, which is commonly used to implement synchronisation classes in Java.util.concurrent. To demonstrate the applicability of our approach, we mechanically verify the implementation of various synchronisation classes like Semaphore, CountDownLatch and Lock.

    Original languageEnglish
    Title of host publicationProceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid)
    EditorsSaddek Bensalem, Simon Bliudze
    Pages107-120
    Number of pages14
    DOIs
    Publication statusPublished - 25 Jun 2018
    Event1st International Workshop on Methods and Tools for Rigorous System Design 2018 - Thessaloniki, Greece
    Duration: 15 Apr 201815 Apr 2018
    Conference number: 1
    https://project.inria.fr/metrid2018/programme/

    Publication series

    NameElectronic Proceedings in Theoretical Computer Science, EPTCS
    Volume272
    ISSN (Print)2075-2180

    Workshop

    Workshop1st International Workshop on Methods and Tools for Rigorous System Design 2018
    Abbreviated titleMeTRiD 2018
    CountryGreece
    CityThessaloniki
    Period15/04/1815/04/18
    Internet address

    Fingerprint Dive into the research topics of 'Verification of Shared-Reading Synchronisers'. Together they form a unique fingerprint.

  • Cite this

    Amighi, A., Huisman, M., & Blom, S. (2018). Verification of Shared-Reading Synchronisers. In S. Bensalem, & S. Bliudze (Eds.), Proceedings of the 1st International Workshop on Methods and Tools for Rigorous System Design (Metrid) (pp. 107-120). (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 272). https://doi.org/10.4204/EPTCS.272.9