An Operational Framework for Specifying Memory Models using   Instantaneous Instruction Execution

Sizhuo Zhang; Muralidaran Vijayaraghavan; Arvind

arXiv:1705.06158·cs.PL·May 18, 2017

An Operational Framework for Specifying Memory Models using Instantaneous Instruction Execution

Sizhuo Zhang, Muralidaran Vijayaraghavan, Arvind

PDF

Open Access

TL;DR

This paper introduces the I2E framework, a simplified way to specify weak memory models that accurately captures modern microarchitectures without complex microarchitectural details.

Contribution

The I2E framework allows for straightforward specification of weak memory models using instantaneous instruction execution, simplifying reasoning and verification tasks.

Findings

01

I2E models capture behaviors of modern microarchitectures accurately.

02

The framework eliminates the need to consider microarchitectural complexities.

03

It uses non-deterministic data movement, invalidation buffers, and timestamps.

Abstract

There has been great progress recently in formally specifying the memory model of microprocessors like ARM and POWER. These specifications are, however, too complicated for reasoning about program behaviors, verifying compilers etc., because they involve microarchitectural details like the reorder buffer (ROB), partial and speculative execution, instruction replay on speculation failure, etc. In this paper we present a new Instantaneous Instruction Execution (I2E) framework which allows us to specify weak memory models in the same style as SC and TSO. Each instruction in I2E is executed instantaneously and in-order such that the state of the processor is always correct. The effect of instruction reordering is captured by the way data is moved between the processors and the memory non-deterministically, using three conceptual devices: invalidation buffers, timestamps and dynamic store…

Figures5

Click any figure to enlarge with its caption.

Tables1

Table 1. Table 1: Methods for r o b 𝑟 𝑜 𝑏 rob

$𝖾𝗇𝗊 (e n)$ : enqueues a new entry $e n$ into $r o b$ .
$𝗀𝖾𝗍𝖱𝖾𝖺𝖽𝗒 ()$ : finds an entry for which all source register values are ready, and returns the $⟨ index, entry ⟩$ pair of it.
$𝗀𝖾𝗍𝖫𝖽 ()$ : finds any entry containing a $𝖫𝖽$ instruction, and returns the $⟨ index, entry ⟩$ pair of it.
$𝗀𝖾𝗍𝖢𝗈𝗆𝗆𝗂𝗍 ()$ : returns the commit slot of $r o b$ .
$𝖽𝖾𝗊 ()$ : deletes the entry, which is the commit slot, from $r o b$ .
$𝖼𝗈𝗆𝗉𝗎𝗍𝖾𝖭𝗆 (i d x)$ : computes the result of the $𝖭𝗆$ instruction at $i d x$ using values in $r f$ and $r o b$ , and returns $⟨$ next PC, computed $v a l$ field $⟩$ .
$𝖼𝗈𝗆𝗉𝗎𝗍𝖾𝖠𝖽𝖽𝗋 (i d x)$ : computes and returns the address of the memory instruction at $i d x$ using values in $r f$ and $r o b$ .
$𝖼𝗈𝗆𝗉𝗎𝗍𝖾𝖲𝗍𝖣𝖺𝗍𝖺 (i d x)$ : computes and returns the store data of the $𝖲𝗍$ instruction at $i d x$ using values in $r f$ and $r o b$ .
$𝖿𝗅𝗎𝗌𝗁 (i d x, p c)$ : it deletes all entries in $r o b$ with indices $\geq i d x$ and updates $p c r$ to $p c$ . For every deleted $𝖫𝖽$ whose $e x$ field is $𝖤𝗑𝖾$ or $𝖱𝖾𝖤𝗑$ (i.e. the load is in memory), it sets the corresponding bit in $l f$ to $𝖳𝗋𝗎𝖾$ .
$𝖿𝗂𝗇𝖽𝖡𝗒𝗉𝖺𝗌𝗌 (i d x, a)$ : it looks for the value for $𝖫𝖽 a$ at $i d x$ by searching older entries in the $r o b$ and then in $s b$ , and returns a $⟨ value, tag ⟩$ pair if it finds an executed store to address $a$ . If the search finds nothing, then a $⊤$ is returned so that the load can be issued to memory. The search is also terminated if a $𝖱𝖾𝖼𝗈𝗇𝖼𝗂𝗅𝖾$ fence is encountered and in that case $ϵ$ is returned to indicate that the load should be stalled.
$𝖿𝗂𝗇𝖽𝖠𝖿𝖿𝖾𝖼𝗍𝖾𝖽𝖫𝖽 (i d x, a)$ : this method is called when a store at $i d x$ resolves its address to $a$ . It identifies $𝖫𝖽 a$ instructions in $r o b$ affected by this store by searching for $𝖫𝖽 a$ instructions from $i d x + 1$ to the youngest entry. The search stops if another $𝖲𝗍 a$ is encountered. Since there can be several affected loads, it returns a list of their indices. If a load has not started execution yet (i.e. $e x$ field is $𝖨𝖽𝗅𝖾$ ), it will not be affected by $𝖲𝗍 a$ and thus will not be returned.
$𝖿𝗂𝗇𝖽𝖲𝗍𝖺𝗅𝖾𝖫𝖽 (i d x, a, t)$ : this method is called when a $𝖫𝖽 a$ at $i d x$ reads from a store with tag $t$ in memory. It identifies $𝖫𝖽 a$ instructions in $r o b$ which are younger than the load at $i d x$ but read values staler than the value of store $t$ . The method searches from $i d x + 1$ to the youngest entry for the first executed $𝖫𝖽 a$ instruction (i.e. $e x$ field is $𝖣𝗈𝗇𝖾$ ), which reads from a store with tag $t^{'} \neq t$ , and returns the index of that instruction in $r o b$ . The method returns $⊤$ if no such load is found or a $𝖲𝗍 a$ is encountered first.

Equations76

\frac{⟨ Ld , t ^{L} , a ⟩ = m r b [ i ] . any ( ) ; ⟨ v , t ^{S} ⟩ = m [ a ] ;}{m r b [ i ] . remove (⟨ Ld , t ^{L} , a ⟩) ; ooo [ i ] . respLd ( t ^{L} , v , t ^{S} ) ;}

\frac{⟨ Ld , t ^{L} , a ⟩ = m r b [ i ] . any ( ) ; ⟨ v , t ^{S} ⟩ = m [ a ] ;}{m r b [ i ] . remove (⟨ Ld , t ^{L} , a ⟩) ; ooo [ i ] . respLd ( t ^{L} , v , t ^{S} ) ;}

\frac{⟨ St , a , v , t ^{S} ⟩ = m r b [ i ] . any ( ) ;}{m r b [ i ] . remove (⟨ St , a , v , t ^{S} ⟩) ; m [ a ] : = ⟨ v , t ^{S} ⟩ ; ooo [ i ] . respSt ( a ) ;}

\frac{⟨ St , a , v , t ^{S} ⟩ = m r b [ i ] . any ( ) ;}{m r b [ i ] . remove (⟨ St , a , v , t ^{S} ⟩) ; m [ a ] : = ⟨ v , t ^{S} ⟩ ; ooo [ i ] . respSt ( a ) ;}

\frac{predicates on the current state}{the action on the current state}

\frac{predicates on the current state}{the action on the current state}

\frac{in s = fetch ( p cr ) ; n p c = b p . predict ( in s ) ;}{r o b . enq (⟨ p cr , n p c , in s , initEx ( in s )⟩) ; p cr : = n p c ;}

\frac{in s = fetch ( p cr ) ; n p c = b p . predict ( in s ) ;}{r o b . enq (⟨ p cr , n p c , in s , initEx ( in s )⟩) ; p cr : = n p c ;}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Nm},op,srcs,dst,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ \langle nextpc,val\rangle=rob.\mathsf{computeNm}(idx);\end{array}}{\begin{array}[]{c}rob[idx]\mathsf{\ \coloneqq\ }\langle pc,nextpc,\langle\mathsf{Nm},op,srcs,dst,val\rangle,\mathsf{Done}\rangle;\\ \mathbf{if}\ nextpc\neq npc\ \mathbf{then}\ rob.\mathsf{flush}(idx+1,nextpc);\\ \end{array}}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Nm},op,srcs,dst,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ \langle nextpc,val\rangle=rob.\mathsf{computeNm}(idx);\end{array}}{\begin{array}[]{c}rob[idx]\mathsf{\ \coloneqq\ }\langle pc,nextpc,\langle\mathsf{Nm},op,srcs,dst,val\rangle,\mathsf{Done}\rangle;\\ \mathbf{if}\ nextpc\neq npc\ \mathbf{then}\ rob.\mathsf{flush}(idx+1,nextpc);\\ \end{array}}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,\epsilon,v,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ a=rob.\mathsf{computeAddr}(idx);\end{array}}{rob[idx].ins\mathsf{\ \coloneqq\ }\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle;}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,\epsilon,v,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ a=rob.\mathsf{computeAddr}(idx);\end{array}}{rob[idx].ins\mathsf{\ \coloneqq\ }\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle;}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,\epsilon,\epsilon\rangle,ex\rangle\rangle=rob.\mathsf{getLd}();\\ v=vp.\mathsf{predict}(\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,\epsilon,\epsilon\rangle,ex\rangle);\\ \end{array}}{rob[idx].ins\mathsf{\ \coloneqq\ }\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle;}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,\epsilon,\epsilon\rangle,ex\rangle\rangle=rob.\mathsf{getLd}();\\ v=vp.\mathsf{predict}(\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,\epsilon,\epsilon\rangle,ex\rangle);\\ \end{array}}{rob[idx].ins\mathsf{\ \coloneqq\ }\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle;}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ \langle res,t\rangle=rob.\mathsf{findBypass}(idx,a);\\ \mathsf{when}(a\neq\epsilon\ \wedge\ res\neq\epsilon\ \wedge\ res\neq\top);\\ \end{array}}{\begin{array}[]{c}\qquad rob[idx]\mathsf{\ \coloneqq\ }\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,res,t\rangle,\mathsf{Done}\rangle;\\ \qquad\mathbf{if}\ v\neq\epsilon\ \wedge\ v\neq res\ \mathbf{then}\ rob.\mathsf{flush}(idx+1,npc);\\ \end{array}}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ \langle res,t\rangle=rob.\mathsf{findBypass}(idx,a);\\ \mathsf{when}(a\neq\epsilon\ \wedge\ res\neq\epsilon\ \wedge\ res\neq\top);\\ \end{array}}{\begin{array}[]{c}\qquad rob[idx]\mathsf{\ \coloneqq\ }\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,res,t\rangle,\mathsf{Done}\rangle;\\ \qquad\mathbf{if}\ v\neq\epsilon\ \wedge\ v\neq res\ \mathbf{then}\ rob.\mathsf{flush}(idx+1,npc);\\ \end{array}}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ res=rob.\mathsf{findBypass}(idx,a);\\ \mathsf{when}(a\neq\epsilon\ \wedge\ res==\top\ \wedge\ \neg l\!f[idx]);\\ \end{array}}{\begin{array}[]{c}ccm.\mathsf{reqLd}(idx,a);\ rob[idx].ex\mathsf{\ \coloneqq\ }\mathsf{Exe};\\ \end{array}}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ res=rob.\mathsf{findBypass}(idx,a);\\ \mathsf{when}(a\neq\epsilon\ \wedge\ res==\top\ \wedge\ \neg l\!f[idx]);\\ \end{array}}{\begin{array}[]{c}ccm.\mathsf{reqLd}(idx,a);\ rob[idx].ex\mathsf{\ \coloneqq\ }\mathsf{Exe};\\ \end{array}}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{St},srcs,\epsilon,\epsilon,t\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ a=rob.\mathsf{computeAddr}(idx);\ v=rob.\mathsf{computeStData}(idx);\\ list=rob.\mathsf{findAffectedLd}(idx,a);\\ \end{array}}{\begin{array}[]{c}rob[idx]\mathsf{\ \coloneqq\ }\langle pc,npc,\langle\mathsf{St},srcs,a,v,t\rangle,\mathsf{Done}\rangle;\\ \begin{array}[]{l}\mathbf{for}\ kIdx=list.\mathsf{first}()\ \mathbf{to}\ list.\mathsf{tail}()\\ \qquad\mathbf{if}\ rob[kIdx].ex==\mathsf{Done}\ \mathbf{then}\\ \qquad\qquad rob.\mathsf{flush}(kIdx,rob[kIdx].pc);\ \mathbf{break};\\ \qquad\mathbf{else}\ rob[kIdx].ex\mathsf{\ \coloneqq\ }\mathsf{ReEx};\\ \end{array}\\ \end{array}}

\frac{\begin{array}[]{c}\langle idx,\langle pc,npc,\langle\mathsf{St},srcs,\epsilon,\epsilon,t\rangle,\mathsf{Idle}\rangle\rangle=rob.\mathsf{getReady}();\\ a=rob.\mathsf{computeAddr}(idx);\ v=rob.\mathsf{computeStData}(idx);\\ list=rob.\mathsf{findAffectedLd}(idx,a);\\ \end{array}}{\begin{array}[]{c}rob[idx]\mathsf{\ \coloneqq\ }\langle pc,npc,\langle\mathsf{St},srcs,a,v,t\rangle,\mathsf{Done}\rangle;\\ \begin{array}[]{l}\mathbf{for}\ kIdx=list.\mathsf{first}()\ \mathbf{to}\ list.\mathsf{tail}()\\ \qquad\mathbf{if}\ rob[kIdx].ex==\mathsf{Done}\ \mathbf{then}\\ \qquad\qquad rob.\mathsf{flush}(kIdx,rob[kIdx].pc);\ \mathbf{break};\\ \qquad\mathbf{else}\ rob[kIdx].ex\mathsf{\ \coloneqq\ }\mathsf{ReEx};\\ \end{array}\\ \end{array}}

\frac{⟨ p c , n p c , in s , Done ⟩ = r o b . getCommit ( ) ; when ( isNmLdRec ( in s )) ;}{r o b . deq ( ) ; r f . update ( in s ) ;}

\frac{⟨ p c , n p c , in s , Done ⟩ = r o b . getCommit ( ) ; when ( isNmLdRec ( in s )) ;}{r o b . deq ( ) ; r f . update ( in s ) ;}

\frac{⟨ p c , n p c , in s , Done ⟩ = r o b . getCommit ( ) ; ⟨ St , sr cs , a , v , t ⟩ = in s ;}{r o b . deq ( ) ; s b . enq ( a , v , t ) ; r f . update ( in s ) ;}

\frac{⟨ p c , n p c , in s , Done ⟩ = r o b . getCommit ( ) ; ⟨ St , sr cs , a , v , t ⟩ = in s ;}{r o b . deq ( ) ; s b . enq ( a , v , t ) ; r f . update ( in s ) ;}

\frac{⟨ p c , n p c , ⟨ Commit ⟩ , Done ⟩ = r o b . getCommit ( ) ; when ( s b . empty ( )) ;}{r o b . deq ( ) ; r f . update (⟨ Commit ⟩) ;}

\frac{⟨ p c , n p c , ⟨ Commit ⟩ , Done ⟩ = r o b . getCommit ( ) ; when ( s b . empty ( )) ;}{r o b . deq ( ) ; r f . update (⟨ Commit ⟩) ;}

\frac{a = s b . anyAddr ( ) ; ⟨ v , t , False ⟩ = s b . oldest ( a ) ; when ( a \neq = ϵ ) ;}{cc m . reqSt ( a , v , t ) ; s b . issue ( a ) ;}

\frac{a = s b . anyAddr ( ) ; ⟨ v , t , False ⟩ = s b . oldest ( a ) ; when ( a \neq = ϵ ) ;}{cc m . reqSt ( a , v , t ) ; s b . issue ( a ) ;}

\begin{array}[]{l}\mathbf{if}\ l\!f[idx]\ \mathbf{then}\ l\!f[idx]\mathsf{\ \coloneqq\ }\mathsf{False};\ {\color[rgb]{0,0,1}/\!/\ \mathrm{wrong\mathchar 45\relax{}path\ load\ response}}\\ \mathbf{else}\\ \quad\mathbf{let}\ \langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle,ex\rangle=rob[idx]\ \mathbf{in}\\ \quad\quad\mathbf{if}\ ex==\mathsf{ReEx}\ \mathbf{then}\ rob[idx].ex\mathsf{\ \coloneqq\ }\mathsf{Idle};\\ \quad\quad\mathbf{else}\ {\color[rgb]{0,0,1}/\!/\ \mathrm{save\ load\ result\ and\ check\ value\ misprediction}}\\ \quad\quad\quad rob[idx]\mathsf{\ \coloneqq\ }\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,res,t\rangle,\mathsf{Done}\rangle;\\ \quad\quad\quad\mathbf{if}\ v\neq\epsilon\ \wedge\ v\neq res\ \mathbf{then}\ rob.\mathsf{flush}(idx+1,npc);\\ \quad\quad\quad\mathbf{else}\ {\color[rgb]{0,0,1}/\!/\ \mathrm{kill\ younger\ load\ with\ staler\ value}}\\ \quad\quad\quad\quad kIdx=rob.\mathsf{findStaleLd}(a,idx,t);\\ \quad\quad\quad\quad\mathbf{if}\ kIdx\neq\top\ \mathbf{then}\ rob.\mathsf{flush}(kIdx,rob[kIdx].pc);\\ \end{array}

