Verification of Causality Requirements in Java Memory Model Is Undecidable
Verification of Causality Requirements in Java Memory Model Is Undecidable
复制标题
Java 内存模型中因果关系要求的验证是不可判定的
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
D. Runje
中科院分区：
文献类型：
--
作者：
M. Botincan;Paola Glavan;D. Runje
Java内存模型的目的是形式化共享的MultithReaded Java程序的行为。其形式化的最微妙之处是因果关系要求，可为错误同步的Java计划提供安全保证。在本文中，我们考虑了验证amultithreaded Java程序的执行是否满足这些因果关系要求的问题，并表明此问题是不可确定的。
The purpose of the Java memory model is to formalize the behavior of the sharedmemory inmultithreaded 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 amultithreaded Java program satisfies these causality requirements and show that this problem is undecidable.