对 Java 内存模型的理解

Java 内存模型

Java内存模型规定了在多线程程序中，什么样的行为是允许出现的，什么样的行为是禁止出现的。这样说可能有点抽象，我们换一个角度。将程序行为抽象成读操作和写操作，每个线程有自己的局部变量，同时线程之间还存在共享变量。那么一个多线程程序执行结束后，所有变量会有一个最终值。Java内存模型来决定什么样的值合法，什么样的值不合法。

内存模型不能要求的太严格，这样会阻碍很多优化方法，降低程序执行的效率，但也不能要求的太松，因为这样会导致一些执行结果违反我们的直觉。例如指令间的重排序问题，如果线程内部的指令完全按照程序中指明的次序执行，并且每次执行一条指令，执行的结果立即生效，那么就会阻碍很多优化方法，但这样对程序员是有好处的，因为程序员很容易推断程序的执行结果，这样写出的程序就容易与自己的意图一致。这种内存模型被称为顺序一致性模型(Sequential Consistency)。反之，如果为了优化程序执行效率，重排序的可能性有很多，那么程序的效率是提高了，但对程序员来说，就很难推断程序的执行结果。这一类的内存模型被称为Relaxed Memory Model。

内存模型的验证论文阅读

动态验证

Hangal2004

• 论文名 Hangal S, Vahia D, Manovit C, et al. TSOtool: A program for verifying memory systems using the memory consistency model[C]//ACM SIGARCH Computer Architecture News. IEEE Computer Society, 2004, 32(2): 114.

• 主要内容

  • 实现工具TSOtool，用于检测多处理器的共享内存系统
  • 内存模型TSO
  • 随机生成包含data race的程序
  • 提出多项式时间算法，incomplete
  • 检测出商业系统中的设计错误
  • 根据内存模型定义一种次序关系，通过程序及结果构造有向图， 在图中找环
  • 时间复杂度：最坏O(n^5)

• 参考文献

  • 验证SC的复杂度, 将问题定义为VSC, VSC-read(map read to write), VSC-conflict(VSC-read + total order of write): Gibbons P B, Korach E. Testing shared memories[J]. SIAM Journal on Computing, 1997, 26(4): 1208-1244.

Manovit 2005

• 论文名 Manovit C, Hangal S. Efficient algorithms for verifying memory consistency[C]//Proceedings of the seventeenth annual ACM symposium on Parallelism in algorithms and architectures. ACM, 2005: 245-252.

• 主要内容　

  • 将vector clock引入TSOtool工具
  • 为VSC-conflict问题提出一个多项式算法
  • 为VSC-read提出多项式算法，快速，有效，但不完备
  • 时间复杂度：O(k*n^3)

• 参考文献

Manovit 2006

• 论文名 Manovit C, Hangal S. Completely verifying memory consistency of test program executions[C]//High-Performance Computer Architecture, 2006. The Twelfth International Symposium on. IEEE, 2006: 166-175.

• 主要内容

  • 在TSOtool中引入回溯，使验证TSO内存模型的算法完备
  • 时间复杂度: O(p*n^3)

• 参考文献

硬件内存模型论文阅读

引言

内存模型定义了内存操作的语义,提出内存模型的目的在于指明内存操作之间的次序有何限制.

内存模型并不直接指定内存操作的次序,它只提供一种行为描述,只要你的执行结果 与 按内存模型规定的次序执行结果 一致就行,并不要求具体实现一定按这个顺序.

Java 内存模型论文阅读

引言

Java 的内存模型最早出现在1995年，但是自1997年起，这一内存模型被发现了许多严重的错误和缺陷，它阻碍了很多优化措施，对程序的安全性也没有足够的保证。2001年JSR 133被确立下来，由William Pugh领导，专家组的成员包括了Adve，Doug Lea， William Pugh等。2004年，JSR 133最终版本发布。2005年，Manson Jeremy, William Pugh, 和 Sarita V. Adve 一同发表了论文 The Java memory model，描述了最新的Java内存模型，这一内存模型在Java 5.0中引入，一直沿用至今。此后，科学家们对Java内存模型进行了进一步的研究的探索，但大的改动并没有出现。

论文介绍

Pugh2000

• 论文名 Pugh W. The Java memory model is fatally flawed[J]. Concurrency - Practice and Experience, 2000, 12(6): 445-455.