\begin{array}[]{l}\mathbf{if}\ l\!f[idx]\ \mathbf{then}\ l\!f[idx]\mathsf{\ \coloneqq\ }\mathsf{False};\ {\color[rgb]{0,0,1}/\!/\ \mathrm{wrong\mathchar 45\relax{}path\ load\ response}}\\ \mathbf{else}\\ \quad\mathbf{let}\ \langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,v,\epsilon\rangle,ex\rangle=rob[idx]\ \mathbf{in}\\ \quad\quad\mathbf{if}\ ex==\mathsf{ReEx}\ \mathbf{then}\ rob[idx].ex\mathsf{\ \coloneqq\ }\mathsf{Idle};\\ \quad\quad\mathbf{else}\ {\color[rgb]{0,0,1}/\!/\ \mathrm{save\ load\ result\ and\ check\ value\ misprediction}}\\ \quad\quad\quad rob[idx]\mathsf{\ \coloneqq\ }\langle pc,npc,\langle\mathsf{Ld},srcs,dst,a,res,t\rangle,\mathsf{Done}\rangle;\\ \quad\quad\quad\mathbf{if}\ v\neq\epsilon\ \wedge\ v\neq res\ \mathbf{then}\ rob.\mathsf{flush}(idx+1,npc);\\ \quad\quad\quad\mathbf{else}\ {\color[rgb]{0,0,1}/\!/\ \mathrm{kill\ younger\ load\ with\ staler\ value}}\\ \quad\quad\quad\quad kIdx=rob.\mathsf{findStaleLd}(a,idx,t);\\ \quad\quad\quad\quad\mathbf{if}\ kIdx\neq\top\ \mathbf{then}\ rob.\mathsf{flush}(kIdx,rob[kIdx].pc);\\ \end{array}

\frac{⟨ Nm , d s t , v ⟩ = p s [ i ] . decode ( ) ;}{p s [ i ] . execute (⟨ Nm , d s t , v ⟩ , \mathchar 45 ) ;}

\frac{⟨ Nm , d s t , v ⟩ = p s [ i ] . decode ( ) ;}{p s [ i ] . execute (⟨ Nm , d s t , v ⟩ , \mathchar 45 ) ;}

\frac{⟨ Ld , a , d s t ⟩ = p s [ i ] . decode ( ) ; when ( p s [ i ] . s b . exist ( a )) ;}{p s [ i ] . execute (⟨ Ld , a , d s t ⟩ , p s [ i ] . s b . youngest ( a )) ;}

\frac{⟨ Ld , a , d s t ⟩ = p s [ i ] . decode ( ) ; when ( p s [ i ] . s b . exist ( a )) ;}{p s [ i ] . execute (⟨ Ld , a , d s t ⟩ , p s [ i ] . s b . youngest ( a )) ;}

\frac{⟨ Ld , a , d s t ⟩ = p s [ i ] . decode ( ) ; when ( \neg p s [ i ] . s b . exist ( a )) ;}{p s [ i ] . execute (⟨ Ld , a , d s t ⟩ , m [ a ]) ; p s [ i ] . ib . rmAddr ( a ) ;}

\frac{⟨ Ld , a , d s t ⟩ = p s [ i ] . decode ( ) ; when ( \neg p s [ i ] . s b . exist ( a )) ;}{p s [ i ] . execute (⟨ Ld , a , d s t ⟩ , m [ a ]) ; p s [ i ] . ib . rmAddr ( a ) ;}

\frac{\begin{array}[]{c}\langle\mathsf{Ld},a,dst\rangle=ps[i].\mathsf{decode}();\\ \mathsf{when}(\neg ps[i].sb.\mathsf{exist}(a)\ \wedge\ ps[i].ib.\mathsf{exist}(a));\\ \end{array}}{v\leftarrow ps[i].ib.\mathsf{getAny}(a);\ ps[i].\mathsf{execute}(\langle\mathsf{Ld},a,dst\rangle,v);}

\frac{\begin{array}[]{c}\langle\mathsf{Ld},a,dst\rangle=ps[i].\mathsf{decode}();\\ \mathsf{when}(\neg ps[i].sb.\mathsf{exist}(a)\ \wedge\ ps[i].ib.\mathsf{exist}(a));\\ \end{array}}{v\leftarrow ps[i].ib.\mathsf{getAny}(a);\ ps[i].\mathsf{execute}(\langle\mathsf{Ld},a,dst\rangle,v);}

\frac{⟨ St , a , v ⟩ = p s [ i ] . decode ( ) ;}{p s [ i ] . execute (⟨ St , a , v ⟩ , \mathchar 45 ) ; p s [ i ] . s b . enq ( a , v ) ; p s [ i ] . ib . rmAddr ( a ) ;}

\frac{⟨ St , a , v ⟩ = p s [ i ] . decode ( ) ;}{p s [ i ] . execute (⟨ St , a , v ⟩ , \mathchar 45 ) ; p s [ i ] . s b . enq ( a , v ) ; p s [ i ] . ib . rmAddr ( a ) ;}

\frac{⟨ Commit ⟩ = p s [ i ] . decode ( ) ; when ( p s [ i ] . s b . empty ( )) ;}{p s [ i ] . execute (⟨ Commit ⟩ , \mathchar 45 ) ;}

\frac{⟨ Commit ⟩ = p s [ i ] . decode ( ) ; when ( p s [ i ] . s b . empty ( )) ;}{p s [ i ] . execute (⟨ Commit ⟩ , \mathchar 45 ) ;}

\frac{⟨ Reconcile ⟩ = p s [ i ] . decode ( ) ;}{p s [ i ] . ib . clear ( ) ; p s [ i ] . execute (⟨ Reconcile ⟩ , \mathchar 45 ) ;}

\frac{⟨ Reconcile ⟩ = p s [ i ] . decode ( ) ;}{p s [ i ] . ib . clear ( ) ; p s [ i ] . execute (⟨ Reconcile ⟩ , \mathchar 45 ) ;}

\frac{\begin{array}[]{c}a=ps[i].sb.\mathsf{anyAddr}();\ old=m[a];\ \mathsf{when}(a\neq\epsilon);\\ \end{array}}{\begin{array}[]{c}v\leftarrow ps[i].sb.\mathsf{rmOldest}(a);\ m[a]\mathsf{\ \coloneqq\ }v;\\ \forall j\neq i.\ \mathbf{if}\ \neg ps[j].sb.\mathsf{exist}(a)\ \mathbf{then}\ ps[j].ib.\mathsf{insert}(a,old);\\ \end{array}}

\frac{\begin{array}[]{c}a=ps[i].sb.\mathsf{anyAddr}();\ old=m[a];\ \mathsf{when}(a\neq\epsilon);\\ \end{array}}{\begin{array}[]{c}v\leftarrow ps[i].sb.\mathsf{rmOldest}(a);\ m[a]\mathsf{\ \coloneqq\ }v;\\ \forall j\neq i.\ \mathbf{if}\ \neg ps[j].sb.\mathsf{exist}(a)\ \mathbf{then}\ ps[j].ib.\mathsf{insert}(a,old);\\ \end{array}}

\frac{⟨⟨ Nm , d s t , v ⟩ , t s ⟩ = p s [ i ] . decodeTS ( ) ;}{p s [ i ] . executeTS (⟨ Nm , d s t , v ⟩ , \mathchar 45 , t s ) ;}

\frac{⟨⟨ Nm , d s t , v ⟩ , t s ⟩ = p s [ i ] . decodeTS ( ) ;}{p s [ i ] . executeTS (⟨ Nm , d s t , v ⟩ , \mathchar 45 , t s ) ;}

\frac{\begin{array}[]{c}\langle\langle\mathsf{Ld},a,dst\rangle,ats\rangle=ps[i].\mathsf{decodeTS}();\\ \mathsf{when}(ps[i].sb.\mathsf{exist}(a));\ \langle v,sts\rangle=ps[i].sb.\mathsf{youngest}(a);\\ \end{array}}{ps[i].\mathsf{executeTS}(\langle\mathsf{Ld},a,dst\rangle,v,\mathsf{max}(ats,ps[i].rts,sts));}

\frac{\begin{array}[]{c}\langle\langle\mathsf{Ld},a,dst\rangle,ats\rangle=ps[i].\mathsf{decodeTS}();\\ \mathsf{when}(ps[i].sb.\mathsf{exist}(a));\ \langle v,sts\rangle=ps[i].sb.\mathsf{youngest}(a);\\ \end{array}}{ps[i].\mathsf{executeTS}(\langle\mathsf{Ld},a,dst\rangle,v,\mathsf{max}(ats,ps[i].rts,sts));}

\frac{\begin{array}[]{c}\langle\langle\mathsf{Ld},a,dst\rangle,ats\rangle=ps[i].\mathsf{decodeTS}();\ \mathsf{when}(\neg ps[i].sb.\mathsf{exist}(a));\\ \langle v,\langle j,sts\rangle,mts\rangle=m[a];\ vts=(\mathbf{if}\ i\neq j\ \mathbf{then}\ mts\ \mathbf{else}\ sts);\\ \end{array}}{\begin{array}[]{c}ps[i].\mathsf{executeTS}(\langle\mathsf{Ld},a,dst\rangle,v,\mathsf{max}(ats,ps[i].rts,vts));\\ ps[i].ib.\mathsf{rmAddr}(a);\\ \end{array}}

\frac{\begin{array}[]{c}\langle\langle\mathsf{Ld},a,dst\rangle,ats\rangle=ps[i].\mathsf{decodeTS}();\ \mathsf{when}(\neg ps[i].sb.\mathsf{exist}(a));\\ \langle v,\langle j,sts\rangle,mts\rangle=m[a];\ vts=(\mathbf{if}\ i\neq j\ \mathbf{then}\ mts\ \mathbf{else}\ sts);\\ \end{array}}{\begin{array}[]{c}ps[i].\mathsf{executeTS}(\langle\mathsf{Ld},a,dst\rangle,v,\mathsf{max}(ats,ps[i].rts,vts));\\ ps[i].ib.\mathsf{rmAddr}(a);\\ \end{array}}

\frac{\begin{array}[]{c}\langle\langle\mathsf{Ld},a,dst\rangle,ats\rangle=ps[i].\mathsf{decodeTS}();\\ \langle v,[ts_{L},ts_{U}]\rangle=ps[i].ib.\mathsf{any}(a);\\ \mathsf{when}(\neg ps[i].sb.\mathsf{exist}(a)\ \wedge\ v\neq\epsilon\ \wedge\ ats\leq ts_{U});\\ \end{array}}{\begin{array}[]{c}ps[i].\mathsf{executeTS}(\langle\mathsf{Ld},a,dst\rangle,v,\mathsf{max}(ats,ps[i].rts,ts_{L}));\\ ps[i].ib.\mathsf{rmOlder}(a,ts_{U});\\ \end{array}}

\frac{\begin{array}[]{c}\langle\langle\mathsf{Ld},a,dst\rangle,ats\rangle=ps[i].\mathsf{decodeTS}();\\ \langle v,[ts_{L},ts_{U}]\rangle=ps[i].ib.\mathsf{any}(a);\\ \mathsf{when}(\neg ps[i].sb.\mathsf{exist}(a)\ \wedge\ v\neq\epsilon\ \wedge\ ats\leq ts_{U});\\ \end{array}}{\begin{array}[]{c}ps[i].\mathsf{executeTS}(\langle\mathsf{Ld},a,dst\rangle,v,\mathsf{max}(ats,ps[i].rts,ts_{L}));\\ ps[i].ib.\mathsf{rmOlder}(a,ts_{U});\\ \end{array}}

\frac{\langle\langle\mathsf{St},a,v\rangle,ts\rangle=ps[i].\mathsf{decodeTS}();}{\begin{array}[]{c}ps[i].\mathsf{executeTS}(\langle\mathsf{St},a,v\rangle,\mathchar 45\relax,\mathchar 45\relax);\\ ps[i].sb.\mathsf{enq}(a,v,ts);\ ps[i].ib.\mathsf{rmAddr}(a);\end{array}}

\frac{\langle\langle\mathsf{St},a,v\rangle,ts\rangle=ps[i].\mathsf{decodeTS}();}{\begin{array}[]{c}ps[i].\mathsf{executeTS}(\langle\mathsf{St},a,v\rangle,\mathchar 45\relax,\mathchar 45\relax);\\ ps[i].sb.\mathsf{enq}(a,v,ts);\ ps[i].ib.\mathsf{rmAddr}(a);\end{array}}

\frac{⟨⟨ Reconcile ⟩ , t s ⟩ = p s [ i ] . decodeTS ( ) ;}{p s [ i ] . executeTS (⟨ Reconcile ⟩ , \mathchar 45 , \mathchar 45 ) ; p s [ i ] . ib . clear ( ) ; p s [ i ] . r t s : = g t s ;}

\frac{⟨⟨ Reconcile ⟩ , t s ⟩ = p s [ i ] . decodeTS ( ) ;}{p s [ i ] . executeTS (⟨ Reconcile ⟩ , \mathchar 45 , \mathchar 45 ) ; p s [ i ] . ib . clear ( ) ; p s [ i ] . r t s : = g t s ;}

\frac{⟨⟨ Commit ⟩ , t s ⟩ = p s [ i ] . decodeTS ( ) ; when ( p s [ i ] . s b . empty ( )) ;}{p s [ i ] . executeTS (⟨ Commit ⟩ , \mathchar 45 , \mathchar 45 ) ;}

\frac{⟨⟨ Commit ⟩ , t s ⟩ = p s [ i ] . decodeTS ( ) ; when ( p s [ i ] . s b . empty ( )) ;}{p s [ i ] . executeTS (⟨ Commit ⟩ , \mathchar 45 , \mathchar 45 ) ;}

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsParallel Computing and Optimization Techniques · Embedded Systems Design Techniques · Distributed systems and fault tolerance

Full text

\copyrightdata

978-1-nnnn-nnnn-n/yy/mm \copyrightdoinnnnnnn.nnnnnnn

\authorinfo

Sizhuo Zhang and Muralidaran Vijayaraghavan and ArvindMIT CSAIL{szzhang, vmurali, arvind}@csail.mit.edu

An Operational Framework for Specifying Memory Models using Instantaneous Instruction Execution

(20yy)

Abstract

There has been great progress recently in formally specifying the memory model of microprocessors like ARM and POWER. These specifications are, however, too complicated for reasoning about program behaviors, verifying compilers etc., because they involve microarchitectural details like the reorder buffer (ROB), partial and speculative execution, instruction replay on speculation failure, etc. In this paper we present a new Instantaneous Instruction Execution ( $\mathrm{I^{2}E}$ ) framework which allows us to specify weak memory models in the same style as SC and TSO. Each instruction in $\mathrm{I^{2}E}$ is executed instantaneously and in-order such that the state of the processor is always correct. The effect of instruction reordering is captured by the way data is moved between the processors and the memory non-deterministically, using three conceptual devices: invalidation buffers, timestamps and dynamic store buffers. We prove that $\mathrm{I^{2}E}$ models capture the behaviors of modern microarchitectures and cache-coherent memory systems accurately, thus eliminating the need to think about microarchitectural details.

category:

C.0 General Modeling of computer architecture

††conference: CONF ’yy Month d–d, 20yy, City, ST, Country

1 Introduction

Computer architects make microarchitectural optimizations in processors which ensure that single-threaded programs can be run unmodified, but often create new and unexpected behaviors for multi-threaded programs. The effect of these optimizations manifests itself through load and store instructions because these are the only instructions through which threads can communicate with each other. Memory models abstract hardware in a way that is useful for programmers to understand the behaviors of their programs.

There are ongoing efforts to specify memory models for multithreaded programming in C, C++ Smith [2015] and other languages. These efforts are influenced by the type of memory models that can be supported efficiently on existing architectures like x86, POWER and ARM. While the memory model for x86 Owens et al. [2009]; Sewell et al. [2010]; Sarkar et al. [2009] is captured succinctly by the Total Store Order (TSO) model, the models for POWER Sarkar et al. [2011] and ARM Flur et al. [2016] are considerably more complex. The formal specifications of the POWER and ARM models have required exposing microarchitectural details like speculative execution, instruction reordering and the state of partially executed instructions, which, in the past, have always been hidden from the user. In addition, details of the memory system like write-though vs write-back caches, shared vs not-shared memory buffers, etc. were also needed for a precise specification of these two models.

Even though empirical evidence is weak, many architects believe that weak memory models, such as the ones for ARM, POWER, Alpha and RMO, offer some performance advantage or simpler implementation over TSO and other stronger memory models. We think that architects are unlikely to give up on weak memory models because of the flexibility they provide for high performance implementations. It is, therefore, important to develop a framework for defining weak memory models, which, like SC and TSO operational models, does not involve microarchitecture and memory system details. This paper offers such a framework based on Instantaneous Instruction Execution ( $\mathrm{I^{2}E}$ ).

In the $\mathrm{I^{2}E}$ framework, instructions are executed in order and atomically, and consequently, the processor always has the up-to-date state. The model descriptions use a multi-ported monolithic memory which executes loads and stores instantaneously. The data movement between the processors and the memory takes place asynchronously in the background. For specifying weak memory models, we combine $\mathrm{I^{2}E}$ with three new conceptual devices: invalidation buffers to capture instruction reordering, timestamps to enforce data dependencies, and dynamic store buffers to model shared store buffers and write-through caches in a topology independent way. We present several different weak memory models – WMM and WMM-D which are similar to the Alpha and RMO models; and WMM-S which is similar to the ARM and POWER models.

To convince the reader that we have not ruled out any fundamental and important microarchitectural optimizations, we give an abstract description of a speculative microarchitecture (OOOVP) with a coherent pipelined memory system (CCM). The structure of OOOVP is common to all high-performance processor implementations, regardless of the memory model they support; implementations of stronger memory models based on OOOVP use extra hardware checks to prevent or kill some specific memory behaviors. We prove that our weakest memory model, WMM, allows all sorts of microarchitecture optimizations, that is, CCM+OOOVP $\subseteq$ WMM.

