Permission-Based Separation Logic for Multithreaded Java Programs

Christian Haack, Marieke Huisman, C. Hurlin

    Research output: Contribution to journalArticleAcademic

    42 Downloads (Pure)

    Abstract

    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 languageUndefined
    Pages (from-to)13-23
    Number of pages11
    JournalNieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica
    Volume15
    Publication statusPublished - 2011

    Keywords

    • EWI-19741
    • IR-76303
    • METIS-277570

    Cite this