• Verification of Causality Requ...

Treffer: Verification of Causality Requirements in Java Memory Model is Undecidable

Title:
Verification of Causality Requirements in Java Memory Model is Undecidable
Authors:
Matko Botinčan, Paola Glavan, Davor Runje
Contributors:
The Pennsylvania State University CiteSeerX Archives
Source:
http://web.math.hr/%7Emabotinc/downloads/ppam09.pdf.
Collection:
CiteSeerX
Subject Terms:
Java memory model, multithreading, verification
Document Type:
Fachzeitschrift text
File Description:
application/pdf
Language:
English
Relation:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.181.9; http://web.math.hr/%7Emabotinc/downloads/ppam09.pdf
Availability:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.181.9
http://web.math.hr/%7Emabotinc/downloads/ppam09.pdf
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.97818516
Database:
BASE

Weitere Informationen

The purpose of the Java memory model is to formalize the behavior of the shared memory in multithreaded Java programs. The subtlest points of its formalization are causality requirements that serve to provide safety and security guarantees for incorrectly synchronized Java programs. In this paper, we consider the problem of verifying whether an execution of a multithreaded Java program satisfies these causality requirements and show that this problem is undecidable.