One optimization that has been discussed in literature but has not been implemented in any commercial microprocessor yet is load-value speculation Lipasti et al. [1996]; Ghandour et al. [2010]; Perais and Seznec [2014a, b]. It allows us to predict a value for a load; the load is killed later if the predicted value does not match the load result from the memory system. Even if load-value speculation is included, our result CCM+OOOVP $\subseteq$ WMM holds. Surprisingly, if value speculation is permitted in the implementation then we can also prove that WMM $\subseteq$ CCM+OOOVP, that is, the WMM and CCM+OOOVP become equivalent. We show via a common programming example that an extra fence needs to be inserted in WMM to enforce data-dependencies. This is an unnecessary cost if we know for sure that our implementation would not use value speculation. WMM-D is a slight modification of WMM to enforce ordering of data-dependent loads using timestamps. We also prove that OOOD (the OOOVP implementation without load-value speculation) is equivalent to WMM-D.

ARM and POWER microarchitectures use shared store-buffers and write-though caches, and unfortunately, such memory systems introduce behaviors not seen in other weak memory models. The ISA for these machines include “weaker” and “stronger” fences with slightly different functionality because weaker fences have smaller performance penalty than the stronger ones. This requires memory fence instructions to enter store buffers, muddying the clean separation between the cache-coherent memory systems and processors. We introduce HMB, an abstract model for hierarchy of shared store buffers or write-through caches, which is adapted from the storage subsystem in the Flowing Model of Flur et al. [2016]. We define WMM-S, an extension of WMM, specifically to deal with such multi-copy non-atomic store systems and show that HMB+OOOS $\subseteq$ WMM-S, in which OOOS is the processor implementation adapted from OOOVP to be compatible with HMB.

In summary, this paper makes the following contributions:

$\mathrm{I^{2}E}$ , a new framework for describing memory models with three new conceptual devices: invalidation buffers, timestamps, and dynamic store buffers; 2. 2.

WMM and WMM-D memory models which are like the RMO and Alpha models; 3. 3.

WMM-S model to embody ARM and POWER like multi-copy non-atomic stores; 4. 4.

OOOVP, an abstract description of the microarchitecture underlying all modern high performance microprocessors; 5. 5.

A proof that CCM+OOOVP = WMM; 6. 6.

A proof that CCM+OOOD = WMM-D; and 7. 7.

A proof that HMB+OOOS $\subseteq$ WMM-S.

Paper organization: Section 2 presents the related work. Section 3 defines CCM+OOOVP, an implementation scheme of multiprocessors. We introduce the $\mathrm{I^{2}E}$ framework in Section 4. We use $\mathrm{I^{2}E}$ and invalidation buffers to define WMM in Section 5. Section 6 defines WMM-D using timestamps to capture data dependency. Section 7 defines WMM-S using dynamic store buffers to model multi-copy non-atomic memory systems. Section 8 offers the conclusion.

2 Related Work

SC Lamport [1979] is the most intuitive memory model, but naive implementations of SC suffer from poor performance. Gharachorloo et al. proposed load speculation and store prefetch to enhance the performance of SC Gharachorloo et al. [1991]. Over the years, researchers have proposed more aggressive techniques to preserve SC Ranganathan et al. [1997]; Guiady et al. [1999]; Gniady and Falsafi [2002]; Ceze et al. [2007]; Wenisch et al. [2007]; Blundell et al. [2009]; Singh et al. [2012]; Lin et al. [2012]; Gope and Lipasti [2014]. Perhaps because of their hardware complexity, the adoption of these techniques in commercial microprocessor has been limited. Instead the manufactures and researchers have chosen to present weaker memory model interfaces, e.g. TSO SPARC International, Inc. [1992], PSO Weaver and Gremond [1994], RMO Weaver and Gremond [1994], x86 Owens et al. [2009]; Sewell et al. [2010]; Sarkar et al. [2009], Processor Consistency Goodman [1991], Weak Consistency Dubois et al. [1986], RC Gharachorloo et al. [1990], CRF Shen et al. [1999], POWER IBM [2013] and ARM ARM [2013]. The tutorials by Adve et al. Adve and Gharachorloo [1996] and by Maranget et al. Maranget et al. [2012] provide relationships among some of these models.

The lack of clarity in the definitions of POWER and ARM memory models in their respective company documents has led some researchers to empirically determine allowed/disallowed behaviors Sarkar et al. [2011]; Mador-Haim et al. [2012]; Alglave et al. [2014]; Flur et al. [2016]. Based on such observations, in the last several years, both axiomatic models and operational models have been developed which are compatible with each other Alglave et al. [2009]; Alglave and Maranget [2011]; Alglave [2012]; Mador-Haim et al. [2012]; Alglave et al. [2014]; Sarkar et al. [2011, 2012]; Alglave et al. [2013]; Flur et al. [2016]. However, these models are quite complicated; for example, the POWER axiomatic model has 10 relations, 4 types of events per instruction, and 13 complex axioms Mador-Haim et al. [2012], some of which have been added over time to explain specific behaviors Alglave et al. [2009]; Alglave and Maranget [2011]; Alglave et al. [2012]; Mador-Haim et al. [2012]. The abstract machines used to describe POWER and ARM operationally are also quite complicated, because they require the user to think in terms of partially executed instructions Sarkar et al. [2011, 2012]. In particular, the processor sub-model incorporates ROB operations, speculations, instruction replay on speculation failures, etc., explicitly, which are needed to explain the enforcement of specific dependency (i.e. data dependency). We present an $\mathrm{I^{2}E}$ model WMM-D in Section 6 that captures data dependency and sidesteps all these complications. Another source of complexity is the multi-copy non-atomicity of stores, which we discuss in Section 7 with our solution WMM-S.

Adve et al. defined Data-Race-Free-0 (DRF0), a class of programs where shared variables are protected by locks, and proposed that DRF0 programs should behave as SC Adve and Hill [1990]. Marino et al. improves DRF0 to the DRFx model, which throws an exception when a data race is detected at runtime Marino et al. [2010]. However, we believe that architectural memory models must define clear behaviors for all programs, and even throwing exceptions is not satisfactory enough.

A large amount of research has also been devoted to specifying the memory models of high-level languages, e.g. C/C++ Smith [2015]; Boehm and Adve [2008]; Batty et al. [2011, 2012]; Pichon-Pharabod and Sewell [2016]; Batty et al. [2016]; Lahav et al. [2016]; Krebbers [2014]; Batty et al. [2013]; Kang et al. [2015] and Java Manson et al. [2005]; Cenciarelli et al. [2007]; Maessen et al. [2000]; Bogdanas and Roşu [2015]; Demange et al. [2013]. There are also proposals not tied to any specific language Boudol and Petri [2009]; Crary and Sullivan [2015]. This remains an active area of research because a widely accepted memory model for high-level parallel programming is yet to emerge, while this paper focuses on the memory models of underlying hardware.

Arvind and Maessen have specified precise conditions for preserving store atomicity even when instructions can be reordered Arvind and Maessen [2006]. In contrast, the models presented in this paper do not insist on store atomicity at the program level.

There are also studies on verifying programs running under weak memory models Torlak et al. [2010]; Kuperstein et al. [2011]; Atig et al. [2010]. Simple memory model definitions like $\mathrm{I^{2}E}$ models will definitely facilitate this research area.

3 Implementation of Modern Multiprocessors

Modern multiprocessor systems consist of out-of-order processors and highly pipelined coherent cache hierarchies. In addition to pipelining and out-of-order execution, the processor may perform branch prediction, i.e. predict the PC of the next instruction during instruction fetch in order to fetch and execute the next instruction, memory dependency speculation, i.e. issue a load to memory even when there is an older store with unresolved address, and even load-value speculation, i.e. predict the result of a load before the load is executed. The memory systems also employ pipelining and out-of-order execution for performance. For example, the memory system may not process requests in the FIFO manner (consider a cache miss followed by a cache hit). These optimizations are never visible to a single-threaded program but can be exposed by multithreaded programs. In this section, we present “physical” models that describe the operations (e.g. the ones mentioned above) inside high-performance processors and cache hierarchies. These physical models are similar to those in Sarkar et al. [2011]; Flur et al. [2016], but here they only serve as a reference to capture the behaviors of modern multiprocessors precisely; we use them to verify the $\mathrm{I^{2}E}$ memory models proposed later. It should be noted that the physical models are presented in an abstract manner, e.g., the inner structure of the branch predictor is abstracted by a function which may return any value. The model also abstracts away resource management issues, such as register renaming, finite-size buffers and associated tags by assuming unbounded resources.

We associate a globally unique tag with each store instruction so that we can identify the store that each load reads from. The tag is also saved in memory when the store writes the memory. Such tags do not exist in real implementations but are needed in our model for reasons that will become clear in Section 3.2.2.

While the processor remains similar for all implementations, it is difficult to offer a common model for two dominant cache hierarchies. Machines, such as Intel x86, have used write-back cache-coherent memory systems. In contrast, ARM and POWER machines employ shared store-buffers and write-through caches in their memory systems. We will first discuss CCM, model of a write-back cache-coherent memory system, and postpone the discussion of HMB, the write-through cache system, until Section 7.

3.1 CCM: the Semantics of Write-Back Cache Hierarchies

Figure 1 shows how out-of-order processors (OOOVP) and a write-back cache hierarchy (CCM) are connected together. A processor $i$ can send load and store requests to CCM by calling the following methods of port $i$ of CCM:

•

$\mathsf{reqLd}(t^{L},a)$ : a load request to address $a$ with tag $t^{L}$ .

•

$\mathsf{reqSt}(a,v,t^{S})$ : a store request that writes data $v$ to address $a$ . $t^{S}$ is the globally unique tag for the store instruction.

Note that the processor also attaches a tag $t^{L}$ to each load request in order to associate the future load response with the requesting load instruction. The memory sends responses back to a processor by calling the following methods of the processor:

•

$\mathsf{respLd}(t^{L},res,t^{S})$ : $res$ is the result for the load with tag $t^{L}$ , and $t^{S}$ is the tag for the store that supplied $res$ to the memory.

•

$\mathsf{respSt}(a)$ : $a$ is the store address.

Store response is needed to inform the processor that a store has been completed. No ordering between the processing of requests inside the memory should be assumed by the processor.

CCM consists of $n$ memory request buffers $mrb[1\ldots n]$ , one for each processor, and a monolithic memory $m$ . A monolithic memory location $m[a]$ contains $\langle v,t^{S}\rangle$ , in which $v$ is the value written by a store with tag $t^{S}$ . The $\mathsf{reqLd}$ and $\mathsf{reqSt}$ methods simply insert the incoming requests from processor $i$ into $mrb[i]$ . CCM processes requests by picking any request from any $mrb$ . If the request is a load $\langle\mathsf{Ld},t^{L},a\rangle$ from $mrb[i]$ , then CCM calls method $\mathsf{respLd}(t^{L},v,t^{S})$ of processor $i$ , where $\langle v,t^{S}\rangle=m[a]$ . If the request is a store $\langle\mathsf{St},a,v,t^{S}\rangle$ , then we update $m[a]$ to be $\langle v,t^{S}\rangle$ , and call method $\mathsf{respSt}(a)$ of processor $i$ . The behavior of CCM is shown in Figure 2.

We describe the behavior of a system as a set of state-transition rules, written as

[TABLE]

The predicates are expressed either by pattern matching or using a $\mathsf{when}(\mathit{expression})$ clause. $mrb[i].\mathsf{any}()$ returns any entry in $mrb[i]$ , and $mrb[i].\mathsf{remove}(en)$ removes entry $en$ from $mrb[i]$ .

To understand how such a simple structure can abstract the write-back cache-coherent hierarchy, we refer to the cache coherence proof by Vijayaraghavan et al. Vijayaraghavan et al. [2015]. It shows that a request can complete only by reading or writing an L1 cache line when it has sufficient permissions, and that under such circumstances a write-back cache-coherent hierarchy is exactly equivalent to the monolithic memory abstraction. However, the order of responses may be different from the order of requests due to the out-of-order processing inside the hierarchy. Such reordering is captured by $mrb$ .

3.2 OOOVP: the Model of Out-of-Order Processors

We will first give an informal description of the behavior of a speculative out-of-order processor OOOVP, shown in Figure 3; the actual rules are presented later.

The processor fetches an instruction from the address given by the PC register, and updates PC based on the prediction by a branch predictor. The fetched instruction is decoded and enqueued into the reorder buffer (ROB). ROB contains all the in-flight instructions in the fetched order but executes them out of order. An instruction can be executed when all of its source operands have been computed, and the result of its execution is stored in its ROB entry. The computed source operands come from either an older ROB entry or the register file. The ROB then commits the instructions in the fetched order. In-order commitment is required to implement precise interrupts and exceptions. After an instruction is committed, it is removed from the ROB and the register file is updated with the result of the instruction’s execution.

When a branch instruction is executed, if the branch target is not equal to the address of the next instruction that was fetched, then all instructions in ROB after the branch are “flushed” (i.e. discarded) and the PC is set to the correct branch target, allowing the correct set of instructions to be fetched.

A store instruction is executed by computing the store address and data, and is enqueued into the store buffer at commit. In the background, the store buffer can send the oldest store for an address into the memory, and delete that store when the response comes back from the memory.

In contrast, the execution of a load instruction splits into two phases. The first phase is to compute the load address. In the second phase, a load will search older entries in the ROB and the store buffer for the latest store to the same address. If such a store is found, that store’s value (and tag) is read – this is called “data forwarding” or “data bypassing”. Otherwise, a load request is sent to the memory with a unique tag (we use the index of the ROB entry). Eventually, the memory system can send a response back to the processor with a load result; the ROB entry for the load (identified with the tag) is updated with the result.

A load can be issued to memory at any time as long as its address is available, even when there are older unresolved branches or stores with uncomputed addresses. If an older store is executed later and writes to the same address, then any such loads that were executed earlier have violated memory dependency and should be flushed. The details will be discussed later. Note that loads which have been issued to the memory can be flushed from ROB for various reasons, and the responses for the flushed loads are discarded.

The processor may also employ a load-value predictor, which predicts the result of any load that does not have a value. The predicted result can be used in the execution of other instructions. When the load gets its value from data forwarding or memory and the value is not equal to the predicted one, all instructions younger than the load are flushed.

There are two fences: $\mathsf{Commit}$ and $\mathsf{Reconcile}$ . The $\mathsf{Commit}$ fence stalls at the commit slot until the store buffer is empty. The $\mathsf{Reconcile}$ fence prevents a younger load from being issued to memory, and also stops the data forwarding across the fence.

In the following we give a precise description of how OOOVP operates. (We will directly use the variable names in Figure 3, e.g., $pcr$ stands for the PC register). We never reuse ROB entries, and follow the convention that younger entries will have larger indices. We refer to the oldest entry in ROB as the commit slot.

3.2.1 Component Functionality

Since the implementation has to deal with partially executed instructions, we need to keep information about in-flight instructions in ROB (all $srcs$ fields represent source register names):

•

$\langle\mathsf{Nm},op,srcs,dst,val\rangle$ : A non-memory instruction (e.g. ALU and branch instructions). $op$ is the type of operation. $val$ represents the computed value for the destination register $dst$ and is initially $\epsilon$ . These instructions include branch instructions.

•

$\langle\mathsf{Ld},srcs,dst,a,v,t\rangle$ : A load instruction to address $a$ . $v$ is the load result for destination register $dst$ , and $t$ is the tag of the store that provides value $v$ . All of $a$ , $v$ and $t$ are initially $\epsilon$ .

•

$\langle\mathsf{St},srcs,a,v,t\rangle$ : A store instruction that writes data $v$ to address $a$ . $t$ is the unique tag for this store assigned at decode time. Both $a$ and $v$ are initially $\epsilon$ .

•

$\langle\mathsf{Commit}\rangle$ and $\langle\mathsf{Reconcile}\rangle$ fences.

We use the $\mathsf{fetch}(pc)$ function to fetch an instruction from memory address $pc$ and decode it into the above form.

$pcr$ is updated speculatively when a new instruction $ins$ is fetched into ROB using the $\mathsf{predict}(ins)$ method of $bp$ . We assume that $bp$ always predicts correctly for non- $\mathsf{Nm}$ instructions. $r\!f$ is updated conservatively when an instruction $ins$ is committed from ROB using the $\mathsf{update}(ins)$ method. Each $sb$ entry also contains an $iss$ bit, which indicates whether the store has been issued to the memory or not. The following methods are defined on $sb$ :

•

$\mathsf{enq}(a,v,t)$ : enqueues the $\langle\mathrm{address,value,tag}\rangle$ tuple $\langle a,v,t\rangle$ into $sb$ , and initializes the $iss$ bit of the new entry as $\mathsf{False}$ .

•

$\mathsf{empty}()$ : returns $\mathsf{True}$ when $sb$ is empty.

•

$\mathsf{anyAddr}()$ : returns any store address present in $sb$ ; or returns $\epsilon$ if $sb$ is empty.

•

$\mathsf{oldest}(a)$ : return the $\langle$ store data, tag, $iss$ bit $\rangle$ of the oldest store for address $a$ in $sb$ .

•

$\mathsf{issue}(a)$ : sets the $iss$ bit of the oldest store for address $a$ to $\mathsf{True}$ .

•

$\mathsf{rmOldest}(a)$ : deletes the oldest store to address $a$ from $sb$ .

