2021.11.20
Introduction
Ingo Molnar: linux应该建立一个内存模型，让各个架构来实现这个模型
已有诸多讨论，让内核使用C11的内存模型，但目前的结论是C11还不能完全满足Linux的需求。
overview
贡献：
- 用cat语言规范化描述的内核内存模型
- 例子
- 规范化RCU，正确实现RCU
- 硬件可用性，与C11对比
Candidate executions
- abstract executions: (E, po, addr, data, rmw)
- execution witnesses: (rf, co)
看这些操作的衍生定义（比如fr）有点懵，直接去看cat的论文吧