Permission-based separation logic for multithreaded Java programs

DOI10.2168/LMCS-11(1:2)2015MaRDI QIDQ5177333zbMATH OpenOpenAlexFDO

Authors Afshin Amighi, Christian Haack, Marieke Huisman, Clément Hurlin

Publication date 11 March 2015

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1411.0851

zbMATH Keywords

Javamultithreaded programsprogram verificationseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: This paper presents a program logic for reasoning about multithreaded Java-like programs with 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.

Recommendations

• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Fine-grained concurrency with separation logic
• Permission accounting in separation logic
• An assertion-based proof system for multithreaded Java
• A shared-variable concurrency analysis of multi-threaded object-oriented programs

Cited in

(4)

• Verification of concurrent systems with VerCors
• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Security monitor inlining and certification for multithreaded Java
• Dynamic separation logic

This page was built for publication: Permission-based separation logic for multithreaded Java programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5177333)