Verifying Class Invariants in Concurrent Programs

M. Zaharieva, Marieke Huisman

    Research output: Book/ReportReportProfessional

    4 Citations (Scopus)
    138 Downloads (Pure)


    Class invariants are a highly useful feature for the verification of object-oriented programs, because they can be used to capture all valid object states. In a sequential program setting, the validity of class invariants is typically described in terms of a visible state semantics, i.e., invariants only have to hold whenever a method begins or ends execution, and they may be broken inside a method body. However, in a concurrent setting, this restriction is no longer usable, because due to thread interleavings, any program state is potentially a visible state. In this paper we present a new approach for reasoning about class invariants in multithreaded programs. We allow a thread to explicitly break an invariant at specific program locations, while ensuring that no other thread can observe the broken invariant. We develop our technique in a permission-based separation logic environment. However, we deviate from separation logic's standard rules and allow a class invariant to express properties over shared memory locations (the invariant footprint), independently of the permissions on these locations. In this way, a thread may break or reestablish an invariant without holding permissions to all locations in its footprint. To enable modular verification, we adopt the restrictions of Muller's ownership-based type system.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages20
    Publication statusPublished - 17 Jan 2014

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    ISSN (Print)1381-3625


    • METIS-304003
    • IR-89408
    • Class Invariants
    • Separation Logic
    • Permissions
    • EWI-24423
    • Verification

    Cite this