An ROB entry is defined as $\langle pc,npc,ins,ex\rangle$ , where $pc$ is the PC of the instruction in the entry, $npc$ is the (predicted) PC of the next instruction, $ins$ is the instruction in this entry, and $ex$ is the state of the instruction. $ex$ field has one of the following values: $\mathsf{Idle}$ , $\mathsf{Exe}$ , $\mathsf{ReEx}$ , and $\mathsf{Done}$ . An instruction is $\mathsf{Idle}$ before it starts execution, and will become $\mathsf{Done}$ after execution finishes. Both $\mathsf{Exe}$ and $\mathsf{ReEx}$ are only used for $\mathsf{Ld}$ instructions to indicate that the load request is being processed in CCM. $\mathsf{ReEx}$ additionally implies that the load needs to be re-executed because the result of the current load request in memory is going to be wrong. We initialize the $ex$ field of an instruction $ins$ using function $\mathsf{initEx}(ins)$ , which returns $\mathsf{Done}$ for fence instructions and returns $\mathsf{Idle}$ otherwise.

$l\!f$ is for filtering out load responses from CCM for the killed instructions. It is a bit vector of the same length as $rob$ (so it is also infinitely long in our description). $l\!f[idx]$ is $\mathsf{True}$ if and only if a $\mathsf{Ld}$ instruction at $idx$ has been flushed from $rob$ while its load request is still being processed in the memory.

Load-value speculation is modeled by the $\mathsf{predict}(en)$ method of $vp$ , which can predict the load result for ROB entry $en$ .

All methods defined for $rob$ are listed in Table 1. Besides, we use $rob[idx]$ to refer to the ROB entry at index $idx$ . We also use $rob[idx].pc$ , $rob[idx].npc$ , $rob[idx].ins$ and $rob[idx].ex$ to refer to the $pc$ , $npc$ , $ins$ and $ex$ fields of $rob[idx]$ , respectively.

3.2.2 Rules to Describe OOOVP Behavior

Figure 4 shows the rules of OOOVP, where $ccm$ represents the CCM port connected to the processor, and Figure 5 shows the interface methods of OOOVP to process the responses from memory.

Rule OOO-LdReq sends a load request to CCM. However, $l\!f$ has to be checked to avoid sending a request with a duplicated $idx$ to memory. (Since we never reuse $rob$ indices here, this check will always pass). When the load response arrives as shown in the $\mathsf{respLd}(idx,res)$ method in Figure 5, we check $l\!f$ to see if it corresponds to a $\mathsf{Ld}$ instruction which has already been killed. If so, we throw away the response and reset the $l\!f$ bit. Otherwise, we check the $ex$ field of the original requesting ROB entry. If it is $\mathsf{ReEx}$ , the load response is discarded and the $ex$ field is set to $\mathsf{Idle}$ so that the load can be re-executed later. Otherwise, we record the load result and flush $rob$ in case of load-value misprediction. If there is no load-value misprediction, we kill eagerly executed younger loads which get results staler than the current load response using the $\mathsf{findStaleLd}$ method.

There are two points worth noticing about loads. First, the load address can be computed from some unverified predicted values, so two loads can be executed out-of-order even if one load uses the result of the other as load address. Second, two loads to the same address on the same processor can return from CCM out-of-order as long as they reads from the same store, making the loads still appear to be executed in order. While this mechanism assumes that the load result has the unique tag associated with the store read by the load, in a real implementation there are no unique tags for stores. In actual implementations, the processors monitors the coherence messages during the period between these two load responses; if the cache-line read by the younger load is invalidated, then the younger load is killed. This mechanism helps maintain the SC for a single address property at the program level while imposing minimum restrictions on the out-of-order execution in hardware. POWER and ARM processors also employ this mechanism Sarkar et al. [2011]; Flur et al. [2016]. (Notice that the tags for stores are solely for the purpose of detecting whether two loads read from the same store). We do not use $\mathsf{findStaleLd}$ to kill loads in OOO-LdBypass, because such loads must have already been killed by the store that forwards the data, as explained below in the OOO-StEx rule.

Rule OOO-StEx computes the store address and data of a $\mathsf{St}$ instruction, and searches for younger loads to the same address which violate memory dependency. The for loop is used to process all violating loads from the oldest to the youngest. If the load has not finished execution, we mark its $ex$ field for re-execution. Otherwise, the load may have propagated the wrong result to younger instructions, so we kill it and flush the subsequent instructions from $rob$ .

4 Defining Memory Models Using I2E

The $\mathrm{I^{2}E}$ framework defines memory models using the structure in Figure 6a. The state of the system with $n$ processors is defined as $\langle ps,m\rangle$ , where $m$ is an $n$ -ported monolithic memory which is connected to the $n$ processors. $ps[i]$ ( $i=1\ldots n$ ) represents the state of the $i^{th}$ processor. Each processor contains a register state $s$ , which represents all architectural registers, including both the general purpose registers and special purpose registers, such as PC. Cloud represents additional state elements, e.g. a store buffer, that a specific memory model may use in its definition.

Since we want our definitions of the memory models to be independent from ISA, we introduce the concept of decoded instruction set (DIS). A decoded instruction contains all the information of an instruction after it has been decoded and has read all source registers. Our DIS has the following five instructions.

•

$\langle\mathsf{Nm},dst,v\rangle$ : instructions that do not access memory, such as ALU or branch instructions. It writes the computation result $v$ into destination register $dst$ .

•

$\langle\mathsf{Ld},a,dst\rangle$ : a load that reads memory address $a$ and updates the destination register $dst$ .

•

$\langle\mathsf{St},a,v\rangle$ : a store that writes value $v$ to memory address $a$ .

•

$\langle\mathsf{Commit}\rangle$ and $\langle\mathsf{Reconcile}\rangle$ : the two types of fences.

The $\mathsf{Commit}$ and $\mathsf{Reconcile}$ fences already appeared in OOOVP, and later we will define their semantics in proposed $\mathrm{I^{2}E}$ models.

Since instructions are executed instantaneously and in-order in $\mathrm{I^{2}E}$ models, the register state of each processor is by definition always up-to-date. Therefore we can define the following two methods on each processor to manipulate the register state $s$ :

•

$\mathsf{decode}()$ : fetches the next instruction and returns the corresponding decoded instruction based on the current $s$ .

•

$\mathsf{execute}(dIns,ldRes)$ : updates $s$ (e.g. by writing destination registers and changing PC) according to the current decoded instruction $dIns$ . A $\mathsf{Ld}$ requires a second argument $ldRes$ which should be the loaded value. For other instructions, the second argument can be set to don’t care (“ $\mathchar 45\relax$ ”).

In $\mathrm{I^{2}E}$ , the meaning of an instruction cannot depend on a future store, so all $\mathrm{I^{2}E}$ models forbid stores from overtaking loads. This automatically excludes all thin-air read behaviors, and matches the in-order commit property of OOOVP.

5 WMM Model

Our first $\mathrm{I^{2}E}$ model, WMM (Figure 6b), adds two conceptual devices to each processor: a store buffer $sb$ and an invalidation buffer $ib$ . Despite the simplicity of these two devices, they make WMM equivalent to CCM+OOOVP. It is notable that WMM can capture the subtle effects induced by various speculations in OOOVP.

The $sb$ in WMM is almost the same as the one in OOOVP except that it does not need the $\mathsf{issue}$ method here and thus the $iss$ bit is also not needed. (The store tag is also not needed here). We change the $\mathsf{rmOldest}(a)$ method of $sb$ to return the $\langle$ address, value $\rangle$ pair of the oldest store for address $a$ in addition to the deletion of that store. We also define the following two new methods on $sb$ :

•

$\mathsf{exist}(a)$ : returns $\mathsf{True}$ if address $a$ is present in $sb$ .

•

$\mathsf{youngest}(a)$ : returns the youngest store data to address $a$ in $sb$ .

Buffering stores in $sb$ allows loads to overtake stores, and enables reorderings of stores. A $\mathsf{Commit}$ fence will flush all stores in the local $sb$ into the monolithic memory to make them globally visible.

In case of load-load reordering, a reordered load may read a stale value, and this behavior is simulated by the $ib$ of each processor in WMM. $ib$ is an unbounded buffer of $\langle\mathrm{address,value}\rangle$ pairs, each representing a stale memory value for an address that can be observed by the processor. A stale value enters $ib$ when some store buffer pushes a value to the monolithic memory. When ordering is needed, stale values should be removed from $ib$ to prevent younger loads from reading them. In particular, the $\mathsf{Reconcile}$ fence will clear the local $ib$ . The following methods are defined on $ib$ :

•

$\mathsf{insert}(a,v)$ : inserts $\langle\mathrm{address,value}\rangle$ pair $\langle a,v\rangle$ into $ib$ .

•

$\mathsf{exist}(a)$ : returns $\mathsf{True}$ if address $a$ is present in $ib$ .

•

$\mathsf{getAny}(a)$ : returns any value $v$ for address $a$ in $ib$ , and removes all values for $a$ , which are inserted into $ib$ before $v$ , from $ib$ .

•

$\mathsf{clear}()$ : removes all contents from $ib$ to make it empty.

•

$\mathsf{rmAddr}(a)$ : removes all (stale) values for address $a$ from $ib$ .

5.1 Operational Semantics of WMM

Figure 7 shows the operational semantics of WMM. The first 7 rules are the instantaneous execution of decoded instructions, while the WMM-DeqSb rule removes the oldest store for any address (say $a$ ) from $sb$ and commits it to the monolithic memory. WMM-DeqSb also inserts the original memory value into the $ib$ of all other processors to allow $\mathsf{Ld}\ a$ in these processors to effectively get reordered with older instructions. However, this insertion in $ib$ should not be done if the corresponding $sb$ on that processor already has a store to $a$ . This restriction is important, because if a processor has address $a$ in its $sb$ , then it can never see stale values for $a$ . For the same reason, when a $\mathsf{St}\ a\ v$ is inserted into $sb$ , we remove all values for $a$ from the $ib$ of the same processor.

Load execution rules in Figure 7 correspond to three places from where a load can get its value. WMM-LdSb executes $\mathsf{Ld}\ a$ by reading from $sb$ . If address $a$ is not found in $sb$ , then the load can read from the monolithic memory (WMM-LdMem). However, in order to allow the load to read a stale value (to model load reordering), WMM-LdIb gets the value from $ib$ . (Since $\mathsf{getAny}$ has side-effects, we use $\leftarrow$ to bind its return value to a free variable). The model allows non-deterministic choice in the selection of WMM-LdMem and WMM-LdIb. To make this idea work, WMM-LdMem has to remove all values for $a$ from $ib$ , because these values are staler than the value in memory. Similarly, WMM-LdIb removes all the values for $a$ , which are staler than the one read, from $ib$ .

Synchronization instructions: Atomic read-modify-write ( $\mathsf{RMW}$ ) instructions can also be included in WMM. $\mathsf{RMW}$ directly operates on the monolithic memory, so the rule to execute $\mathsf{RMW}$ is simply the combination of WMM-LdMem, WMM-St and WMM-DeqSb.

5.2 Litmus Tests for WMM

WMM executes instructions instantaneously and in order, but because of store buffers ( $sb$ ) and invalidation buffers ( $ib$ ), a processor can see the effect of loads and stores on some other processor in a different order than the program order on that processor. We explain the reorderings permitted and forbidden by the definition of WMM using well-known examples.

Fences for mutual exclusion: Figure 9 shows the kernel of Dekker’s algorithm in WMM, which guarantees mutual exclusion by ensuring registers $r_{1}$ and $r_{2}$ cannot both be zero at the end. All four fences are necessary. Without the $\mathsf{Reconcile}$ fence $I_{3}$ , $I_{4}$ could read 0 from $ib$ , as if $I_{4}$ overtakes $I_{1}$ and $I_{2}$ . Without the $\mathsf{Commit}$ fence $I_{2}$ , $I_{1}$ could stay in the $sb$ , and $I_{8}$ gets 0 from memory.

Fences for message passing: Figure 9 shows a way of passing data 42 from P1 to P2 by setting a flag at address $f$ . Fences $I_{2}$ and $I_{5}$ are necessary. Without the $\mathsf{Commit}$ fence $I_{2}$ , the two stores on P1 may get reordered in writing memory, so $I_{6}$ may not see the new data. Without the $\mathsf{Reconcile}$ fence $I_{5}$ , $I_{6}$ could see the stale value 0 from $ib$ . It is as if the two loads on P2 are reordered.

Memory dependency speculation: WMM is able to capture the behaviors caused by memory dependency speculation in hardware. For example, the behavior in Figure 11 is possible in CCM+OOOVP due to memory dependency speculation, i.e. P2 predicts that the store address of $I_{5}$ is not $a$ , and execute $I_{6}$ early to get value 0. WMM allows this behavior because $I_{6}$ can read 0 from $ib$ .

Load-value speculation: WMM can capture the behaviors caused by load-value speculation in hardware. For instance, the behavior in Figure 11 is the result of such speculation in CCM+OOOVP, i.e. P2 can predict the result of $I_{4}$ to be $a$ and execute $I_{5}$ early to get value 0. When $I_{4}$ returns from memory later with value $a$ , the prediction on $I_{4}$ turns out to be correct and the result of $I_{5}$ can be kept. WMM allows this behavior because $I_{5}$ can read 0 from $ib$ .

SC for a single address: WMM maintains SC for all accesses to a single address, i.e. all loads the stores to a single address can be put into a total order, which is consistent with the program order ( $\xrightarrow{po}$ ), read-from relation ( $\xrightarrow{r\!f}$ ), and coherence order ( $\xrightarrow{co}$ ). The coherence order is a total order of stores to this address; in WMM it is the order of writing the monolithic memory. This property holds for WMM because both $sb$ and $ib$ manages values of the same address in a FIFO manner. This property also implies the following two axioms Batty et al. [2011]; Maranget et al. [2012]; Smith [2015] ( $L_{1},L_{2},S_{1},S_{2}$ denote loads and stores to the same address):

CoRR

(Read-Read Coherence): $L_{1}\xrightarrow{po}L_{2}\ \wedge\ S_{1}\xrightarrow{r\!f}L_{1}\ \wedge\ S_{2}\xrightarrow{r\!f}L_{2}\Longrightarrow S_{1}==S_{2}\ \vee\ S_{1}\xrightarrow{co}S_{2}$ .

CoWR

(Write-Read Coherence): $S_{2}\xrightarrow{r\!f}L_{1}\ \wedge\ S_{1}\xrightarrow{po}L_{1}\Longrightarrow S_{1}==S2\ \vee\ S_{1}\xrightarrow{co}S_{2}$ .

WMM satisfies these two axioms. As for CCM+OOOVP, The coherence order is the order of writing the monolithic memory in CCM, and these two axioms hold due to the $\mathsf{findAffectedLd}$ and $\mathsf{findStaleLd}$ methods used in OOOVP (see Appendix C for the proof).

SC for well-synchronized programs: The critical sections in well-synchronized programs are all protected by locks. To maintain SC behaviors for such programs in WMM, we can add a $\mathsf{Reconcile}$ after acquiring the lock and a $\mathsf{Commit}$ before releasing the lock.

Fences to restore SC: For any program, if we insert a $\mathsf{Commit}$ followed by a $\mathsf{Reconcile}$ before every $\mathsf{Ld}$ and $\mathsf{St}$ instruction, the program behavior in WMM will be sequential consistent.

In summary, WMM can reorder stores to different addresses, and allows a load to overtake other loads (to different addresses), stores and $\mathsf{Commit}$ fences. A load cannot overtake any $\mathsf{Reconcile}$ fence, while dependencies generally do not enforce ordering.

5.3 Equivalence of CCM+OOOVP and WMM

Theorem 1.

CCM+OOOVP $\subseteq$ WMM.

Proof.

First of all, for any execution in CCM+OOOVP which contains flushes on $rob$ , if we exclude the flushes and the part of the execution, of which the effects are canceled by the flushes, we will get a new execution with the same program results. Similarly, we could exclude any load re-execution (i.e. a store sets the $ex$ field of a load to $\mathsf{ReEx}$ ). Thus, we only need to consider executions in CCM+OOOVP without any $rob$ flush or load re-execution. For any such execution $E$ in CCM+OOOVP, we could simulate $E$ in WMM using the following way to get the same program behavior:

•

When an instruction is committed from an ROB in $E$ , we execute that instruction in WMM.

•

When a store writes the monolithic memory of CCM ( $ccm.m$ ) and is dequeued from a store buffer in $E$ , we also dequeue that store and writes the monolithic memory ( $m$ ) in WMM.

After each step of our simulation, we prove inductively that the following invariants hold:

The WMM states of $m$ and all store buffers are the same as the CCM+OOOVP states of $ccm.m$ and all store buffers. 2. 2.

All instructions committed from ROBs in CCM+OOOVP have also been executed in WMM with the same results.

The only non-trivial case is when a load $L$ to address $a$ is committed from the ROB of processor $i$ ( $ooo[i].rob$ ) in CCM+OOOVP and $L$ is executed correspondingly by $ps[i]$ in WMM. Assume that $L$ reads from store $S$ in CCM+OOOVP (via memory, store buffer or ROB). We consider the status of $S$ in CCM+OOOVP when $L$ is committed from ROB. If $S$ is still in the store buffer ( $ooo[i].sb$ ) or $ccm.m$ , then WMM can execute $L$ by reading from $ps[i].sb$ or $m$ . Otherwise $S$ must have been overwritten by another store in $ccm.m$ before $L$ is committed from ROB. In this case, WMM will insert the value of $S$ into $ps[i].ib$ when the overwrite happens in WMM, because there cannot be any store to $a$ in $ooo[i].sb$ at the time of the overwrite. Now we only need to show that the value of $S$ is not removed from $ps[i].ib$ by any store, $\mathsf{Reconcile}$ or load before $L$ is executed in WMM so that $L$ could read the value of $S$ from $ps[i].ib$ in WMM. We consider the time period after the overwrite and before the commit of $L$ in CCM+OOOVP, as well as the corresponding period in WMM (i.e. after the overwrite and before the execution of $L$ ). Since there cannot be any store to $a$ or $\mathsf{Reconcile}$ fence committed from $ooo[i].rob$ during that period (otherwise $L$ cannot read from $S$ ), the value of $S$ will not be removed from $ps[i].ib$ by stores or $\mathsf{Reconcile}$ fences during that period, and $ps[i].sb$ will not contain any store to $a$ when $L$ is executed. Furthermore, the CoRR axiom of CCM+OOOVP implies that each load $L^{\prime}$ to address $a$ committed from $ooo[i].rob$ during that period must read from either $S$ or another $S$ which writes $ccm.m$ before $S$ . Thus, the execution of $L^{\prime}$ in WMM cannot remove $S$ from $ps[i].ib$ , and $L$ can indeed read $S$ from $ps[i].ib$ . ∎

