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

3936 软件学报 2025 年第 36 卷第 9 期

Algorithms for the Construction and Analysis of Systems. Saarbrücken: Springer, 2011. 41–44. [doi: 10.1007/978-3-642-19835-9_5]
[13] Waterman A, Asanović K, eds. The RISC-V instruction set manual, Vol. I: Unprivileged ISA. Version 20191214-draft, 2019. https://riscv.
github.io/riscv-isa-manual/snapshot/unprivileged/
[14] Liu C, Wu YJ, Wu JZ, Zhao C. Survey on RISC-V system architecture research. Ruan Jian Xue Bao/Journal of Software, 2021, 32(12):
3992–4024 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/6490.htm [doi: 10.13328/j.cnki.jos.006490]
[15] Gharachorloo K, Lenoski D, Laudon J, Gibbons P, Gupta A, Hennessy J. Memory consistency and event ordering in scalable shared-
memory multiprocessors. In: Sohi GS, ed. 25 Years of the Int’l Symposia on Computer Architecture (Selected Papers). New York: ACM,
1998. 376–387. [doi: 10.1145/285930.285997]
[16] Litmus-tests-riscv. 2022. https://github.com/litmus-tests/litmus-tests-riscv
[17] Gray KE, Kernels G, Mulligan D, Pulte C, Sarkar S, Sewell P. An integrated concurrency and core-ISA architectural envelope definition,
and test oracle, for IBM POWER multiprocessors. In: Proc. of the 48th Int’l Symp. on Microarchitecture. Waikiki: ACM, 2015. 635–646.
[doi: 10.1145/2830772.2830775]
[18] Armstrong A, Bauereiss T, Campbell B, Reid A, Gray KE, Norton RM, Mundkur P, Wassell M, French J, Pulte C, Flur S, Stark I,
Krishnaswami N, Sewell P. ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS. In: Proc. of the 2019 ACM on Programming
Languages. ACM, 2019. 71. [doi: 10.1145/3290384]
[19] Jackson D. Alloy: A language and tool for exploring software designs. Communications of the ACM, 2019, 62(9): 66–76. [doi: 10.1145/
3338843]
[20] Hopcroft JE, Motwani R, Ullman JD. Introduction to Automata Theory, Languages, and Computation. 3rd ed., Boston: Addison-Wesley
Longman Publishing Co. Inc., 2006.
[21] Alglave J, Kroening D, Tautschnig M. Partial orders for efficient bounded model checking of concurrent software. In: Proc. of the 25th
Int’l Conf. on Computer Aided Verification. Saint Petersburg: Springer, 2013. 141–157. [doi: 10.1007/978-3-642-39799-8_9]

附中文参考文献:
[4] 王超, 吕毅, 吴鹏, 贾巧雯. TSO 内存模型下限界可线性化的可判定性研究. 软件学报, 2022, 33(8): 2896–2917. http://www.jos.org.cn/
1000-9825/6604.htm [doi: 10.13328/j.cnki.jos.006604]
[9] 王戟, 詹乃军, 冯新宇, 刘志明. 形式化方法概貌. 软件学报, 2019, 30(1): 33–61. http://www.jos.org.cn/1000-9825/5652.htm [doi:
10.13328/j.cnki.jos.005652]
[14] 刘畅, 武延军, 吴敬征, 赵琛. RISC-V 指令集架构研究综述. 软件学报, 2021, 32(12): 3992–4024. http://www.jos.org.cn/1000-9825/
6490.htm [doi: 10.13328/j.cnki.jos.006490]

徐学政(1993－), 男, 博士, 助理研究员, 主要研 王涛(1987－), 男, 博士, 副研究员, 主要研究领
究领域为程序分析, 系统软件. 域为系统软件, 智能计算机系统.

杨德亨(1996－), 男, 博士, 助理研究员, 主要研 黄安文(1983－), 男, 博士, 副研究员, 主要研究
究领域为软件工程, 程序分析. 领域为计算机体系结构, 微处理器体系结构.

王璐(1991－), 女, 博士, 助理研究员, 主要研究 李琼(1967－), 女, 博士, 研究员, 博士生导师, 主
领域为体系结构, 微处理器设计. 要研究领域为高性能计算机系统结构, 智能计
算, 信息存储.