Permission-Based Separation Logic for Multithreaded Java Programs

Christian Haack, Marieke Huisman, Clément Hurlin

    Research output: Contribution to journalArticleAcademic

    98 Downloads (Pure)


    This paper motivates and 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. This paper presents the basic principles to reason about thread creation and thread joining. It finishes with an outlook how this logic will evolve into a full-fledged verification technique for Java (and possibly other multithreaded languages).
    Original languageEnglish
    Pages (from-to)13-23
    Number of pages11
    JournalNieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica
    Publication statusPublished - 2011


    Dive into the research topics of 'Permission-Based Separation Logic for Multithreaded Java Programs'. Together they form a unique fingerprint.

    Cite this