2022.02.27
Abstract
Sail的目的：
Our model is expressed in a mathematically rigor- ous language that can be automatically translated to an executable test-oracle tool; this lets one either inter- actively explore or exhaustively compute the set of all allowed behaviours of intricate test cases, to provide a reference for hardware and software development.
Intro
尽管[3, 4]做得很好了，“我们”做的比[3, 4]更好。
在[3]上做了拓展。 做出的新贡献：
- 并发和ISA之间的接口
- Sail语言（描述ISA）
- 重新整理ISA文档
- 拓展前人的并发模型[3]
- Test-Oracle Tool（生成可执行模型?[21]?）
- 测试了本工作的正确性
1.5 Lem
Lem是个语法框架[21]。
2 ISA/Concurrency Interface
如何正确地关联ISA和并发。 ISA描述能够正确地导出已知的并发现象。
2.1.1 No single program point
乱序和猜测执行造成。 例子：MP+sync+ctrl 解决：正在执行的指令树结构。
2.1.2 No per-thread register state
寄存器重命名造成。 例子：MP+sync+rs 解决：需要树结构
2.1.3 Register self-reads？？？
2.1.4 Dependencies and register granularity
位操作寄存器，位操作指令
2.1.5 Reading from uncommitted instructions
2.1.6 Non-atomic intra-instruction semantics for register reads
指令执行并非3阶段： not started, fully executed but not committed, committed
stw RS,D(RA)：算出EA后，若和后续写指令地址X相关，则X可以提前。
2.1.7 Undefined values
2.2 The ISA semantics interface
Lem
3. Sail: ISA Definition Language
相关工作：
- gem5, QEMU中间表示
- Fox [23] for ARM in his L3 IDL
- [24] for x86 in ACL2
现有的ISA描述语言不能处理弱内存一致性的ISA和并发之间的关系。