• 主要内容 介绍了现有Java内存模型的不足之处： * 难以理解，不同的人有不同解读 * 禁止了很多编译器优化，大多数JVM实现都违反Java内存模型 * 一些常用编程范式违反Java内存模型 * 没有考虑到在共享内存，弱一致性内存模型下实现Java所带来的一些问题

• 参考文献

  • Gontmakher 1997: 证明了Java内存模型需要Coherence

Manson 2005

• 论文名 Manson J, Pugh W, Adve S V. The Java memory model[M]. ACM, 2005.

• 主要内容 JSR 133的成果，介绍了新的Java内存模型，由Java 5.0引入，沿用至今。 基本思想包括： * 对满足 Data Race Free 的程序保证顺序一致性(sequential consistency) * 对没有正确同步的程序，使用causality的概念加以限制，以保证程序的安全性 * 新的内存模型足够强，以保证安全性，又足够弱，以保证编译器可以使用足够的优化

• 参考文献

  • Lamport 1979: 提出 Sequential Consistency 概念
  • Relaxed models in academia and commercial hardware - Adve 1990 - Adve 1993 - Dubois 1986 - Gharachorloo 1990 - IBM 1983(System/370 Principles of Operation) - May 1994(The PowerPC Architecture) - Sites 1995(Alpha AXP Architecture Reference Manual) - Weaver 1994(The SPARC Architecture Manual)
  • SC for DRF - Adve 1990 - Adve 1993 - Gharachorloo 1990
  • Flaws in original Java Memory Model - Pugh 1999
  • Original Java Memory Model Research - Gosling 1996 - Kotrajaras 2001 - Saraswat 2004

Polyakov 2006

• 论文名 Polyakov S, Schuster A. Verification of the Java causality requirements [M]//Hardware and Software, Verification and Testing. Springer Berlin Heidelberg, 2006: 224-246.

• 主要内容 * 证明验证causality是NP-complete的 * 跟踪每个线程实际运行时 read 操作的顺序可以简化验证 * 对可简化的验证提出了多项式算法 * 不能简化的提出非多项式算法（仅用于短的测试序列） * 使用了Post-mortem的方法，实际运行一个多线程程序，在JVM或者定制过的JVM或者模拟器上运行程序，拿到trace，分析trace，以验证内存是否有问题 * 使用frontier graph验证

• 参考文献

  • Boehm 2005: 通过库实现多线程不能保证程序正确性
  • causal acyclicity 形式化定义(reach condition)： - Sufficient System Requirements for Supporting the PLpc Memory Model. 1993 - Specifying System Requirements for Memory Consistency Models. 1993
  • Gibbons 1993：使用frontier graph验证SC

Data Race Free 的前世今生

Data Race Free 是多线程程序是非常重要的概念，因为Java 和 C++的内存模型都是基于 Data Race Free 的，这篇文章将介绍这个概念的由来，另一篇文章《Data Race Free的理解》介绍它的主要思想。

事情要追溯到遥远的1979年， Lamport 在他的著名论文 How to make a multiprocessor computer that correctly executes multiprocess programs 中提出了今后在内存模型领域被广泛使用的概念 ：sequential consistency，即顺序一致性。这篇文章告诉我们，你要做一台多处理器的计算机，需要满足什么条件，才能保证程序的正确性。当然，这里的程序跑在不同处理器上，共享同一块内存。虽然现在不说多处理器了，都说多核，多线程，但是问题的本质是没有变的。就是多个执行单元一起完成一个任务，并且通过共享存储单元的方式通信，在这种情况下，底层的系统需要提供什么样的支持，才能保证计算的结果和程序员的预期是一样的。

对Data Race Free 的理解

Data Race Free 的动机

Data Race Free 是对多线程程序 同步程度 的一种描述，假如你的多线程程序的同步程度满足 DRF 的要求，那么，你的程序会有这样一个好处：

程序在弱一致性模型下执行，执行的结果与在SC模型下执行一样

这意味着，程序员在写程序时，可以按SC模型来推断程序的执行。而程序在底层运行时，可以享受弱一致性模型带来的种种优化措施。

Data Race Free 具体内容

DRF 要求多线程程序中不能有冲突的操作。

什么是冲突的操作呢？

冲突的操作是指：两个操作来自不同线程，操作同一地址，至少有一个是写操作。

如何让冲突的操作不冲突呢？

需要使用同步操作将冲突的操作隔离开。

为什么要用同步操作将冲突的操作隔离开呢?