Reasoning about Java's Reentrant Locks

C. Haack, Marieke Huisman, C. Hurlin

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

    28 Citations (Scopus)

    Abstract

    This paper presents a verification technique for a concurrent Java-like language with reentrant locks. The verification technique is based on permission-accounting separation logic. As usual, each lock is associated with a resource invariant, i.e. when acquiring the lock the resources are obtained by the thread holding the lock, and when releasing the lock, the resources are released. To accommodate for reentrancy, the notion of lockset is introduced: a multiset of locks held by a thread. Keeping track of the lockset enables the logic to ensure that resources are not re-acquired upon reentrancy, thus avoiding the introduction of new resources in the system. To be able to express flexible locking policies, we combine the verification logic with value-parametrized classes. Verified programs satisfy the following properties: data race freedom, absence of null-dereferencing and partial correctness. The verification technique is illustrated on several examples, including a challenging lock-coupling algorithm.
    Original languageUndefined
    Title of host publicationThe Sixth ASIAN Symposium on Programming Languages and Systems
    EditorsG. Ramalingam
    Place of PublicationLondon
    PublisherSpringer
    Pages171-187
    Number of pages17
    ISBN (Print)978-3-540-89329-5
    DOIs
    Publication statusPublished - 1 Sep 2008
    EventThe Sixth ASIAN Symposium on Programming Languages and Systems - Bangalore, India
    Duration: 9 Dec 200811 Dec 2008

    Publication series

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

    Conference

    ConferenceThe Sixth ASIAN Symposium on Programming Languages and Systems
    Period9/12/0811/12/08
    Other9-11 Dec 2008

    Keywords

    • Multithreading
    • Program Verification
    • Reentrant Locks
    • METIS-256136
    • EWI-14818
    • IR-62675
    • Java

    Cite this