Theorem 2.

WMM $\subseteq$ CCM+OOOVP.

Proof.

For any WMM execution $E$ , we could construct a rule sequence $E^{\prime}$ in CCM+OOOVP, which has the same program behavior. The first part of $E^{\prime}$ is to fetch all instructions executed in $E$ into the ROB of each processor (using OOO-Fetch rules), then predict the value of every load to the result of that load in $E$ (using OOO-LdPred rules), and finally compute all $\mathsf{Nm}$ instructions, load/store addresses and store data. The rest of $E^{\prime}$ is to simulate each rule in WMM using the following way:

•

When a store is dequeued from $ps[i].sb$ and written into $m$ in WMM, we also fire the OOO-StReq and CCM-St rules consecutively to write that store into $ccm.m$ and dequeues it from $ooo[i].sb$ in CCM+OOOVP.

•

When an instruction $I$ is executed by $ps[i]$ in WMM, we commit $I$ from $ooo[i].rob$ in CCM+OOOVP. If $I$ is a $\mathsf{Ld}$ , we additionally schedule rules to execute this load in CCM+OOOVP:

–

If $I$ reads from $ps[i].sb$ in WMM, then we fire an OOO-LdBypass rule for $I$ right before it is committed from ROB.

–

If $I$ reads from $m$ in WMM, then we fire an OOO-LdReq rule and a CCM-Ld rule consecutively to execute it load right before it is committed from ROB.

–

If $I$ reads from $ps[i].ib$ , then we fire a OOO-LdReq rule and a CCM-Ld rule consecutively to execute it right before the load value (which $I$ gets in WMM) is overwritten in $ccm.m$ .

Although the construction of the rule sequence is not in order, the sequence constructed after every step is always a valid rule sequence in CCM+OOOVP for all instructions already executed by WMM. When we schedule rules for an instruction $I$ in CCM+OOOVP, the constructed $E^{\prime}$ does not contain any rule for instructions younger than $I$ in program order, and thus the rules for $I$ will not affect any existing rule in $E^{\prime}$ . Besides, all operations that the execution of $I$ depends on (e.g., executing an instruction older than $I$ , or writing a store, which $I$ will read from $ccm.m$ in the scheduled rule, into $ccm.m$ ) are already in the constructed $E^{\prime}$ , so the scheduled rules for $I$ will not depend on any rule scheduled in the future construction. We can prove inductively that the following invariants hold after each construction step:

The states of $m$ and all $sb$ in WMM are the same as the states of $ccm.m$ and all $sb$ in CCM+OOOVP. 2. 2.

All instructions executed in WMM have also been executed (with the same results) and committed from ROBs in CCM+OOOVP. 3. 3.

There is no ROB flush or load re-execution in $E^{\prime}$ .

The only non-trivial case is that a load $L$ to address $a$ reads the value of a store $S$ from $ps[i].ib$ in WMM. In this case, the overwrite of $S$ in $ccm.m$ must happen in the constructed $E^{\prime}$ , and $L$ must be in $ooo[i].rob$ at the time of overwrite. Since $S$ is inserted into $ps[i].ib$ and is not removed by any store or $\mathsf{Reconcile}$ before $L$ is executed in WMM, there is no store to $a$ or $\mathsf{Reconcile}$ fence older than $L$ in $ooo[i].rob$ or $ooo[i].sb$ right before the overwrite in CCM+OOOVP. Thus the OOO-LdReq and CCM-Ld rules are able to fire and read the value of $S$ at that time. The CoRR axiom of WMM implies that any load $L^{\prime}$ to $a$ which is older than $L$ must read from either $S$ or another store that writes $m$ before $S$ . Thus $L^{\prime}$ must get its result (not predicted values) before the overwrite in CCM+OOOVP, and $L$ cannot be killed by $L^{\prime}$ . ( $L$ cannot be killed or re-executed by any store because all OOO-StEx rules are fired at the beginning). ∎

6 Modeling Data Dependency

Current commercial processors do not use load-value speculation, and these processors can be modeled by CCM+OOOD, in which OOOD is derived by removing the value predictor $vp$ and related operations (e.g. the OOO-LdPred rule) from OOOVP. The removal of $vp$ implies the enforcement of data-dependency ordering in hardware (CCM+OOOD). For example, the behavior in Figure 11 is forbidden by CCM+OOOD. However, it requires inserting a $\mathsf{Reconcile}$ fence between $I_{4}$ and $I_{5}$ to forbid this behavior in WMM. This fence may cause performance loss because it would prevent the execution of loads that follow $I_{5}$ but do not depend on $I_{4}$ . This is an unnecessary cost if programs are running on commercial hardware captured by CCM+OOOD. To avoid extra $\mathsf{Reconcile}$ fences, we present WMM-D, an $\mathrm{I^{2}E}$ model equivalent to CCM+OOOD. WMM-D is derived from WMM by introducing timestamps to exclude exactly the behaviors that violate data-dependency orderings.

6.1 Enforcing Data Dependency with Timestamps

We derive our intuition for timestamps by observing how OOOD works. In Figure 11, assume instruction $I_{k}$ ( $k=1\ldots 5$ ) gets its result or writes memory at time $t_{k}$ in CCM+OOOD. Then $t_{5}\geq t_{4}$ because the result of $I_{4}$ is a source operand of $I_{5}$ (i.e. the load address). Since $I_{4}$ reads the value of $I_{3}$ from memory, $t_{4}\geq t_{3}$ , and thus $t_{5}\geq t_{3}\geq t_{1}$ . As we can see, the time ordering reflects enforcement of data dependencies. Thus, a natural way to extend WMM to WMM-D is to attach a timestamp to each value, which will, in turn, impose additional constraints on rule firing in WMM. Now we explain how to add timestamps to WMM to get WMM-D.

Let us assume there is a global clock which is incremented every time a store writes the monolithic memory. We attach a timestamp to each value in WMM, i.e. an architecture register value, the $\langle\mathrm{address,value}\rangle$ pair of a store, and a monolithic memory value. The timestamp represents when the value is created. Consider an instruction $r_{3}=r_{1}+r_{2}$ . The timestamp of the new value in $r_{3}$ will be the maximum timestamp of $r_{1}$ and $r_{2}$ . Similarly, the timestamp of the $\langle\mathrm{address,value}\rangle$ pair of a store ( $\mathsf{St}\ a\ v$ ), i.e. the creation time of the store, is the maximum timestamp of all source operands to compute $\langle a,v\rangle$ . The timestamp of a monolithic memory value is the time when the value becomes visible in memory, i.e. one plus the time when the value is stored.

Next consider a load $L$ ( $\mathsf{Ld}\ a$ ) on processor $i$ , which reads the value of a store $S$ ( $\mathsf{St}\ a\ v$ ). No matter how WMM executes $L$ (e.g. by reading $sb$ , memory, or $ib$ ), the timestamp $ts$ of the load value (i.e. the timestamp for the destination register) is always the maximum of (1) the timestamp $ats$ of the address operand, (2) the time $rts$ when processor $i$ executes the last $\mathsf{Reconcile}$ fence, and (3) the time $vts$ when $S$ becomes visible to processor $i$ . Both $ats$ and $rts$ are straightforward. As for $vts$ , if $S$ is from another processor $j$ ( $j\neq i$ ), then $S$ is visible after it writes memory, so $vts$ is timestamp of the monolithic memory value written by $S$ . Otherwise, $S$ is visible to processor $i$ after it is created, so $vts$ is the creation time of $S$ .

A constraint for $L$ , which we refer to as stale-timing, is that $ts$ must be $\leq$ the time $ts_{E}$ when $S$ is overwritten in memory. This constraint is only relevant when $L$ reads from $ib$ . This constraint is needed because a load cannot return a value in CCM+OOOD if the value has been overwritten in CCM at the time of load execution.

To carry out the above timestamp calculus for load $L$ in WMM, we need to associate the monolithic memory $m[a]$ with the creation time of $S$ and the processor that created $S$ , when $S$ updates $m[a]$ . When $S$ is overwritten and its $\langle a,v\rangle$ is inserted into $ps[i].ib$ , we need to attach the time interval $[vts,ts_{E}]$ (i.e. the duration that $S$ is visible to processor $i$ ) to that $\langle a,v\rangle$ in $ps[i].ib$ .

It should be noted that PC should never be involved in the timestamp mechanism of WMM-D, because the PC of each instruction can be known in advance due to the branch predictor $bp$ in OOOD.

By combining the above timestamp mechanism with the original WMM rules, we have derived WMM-D.

6.2 WMM-D Operational Semantics

Figure 12 shows the operational semantics of WMM-D. We list the things one should remember before reading the rules in the figure.

•

The global clock name is $gts$ (initialized as 0), which is incremented when the monolithic memory is updated.

•

Each register has a timestamp (initialized as 0) which indicates when the register value was created.

•

Each $sb$ entry $\langle a,v\rangle$ has a timestamp, i.e. the creation time of the store that made the entry. Timestamps are added to the method calls on $sb$ as appropriate.

•

Each monolithic memory location $m[a]$ is a tuple $\langle v,\langle i,sts\rangle,mts\rangle$ (initialized as $\langle 0,\langle\mathchar 45\relax,0\rangle,0\rangle$ ), in which $v$ is the memory value, $i$ is the processor that writes the value, $sts$ is the creation time of the store that writes the value, and $mts$ is the timestamp of the memory value (i.e. one plus the time of memory write).

•

Each $ib$ entry $\langle a,v\rangle$ has a time interval $[ts_{L},ts_{U}]$ , in which $ts_{L}$ is the time when $\langle a,v\rangle$ becomes visible to the processor of $ib$ , and $ts_{U}$ is the time when $\langle a,v\rangle$ is overwritten in memory and gets inserted into $ib$ . Thus, the $\mathsf{insert}$ method on $ib$ takes the time interval as an additional argument.

•

Each processor $ps[i]$ has a timestamp $rts$ (initialized as 0), which records when the latest $\mathsf{Reconcile}$ was executed by $ps[i]$ .

Some of the timestamp manipulation is done inside the decode and execute methods of each processor $ps[i]$ . Therefore we define the following methods:

•

$\mathsf{decodeTS}()$ : returns a pair $\langle dIns,ts\rangle$ , in which $dIns$ is the decoded instruction returned by the original $\mathsf{decode}()$ method, and $ts$ is the maximum timestamp of all source registers (excluding PC) of $dIns$ .

•

$\mathsf{executeTS}(dIns,ldRes,ts)$ : first calls the original method $\mathsf{execute}(dIns,ldRes)$ , and then writes timestamp $ts$ to the destination register of instruction $dIns$ .

We also replace the $\mathsf{getAny}$ method on $ib$ with the following two methods to facilitate the check of the stale-timing constraint:

•

$\mathsf{any}(a)$ : returns the $\langle\mathrm{value,time\ interval}\rangle$ pair of any stale value for address $a$ in $ib$ . If $ib$ does not contain any stale value for $a$ , $\langle\epsilon,\mathchar 45\relax\rangle$ is returned.

•

$\mathsf{rmOlder}(a,ts)$ : removes all stale values for address $a$ , which are inserted into $ib$ when $gts<ts$ , from $ib$ .

In Figure 12, WMM-D-Nm and WMM-D-St compute the timestamps of a $\mathsf{Nm}$ instruction result and a store $\langle a,v\rangle$ pair from the timestamps of source registers respectively. WMM-D-Rec updates $ps[i].rts$ with the current time because a $\mathsf{Reconcile}$ is executed. WMM-D-DeqSb attaches the appropriate time interval to the stale value inserted into $ib$ as described in Section 6.1.

In all three load execution rules (WMM-D-LdSb, WMM-D-LdMem, and WMM-D-LdIb), the timestamp of the load result is $\geq$ the timestamp of the address operand ( $ats$ ) and the latest $\mathsf{Reconcile}$ execution time ( $ps[i].rts$ ). Besides, the timestamp of the load result is also lower-bounded by the beginning time that the value is readable by the processor of the load ( $ps[i]$ ), In WMM-D-LdSb and WMM-D-LdIb, this beginning time (i.e. $sts$ or $ts_{L}$ ) is stored in the $sb$ or $ib$ entry; while in WMM-D-LdMem, this beginning time is one of the two times (i.e. $sts$ and $mts$ ) stored in the monolithic memory location depending on whether the memory value $v$ is written by $ps[i]$ (i.e. whether $i$ is equal to $j$ ). In WMM-D-LdIb, the stale-timing constraint requires that $\mathsf{max}(ats,ps[i].rts,ts_{L})$ (i.e. the timestamp of the load value) is no greater than $ts_{U}$ (i.e. the time when the stale value is overwritten). Here we only compare $ats$ with $ts_{U}$ , because $ts_{L}\leq ts_{U}$ is obvious, and the clearing of $ib$ done by $\mathsf{Reconcile}$ fences already ensures $ps[i].rts\leq ts_{U}$ .

6.3 Litmus Tests for WMM-D

Enforcing data dependency: First revisit the behavior in Figure 11. In WMM-D, the timestamp of the source operand of $I_{5}$ (i.e. the result of $I_{4}$ ) is 2, while the time interval of the stale value 0 for address $a$ in the $ib$ of P1 is $[0,0]$ . Thus $I_{5}$ cannot read 0 from $ib$ , and the behavior is forbidden. For a similar reason, WMM-D forbids the behavior in Figure 14, in which $I_{4}$ carries data dependency to $I_{7}$ transitively. This behavior is also impossible in CCM+OOOD.

Allowing other speculations: WMM-D still allows the behavior in Figure 11 which can result from memory dependency speculation in hardware. As we can see, WMM-D still allows implementations to speculate on all dependencies other than data dependency.

Loads to the same address: Remember that two loads to the same address can be executed out of order in OOOD as long as they read from the same store. WMM-D captures this subtle optimization. Consider the Read-from-Same-Write (RSW) program in Figure 14. The behavior is observable in CCM+OOOD, because $I_{7}$ to $I_{9}$ can be executed before $I_{4}$ to $I_{6}$ . It is fine for $I_{6}$ and $I_{7}$ , which read the same address $c$ , to be executed out-of-order, because they both read from the initialization store. WMM-D allows this behavior, because the timestamp of the address operand of $I_{9}$ is 0, and $I_{9}$ can read stale value 0 from $ib$ . (This behavior is also observable on POWER and ARM processors Sarkar et al. [2011]; Flur et al. [2016]).

6.4 Equivalence of WMM-D and CCM+OOOD

To simplify the proof, we change the $\mathsf{findBypass}(idx)$ method in OOOD to return $\epsilon$ whenever there is a $\mathsf{Reconcile}$ fence at index smaller than $idx$ in ROB, i.e. a load will always be stalled when there is an older $\mathsf{Reconcile}$ in ROB. This change in $\mathsf{findBypass}$ only affects one scenario: a load used to be able to bypass from a store when there is a $\mathsf{Reconcile}$ fence older than both the load and store in ROB, and operations dependent on the load result could used to be done before the $\mathsf{Reconcile}$ is committed from ROB. Since the bypass and those dependent operations are all local to the processor, they can still be performed with the same effects immediately after the $\mathsf{Reconcile}$ is committed from ROB. Thus, the change in $\mathsf{findBypass}$ does not affect the semantics of OOOD.

Theorem 3.

CCM+OOOD $\subseteq$ WMM-D.

Proof.

We also introduce the global clock $gts$ to CCM+OOOD; $gts$ is be incremented whenever the CCM-St fires. This proof is almost the same as that of Theorem 1 except for a new invariant: The timestamp computed for each instruction result (i.e. $\mathsf{Nm}$ result, store address and data, and load value) in WMM-D is $\leq$ the the value of $gts$ when the instruction gets its result in CCM+OOOD. See Appendix A for the complete proof. ∎

Theorem 4.

WMM-D $\subseteq$ CCM+OOOD.

Proof.

We also introduce the global clock $gts$ to CCM+OOOD, $gts$ is be incremented whenever the CCM-St fires. This proof is similar to the proof for Theorem 2 except for the following two points:

Without a value predictor in OOOD, the time when an instruction can be executed in CCM+OOOD is subject to when the source operands of the instruction become ready. When constructing the execution for CCM+OOOD (to simulate the behavior of WMM-D), we always fire the instruction execution rule as early as possible. In particular for each $\mathsf{Ld}$ instruction, we execute it (by firing the OOO-LdAddr and OOO-LdBypass rules or the OOO-LdAddr, OOO-LdReq, and CCM-Ld rules) as soon as the source operands are ready and the expected load value (i.e. the value read in WMM-D) becomes visible to the processor. 2. 2.

A new invariant: the value of $gts$ in CCM+OOOD when an instruction gets its result ( $\mathsf{Nm}$ result, store address and data, or load value) is equal to the timestamp of that result in WMM-D.

See Appendix A for the complete proof. ∎

7 Modeling Multi-Copy Non-Atomic Stores

