0.什么是Java内存模型：这篇文章讨论什么不讨论什么
内存模型规定了在给定程序的条件下，某个特定的程序执行过程是否合法。内存模型只是Java运行环境与上层Java程序员之间关于内存操作语义的约定，并不规定Java内存管理的具体实现。这篇文章也只是试图用易于理解的方式描述这种约定，而不会讨论内存模型约束下内存管理机制的具体实现。
1. 定义几个基本概念
1.1 共享变量：
存储在堆内存中可以被跨线程访问的变量，包括：实例属性、类属性和数组元素。
1.2 跨线程操作
下面罗列Java内存模型所定义的所有跨线程操作：
- 读非volatile共享变量
- 写非volatile共享变量
- Synchronization actions, which are: [list]
- Volatile read. A volatile read of a variable.
- Volatile write. A volatile write of a variable.
- Lock. Locking a monitor
- Unlock. Unlocking a monitor.
- The (synthetic) first and last action of a thread.
- Actions that start a thread or detect that a thread has terminated
[/list]
线程模型只关心跨线程操作，线程内操作的对象（局部变量）与跨线程操作的对象没有交集，所以可以毫无影响的被排除在讨论范围之外。
形式化的定义一个跨线程操作为一个四元组：< t, k, v, u >,其中:
- t:执行该跨线程操作的线程
- k:跨线程操作的类型
- v:跨线程操作的对象是哪个共享变量/monitor
- u:该跨线程操作的唯一标识
2. 夹逼Java内存模型
2.1 编程顺序
首先定义线程内语义和跨线程语义（内存模型）：
每个线程在执行过程中，除非遇到跨线程操作，程序的语义由标准的单线程程序执行语义决定。一旦遇到跨线程操作，跨线程操作的语义由内存模型决定。
具体的讲即：如果线程在执行过程中遇到一个跨线程读操作，该读操作的语义由内存模型决定，并且此后线程执行过程中所读取的值都和该跨线程读操作所读到的值相等。于是编程顺序的定义为：某一线程在执行过程中，可能会发起一系列的跨线程操作。这些跨线程操作，在受到线程内语义的约束下的实际执行顺序，被称作编程顺序。
2.2 Sequentially Consistent
A set of actions is sequentially consistent if all actions occur in a total order (the execution order) that is consistent with program order, and furthermore, each read r of a variable v sees the value written by the write w to v such that:
w comes before r in the execution order, and
there is no other write w' such that w comes before w' and w' comes before r in the execution order.
2.3 Synchronization Order
Synchronization actions induce the synchronized-with relation on actions, defined as follows:
An unlock action on monitor m synchronizes-with all subsequent lock actions on m (where "subsequent" is defined according to the synchronization order).
A write to a volatile variable v (§8.3.1.4) synchronizes-with all subsequent reads of v by any thread (where "subsequent" is defined according to the synchronization order).
An action that starts a thread synchronizes-with the first action in the thread it starts.
The write of the default value (zero, false, or null) to each variable synchronizes-with the first action in every thread.
Although it may seem a little strange to write a default value to a variable before the object containing the variable is allocated, conceptually every object is created at the start of the program with its default initialized values.
The final action in a thread T1 synchronizes-with any action in another thread T2 that detects that T1 has terminated.
T2 may accomplish this by calling T1.isAlive() or T1.join().
If thread T1 interrupts thread T2, the interrupt by T1 synchronizes-with any point where any other thread (including T2) determines that T2 has been interrupted (by having an InterruptedException thrown or by invoking Thread.interrupted or Thread.isInterrupted).
The source of a synchronizes-with edge is called a release, and the destination is called an acquire.
2.4 Happens-before Order
第一种，同一个线程内,如果有两个跨线程操作x和y，按照编程顺序，x在y之前执行，那么称x和y之前存在Happens-before关系，记作：x -hb-> y。
第二种，同步跨线程操作之间存在事先定义的Happens-before关系
第三种，There is a happens-before edge from the end of a constructor of an object to the start of a finalizer (§12.6) for that object.
第四种，传递的，如果满足x -hb-> y，并且y -hb-> z，那么必有：x -hb-> z。
Happens-before关系是多个程序操作之间的一种特殊关系，若 x -hb-> y，并不意味着，物理的x一定在y之前执行。
准确而言，x -hb-> y只保证在逻辑上，对于任意的两个观察操作o1和o2，当满足o1 -hb-> o2时，
o1和o2观察到的执行顺序是x在y之前执行。
2.5 Happens-before Consistency
We say that a read r of a variable v is allowed to observe a write w to v if, in the happens-before partial order of the execution trace:
r is not ordered before w (i.e., it is not the case that hb(r, w)), and
there is no intervening write w' to v (i.e. no write w' to v such that hb(w, w') and hb(w', r)).
Informally, a read r is allowed to see the result of a write w if there is no happens-before ordering to prevent that read.
A set of actions A is happens-before consistent if for all reads r in A, where W(r) is the write action seen by r, it is not the case that either hb(r, W(r)) or that there exists a write w in A such that w.v = r.v and hb(W(r), w) and hb(w, r).
In a happens-before consistent set of actions, each read sees a write that it is allowed to see by the happens-before ordering.
2.6 Happens-before Consistency is too waek and causality
Example 17.4.8-1.
We refer to the issue of when reads can see future writes as causality, because of issues that arise in cases like the one found in Table 17.6. In that case, the reads cause the writes to occur, and the writes cause the reads to occur. There is no "first cause" for the actions. Our memory model therefore needs a consistent way of determining which reads can see writes early.
3. Java内存模型
3.1 Executions
An execution E is described by a tuple < P, A, po, so, W, V, sw, hb >, comprising:
P - a program
A - a set of actions
po - program order, which for each thread t, is a total order over all actions performed by t in A
so - synchronization order, which is a total order over all synchronization actions in A
W - a write-seen function, which for each read r in A, gives W(r), the write action seen by r in E.
V - a value-written function, which for each write w in A, gives V(w), the value written by w in E.
sw - synchronizes-with, a partial order over synchronization actions
hb - happens-before, a partial order over actions
Note that the synchronizes-with and happens-before elements are uniquely determined by the other components of an execution and the rules for well-formed executions
3.2 Well-Formed Executions（满足Happens-before的Execution）
17.4.7.
3.3 Causality约束
A well-formed execution E = < P, A, po, so, W, V, sw, hb > is validated by committing actions from A. If all of the actions in A can be committed, then the execution satisfies the causality requirements of the Java programming language memory model.
先定义一组累进Action序列：
Starting with the empty set as C0, we perform a sequence of steps where we take actions from the set of actions A and add them to a set of committed actions Ci to get a new set of committed actions Ci+1. To demonstrate that this is reasonable, for each Ci we need to demonstrate an execution E containing Ci that meets certain conditions.
Formally, an execution E satisfies the causality requirements of the Java programming language memory model if and only if there exist:
Sets of actions C0, C1, ... such that:
C0 is the empty set
Ci is a proper subset of Ci+1
A = ∪ (C0, C1, ...)
（If A is finite, then the sequence C0, C1, ... will be finite, ending in a set Cn = A.
If A is infinite, then the sequence C0, C1, ... may be infinite, and it must be the case that the union of all elements of this infinite sequence is equal to A.
）
Well-formed executions E1, ..., where Ei = < P, Ai, poi, soi, Wi, Vi, swi, hbi >.
Given these sets of actions C0, ... and executions E1, ... , every action in Ci must be one of the actions in Ei. All actions in Ci must share the same relative happens-before order and synchronization order in both Ei and E. Formally:
1. Ci is a subset of Ai
2. hbi|Ci = hb|Ci
3. soi|Ci = so|Ci
The values written by the writes in Ci must be the same in both Ei and E. Only the reads in Ci-1 need to see the same writes in Ei as in E. Formally:
4. Vi|Ci = V|Ci
5. Wi|Ci-1 = W|Ci-1
All reads in Ei that are not in Ci-1 must see writes that happen-before them. Each read r in Ci - Ci-1 must see writes in Ci-1 in both Ei and E, but may see a different write in Ei from the one it sees in E. Formally:
//All reads in Ei that are not in Ci-1 must see writes that happen-before them.
//在某个E中进行的读操作，若要看到本次E中进行的写操作，则写与读之间必须满足hb关系
6. For any read r in Ai - Ci-1, we have hbi(Wi(r), r)
//只能看到在之前的E中执行，并前已经flush到C中（即出现在ci-1中）的写操作
7. For any read r in (Ci - Ci-1), we have Wi(r) in Ci-1 and W(r) in Ci-1
Given a set of sufficient synchronizes-with edges for Ei, if there is a release-acquire pair that happens-before (§17.4.5) an action you are committing, then that pair must be present in all Ej, where j ≥ i. Formally:
8. Let sswi be the swi edges that are also in the transitive reduction of hbi but not in po. We call sswi the sufficient synchronizes-with edges for Ei. If sswi(x, y) and hbi(y, z) and z in Ci, then swj(x, y) for all j ≥ i.
If an action y is committed, all external actions that happen-before y are also committed.
9. If y is in Ci, x is an external action and hbi(x, y), then x in Ci.