Permission-based separation logic for multi-threaded Java programs

A. Amighi, Christian Haack, Marieke Huisman, C. Hurlin

    Research output: Contribution to journalArticleAcademicpeer-review

    13 Citations (Scopus)
    89 Downloads (Pure)

    Abstract

    This paper presents a program logic for reasoning about multithreaded Java-like programs with concurrency primitives such as dynamic thread creation, thread joining and reentrant object monitors. The logic is based on concurrent separation logic. It is the first detailed adaptation of concurrent separation logic to a multithreaded Java-like language. The program logic associates a unique static access permission with each heap location, ensuring exclusive write accesses and ruling out data races. Concurrent reads are supported through fractional permissions. Permissions can be transferred between threads upon thread starting, thread joining, initial monitor entrancies and final monitor exits. In order to distinguish between initial monitor entrancies and monitor reentrancies, auxiliary variables keep track of multisets of currently held monitors. Data abstraction and behavioral subtyping are facilitated through abstract predicates, which are also used to represent monitor invariants, preconditions for thread starting and postconditions for thread joining. Value-parametrized types allow to conveniently capture common strong global invariants, like static object ownership relations. The program logic is presented for a model language with Java-like classes and interfaces, the soundness of the program logic is proven, and a number of illustrative examples are presented.
    Original languageUndefined
    Pages (from-to)2
    Number of pages65
    JournalLogical methods in computer science
    Volume11
    Issue number1
    DOIs
    Publication statusPublished - Feb 2015

    Keywords

    • EWI-25324
    • IR-94681
    • METIS-312455

    Cite this

    Amighi, A. ; Haack, Christian ; Huisman, Marieke ; Hurlin, C. / Permission-based separation logic for multi-threaded Java programs. In: Logical methods in computer science. 2015 ; Vol. 11, No. 1. pp. 2.
    @article{dc336077fa6e4e39acd242a53803f576,
    title = "Permission-based separation logic for multi-threaded Java programs",
    abstract = "This paper presents a program logic for reasoning about multithreaded Java-like programs with concurrency primitives such as dynamic thread creation, thread joining and reentrant object monitors. The logic is based on concurrent separation logic. It is the first detailed adaptation of concurrent separation logic to a multithreaded Java-like language. The program logic associates a unique static access permission with each heap location, ensuring exclusive write accesses and ruling out data races. Concurrent reads are supported through fractional permissions. Permissions can be transferred between threads upon thread starting, thread joining, initial monitor entrancies and final monitor exits. In order to distinguish between initial monitor entrancies and monitor reentrancies, auxiliary variables keep track of multisets of currently held monitors. Data abstraction and behavioral subtyping are facilitated through abstract predicates, which are also used to represent monitor invariants, preconditions for thread starting and postconditions for thread joining. Value-parametrized types allow to conveniently capture common strong global invariants, like static object ownership relations. The program logic is presented for a model language with Java-like classes and interfaces, the soundness of the program logic is proven, and a number of illustrative examples are presented.",
    keywords = "EWI-25324, IR-94681, METIS-312455",
    author = "A. Amighi and Christian Haack and Marieke Huisman and C. Hurlin",
    note = "eemcs-eprint-25324",
    year = "2015",
    month = "2",
    doi = "10.2168/LMCS-11(1:2)2015",
    language = "Undefined",
    volume = "11",
    pages = "2",
    journal = "Logical methods in computer science",
    issn = "1860-5974",
    publisher = "Technischen Universitat Braunschweig",
    number = "1",

    }

    Permission-based separation logic for multi-threaded Java programs. / Amighi, A.; Haack, Christian; Huisman, Marieke; Hurlin, C.

    In: Logical methods in computer science, Vol. 11, No. 1, 02.2015, p. 2.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Permission-based separation logic for multi-threaded Java programs

    AU - Amighi, A.

    AU - Haack, Christian

    AU - Huisman, Marieke

    AU - Hurlin, C.

    N1 - eemcs-eprint-25324

    PY - 2015/2

    Y1 - 2015/2

    N2 - This paper presents a program logic for reasoning about multithreaded Java-like programs with concurrency primitives such as dynamic thread creation, thread joining and reentrant object monitors. The logic is based on concurrent separation logic. It is the first detailed adaptation of concurrent separation logic to a multithreaded Java-like language. The program logic associates a unique static access permission with each heap location, ensuring exclusive write accesses and ruling out data races. Concurrent reads are supported through fractional permissions. Permissions can be transferred between threads upon thread starting, thread joining, initial monitor entrancies and final monitor exits. In order to distinguish between initial monitor entrancies and monitor reentrancies, auxiliary variables keep track of multisets of currently held monitors. Data abstraction and behavioral subtyping are facilitated through abstract predicates, which are also used to represent monitor invariants, preconditions for thread starting and postconditions for thread joining. Value-parametrized types allow to conveniently capture common strong global invariants, like static object ownership relations. The program logic is presented for a model language with Java-like classes and interfaces, the soundness of the program logic is proven, and a number of illustrative examples are presented.

    AB - This paper presents a program logic for reasoning about multithreaded Java-like programs with concurrency primitives such as dynamic thread creation, thread joining and reentrant object monitors. The logic is based on concurrent separation logic. It is the first detailed adaptation of concurrent separation logic to a multithreaded Java-like language. The program logic associates a unique static access permission with each heap location, ensuring exclusive write accesses and ruling out data races. Concurrent reads are supported through fractional permissions. Permissions can be transferred between threads upon thread starting, thread joining, initial monitor entrancies and final monitor exits. In order to distinguish between initial monitor entrancies and monitor reentrancies, auxiliary variables keep track of multisets of currently held monitors. Data abstraction and behavioral subtyping are facilitated through abstract predicates, which are also used to represent monitor invariants, preconditions for thread starting and postconditions for thread joining. Value-parametrized types allow to conveniently capture common strong global invariants, like static object ownership relations. The program logic is presented for a model language with Java-like classes and interfaces, the soundness of the program logic is proven, and a number of illustrative examples are presented.

    KW - EWI-25324

    KW - IR-94681

    KW - METIS-312455

    U2 - 10.2168/LMCS-11(1:2)2015

    DO - 10.2168/LMCS-11(1:2)2015

    M3 - Article

    VL - 11

    SP - 2

    JO - Logical methods in computer science

    JF - Logical methods in computer science

    SN - 1860-5974

    IS - 1

    ER -