Unlike the multi-copy atomic stores in WMM, stores in ARM and POWER multiprocessors are multi-copy non-atomic, i.e. a store may become visible to different processors at different times. This is caused by sharing store buffers or write-through caches in the memory system. If multiple threads share a store buffer or a write-through cache, a store by any of these threads may be seen by all these threads before other processors. Although we could tag stores with thread IDs in the store buffer, it is infeasible to distinguish between stores by different threads in the write-through cache. While CCM cannot model such store behaviors, the storage subsystem of the Flowing model is believed to have captured precisely the behaviors of this multi-copy non-atomicity given a topology of the hierarchy of shared store buffers or write-through caches Flur et al. [2016].

In this section, we first introduce a new $\mathrm{I^{2}E}$ model, WMM-S, which captures the multi-copy non-atomic store behaviors in a topology-independent way. WMM-S is derived from WMM by changing the store buffers to a new conceptual device: dynamic store buffers. Next we introduce HMB+OOOS, the physical model for multiprocessors with multi-copy non-atomic stores; HMB is the memory abstraction taken from the Flowing model and OOOS is the processor model adapted from OOOVP. We will finally prove HMB+OOOS $\subseteq$ WMM-S.

7.1 WMM-S: Copying From One Store Buffer into Another

We can model the multi-copy non-atomicity of stores by introducing a background rule to make copies of a store in a store buffer into other store buffers. We refer to these store buffers with the ability of copying stores as dynamic store buffers. (We will still use store buffers to refer to dynamic store buffers in the rest of this section). However, we need to ensure that all stores for an address can be put in a total order, i.e. the coherent order ( $\xrightarrow{co}$ ), and the order seen by any processor is consistent with this total order (i.e. SC for a single address). WMM-S is an $\mathrm{I^{2}E}$ model to generate such behaviors.

To identify all the copies of a store in various store buffers, we assign a unique tag $t$ when a store is inserted in the store buffer, and this tag is copied when a store is copied from one store buffer to another. When a store is committed from the store buffer to the memory, all its copies must be deleted from all the store buffers which have them. A store can be committed only if all its copies are the oldest store for that address in their respective store buffers.

All the stores for an address in a store buffer are kept as a strictly ordered list, where the youngest store is the one that entered the store buffer last. We make sure that all ordered lists are can be combined transitively to form a strict partial order, which has now to be understood in terms of the tags on stores because of the copies. By the end of the program, this partial order on the stores for an address becomes the coherence order, so we refer to this partial order as the partial coherence order.

Consider the states of store buffers shown in Figure 15. $A$ , $B$ , $C$ and $D$ are different stores to the same address, and their tags are $t_{A}$ , $t_{B}$ , $t_{C}$ and $t_{D}$ , respectively. $A^{\prime}$ and $B^{\prime}$ are copies of $A$ and $B$ respectively created by the background copy rule. Ignoring $C^{\prime}$ , the partial coherence order contains: $t_{D}\xrightarrow{co}t_{B}\xrightarrow{co}t_{A}$ ( $D$ is older than $B$ , and $B$ is older than $A^{\prime}$ in P2), and $t_{C}\xrightarrow{co}t_{B}$ ( $C$ is older than $B^{\prime}$ in P3). Note that $t_{D}$ and $t_{C}$ are not related here.

At this point, if we copied $C$ in P3 as $C^{\prime}$ into P1, we would add a new edge $t_{A}\xrightarrow{co}t_{C}$ , which would break the partial order by introducing the cycle $t_{A}\xrightarrow{co}t_{C}\xrightarrow{co}t_{B}\xrightarrow{co}t_{A}$ . Therefore copying of $C$ into P1 should not be allowed in this state. Similarly, copying a store with tag $t_{A}$ into P1 or P2 should be forbidden because it would immediately create a cycle: $t_{A}\xrightarrow{co}t_{A}$ . In general, the background copy rule must be constrained so that invariance of the partial coherence order after copying is maintained.

The operational semantics of WMM-S is defined by adding/replacing three rules to that of WMM (Figure 7). These new rules are shown in Figure 16: A new background rule WMM-S-Copy is added to WMM and the WMM-S-St and WMM-S-DeqSb rules replace the WMM-St and WMM-DeqSb rules of WMM, respectively. Before reading these new rules, one should note the following facts:

•

The $\mathsf{decode}$ method now returns $\langle\mathsf{St},a,v,t\rangle$ for a store, in which $t$ is the unique tag assigned to the store. Each store buffer entry becomes a tuple $\langle a,v,t\rangle$ , in which $t$ is the tag. Tags are also introduced into the methods of $sb$ appropriately.

•

The $sb$ now has the following three methods:

–

$\mathsf{hasTag}(t)$ : returns $\mathsf{True}$ if $sb$ contains a store with tag $t$ .

–

$\mathsf{oldest}(a)$ : returns the $\langle\mathrm{value,tag}\rangle$ pair of the oldest store to address $a$ in $sb$ . It returns $\langle\epsilon,\epsilon\rangle$ if $sb$ does not contain $a$ .

–

$\mathsf{any}()$ : returns the $\langle\mathrm{address,value,tag}\rangle$ tuple of any store present in $sb$ . It returns $\langle\epsilon,\epsilon,\epsilon\rangle$ if $sb$ is empty.

•

A new function $\mathsf{noCycle}(a,t,j)$ is defined to check whether the background rule could copy a store with tag $t$ for address $a$ into the $sb$ of processor $j$ . It returns $\mathsf{True}$ if the partial coherence order among the tags of all stores for address $a$ does not contain any cycle after doing the copy.

In Figure 16, WMM-S-St simply introduces the store tag to the original WMM-St rule. In WMM-S-DeqSb, when we write a store ( $\langle a,v,t\rangle$ ) into memory, we ensure that each copy of this store is the oldest one to address $a$ in its respective $sb$ . The old memory value is inserted into the $ib$ of each processor whose $sb$ does not contain address $a$ . WMM-S-Copy copies a store ( $\langle a,v,t\rangle$ ) from $ps[i]$ to $ps[j]$ . The check on $\mathsf{noCycle}(a,t,j)$ guarantees that no cycle is formed in the partial coherence order after the copy. Copying stores from $ps[i]$ to $ps[i]$ will be automatically rejected because $\mathsf{noCycle}$ will return $\mathsf{False}$ . Since we enqueue a store into $ps[j].sb$ , we need to remove all stale values for address $a$ from $ps[j].ib$ .

WMM-S still use the WMM-Com to execute a $\mathsf{Commit}$ fence, but this rules has very different implications here. In WMM-S, a store cannot be moved from $sb$ to memory unless all its copies in other store buffers can be moved at the same time. Hence the effect of a $\mathsf{Commit}$ fence is not local; it implicitly affects all other store buffers. In literature, such fences are known as cumulative.

7.2 Litmus Tests for WMM-S

We show by examples that WMM-S allows multi-copy non-atomic store behaviors, and that fences in WMM-S have the cumulative properties similar to those in POWER and ARM memory models.

We first consider the Write-Write Causality (WWC) example in Figure 18 (which is forbidden by WMM). WMM-S allows this behavior by first copying $I_{1}$ into the $sb$ of P2 to let all instructions on P2 and P3 proceed. $I_{1}$ will write memory only after $I_{5}$ has done so. This behavior is allowed in hardware in case a store buffer is shared by P1 and P2 but not P3. To forbid this behavior in WMM-S, a $\mathsf{Commit}$ fence is required between $I_{2}$ and $I_{3}$ on P2 to push $I_{1}$ into memory. The inserted $\mathsf{Commit}$ fence has a cumulative global effect in ordering $I_{1}$ before $I_{3}$ (and hence $I_{5}$ ).

Figure 18 shows another well-known example called Independent Reads of Independent Writes (IRIW), which is forbidden by WMM. WMM-S allows this by copying $I_{1}$ and $I_{2}$ into the $sb$ of P3 and P4 respectively. This behavior is possible in hardware, in case P1 and P3 shares a store buffer while P2 and P4 shares a different one.

To forbid the behavior in Figure 18 in WMM-S, we can insert a $\mathsf{Commit}$ fence between $I_{3}$ and $I_{4}$ on P3, and another $\mathsf{Commit}$ fence between $I_{6}$ and $I_{7}$ on P4. As we can see, a $\mathsf{Commit}$ followed by a $\mathsf{Reconcile}$ in WMM-S has a similar effect as the POWER $\mathsf{sync}$ fence and the ARM $\mathsf{dmb}$ fence. Cumulation is achieved by globally advertising observed stores ( $\mathsf{Commit}$ ) and preventing later loads from reading stale values ( $\mathsf{Reconcile}$ ).

7.3 HMB+OOOS: a Physical Model for Muiltiprocessors with Multi-Copy Non-Atomic Memory

For clarity of discussion, we reiterate the important concepts of the original Flowing model (see Section 7.1 $\sim$ 7.4 in Flur et al. [2016]) while describing the changes made for HMB due the differences in the fences of WMM-S and ARM. HMB has $n$ ports, each of which will be connected to a processor. In addition to the $\mathsf{reqLd}(idx,a)$ and $\mathsf{reqSt}(a,v,t)$ port methods ( $idx$ is the ROB index, i.e. the load request tag, and $t$ is the unique store tag), HMB provides a $\mathsf{reqCom}()$ port method so that the processor could send a $\mathsf{Commit}$ fence (instead of the ARM $\mathsf{dmb}$ fence) as a barrier request into the memory system. Inside HMB, there are $k$ segments $s[1\ldots k]$ , and a monolithic memory $m$ (same as the one in CCM). All the segments and the monolithic memory are connected together into a tree rooted at $m$ . Each segment contains a list of memory requests (i.e. loads, stores and $\mathsf{Commit}$ ). Each port of HMB is connected to a segment in the tree, and the port methods (i.e. $\mathsf{reqLd}$ , $\mathsf{reqSt}$ and $\mathsf{reqCom}$ ) simply add the new request to the top of the list of the connected segment. HMB has the following three internal rules:

HMB-Reorder: Two consecutive requests $r_{new}$ and $r_{old}$ in the same segment ( $r_{new}$ is closer to the top of the list of the segment) can be reordered except for the following two cases:

(a)

$r_{new}$ and $r_{old}$ are memory accesses to the same address. 2. (b)

$r_{new}$ is a $\mathsf{Commit}$ and $r_{old}$ is a store. 2. 2.

HMB-Bypass: When a load request $r=\langle\mathsf{Ld},pid,idx,a\rangle$ (i.e. a load to address $a$ from the ROB entry with index $idx$ of processor $pid$ ) and a store request $r^{\prime}=\langle\mathsf{St},a,v,t\rangle$ (i.e. a store to address $a$ with data $v$ and tag $t$ ) are two consecutive requests in the segment and $r^{\prime}$ is closer to the bottom of the segment, we can remove $r$ from the segment and call method $\mathsf{respLd}(idx,v,t)$ of processor $pid$ (i.e. $r$ is satisfied by $r^{\prime}$ ). 3. 3.

HMB-Flow: The request $r$ at the bottom of segment $s[i]$ can be removed from $s[i]$ . If the parent of $s[i]$ is another segment $s[j]$ , we add $r$ to the top of $s[j]$ (i.e. $r$ flows from $s[i]$ to its parent $s[j]$ ). Otherwise, the parent of $s[i]$ is $m$ , and we take the following actions according to the type of $r$ :

•

If $r$ is $\langle\mathsf{Ld},pid,idx,a\rangle$ , we call method $\mathsf{respLd}(idx,v,t)$ of processor $pid$ , in which pair $\langle v,t\rangle$ is the current state of $m[a]$ .

•

If $r$ is $\langle\mathsf{Commit},pid\rangle$ , i.e. a $\mathsf{Commit}$ fence from processor $pid$ , we call method $\mathsf{respCom}()$ (which is defined later) of processor $pid$ to indicate the completion of the fence.

•

If $r$ is $\langle\mathsf{St},a,v,t\rangle$ , we update $m[a]$ to be $\langle v,t\rangle$ . No response is sent for the store request.

We adapt OOOVP to OOOS to fit the new memory system. The operational semantics (the changed part) and the interface methods of OOOS are shown in Figures 20 and 20 respectively, where $hmb$ represents the HMB interface port connected to the processor, and method $rob.\mathsf{setCommit}(en)$ sets the commit slot of ROB to $en$ .

The first change for OOOS is to remove $sb$ from each processor, because store buffering is already modeled inside HMB. Thus when a store is committed from ROB in rule OOOS-StCom, the store request is directly sent to HMB. The second change is sending a $\mathsf{Commit}$ request to HMB when a $\mathsf{Commit}$ fence reaches the commit slot of ROB as shown in rule OOOS-ComReq. When the $\mathsf{Commit}$ response comes back from HMB via method $\mathsf{respCom}$ , the fence is committed from ROB. To avoid duplicate $\mathsf{Commit}$ requests to HMB, we change function $\mathsf{initEx}$ to also return $\mathsf{Idle}$ for a $\mathsf{Commit}$ fence, and hence the $ex$ field of a $\mathsf{Commit}$ fence will be set to $\mathsf{Idle}$ in rule OOO-Fetch. When the $\mathsf{Commit}$ request is sent to HMB in rule OOOS-ComReq, we set the $ex$ field to $\mathsf{Exe}$ .

The last change is about detecting whether the out-of-order execution of loads to the same address in the same processor violates SC for single address. The detection is harder in case of HMB than that in CCM, because loads can be satisfied in any segment or monolithic memory inside HMB, while loads can only be satisfied in the monolithic memory in case of CCM. The original Flowing model has specified complicated conditions of this check to avoid unnecessary flush of loads, but we believe those conditions may still cause some loads to be flushed unnecessarily. Instead of further complicating the check, we simply guarantee that loads to the same address are issued to HMB in order. Since HMB keeps the order of memory accesses to the same address, this can ensure SC for single address. Rule OOOS-LdReq enforces the in-order issue by killing younger loads in the same way as the OOO-StEx rule does. This also makes OOOS+CCM obey the CoRR and CoWR axioms (see Appendix C for the proof).

7.4 WMM-S Abstracting HMB+OOOS

Theorem 5.

HMB+OOOS $\subseteq$ WMM-S.

Proof.

Similar to the proof of Theorem 1, we only consider executions in HMB+OOOS without any ROB flush or load re-execution. At any moment in HMB+OOOS, we define a store $S$ is observed by commits of processor $i$ ( $ooo[i]$ ) if and only if $S$ has been committed from $ooo[i].rob$ or $S$ has been returned by a load $L$ which has been committed from $ooo[i].rob$ . For two stores $S_{1}$ and $S_{2}$ both observed by commits of a processor, we say $S_{1}$ is closer to the root than $S_{2}$ in HMB, when the segment of $S_{1}$ is closer to the root than that of $S_{2}$ in the tree hierarchy of HMB (assuming each edge in the tree has length 1), or when $S_{1}$ and $S_{2}$ are in the same segment and $S_{1}$ is closer to the bottom of the segment.

For any execution $E$ in HMB+OOOS, we simulate it in WMM-S using the following way:

•

When a store request flows into the monolithic memory inside HMB ( $hmb.m$ ) using the HMB-Flow rule of HMB+OOOS, WMM-S fires a WMM-S-DeqSb rule to dequeue that store from all store buffers and write it into the monolithic memory ( $m$ ).

•

When a $\mathsf{Nm}$ , $\mathsf{Reconcile}$ , or $\mathsf{St}$ instruction is committed from ROB in HMB+OOOS, we execute that instruction in WMM-S.

•

When a $\mathsf{Commit}$ fence is committed from ROB in the $\mathsf{respCom}$ method called by a HMB-Flow rule in HMB+OOOS, we execute that fence in WMM-S.

•

When a $\mathsf{Ld}$ instruction $L$ , which reads from a store $S$ , is committed from $ooo[i].rob$ in HMB+OOOS, we execute $L$ using the following actions in WMM-S according to the status of $S$ right before the commit of $L$ in HMB+OOOS:

–

If $S$ is in $hmb.m$ at that time, then WMM-S executes $L$ by reading from $m$ .

–

If $S$ has been overwritten in $hmb.m$ before the commit of $L$ , then $L$ can read $ps[i].ib$ in WMM-S.

–

If $S$ is in a segment inside HMB at that time, then $L$ should read $ps[i].sb$ in WMM-S. In case $S$ is not observed by commits of $ooo[i]$ right before the commit of $L$ , we fire a WMM-S-Copy rule to copy $S$ into $ps[i].sb$ right before $L$ reads $ps[i].sb$ .

After each step of the simulation, we could prove inductively that the following invariants hold:

All stores in $ps[i].sb$ in WMM-S are exactly the set of stores, which are in the segments of HMB and observed by commits of $ooo[i]$ . The segments that contain these stores must be on the path from the root to port $i$ in the tree hierarchy of HMB. 2. 2.

In case $S_{1}$ and $S_{2}$ are two stores to the same address in $ps[i].sb$ , $S_{1}$ is older than $S_{2}$ in $ps[i].sb$ if and only if $S_{1}$ is closer to the root than $S_{2}$ in HMB.

We do not take any action in WMM-S when requests flow between segments in HMB or when requests are reordered in HMB. These operations in HMB+OOOS do not affect the above invariants.

