# 关于Java Memory Model

## 1、背景

Java内存模型是由基本模型演化过来的，主要经历三个模型。

### 1.2、Happens-Before Memory Model

• 如果x和y在同一个线程，并且在program order下x在y之前，那么x happen-before y
• 一个volatile变量的写action happen-before后续对该变量的读action
• 如果x happen-before y，并且y happen-before z，那么x happen-before z
• ……

It should be noted that the presence of a happens-before relationship between two actions does not necessarily imply that they have to take place in that order in an implementation. If the reordering produces results consistent with a legal execution, it is not illegal.

• w happen-before r，并且不存在其他的写操作w’满足w happen-before w’并且w’ happen-before r
• w和r之间不存在happen-before关系

init:a = 0, b = 0

---------------|----------
1, r1 = a      | 3, r2 = b
2, b = 1       | 4, a = 2

hb(a  = 0, r1 = a)
hb(r1 = a, b  = 1)
hb(b  = 0, r2 = b)
hb(r2 = b, a  = 2)

(a) r1 = 0; r2 = 0
(b) r1 = 2; r2 = 0
(c) r1 = 0; r2 = 1
(d) r1 = 2; r2 = 1

init:a = 0, b = 0

---------------|----------
r1 = a         | r2 = b
if(r1 != 0)    | if(r2 != 0)
b = 1       |   a = 2

### 1.3、Java Memory Model

An action can occur earlier in an execution than it appears in program order. However, that write must have been able to occur in the execution without assuming that any additional reads see values via a data race.

hb(a = 0, r1 = a)
hb(b = 0, r1 = a)
hb(r1 = a, b = 1)

init:x = y = 0

---------------|----------
r3 = x         | r2 = y
if (r3 == 0)   | x = r2
x = 42       |
r1 = x         |
y = r1         |

output: r1 == r2 == r3 == 42

r3 = x  (0)
x  = 42
r1 = x  (42)
y  = r1 (42)	# to be committed
r2 = y  (0)
x  = r2

y  = r1 (42)    # committed
r3 = x  (0)
x  = 42
r1 = x  (42)
r2 = y  (0)     # to be committed 可以看见y = r1(42)
x  = r2

y  = r1 (42)
r2 = y  (42)    # committed
r3 = x  (0)
x  = 42
r1 = x  (42)
x  = r2 (42)    # to be committed

y  = r1 (42)
r2 = y  (42)
x  = r2         # committed
r3 = x  (0)     # to be committed， 可以看见x = r2(42)
x  = 42
r1 = x  (42)	# to be committed， 可以看见x = r2(42)

y  = r1 (42)
r2 = y  (42)
x  = r2 (42)
r3 = x  (42)     # committed
r1 = x  (42)	 # committed

## 2、Rules

5 $$W_i|C_{i-1}=W|C_{i-1}$$
6 For any read $$r\in A_i-C_{i-1}$$ we have $$W_i(r)\stackrel{hb_i}{\longrightarrow} r$$
7 For any read $$r\in C_i-C_{i-1}$$ we have $$W_i(r)\in C_{i-1}$$ and $$W(r)\in C_{i-1}$$

• $$W_i(r)\in C_{i-1}$$规定了rule 6中满足happen-before的写action必须已经提交过了。
• $$W(r)\in C_{i-1}$$规定了读action最终所看见的写action也必须已经提交过了，这里有两层意思：
第一、如果读action所看见的写action不变（即一直是当前这一步中所看见的满足happen-before关系的写action），那么这两个规则表达的是同一个意思，即该写action必须已经提交了。
第二、如果读action所看见写action会变，根据rule 5，当前所提交的写action在下一步可以改为看见满足data race的写action，但是该写action必须在上一步已经提交过了。

## 3、举例

init:x = y = 0

---------------|----------
r3 = x         | r2 = y
if (r3 == 0)   | x = r2
x = 42       |
r1 = x         |
y = r1         |

output: r1 == r2 == r3 == 42

Action    | Value | Commited In | Final Value In | index
----------|-------|-------------|----------------|-------
x  = 0    | 0     | C1          | E1             |   1
y  = 0    | 0     | C1          | E1             |   2
y  = 42   | 42    | C1          | E1             |   3
r2 = y    | 0     | C2          | E2             |   4
r2 = y    | 42    | C2          | E3             |   5
x  = r2   | 42    | C3          | E3             |   6
r3 = x    | 0     | C4          | E4             |   7
r3 = x    | 42    | C4          | E5             |   8
r1 = x    | 0     | C5          | E5             |   9
r1 = x    | 42    | C5          | E6             |   10


﻿