memory-model-alloy.tex

\section{Alloy中的形式公理规范}
% \section{Formal Axiomatic Specification in Alloy}
\label{sec:alloy}

\lstdefinelanguage{alloy}{
  morekeywords={abstract, sig, extends, pred, fun, fact, no, set, one, lone, let, not, all, iden, some, run, for},
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  commentstyle=\color{green!40!black},
  keywordstyle=\color{blue!40!black},
  moredelim=**[is][\color{red}]{@}{@},
  escapeinside={!}{!},
}
\lstset{language=alloy}
\lstset{aboveskip=0pt}
\lstset{belowskip=0pt}

我们在Alloy（\url{http://alloy.mit.edu}）中呈现了RVWMO内存模型的一种形式规范。
这个模型可以从\url{https://github.com/daniellustig/riscv-memory-model}在线获得。
% We present a formal specification of the RVWMO memory model in Alloy (\url{http://alloy.mit.edu}).
% This model is available online at \url{https://github.com/daniellustig/riscv-memory-model}.

该线上材料也包含了一些石蕊测试和一些关于Alloy可以怎样被用于对第~\ref{sec:memory:porting}节中的一些映射进行模型检查的例子。
% The online material also contains some litmus tests and some examples of how Alloy can be used to model check some of the mappings in Section~\ref{sec:memory:porting}.

\begin{figure}[h!]
  {
  \tt\bfseries\centering\footnotesize
  \begin{lstlisting}
////////////////////////////////////////////////////////////////////////////////
// =RVWMO PPO=

// 保留的程序次序
fun ppo : Event->Event {
  // same-address ordering
  po_loc :> Store
  + rdw
  + (AMO + StoreConditional) <: rfi

  // 显式同步
  + ppo_fence
  + Acquire <: ^po :> MemoryEvent
  + MemoryEvent <: ^po :> Release
  + RCsc <: ^po :> RCsc
  + pair

  // 句法依赖
  + addrdep
  + datadep
  + ctrldep :> Store

  // 管道依赖
  + (addrdep+datadep).rfi
  + addrdep.^po :> Store
}

// 全局内存次序尊重保留的程序次序
fact { ppo in ^gmo }
\end{lstlisting}}
  \caption{Alloy中的形式化RVWMO内存模型（1/5：PPO）  
  % The RVWMO memory model formalized in Alloy (1/5: PPO)
  }
  \label{fig:alloy1}
\end{figure}
\begin{figure}[h!]
  {
  \tt\bfseries\centering\footnotesize
  \begin{lstlisting}
////////////////////////////////////////////////////////////////////////////////
// =RVWMO 公理=

// 加载值公理
fun candidates[r: MemoryEvent] : set MemoryEvent {
  (r.~^gmo & Store & same_addr[r]) // 在gmo中写前趋r
  + (r.^~po & Store & same_addr[r]) // 在po中写前趋r
}

fun latest_among[s: set Event] : Event { s - s.~^gmo }

pred LoadValue {
  all w: Store | all r: Load |
    w->r in rf <=> w = latest_among[candidates[r]]
}

// 原子性公理
pred Atomicity {
  all r: Store.~pair |            // 从lr开始,
    no x: Store & same_addr[r] |  // 对于相同的地址，没有存储x
      x not in same_hart[r]       // 使得x来自不同的硬件线程，
      and x in r.~rf.^gmo         // 在gmo中x跟着(存储r的“读从”)，
      and r.pair in x.^gmo        // 以及在gmo中，r跟着x
}

// 进程公理被隐去：Alloy只考虑有限的执行

pred RISCV_mm { LoadValue and Atomicity /* and Progress */ }

\end{lstlisting}}
  \caption{Alloy中的形式化RVWMO内存模型（2/5：公理）
    % The RVWMO memory model formalized in Alloy (2/5: Axioms)
    }
  \label{fig:alloy2}
\end{figure}
\begin{figure}[h!]
  {
  \tt\bfseries\centering\footnotesize
  \begin{lstlisting}
////////////////////////////////////////////////////////////////////////////////
// 内存的基础模型

sig Hart {  // 硬件线程
  start : one Event
}
sig Address {}
abstract sig Event {
  po: lone Event // 程序次序
}

abstract sig MemoryEvent extends Event {
  address: one Address,
  acquireRCpc: lone MemoryEvent,
  acquireRCsc: lone MemoryEvent,
  releaseRCpc: lone MemoryEvent,
  releaseRCsc: lone MemoryEvent,
  addrdep: set MemoryEvent,
  ctrldep: set Event,
  datadep: set MemoryEvent,
  gmo: set MemoryEvent,  // 全局内存次序
  rf: set MemoryEvent
}
sig LoadNormal extends MemoryEvent {} // l{b|h|w|d}
sig LoadReserve extends MemoryEvent { // lr
  pair: lone StoreConditional
}
sig StoreNormal extends MemoryEvent {}       // s{b|h|w|d}
// 模型中所有的StoreConditionals 都假定是成功的
sig StoreConditional extends MemoryEvent {}  // sc
sig AMO extends MemoryEvent {}               // amo
sig NOP extends Event {}

fun Load : Event { LoadNormal + LoadReserve + AMO }
fun Store : Event { StoreNormal + StoreConditional + AMO }

sig Fence extends Event {
  pr: lone Fence, // 操作位
  pw: lone Fence, // 操作位
  sr: lone Fence, // 操作位
  sw: lone Fence  // 操作位
}
sig FenceTSO extends Fence {}

/* Alloy编码细节：操作码位要么被设置（被编码，例如 as f.pr in iden），
 * 要么不被设置（f.pr not in iden）。这些位不能被用作其它任何用途 */
fact { pr + pw + sr + sw in iden }
// 对排序注释也是类似的
fact { acquireRCpc + acquireRCsc + releaseRCpc + releaseRCsc in iden }
// 不要试图通过pr/pw/sr/sw来编码FenceTSO；只把它当做is那样使用
fact { no FenceTSO.(pr + pw + sr + sw) }
\end{lstlisting}}
  \caption{Alloy中的形式化RVWMO内存模型（3/5：内存的模型）}
  \label{fig:alloy3}
\end{figure}

\begin{figure}[h!]
  {
  \tt\bfseries\centering\footnotesize
  \begin{lstlisting}
////////////////////////////////////////////////////////////////////////////////
// =基本模型规则 =

// 次序注释组
fun Acquire : MemoryEvent { MemoryEvent.acquireRCpc + MemoryEvent.acquireRCsc }
fun Release : MemoryEvent { MemoryEvent.releaseRCpc + MemoryEvent.releaseRCsc }
fun RCpc : MemoryEvent { MemoryEvent.acquireRCpc + MemoryEvent.releaseRCpc }
fun RCsc : MemoryEvent { MemoryEvent.acquireRCsc + MemoryEvent.releaseRCsc }

// 没有像store - acquire或者load - release那样的东西，除非两者结合
fact { Load & Release in Acquire }
fact { Store & Acquire in Release }

// FENCE PPO
fun FencePRSR : Fence { Fence.(pr & sr) }
fun FencePRSW : Fence { Fence.(pr & sw) }
fun FencePWSR : Fence { Fence.(pw & sr) }
fun FencePWSW : Fence { Fence.(pw & sw) }

fun ppo_fence : MemoryEvent->MemoryEvent {
    (Load  <: ^po :> FencePRSR).(^po :> Load)
  + (Load  <: ^po :> FencePRSW).(^po :> Store)
  + (Store <: ^po :> FencePWSR).(^po :> Load)
  + (Store <: ^po :> FencePWSW).(^po :> Store)
  + (Load  <: ^po :> FenceTSO) .(^po :> MemoryEvent)
  + (Store <: ^po :> FenceTSO) .(^po :> Store)
}

// 辅助定义
fun po_loc : Event->Event { ^po & address.~address }
fun same_hart[e: Event] : set Event { e + e.^~po + e.^po }
fun same_addr[e: Event] : set Event { e.address.~address }

// 初始化存储
fun NonInit : set Event { Hart.start.*po }
fun Init : set Event { Event - NonInit }
fact { Init in StoreNormal }
fact { Init->(MemoryEvent & NonInit) in ^gmo }
fact { all e: NonInit | one e.*~po.~start }  // 各事件都确实地在one硬件线程中
fact { all a: Address | one Init & a.~address } // one初始化各地址的存储
fact { no Init <: po and no po :> Init }
\end{lstlisting}}
  \caption{Alloy中的形式化RVWMO内存模型（4/5：基础模型规则）}
  \label{fig:alloy4}
\end{figure}

\begin{figure}[h!]
  {
  \tt\bfseries\centering\footnotesize
  \begin{lstlisting}
// po
fact { acyclic[po] }

// gmo
fact { total[^gmo, MemoryEvent] } // gmo是在所有MemoryEvents上的总次序

//rf
fact { rf.~rf in iden } // 每个读返回唯一写的值
fact { rf in Store <: address.~address :> Load }
fun rfi : MemoryEvent->MemoryEvent { rf & (*po + *~po) }

//dep
fact { no StoreNormal <: (addrdep + ctrldep + datadep) }
fact { addrdep + ctrldep + datadep + pair in ^po }
fact { datadep in datadep :> Store }
fact { ctrldep.*po in ctrldep }
fact { no pair & (^po :> (LoadReserve + StoreConditional)).^po }
fact { StoreConditional in LoadReserve.pair } // 假设所有的SC都成功了

// rdw
fun rdw : Event->Event {
  (Load <: po_loc :> Load)  // start with all same_address load-load pairs,
  - (~rf.rf)                // subtract pairs that read from the same store,
  - (po_loc.rfi)            // and subtract out "fri-rfi" patterns
}

// 过滤出冗余的实例和/或可视化效果
fact { no gmo & gmo.gmo } // 保持可视化效果整洁
fact { all a: Address | some a.~address }

////////////////////////////////////////////////////////////////////////////////
// =可选：操作码编码约束=

// 神圣的屏障列表
fact { Fence in
  Fence.pr.sr
  + Fence.pw.sw
  + Fence.pr.pw.sw
  + Fence.pr.sr.sw
  + FenceTSO
  + Fence.pr.pw.sr.sw
}

pred restrict_to_current_encodings {
  no (LoadNormal + StoreNormal) & (Acquire + Release)
}

////////////////////////////////////////////////////////////////////////////////
// =Alloy捷径 =
pred acyclic[rel: Event->Event] { no iden & ^rel }
pred total[rel: Event->Event, bag: Event] {
  all disj e, e': bag | e->e' in rel + ~rel
  acyclic[rel]
}
\end{lstlisting}}
  \caption{Alloy中的形式化RVWMO内存模型（5/5：辅助内容）
    % The RVWMO memory model formalized in Alloy (5/5: Auxiliaries)
    ]}
  \label{fig:alloy5}
\end{figure}