Page 24 - 《软件学报》2025年第9期

徐学政 等: RISC-V 内存一致性模型的同地址顺序一致性定理证明 3935

P0 P1
a: W x=1 c: R x=2
co rf

b: W x=2
图 14 证明 WWR 模式不存在传递性的 Litmus 示例

5 案例分析: 应用 SCPL 进行 Litmus 测试合法性判定

应用内存一致性的公理模型可形式化地对 Litmus 测试的合法性进行判定, 从而指导软件开发和芯片验证. 例
如, 借助模型检验 [21] 可自动对 Litmus 测试进行判定. 其中, 借助 SCPL 将大大简化公理模型对部分 Litmus 测试的
形式化验证. 以第 1.2 节中的程序为例, 利用 SCPL 容易判定其非法性.
命题 4. ∀a∈R, b∈R, c∈W, d∈W, poloc(a,b)∧poloc(c,d)∧co(c,d)∧rfe(d,a)∧rfe(c,b)→False.
证明: 根据 co(c,d)、rf(c,b) 以及 fr 的定义可得 fr(b,d), 又由 rf(d,a)、poloc(a,b) 以及 SCPL 定理推出矛盾. 得证.
如果不利用 SCPL 定理, 可通过与引理 10 类似的方法进行证明, 相比之下, 基于 SCPL 的证明更为直接.

6 总 结

本文证明了 RVWMO 满足 SCPL. 证明过程将序列模式的构建抽象为确定有限状态自动机, 通过对各个模式
满足 SCPL 以及模式转换正确性的证明, 从而实现对任意访存序列满足 SCPL 的证明. 通过实验 (图 2) 以及案例
分析 (第 5 节) 可见, SCPL 定理将大大简化 RVWMO 模型的相关形式化方法.
本研究是对 RVWMO 相关形式化方法的一个理论补充.

References:
[1] Lamport L. How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. on Computers, 1997, 46(7):
779–782. [doi: 10.1109/12.599898]
[2] Sorin DJ, Hill MD, Wood DA. A Primer on Memory Consistency and Cache Coherence. Cham: Springer, 2011. [doi: 10.1007/978-3-031-
01733-9]
[3] Sewell P, Sarkar S, Owens S, Nardelli FZ, Myreen MO. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors.
Communications of the ACM, 2010, 53(7): 89–97. [doi: 10.1145/1785414.1785443]
[4] Wang C, Lü Y, Wu P, Jia QW. Decidability of bounded linearizability on TSO memory model. Ruan Jian Xue Bao/Journal of Software,
2022, 33(8): 2896–2917 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6604.htm [doi: 10.13328/j.cnki.jos.006604]
[5] Sarkar S, Sewell P, Alglave J, Maranget L, Williams D. Understanding POWER multiprocessors. In: Proc. of the 32nd ACM SIGPLAN
Conf. on Programming Language Design and Implementation. San Jose: ACM, 2011. 175–186. [doi: 10.1145/1993498.1993520]
[6] Alglave J, Deacon W, Grisenthwaite R, Hacquard A, Maranget L. Armed cats: Formal concurrency modelling at ARM. ACM Trans. on
Programming Languages and Systems (TOPLAS), 2021, 43(2): 8. [doi: 10.1145/3458926]
[7] Alglave J, Maranget L, Tautschnig M. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. on
Programming Languages and Systems (TOPLAS), 2014, 36(2): 7. [doi: 10.1145/2627752]
[8] Alglave J, Cousot P. Ogre and Pythia: An invariance proof method for weak consistency models. In: Proc. of the 44th ACM SIGPLAN
Symp. on Principles of Programming Languages. Paris: ACM, 2017. 3–18. [doi: 10.1145/3009837.3009883]
[9] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1): 33–61 (in
Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm [doi: 10.13328/j.cnki.jos.005652]
[10] Alglave J. A shared memory poetics [Ph.D. Thesis]. Paris: Université Paris, 2010.
[11] Alglave J, Maranget L, McKenney PE, Parri A, Stern A. Frightening small children and disconcerting grown-ups: Concurrency in the
Linux kernel. In: Proc. of the 23rd Int’l Conf. on Architectural Support for Programming Languages and Operating Systems.
Williamsburg: ACM, 2018. 405–418. [doi: 10.1145/3173162.3177156]
[12] Alglave J, Maranget L, Sarkar S, Sewell P. Litmus: Running tests against hardware. In: Proc. of the 17th Int’l Conf. on Tools and