Here we only consider the final case, i.e. a load $L$ to address $a$ , which reads from a store $S$ , is committed from $ooo[i].sb$ in HMB+OOOS, and $S$ remains in a segment of HMB at the commit time of $L$ . If $S$ has already been observed by commits of $ooo[i]$ before the commit of $L$ , the CoRR and CoWR axioms of HMB+OOOS imply that there cannot be any store to $a$ which is also observed by commits of $ooo[i]$ and is further from root than $S$ in HMB. Thus, $S$ must be the youngest store to $a$ in $ps[i].sb$ and $L$ can read from it in WMM-S. Otherwise, $S$ is not observed by commits of $ooo[i]$ right before the commit of $L$ , and the CoRR and CoWR axioms of HMB+OOOS imply that $S$ must be further from root in the tree hierarchy of HMB than any store observed by commits of $ooo[i]$ at that time. Therefore, if we insert $S$ into $ps[i].sb$ , both invariants still hold. Since there is no cycle in the tree hierarchy of HMB and the order of stores to the same address in any store buffer in WMM-S is the same as the order of distance from the root of those stores in HMB, the $\mathsf{noCycle}$ check in the WMM-S-Copy rule which copies $S$ into $ps[i].sb$ must succeed. Then $L$ can read from $S$ in $ps[i].sb$ .

See Appendix B for remaining cases. ∎

8 Conclusion

We provide a framework which uses simple hardware abstractions based on $\mathrm{I^{2}E}$ processors, monolithic memory, invalidation buffers, timestamps and dynamic store buffers to capture all microarchitectural optimizations present in modern processors. We have proved the equivalences between the simple abstractions and their realistic microarchitectural counterparts; we believe this work can be useful for both programmers to reason about their programs on real hardware, and on architects to reason about the effect of their optimizations on program behavior.

Appendix A Proof of Equivalence Between WMM-D and CCM+OOOD

Theorem 3.

CCM+OOOD $\subseteq$ WMM-D.

Proof.

In order to relate the time in CCM+OOOD to that in WMM-D, we also introduce the global clock $gts$ to CCM+OOOD. $gts$ is be incremented by one whenever the CCM-St rule fires, i.e. when the monolithic memory of CCM ( $ccm.m$ ) is written. In the rest of this proof, we mean the value of $gts$ when referring to time. Similar to the proof of Theorem 1 (i.e. CCM+OOOVP $\subseteq$ WMM in the paper), we only need to consider executions in CCM+OOOD without any ROB flush or load re-execution.

For any execution $E$ in CCM+OOOD, we simulate it using the same way as in the proof of Theorem 1, i.e. when CCM+OOOD commits an instruction from ROB or writes a store into $ccm.m$ , WMM-D executes that instruction or writes that store into $m$ . After each step of simulation, we maintain the following invariants ( $ooo[i]$ represents processor $i$ in CCM+OOOD):

The states of $m$ and all $sb$ in WMM are the same as $ccm.m$ and all $sb$ in CCM+OOOD. 2. 2.

The $gts$ in WMM is the same as that in CCM+OOOD. 3. 3.

All instructions committed from ROBs in CCM+OOOD have also been executed with the same results in WMM. 4. 4.

The $rts$ of each processor $ps[i]$ in WMM is equal to the time when the last $\mathsf{Reconcile}$ fence is committed from $ooo[i].rob$ . 5. 5.

The timestamp of the result of each $\mathsf{Nm}$ or $\mathsf{Ld}$ instruction in WMM is $\leq$ the time when the instruction gets its result in CCM+OOOD by the OOO-NmEx, OOO-LdBypass, or CCM-Ld rule. 6. 6.

The timestamp of each store in any $sb$ in WMM is $\leq$ the time when the store is executed in CCM+OOOD by the OOO-StEx rule. 7. 7.

For each monolithic memory location $m[a]=\langle v,\langle i,sts\rangle,mts\rangle$ in WMM, $sts$ is $\leq$ the time when the store that writes $v$ to memory is executed in $ooo[i].rob$ in CCM+OOOD, and $mts$ is equal to the time right after that store writes $ccm.m$ in CCM+OOOD. 8. 8.

For each invalidation buffer entry $\langle a,v,[ts_{L},ts_{U}]\rangle$ of $ps[i].ib$ in WMM, $ts_{U}$ is the time right before value $v$ is overwritten by another store in $ccm.m$ . If the store that writes $v$ to memory is from processor $i$ , then $ts_{L}$ is $\leq$ the time when that store is executed in $ooo[i].rob$ by the OOO-StEx rule. Otherwise, $ts_{L}$ is equal to the time right after $v$ is written to $ccm.m$ .

The above invariants can be proved inductively in the same way used in the proof of Theorem 1.

In particular, we consider the case that CCM+OOOD commits a load $L$ to address $a$ , which reads the value of store $S$ , from $ooo[i].rob$ . In this case, WMM executes $L$ on $ps[i]$ according to the status of $S$ in CCM+OOOD when $L$ is committed from $ooo[i].rob$ :

•

If $S$ is still in $ooo[i].sb$ when $L$ commits from ROB, then WMM-D can execute $L$ by reading $ps[i].sb$ (i.e. the WMM-D-LdMem rule).

•

If $S$ is in $ccm.m$ at that time, then WMM-D executes $L$ by reading $m$ (i.e. the WMM-D-LdMem rule). Note that $S$ may be from processor $i$ or another processor $j$ . In either case, the WMM-D-LdMem rule maintains all the invariants.

•

The final case is that $S$ has been overwritten by another store in $ccm.m$ before $L$ is committed from ROB. In this case, WMM-D executes $L$ by reading $ps[i].ib$ (i.e. the WMM-D-LdIb rule). For the same reason used in the proof of Theorem 1, the value of $S$ will be in $ps[i].ib$ when $L$ is executed in WMM-D. We assume the time interval of $S$ in $ps[i].ib$ is $[ts_{L},ts_{U}]$ . The guard of the WMM-D-LdIb rule, i.e. $ats<ts_{U}$ ( $ats$ is the timestamp of the load address), will be satisfied, because timestamps in WMM is always $\leq$ the corresponding time in CCM+OOOD, and the source register values for the load address must have been computed before the load value is overwritten in $ccm.m$ in CCM+OOOD. No matter $S$ is from processor $i$ or another processor, the way of setting $ts_{L}$ when $S$ is inserted into $ps[i].ib$ ensures that the timestamp computed for the load result in the WMM-D-LdIb rule conforms to all the invariants.

∎

Theorem 4.

WMM-D $\subseteq$ CCM+OOOD.

Proof.

We still introduce $gts$ into CCM+OOOD, and $gts$ is incremented by one whenever a store writes $ccm.m$ . Since multiple rules of CCM+OOOD may fire under the same $gts$ , we introduce a pair $\langle ut,lt\rangle$ to specify the exact time when each rule fires; $ut$ is the upper time, which specifies the value of $gts$ when the rule fires; $lt$ is the lower time, a rational number inside $(0,1]$ , which is used to order rules with the same upper time. When comparing two time pairs, we first compare the $ut$ part, and only compare the $lt$ part when $ut$ parts are equal. All OOO-StReq rules must have $lt=1$ , while all other rules in CCM+OOOD must have $0<lt<1$ .

For any WMM execution $E$ , we could construct a rule sequence $E^{\prime}$ in CCM+OOOD, which has the same program behavior. In the construction of $E^{\prime}$ , we always fire the OOO-StReq and CCM-St rules atomically to write a store to $ccm.m$ , so we only use OOO-StReq to denote this sequence in the rest of the proof. Similarly, we always fire OOO-LdAddr and OOO-LdBypass atomically to forward data to a load, and always fire OOO-LdAddr, OOO-LdReq, and CCM-Ld rules atomically to satisfy a load from $ccm.m$ , so we will only mention the OOO-LdBypass and OOO-LdReq rules to refer to the above two atomic sequences in the rest of the proof.

The first part of $E^{\prime}$ is to fetch all instructions executed in $E$ into the ROB of each processor (using OOO-Fetch rules). The construction of the rest of $E^{\prime}$ is similar to that in the proof of Theorem 2 (i.e. WMM $\subseteq$ CCM+OOOVP in the paper), i.e. when WMM-D writes a store to $m$ or executes an instruction, we write that store to $ccm.m$ or schedule rules to execute and commit that instruction in CCM+OOOD. We maintain the following invariants after each step of construction (the states of CCM+OOOD refers to the states after firing all rules in the constructed $E^{\prime}$ ):

The states of $m$ and all $sb$ in WMM are the same as the states of $ccm.m$ and all $sb$ in CCM+OOOD. 2. 2.

The $gts$ in WMM is the same as that in CCM+OOOD. 3. 3.

The upper time assigned to each rule in $E^{\prime}$ is equal to the value of $gts$ when the rule fires. The lower time assigned to each OOO-StReq is 1, while the lower time assigned to each other rule is within $(0,1)$ . 4. 4.

All instructions executed in WMM have also been executed (with the same results) and committed from ROBs in CCM+OOOD. 5. 5.

The value of $gts$ when each instruction is executed or each store is written into $m$ in WMM-D is equal to the upper time of the rule to commit that instruction from ROB or write that store to $ccm.m$ in CCM+OOOD. 6. 6.

For each $\mathsf{Nm}$ , $\mathsf{St}$ or $\mathsf{Ld}$ instruction executed in WMM-D, the timestamp computed for the execution result (i.e. $\mathsf{Nm}$ instruction result, store address and data, or load result) in WMM-D is equal to the upper time of corresponding rule in CCM+OOOD (i.e. OOO-NmEx, OOO-StEx, OOO-LdBypass, or OOO-LdReq) that executes the instruction. 7. 7.

No flush or load re-execution happens in any ROB.

Besides proving the above invariants, we also need to show that the rules scheduled in $E^{\prime}$ can indeed fire, e.g., the time of a rule to execute an instruction is smaller than the time of committing that instruction, but is larger than the time of each rule that computes the source operand of that instruction.

The detailed way of constructing $E^{\prime}$ to simulate each rule in WMM is shown below (the current states of CCM+OOOD refers to the states after firing all existing rules in the constructed $E^{\prime}$ ):

•

When WMM-D writes a store from $ps[i].sb$ into $m$ , we fire the OOO-StReq rule to write that store from $ooo[i].sb$ to $ccm.m$ at time $\langle ut,1\rangle$ in $E^{\prime}$ , in which $ut$ is the current $gts$ in CCM+OOOD.

•

When an instruction $I$ is executed by $ps[i]$ in WMM-D, we commit $I$ from $ooo[i].rob$ in $E^{\prime}$ at time $\langle ut_{c},lt_{c}\rangle$ , in which $ut_{c}$ is the current $gts$ in CCM+OOOD, and $lt_{c}$ is chosen so that this commit rule happens after all existing rules in $E^{\prime}$ . If $I$ is $\mathsf{Nm}$ , $\mathsf{St}$ or $\mathsf{Ld}$ , we also need to schedule rules to execute it. Assume the maximum time among all the rules to compute the source register values of $I$ is $\langle ut_{a},lt_{a}\rangle$ . (All such rules must have been scheduled in the previous construction steps).

–

If $I$ is $\mathsf{Nm}$ or $\mathsf{St}$ , then we schedule the corresponding OOO-NmEx or OOO-StEx rule for $I$ to fire at time $\langle ut_{a},lt_{a}^{\prime}\rangle$ . $lt_{a}^{\prime}$ is chosen so that $lt_{a}<lt_{a}^{\prime}<1$ and $\langle ut_{a},lt_{a}^{\prime}\rangle<\langle ut_{c},lt_{c}\rangle$ .

–

If $I$ is $\mathsf{Ld}$ , we assume that $I$ reads from a store $S$ in $E$ , and that $ooo[i]$ commits the last $\mathsf{Reconcile}$ older than $I$ at time $\langle ut_{r},lt_{r}\rangle$ in the previously constructed $E^{\prime}$ .

If $S$ and $I$ are from the same processor (i.e. $ooo[i]$ ), let $\langle ut_{s},lt_{s}\rangle$ be the time of the OOO-StEx rule for $S$ in the previously constructed $E^{\prime}$ . We fire either a OOO-LdBypass rule or a OOO-LdReq rule (depending on where $S$ is at the rule firing time) to execute $I$ in $E^{\prime}$ at time $\langle ut_{e},lt_{e}\rangle$ , in which $ut_{e}=\max(ut_{a},ut_{r},ut_{s})$ . $lt_{e}$ is chosen so that $\langle ut_{c},lt_{c}\rangle>\langle ut_{e},lt_{e}\rangle>\max(\langle ut_{a},lt_{a}\rangle,\langle ut_{r},lt_{r}\rangle,\langle ut_{s},lt_{s}\rangle)$ and $0<lt_{e}<1$ .

*

Otherwise, $S$ and $I$ are from different processors, and let $\langle ut_{w},1\rangle$ be the time of the OOO-StReq rule that writes $S$ into $ccm.m$ in the previously constructed $E^{\prime}$ . We fire a OOO-LdReq rule to execute $I$ at time $\langle ut_{e},lt_{e}\rangle$ , in which $ut_{e}=\max(ut_{a},ut_{r},ut_{w}+1)$ . $lt_{e}$ is chosen so that $\langle ut_{c},lt_{c}\rangle>\langle ut_{e},lt_{e}\rangle>\max(\langle ut_{a},lt_{a}\rangle,\langle ut_{r},lt_{r}\rangle)$ and $0<lt_{e}<1$ .

Note that $lt_{e}$ always exists, because $\langle ut_{c},lt_{c}\rangle$ is larger than the time of any existing rule in $E^{\prime}$ .

Similar to the proof of Theorem 2, the construction of $E^{\prime}$ here is not in order, but the $E^{\prime}$ constructed after every step is always a valid rule sequence in CCM+OOOD for all instructions already executed by WMM-D. For the same reason in the proof of Theorem 2, when we schedule rules for instruction $I$ in a construction step, the rules for $I$ will neither affect any existing rule in $E^{\prime}$ nor depend on any rule scheduled in future construction steps. We can prove inductively that the invariants hold and the scheduled rules in $E^{\prime}$ can indeed fire after each step of construction.

The only non-trivial case is when $ps[i]$ in WMM-D executes a $\mathsf{Ld}\ a$ instruction $I$ , which reads the value of a store $S$ from $ps[j]$ ( $j$ may or may not be equal to $i$ ). (In the following proof we will directly use the time variables, e.g. $ut_{a},lt_{a},ut_{e},lt_{e}$ , etc., in the above description of the construction step for $I$ ). Due to the way of choosing $\langle ut_{e},lt_{e}\rangle$ , at time $\langle ut_{e},lt_{e}\rangle$ in CCM+OOOD, we are able to compute the load address for $I$ , and all $\mathsf{Reconcile}$ fences older than $I$ have been committed from $ooo[i].rob$ . Thus, $I$ could be executed in CCM+OOOD at that time. Furthermore, if $i$ is equal to $j$ , then store address and data of $S$ must have been computed before $\langle ut_{e},lt_{e}\rangle$ in the constructed $E^{\prime}$ (because $\langle ut_{s},lt_{s}\rangle<\langle ut_{e},lt_{e}\rangle$ ); otherwise $S$ must have been written into $ccm.m$ before $\langle ut_{e},lt_{e}\rangle$ in the constructed $E^{\prime}$ (because $\langle ut_{w},1\rangle<\langle ut_{e},lt_{e}\rangle$ ). That is, $S$ is visible to $ooo[i]$ at time $\langle ut_{e},lt_{e}\rangle$ . Besides, $ats$ and $ps[i].rts$ in the WMM-D rule to execute $I$ (i.e. WMM-D-LdIb, WMM-D-LdMem or WMM-D-LdSb) are always equal to $ut_{a}$ and $ut_{r}$ respectively according to the invariants. The rest of the proof depends on how $I$ is executed in WMM-D.

•

$I$ ** is executed by reading $ps[i].ib$ (i.e. the WMM-D-LdIb rule):**

For the time interval $[ts_{L},ts_{U}]$ of the $ib$ entry read in the WMM-D-LdIb rule for $I$ , $ts_{U}$ should be the value of $gts$ in WMM-D when $S$ is overwritten by another store in $m$ . If $i$ is equal to $j$ , then $ts_{L}$ is the computed timestamp of the $S$ in the WMM-D-St rule, and should be equal to $ut_{s}$ ; otherwise $ts_{L}$ is one plus the value of $gts$ when $S$ writes $m$ in WMM-D, and should be equal to $ut_{w}+1$ . Then the computed timestamp of the load value of $I$ in WMM-D-LdIb rule must be equal to $ut_{e}$ .

Now we only need to show that $I$ can read the value of $S$ in CCM+OOOD at time $\langle ut_{e},lt_{e}\rangle$ , and that $I$ will not be killed or forced to re-execute later. Since the value of $S$ is enqueued into $ps[i].ib$ and stays there until $I$ is executed in WMM-D, we know the following things about $E$ :

–

$ps[i].sb$ does not contain any store to $a$ older than $I$ ever since $S$ is written into $m$ .

–

There is no $\mathsf{Reconcile}$ older than $I$ executed by $ps[i]$ ever since the overwrite of $S$ , i.e. $ps[i].rts\leq ts_{U}$ .

–

Any load older than $I$ in $ps[i]$ must read from either $S$ or some other store which writes $m$ before $S$ .

According to the invariants and the requirement $ats\leq ts_{U}$ of WMM-D-LdIb, we can deduce the following implications:

$S$ is overwritten in $ccm.m$ at time $\langle ts_{U},1\rangle$ . 2. 2.

$ut_{a}=ats\leq ts_{U}$ . 3. 3.

$ut_{r}=ps[i].rts\leq ts_{U}$ . 4. 4.

Neither $ooo[i].rob$ nor $ooo[i].sb$ contains any store to $a$ older than $L$ ever since $S$ is written into $ccm.m$ . In particular, if $i$ is equal to $j$ , then there is no store between $I$ and $S$ in processor $i$ . 5. 5.

Any load older than $I$ in $ooo[i]$ must read from either $S$ or some other store which writes $ccm.m$ before $S$ . Thus, if $I$ is killed by an older load $I^{\prime}$ , then $I^{\prime}$ must read from a store that writes $ccm.m$ before $S$ .

