TSO: PF <= PX 증명 전략

[kyeongmincho]

• PF의 실행이 있을 때,
  • 메모리 리스트가 있고
  • 각 스레드별로 이벤트들이 순서대로 있다.
• 같은 결과를 내는 PX의 실행이 있고 /\ 그 실행은 PF의 이벤트들을 다음과 같이 정렬하면 된다:
  1. 해당 step 후 vwn의 상태에 따라 내림차순
  2. (vwn이 같다면) w/u가 r 보다 먼저
  3. (r-r 순서라면) 같은 스레드 내에선 앞에 r이 먼저

[kyeongmincho]

px semantics로 실행가능한지?

• W@n -> R@n인가? by w-r 정렬
• w@n -> w@n+1 인가? by vwn

[kyeongmincho]

구체적 증명

1. 정렬한 L이 있다.
2. i까지 실행했을 때 state~L[0..i]의 관계 ~이 있다.
3. i -> i+1 로 스탭이 가능하다.
4. empty state ~ 0
5. final state ~ n

PX

: promise free + write(pro+ful) 스탭으로 이루어져 있다
px<=ps 증명은 쉽다. 왜냐하면 write = pro+ful
pf <= px: read->read, fulfill -> write ...

~

• L은 이제 고정되었다면
• exist M,
  • PF 실행 메모리의 프리픽스
  • M의 모든 메시지는 L[0..i] 사이에서 fulfill 되어있다.
  • L[0..i] 사이에서 fulfill 된 모든 메세지는 M에 있다.
• 스레드는 i까지 있는 제일 큰 수에서의 state가 되어야 한다
  • for each tid,
    • L[0..i]에서 tid 실행한 개수 = j
    • eu[tid][j]가 그때의 state
  • 필요한 렘마
    • L이 (tid, 0), (tid, 1), (tid, 2) , ... 다 가지고 있고, 중복 없고, 빠지는 거 없다
    • 0 < 1 < 2 로 오더가 있다

[sunghwanl]

Proof structure

- simulation relation: "view exec" executed up to writing n-th message 
(eu denotes only local components, i.e., state and local)

PF exec
memory: [1, 2, ..., n, n+1, ... N]
eu1_1 ->* eu1_i1 ->* eu1_final
eu2_1 ->* eu2_i2 ->* eu2_final
...

View exec
memory: [1, 2, ..., n]
<eu1_1, eu2_1, ...> ->* <eu1_i1, eu2_i2, ...>

Invariant
eu1_i1.coh, eu1_i1.vrn, eu2_i2.coh, eu2_i2.vrn <= n
forall n < m <= N, exists t, m \in eut_it.promises


- step simulation (who writes n+1?)

exists t, 
  eut_it ->* eut_it' -write n+1-> eut_it'' ->* eut_final /\
  never read from nor write to m > n

[kyeongmincho]

0812 미팅

1. pf 실행이 있다면, 모든 promise를 마친 시점부터 실행이 끝날 때까지의 "스레드별 eu 리스트"가 반드시 존재한다. 이를 eutrs라 하자. (eu뿐만 아니라 event도 같이 담김)

• eutrs[tid][0] = after-p[tid]
• eutrs[tid][끝] = exec[tid]
• forall n < 끝, eutrs[tid][n] -step-> eutrs[tid][n+1]

2. eutrs를 이용하여 리스트를 만들 건데 이 리스트의 order 조건은 다음의 우선순위대로 한다.

• left.local.cohmax < right.local.cohmax
• left.event is kind of write, while right.event is not
• left's eutrs[tid] index < right's eutrs[tid] index

3. order를 이용하여 eutrs의 스탭을 linearize한 리스트 L of (tid, n)이 있다. 그러기 위해선 order는 acyclic해야 한다. ("2.의 세 조건이 전부 같을 리는 없다")

• (tid, n) := tid의 n번째 스탭

4. L을 이용하여 시뮬레이션 한다. (추후 구체화)