Making the Java Memory Model Safe
Making the Java Memory Model Safe
复制标题
DOI：
10.1145/2518191
复制
发表时间：
2013-12-01
影响因子：
1.3
通讯作者：
Lochbihler, Andreas
中科院分区：
文献类型：
--
作者：
Lochbihler, Andreas
这项工作提出了一个机器检查的形式化的Java内存模型，并将其连接到一个操作语义的Java和Java字节码。对于整个模型，证明了数据竞争自由保证和类型安全。该模型通过动态内存分配、线程生成和连接、无限执行、等待通知机制和线程中断扩展了以前的形式化，所有这些都以微妙的方式与内存模型相互作用。正式化导致了对现有JMM规范的大量澄清和修复。
This work presents a machine-checked formalisation of the Java memory model and connects it to an operational semantics for Java and Java bytecode. For the whole model, I prove the data race freedom guarantee and type safety. The model extends previous formalisations by dynamic memory allocation, thread spawns and joins, infinite executions, the wait-notify mechanism, and thread interruption, all of which interact in subtle ways with the memory model. The formalisation resulted in numerous clarifications of and fixes to the existing JMM specification.