形式化方法与系统软件：实践与发展建议

doi:10.3981/j.issn.2097-0781.2023.01.003

前瞻科技 ›› 2023, Vol. 2 ›› Issue (1): 33-45.DOI: 10.3981/j.issn.2097-0781.2023.01.003

形式化方法与系统软件：实践与发展建议

丁浩然¹(), 王肇国¹, 付明², 陈海波¹^,^†()

1.上海交通大学软件学院，上海 200240
2.华为德累斯顿研究所，德国德累斯顿 01069

收稿日期:2023-01-06 修回日期:2023-02-09 出版日期:2023-03-20 发布日期:2023-03-24
通讯作者: ^†
作者简介:丁浩然，博士研究生。研究方向为基于形式化方法的系统软件验证与优化。参与设计和实现了世界上第1个形式化验证过的细粒度并发内存文件系统AtomFS、自动生成并验证SQL优化规则的工具WeTune等，相关成果发表在中国计算机学会推荐的系统和数据库领域A类国际顶级会议SOSP和SIGMOD。电子信箱：nhaorand@sjtu.edu.cn。
陈海波，上海交通大学特聘教授，博士研究生导师。上海交通大学并行与分布式系统研究所所长，领域操作系统教育部工程研究中心主任。中国计算机学会系统软件专业委员会副主任，OpenHarmony技术指导委员会创始主席，国际计算机学会（ACM）旗舰杂志Communications of the ACM首位中国学者编委与领域共同主席。国家杰出青年科学基金获得者，国际电气与电子工程师协会（IEEE）会士，ACM杰出科学家。主要研究领域为操作系统、分布式系统与形式化方法。研究成果通过产学研深度结合被应用到数十亿设备，产生了广泛的学术与产业影响。获陈嘉庚青年科学奖、教育部技术发明奖一等奖、中国青年科技奖、全国优秀博士学位论文奖及华为卓越贡献个人奖，ASPLOS、EuroSys、VEE等最佳论文奖，DSN时间检验奖，SIGMOD研究亮点奖等。主持撰写的《现代操作系统：原理与实现》获得2020年度“最受读者喜爱的IT图书奖”。电子信箱：haibochen@sjtu.edu.cn。

Formal Methods and System Software: Practice and Suggestions

DING Haoran¹(), WANG Zhaoguo¹, FU Ming², CHEN Haibo¹^,^†()

1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China
2. Huawei Dresden Research Center, Dresden 01069, Germany

Received:2023-01-06 Revised:2023-02-09 Online:2023-03-20 Published:2023-03-24
Contact: ^†

摘要/Abstract

摘要：

对高可靠系统软件需求的不断增加使得形式化方法在工业界引起了广泛的兴趣。文章概述了当前主流形式化方法，分析了国内外研究态势，并介绍了形式化方法在设计和实现操作系统、编译器、同步原语、文件系统、数据库系统和分布式共识协议等方面的实践。基于这些实践，进一步总结了形式化方法在系统软件中应用的经验，并从理论和工程两方面讨论其可能面临的挑战，最后针对这些挑战提出发展建议。

关键词: 形式化方法, 操作系统, 数据库, 文件系统, 分布式共识协议

Abstract:

The growing need for highly reliable system software has drawn widespread interest in formal methods in the industry. This paper presents an overview of the mainstream formal methods and analyzes the current research status in this regard. Then, it describes the application of formal methods in the design and implementation of operating systems, compilers, synchronization primitives, file systems, database systems, and distributed consensus protocols. On this basis, it summarizes the experience learned in applying formal methods to system software and discusses potential challenges from the theoretical and engineering aspects. Finally, it gives some suggestions on how to address these challenges.

Key words: formal methods, operating systems, database, file systems, distributed consensus protocols

丁浩然, 王肇国, 付明, 陈海波. 形式化方法与系统软件：实践与发展建议[J]. 前瞻科技, 2023, 2(1): 33-45.

DING Haoran, WANG Zhaoguo, FU Ming, CHEN Haibo. Formal Methods and System Software: Practice and Suggestions[J]. Science and Technology Foresight, 2023, 2(1): 33-45.

图/表 5

图1 形式化方法应用案例概览

图2 VSync系统流程图

图3 CLoF系统流程图

图4 文件系统操作的可线性化

图5 WeTune系统架构图

参考文献 44

