Permission-Based Separation Logic for Multithreaded Java Programs

Christian Haack, Marieke Huisman, C. Hurlin

Research output: Contribution to journalArticleAcademic

28 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

@article{a42c218cb9a54b39b7609a428a740b7e,
title = "Permission-Based Separation Logic for Multithreaded Java Programs",
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).",
keywords = "EWI-19741, IR-76303, METIS-277570",
author = "Christian Haack and Marieke Huisman and C. Hurlin",
year = "2011",
language = "Undefined",
volume = "15",
pages = "13--23",
journal = "Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica",

}

Permission-Based Separation Logic for Multithreaded Java Programs. / Haack, Christian; Huisman, Marieke; Hurlin, C.

In: Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica, Vol. 15, 2011, p. 13-23.

Research output: Contribution to journalArticleAcademic

TY - JOUR

T1 - Permission-Based Separation Logic for Multithreaded Java Programs

AU - Haack, Christian

AU - Huisman, Marieke

AU - Hurlin, C.

PY - 2011

Y1 - 2011

N2 - 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).

AB - 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).

KW - EWI-19741

KW - IR-76303

KW - METIS-277570

M3 - Article

VL - 15

SP - 13

EP - 23

JO - Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica

JF - Nieuwsbrief van de Nederlandse Vereniging voor Theoretische Informatica

ER -