Thus, at time $\langle ut_{e},lt_{e}\rangle$ in CCM+OOOD, $S$ has not been overwritten in $ccm.m$ , i.e. $S$ is in $ooo[i].rob$ , $ooo[i].sb$ or $ccm.m$ (note that $S$ is visible to $ooo[i]$ at that time). We do a case analysis on whether $i$ is equal to $j$ (i.e. whether $S$ is also from processor $i$ ):

–

In case $i$ is equal to $j$ , the above implication 4 ensures that $I$ could read the value of $S$ from $ooo[i].rob$ or $ooo[i].sb$ or $ccm.m$ at time $\langle ut_{e},lt_{e}\rangle$ , and $I$ will not be killed or forced to re-execute by any older store. According to the above implication 5, if $I$ is killed by an older load $I^{\prime}$ later, then $I^{\prime}$ must be older than $S$ , because $I^{\prime}$ reads from a store that writes $ccm.m$ before $S$ . However in this case, the $\mathsf{findStaleLd}$ method performed by $I^{\prime}$ will be stopped by $S$ , and $I$ will not be killed.

–

In case $j\neq i$ , the above implication 4 guarantees that $I$ could read the value of $S$ from $ccm.m$ at time $\langle ut_{e},lt_{e}\rangle$ , and $I$ will not be killed or forced to re-execute by any older store. According to the above implications 5 and 4, if $I$ is killed by an older load $I^{\prime}$ , then $I^{\prime}$ must get its value before $S$ is written into $ccm.m$ , because $I^{\prime}$ reads from a store that writes $ccm.m$ before $S$ . However in this case, $I^{\prime}$ will get its value before $I$ does, and hence $I^{\prime}$ cannot kill $I$ .

•

$I$ ** is executed by reading $m$ (i.e. the WMM-D-LdMem rule):**

For the monolithic memory location $m[a]=\langle v,\langle j,sts\rangle,mts\rangle$ read in the WMM-D-LdMem rule for $I$ , $v$ is the value of $S$ , $sts$ is the timestamp computed in the WMM-D-St rule for $S$ , $mts$ is one plus the time when $S$ is written into $m[a]$ . If $i$ is equal to $j$ , then $vts$ in the WMM-D-LdMem rule for $I$ is equal to $sts$ , which is also equal to $ut_{s}$ ; otherwise we have $vts=mts=ut_{w}+1$ . Then the computed timestamp of the load value of $I$ in WMM-D-LdMem rule must be equal to $ut_{e}$ .

Now we only need to show that $I$ can read the value of $S$ in CCM+OOOD at time $\langle ut_{e},lt_{e}\rangle$ , and that $I$ will not be killed or forced to re-execute later. According to invariants and the fact that $I$ reads the value of $S$ from $m$ , we can deduce the following implications:

$S$ is in $ccm.m$ when $L$ is committed from ROB, so $S$ must have not been overwritten in $ccm.m$ at time $\langle ut_{e},lt_{e}\rangle$ ( $<\langle ut_{c},lt_{c}\rangle$ ), i.e. $S$ is in $ooo[i].rob$ , $ooo[i].sb$ or $ccm.m$ at that time (note that $S$ is visible to $ooo[i]$ at that time). 2. 2.

If $i$ is equal to $j$ , then there is no store to $a$ between $I$ and $S$ in processor $i$ ; otherwise there is no store to $a$ older than $I$ in $ooo[i].rob$ or $ooo[i].sb$ ever since $S$ is written into $ccm.m$ . 3. 3.

Any load older than $I$ in $ooo[i]$ must read from either $S$ or some other store which writes $ccm.m$ before $S$ .

The first and second implications ensure that $I$ can read the value of $S$ at time $\langle ut_{e},lt_{e}\rangle$ , and $I$ will not be killed or forced to re-execute by any older store. The second and third implications ensure that $I$ will not be killed by any older load, for the same reason used in the previous case where $I$ reads from $ps[i].ib$ .

•

$I$ ** is executed by reading $ps[i].sb$ (i.e. the WMM-D-LdSb rule):**

In this case, $i$ is equal to $j$ , i.e. $S$ is also from processor $i$ . For the timestamp $sts$ of the store buffer entry read in the WMM-D-LdSb rule for $I$ , $sts$ is the timestamp computed in the WMM-D-St rule for $S$ , and it is equal to $ut_{s}$ according to invariants. Then the computed timestamp of the load value of $I$ in WMM-D-LdMem rule must be equal to $ut_{e}$ .

Now we only need to show that $I$ can read the value of $S$ in CCM+OOOD at time $\langle ut_{e},lt_{e}\rangle$ , and that $I$ will not be killed or forced to re-execute later. According to invariants and the fact that $I$ reads the value of $S$ from $ps[i].sb$ , we can deduce the following implications:

$S$ is in either $ooo[i].rob$ or $ooo[i].sb$ at time $\langle ut_{e},lt_{e}\rangle$ (note that the store address and data of $S$ have been computed at this time). 2. 2.

There is no store to $a$ between $I$ and $S$ in $ooo[i]$ . 3. 3.

Any load to $a$ between $I$ and $S$ in $ooo[i]$ must also get the value of $S$ as its result.

The first two implications ensure that $I$ can read the value of $S$ at time $\langle ut_{e},lt_{e}\rangle$ , and $I$ will not be killed or forced to re-execute by any older store. The last implication ensures that $I$ will not be killed by any older load.

∎

Appendix B Proof of WMM-S Abstracting HMB+OOOS

Theorem 5.

HMB+OOOS $\subseteq$ WMM-S.

Proof.

We use $ooo[i]$ to denote processor $i$ in HMB+OOOS, and use $hmb.m$ to denote the monolithic memory in HMB. Section 7.4 in the paper has already stated the invariants and the way to simulate the behavior of HMB+OOOS in WMM-S. That section has also proved the correctness in case that a load $L$ to address $a$ , which reads from a store $S$ , is committed from $ooo[i].rob$ in HMB+OOOS, and that $S$ remains in a segment of HMB at the commit time of $L$ . Here we complete the proof for the remaining cases:

•

In case a store $S$ to address $a$ is flowed into $hmb.m$ in the HMB-Flow rule, $S$ must be closer to the root (i.e. $hmb.m$ ) than any other stores in HMB. According to invariants, in WMM-S, all the copies of $S$ must be the the oldest stores to $a$ in their respective store buffers. Thus, WMM-S can fire the WMM-S-DeqSb rule to write $S$ into the monolithic memory ( $m$ ), and all the invariants still hold.

•

In case a $\mathsf{Nm}$ , $\mathsf{Reconcile}$ , or $\mathsf{St}$ instruction is committed from $ooo[i].rob$ , it is trivial to prove that WMM-S can fire a WMM-Nm, WMM-Rec, or WMM-S-St rule to execute that instruction, and all the invariants still hold.

•

In case a $\mathsf{Commit}$ fence is committed from $ooo[i].rob$ , the $\mathsf{Commit}$ response from HMB ensures that there must not be any store in any segment of HMB which are observed by commits of $ooo[i]$ at that time. Therefore, $ps[i].sb$ in WMM-S should also be empty, and the $\mathsf{Commit}$ fence can be executed.

•

Consider the case that a load $L$ to address $a$ , which reads from a store $S$ , is committed from $ooo[i].rob$ in HMB+OOOS, and that $S$ is in $hmb.m$ at the commit time of $L$ . In this case, there cannot be any store to $a$ in any segment of $hmb$ which are observed by commits of $ooo[i]$ , because otherwise either the CoRR or CoWR axiom will be violated in HMB+OOOS. Thus, $ps[i].sb$ cannot have any store to $a$ and $L$ can read the value of $S$ from $m$ in WMM-S.

•

Consider the case that a load $L$ to address $a$ , which reads from a store $S$ , is committed from $ooo[i].rob$ in HMB+OOOS, and that $S$ has been overwritten in $hmb.m$ before the commit of $L$ . In this case, there cannot be any store to $a$ in any segment of $hmb$ which are observed by commits of $ooo[i]$ right before the overwrite of $S$ , because otherwise either the CoRR or CoWR axiom will be violated in HMB+OOOS. Thus, $ps[i].sb$ cannot have any store to $a$ right before $S$ is overwritten in $m$ in WMM-S, so the value of $S$ will be inserted into $ps[i].ib$ . According to the CoRR and CoWR axioms of HMB+OOOS, during the period between the overwrite and the commit of $L$ , no store to $a$ can be committed from $ooo[i].rob$ , and no load to $a$ committed from $ooo[i].rob$ can read from a store which writes $hmb.m$ after $S$ . In addition, no $\mathsf{Reconcile}$ fence can be committed during that period, otherwise the $\mathsf{Reconcile}$ fence will forbid $L$ from reading across it to get the value of $S$ . Thus, the value of $S$ will stay in $ps[i].ib$ until $L$ is executed by the WMM-LdIb rule in WMM-S.

∎

Appendix C CoRR and CoWR Axioms for Physical Models

In the paper, we have introduced the following axioms ( $L_{1},L_{2},S_{1},S_{2}$ denote loads and stores to the same address):

CoRR

(Read-Read Coherence): $L_{1}\xrightarrow{po}L_{2}\ \wedge\ S_{1}\xrightarrow{r\!f}L_{1}\ \wedge\ S_{2}\xrightarrow{r\!f}L_{2}\Longrightarrow S_{1}==S_{2}\ \vee\ S_{1}\xrightarrow{co}S_{2}$ .

CoWR

(Write-Read Coherence): $S_{2}\xrightarrow{r\!f}L_{1}\ \wedge\ S_{1}\xrightarrow{po}L_{1}\Longrightarrow S_{1}==S2\ \vee\ S_{1}\xrightarrow{co}S_{2}$ ..

We have used the fact that physical models (i.e. CCM+OOOVP, CCM+OOOD and HMB+OOOS) satisfy these two axioms in the proofs of the relations between $\mathrm{I^{2}E}$ models with physical models. Now we formally prove that these axioms hold for all the physical models. We will directly use $L_{1},L_{2},S_{1},S_{2}$ in the proofs, and all the operations about $L_{1}$ and $L_{2}$ discussed in the proofs are the final operations of $L_{1}$ and $L_{2}$ to get their load results, i.e. $L_{1}$ and $L_{2}$ should not be killed or forced to re-execute afterwards.

C.1 CoRR and CoWR Axioms for CCM+OOOVP/OOOD

Lemma 1.

CCM+OOOVP satisfies the CoRR axiom.

Proof.

We assume $L_{1}$ and $L_{2}$ are both from processor $i$ ( $ooo[i]$ ). We do a case analysis on how $L_{1}$ get its final result, i.e. the value of $S_{1}$ , and prove that $S_{2}\xrightarrow{co}S_{1}$ is impossible in each case.

First consider the case that $L_{1}$ gets its final result via the OOO-LdBypass rule. In this case, $S_{1}$ is also from $ooo[i]$ . If we have $S_{2}\xrightarrow{co}S_{1}$ , then $L_{2}$ must get its final result, i.e. the value of $S_{2}$ , before the OOO-StEx rule for $S_{1}$ has fired. However, in this case, $L_{2}$ will be killed later when the OOO-StEx rule for $S_{1}$ fires.

Next consider the case that $L_{1}$ reads the value of $S_{1}$ from the monolithic memory of CCM ( $ccm.m$ ). If we have $S_{2}\xrightarrow{co}S_{1}$ , then $L_{2}$ must get its final result before $L_{1}$ gets the response from CCM, and there should not be any store to $a$ between $L_{1}$ and $L_{2}$ in $ooo[i]$ (otherwise $L_{2}$ will be killed by the store). However, in this case, when $L_{1}$ gets its response from CCM, it will kill $L_{2}$ . ∎

Lemma 2.

CCM+OOOVP satisfies the CoWR axiom.

Proof.

We assume $L_{1}$ and $S_{1}$ are both from processor $i$ ( $ooo[i]$ ). If we have $S_{2}\xrightarrow{co}S_{1}$ , then $L_{1}$ must get its final result, i.e. the value of $S_{2}$ , before the OOO-StEx rule for $S_{1}$ has fired. However, in this case, $L_{1}$ will be killed later when the OOO-StEx rule for $S_{1}$ fires. ∎

Since CCM+OOOD $\subseteq$ CCM+OOOVP, CCM+OOOD also satisfies the CoRR and CoWR axioms.

C.2 CoRR and CoWR Axioms for HMB+OOOS

Lemma 3.

HMB+OOOS satisfies the CoRR axiom.

Proof.

We assume $L_{1}$ and $L_{2}$ are both from processor $i$ ( $ooo[i]$ ). We do a case analysis on how $L_{1}$ get its final result, i.e. the value of $S_{1}$ , and prove that $S_{2}\xrightarrow{co}S_{1}$ is impossible in each case.

First consider the case that $L_{1}$ gets its final result via the OOO-LdBypass rule. In this case, $S_{1}$ is also from $ooo[i]$ . If we have $S_{2}\xrightarrow{co}S_{1}$ , then $L_{2}$ must get its final result, i.e. the value of $S_{2}$ , before the OOO-StEx rule for $S_{1}$ has fired. However, in this case, $L_{2}$ will be killed later when the OOO-StEx rule for $S_{1}$ fires.

Next consider the case that $L_{1}$ reads the value of $S_{1}$ from HMB. If we have $S_{2}\xrightarrow{co}S_{1}$ , then before $L_{1}$ issues its request to HMB, $L_{2}$ must either issue its request to HMB or get bypassing from ROB . Furthermore, there should not be any store to $a$ between $L_{1}$ and $L_{2}$ in $ooo[i]$ (otherwise $L_{2}$ will be killed by the store). However, in this case, when $L_{1}$ issues its request to HMB, it will kill $L_{2}$ . ∎

Lemma 4.

HMB+OOOS satisfies the CoWR axiom.

Proof.

The argument is the same as that for CCM+OOOVP. ∎

Bibliography62

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1Adve and Gharachorloo [1996] S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. computer , 29(12):66–76, 1996.
2Adve and Hill [1990] S. V. Adve and M. D. Hill. Weak ordering a new definition. In ACM SIGARCH Computer Architecture News , volume 18, pages 2–14. ACM, 1990.
3Alglave [2012] J. Alglave. A formal hierarchy of weak memory models. Formal Methods in System Design , 41(2):178–210, 2012.
4Alglave and Maranget [2011] J. Alglave and L. Maranget. Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings , chapter Stability in Weak Memory Models, pages 50–66. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. ISBN 978-3-642-22110-1. 10.1007/978-3-642-22110-1_6 . URL http://dx.doi.org/10.1007/978-3-642-22110-1_6 . · doi ↗
5Alglave et al. [2009] J. Alglave, A. Fox, S. Ishtiaq, M. O. Myreen, S. Sarkar, P. Sewell, and F. Z. Nardelli. The semantics of power and arm multiprocessor machine code. In Proceedings of the 4th workshop on Declarative aspects of multicore programming , pages 13–24. ACM, 2009.
6Alglave et al. [2012] J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. Fences in weak memory models (extended version). Formal Methods in System Design , 40(2):170–205, 2012.
7Alglave et al. [2013] J. Alglave, D. Kroening, V. Nimal, and M. Tautschnig. Software verification for weak memory via program transformation. In Programming Languages and Systems , pages 512–532. Springer, 2013.
8Alglave et al. [2014] J. Alglave, L. Maranget, and M. Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Transactions on Programming Languages and Systems (TOPLAS) , 36(2):7, 2014.

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

An Operational Framework for Specifying Memory Models using Instantaneous Instruction Execution

Abstract

category:

1 Introduction

2 Related Work

3 Implementation of Modern Multiprocessors

3.1 CCM: the Semantics of Write-Back Cache Hierarchies

3.2 OOOVP: the Model of Out-of-Order Processors

3.2.1 Component Functionality

3.2.2 Rules to Describe OOOVP Behavior

4 Defining Memory Models Using I2E

5 WMM Model

5.1 Operational Semantics of WMM

5.2 Litmus Tests for WMM

5.3 Equivalence of CCM+OOOVP and WMM

Theorem 1**.**

Proof.

Theorem 2**.**

Proof.

6 Modeling Data Dependency

6.1 Enforcing Data Dependency with Timestamps

6.2 WMM-D Operational Semantics

6.3 Litmus Tests for WMM-D

6.4 Equivalence of WMM-D and CCM+OOOD

Theorem 3**.**

Proof.

Theorem 4**.**

Proof.

7 Modeling Multi-Copy Non-Atomic Stores

7.1 WMM-S: Copying From One Store Buffer into Another

7.2 Litmus Tests for WMM-S

7.3 HMB+OOOS: a Physical Model for Muiltiprocessors with Multi-Copy Non-Atomic Memory

7.4 WMM-S Abstracting HMB+OOOS

Theorem 5**.**

Proof.

8 Conclusion

Appendix A Proof of Equivalence Between WMM-D and CCM+OOOD

Theorem 3**.**

Proof.

Theorem 4**.**

Proof.

Appendix B Proof of WMM-S Abstracting HMB+OOOS

Theorem 5**.**

Proof.

Appendix C CoRR and CoWR Axioms for Physical Models

C.1 CoRR and CoWR Axioms for CCM+OOOVP/OOOD

Lemma 1**.**

Proof.

Lemma 2**.**

Proof.

C.2 CoRR and CoWR Axioms for HMB+OOOS

Lemma 3**.**

Proof.

Lemma 4**.**

Proof.

Theorem 1.

Theorem 2.

Theorem 3.

Theorem 4.

Theorem 5.

Theorem 3.

Theorem 4.

Theorem 5.

Lemma 1.

Lemma 2.

Lemma 3.

Lemma 4.