[1]	王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌[J]. 软件学报, 2019, 30(1): 33-61.
[2]	Klein G, Elphinstone K, Heiser G, et al. seL4: Formal verification of an OS kernel[C]// Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. New York: ACM Press, 2009: 207-220.
[3]	Luke N, Sigurbjarnarson H, Zhang K Y, et al. Hyperkernel: Push-button verification of an OS kernel[C]// Proceedings of the 26th Symposium on Operating Systems Principles. New York: ACM Press, 2017:252-269.
[4]	Nipkow T, Paulson L C, Wenzel M. Isabelle/HOL: A proof assistant for higher-order logic[M]. Berlin, Heidelberg: Springer, 2002.
[5]	Kokologiannakis M, Vafeiadis V. GenMC: A model checker for weak memory models[C]// Silva A, Leino K R M. Proceedings of the 33rd International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2021: 427-440.
[6]	Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR[C]// Goos G, Hartmains J.Proceedings of the 5th International Symposium on Programming. Berlin, Heidelberg: Springer, 1982: 337-351.
[7]	de Lima Chehab R L, Paolillo A, Behrens D, et al. CLoF: A compositional lock framework for multi-level NUMA systems[C]// Proceedings of the ACM SIGOPS 28th Symposium on Operating Systems Principles. New York: ACM Press, 2021: 851-865.
[8]	Chen H G, Ziegler D, Chajed T, et al. Using Crash Hoare logic for certifying the FSCQ file system[C]// Proceedings of the 25th Symposium on Operating Systems Principles. New York: ACM Press, 2015: 18-37.
[9]	Xu F W, Fu M, Feng X Y, et al. A practical verification framework for preemptive OS kernels[C]// Chaudhuri S, Farzar A.Proceedings of the 28th International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2016: 59-79.
[10]	Zou M, Ding H R, Du D, et al. Using concurrent relational logic with helpers for verifying the AtomFS file system[C]// Proceedings of the 27th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2019: 259-274.
[11]	Gu R H, Shao Z, Chen H, et al. CertiKOS: An extensible architecture for building certified concurrent OS kernels[C]// Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation. New York: ACM Press, 2016: 653-669.
[12]	Li X, Li X, Dall C, et al. Design and verification of the arm confidential compute architecture[C]// Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press, 2022: 465-484.
[13]	Chajed T, Tassarotti J, Theng M, et al. GoJournal: A verified, concurrent, crash-safe journaling system[C]// Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press, 2021: 423-439.
[14]	Jiang H R, Liang H J, Xiao S Y, et al. Towards certified separate compilation for concurrent programs[C]// Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2019: 111-125.
[15]	Hawblitzel C, Howell J, Kapritsos M, et al. IronFleet: Proving practical distributed systems correct[C]// Proceedings of the 25th Symposium on Operating Systems Principles. New York: ACM Press, 2015, doi: 10.1145/2815400.2815428.
[16]	Bond B, Hawblitzel C, Kapritsos M, et al. Vale: Verifying high-performance cryptographic assembly code[C]// Proceedings of the 26th USENIX Conference on Security Symposium. New York: ACM Press, 2017: 917-934.
[17]	Lorch J R, Chen Y X, Kapritsos M, et al. Armada: Low-effort verification of high-performance concurrent programs[C]// Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: ACM Press, 2020: 197-210.
[18]	Hance T, Lattuada A, Hawblitzel C, et al. Storage systems are distributed systems (so verify them that way!)[C]// Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation. New York: ACM Press, 2020: 99-115.
[19]	Chajed T, Tassarotti J, Theng M, et al. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning[C]// Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press, 2022: 447-463.
[20]	Leino K R M. Dafny: An automatic program verifier for functional correctness[C]// Clarke E M,Voronkov A. Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Berlin, Heidelberg: Springer, 2010: 348-370.
[21]	de Moura L, Bjørner N. Z3: An efficient SMT solver[C]// Ramakrishnan C R, Rehof J. Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 2008: 337-340.
[22]	Sigurbjarnarson H, Bornholt J, Torlak E, et al. Push-button verification of file systems via crash refinement[C]// Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press, 2016, doi: 10.5555/3026877.3026879.
[23]	Nelson L, van Geffen J, Torlak E, et al. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel[C]// Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation. New York: ACM Press, 2020: 41-61.
[24]	Yao J, Tao R, Gu R, et al. DuoAI:Fast, Automated inference of inductive invariants for verifying distributed protocols[C]// Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. New York: ACM Press, 2022: 485-501.
[25]	Torlak E, Bodik R. Growing solver-aided languages with rosette[C]// Proceedings of the 2013 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software. New York: ACM Press, 2013: 135-152.
[26]	Nelson L, Bornholt J, Gu R H, et al. Scaling symbolic evaluation for automated verification of systems code with Serval[C]// Proceedings of the 27th ACM Symposium on Operating Systems Principles. New York: ACM Press, 2019: 225-242.
[27]	Biere A, Cimatti A, Clarke E, et al. Symbolic model checking without BDDs[C]// Cleaveland W R.Proceedings of the 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer, 1999: 193-207.
[28]	Oberhauser J, De Lima Chehab R L, Behrens D, et al. VSync: Push-button verification and optimization for synchronization primitives on weak memory models[C]// Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems. New York: ACM Press, 2021: 530-545.
[29]	Lu L Y, Arpaci-Dusseau A C, Arpaci-Dusseau R H, et al. A study of linux file system evolution[C]// Proceedings of the 11th USENIX Conference on File and Storage Technologies (FAST’13). New York: ACM Press, 2013, doi: 10.5555/2591272.2591276.
[30]	Lamport L. The part-time parliament[J]. ACM Transactions on Computer Systems, 1998, 16(2): 133-169. DOI URL
[31]	Lamport L, Matthews J, Tuttle M, et al. Specifying and verifying systems with TLA⁺[C]// Proceedings of the 10th Workshop on ACM SIGOPS European Workshop. New York: ACM Press, 2002: 45-48.
[32]	Ongaro D, Ousterhout J. In search of an understandable consensus algorithm[C]// Proceedings of the 2014 USENIX conference on USENIX Annual Technical Conference. New York: ACM Press, 2014: 305-320.
[33]	Wang Z G, Zhao C G, Mu S, et al. On the parallels between paxos and raft, and how to port optimizations[C]// Proceedings of the 2019 ACM Symposium on Principles of Distributed Computing. New York: ACM Press, 2019: 445-454.
[34]	Begoli E, Camacho-Rodríguez J, Hyde J, et al. Apache Calcite: A foundational framework for optimized query processing over heterogeneous data sources[C]// Proceedings of the 2018 International Conference on Management of Data. New York: ACM Press, 2018: 221-230.
[35]	Wang Z G, Zhou Z, Yang Y C, et al. WeTune: Automatic discovery and verification of query rewrite rules[C]// Proceedings of the 2022 International Conference on Management of Data. New York: ACM Press, 2022: 94-107.
[36]	Kim J, Sjöberg V, Gu R H, et al. Safety and liveness of MCS lock—Layer by layer[C]// Proceedings of the 15th Asian Symposium on Programming Languages and Systems. Berlin: Springer, 2017: 273-297.
[37]	Chabbi M, Fagan M, Mellor-Crummey J. High performance locks for multi-level NUMA systems[J]. ACM SIGPLAN Notices, 2015, 50(8): 215-226.
[38]	Dice D, Kogan A. Compact NUMA-aware locks[C]// Proceedings of the Fourteenth EuroSys Conference 2019. New York: ACM Press, 2019: 1-15.
[39]	Herlihy M P, Wing J M. Linearizability: A correctness condition for concurrent objects[J]. ACM Transactions on Programming Languages and Systems, 1990, 12(3): 463-492. DOI URL
[40]	Biely M, Milosevic Z, Santos N, et al. S-paxos: Offloading the leader for high throughput state machine replication[C]// Proceedings of the 2012 IEEE 31st Symposium on Reliable Distributed Systems. Piscataway: IEEE Press, 2013: 111-120.
[41]	Marandi P J, Primi M, Schiper N, et al. Ring Paxos: A high-throughput atomic broadcast protocol[C]// Proceedings of the 2010 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN). Piscataway:IEEE Press, 2010: 527-536.
[42]	Abadi M, Lamport L. The existence of refinement mappings[J]. Theoretical Computer Science, 1991, 82(2): 253-284. DOI URL
[43]	Zhou Q, Arulraj J, Navathe S B, et al. SPES: A symbolic approach to proving query equivalence under bag semantics[C]// Proceedings of the 2022 IEEE 38th International Conference on Data Engineering (ICDE). Piscataway:IEEE Press, 2022: 2735-2748.
[44]	Chu S M, Weitz K, Cheung A, et al. HoTTSQL: Proving query rewrites with univalent SQL semantics[J]. ACM SIGPLAN Notices, 2017, 52(6): 510-524. DOI URL

形式化方法与系统软件：实践与发展建议

Formal Methods and System Software: Practice and Suggestions

RichHTML

PDF

可视化

摘要/Abstract

引用本文

使用本文

图/表 5

参考文献 44

相关文章 3

编辑推荐

Metrics

访问统计

友情链接

联系我们

官方微信公众号

[1]	詹乃军, 王戟. 复杂系统规约、分析与验证发展现状与展望[J]. 前瞻科技, 2023, 2(1): 7-22.
[2]	吕继东, 卢万里, 唐涛, 罗正伟. 列车运行控制系统的形式化研究进展与趋势[J]. 前瞻科技, 2023, 2(1): 106-117.
[3]	陈厅, 吴国政, 刘哲, 蒲戈光, 赵瑞珍, 刘克. NSFC形式化方法领域基金项目申请资助情况分析[J]. 前瞻科技, 2023, 2(1): 132-140.