Resource protection using atomics: patterns and verifications

A. Amighi, Stefan Blom, Marieke Huisman

    Research output: Book/ReportReportProfessional

    38 Downloads (Pure)

    Abstract

    Modular reasoning about non-blocking concurrent data structures is crucial to establish the correctness of concurrent applications. To achieve this, specifications of the synchronization mechanisms used by these non-blocking concurrent classes to prevent concurrent access to shared data, are essential. This paper presents an approach to specifying such lock-free synchronization mechanisms in terms of the thread's role and permissions. The approach is formalized in a specification for the AtomicInteger class from the java.util.concurrent library, using abstract predicates and permission-based concurrent Separation Logic. The specification is set up to capture different synchronization patterns, both cooperative and competitive. We illustrate the use of the patterns in three case studies, where for each case study we verify that it indeed correctly synchronizes access to the protected data.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages14
    Publication statusPublished - 1 May 2013

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematica and Information Technology (CTIT)
    No.TR-CTIT-13-10
    ISSN (Print)1381-3625

    Keywords

    • Permissions
    • Separation Logic
    • Verification
    • Java volatiles
    • Specification
    • Concurrency
    • IR-85886
    • METIS-296412
    • EWI-23306
    • atomics

    Cite this

    Amighi, A., Blom, S., & Huisman, M. (2013). Resource protection using atomics: patterns and verifications. (CTIT Technical Report Series; No. TR-CTIT-13-10). Enschede: Centre for Telematics and Information Technology (CTIT).