前瞻科技

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

PDF下载

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

前瞻科技 | 综述与述评 2023,2(1): 33-45

收起

前瞻科技 | 综述与述评 2023, 2(1): 33-45

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

全屏

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

作者信息

1.上海交通大学软件学院，上海 200240

2.华为德累斯顿研究所，德国德累斯顿 01069

丁浩然，博士研究生。研究方向为基于形式化方法的系统软件验证与优化。参与设计和实现了世界上第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

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

Affiliations

1. School of Software, Shanghai Jiao Tong University, Shanghai 200240, China

2. Huawei Dresden Research Center, Dresden 01069, Germany

出版时间: 2023-03-20 doi: 10.3981/j.issn.2097-0781.2023.01.003

文章导航

摘要

收起

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

关键词

形式化方法 / 操作系统 / 数据库 / 文件系统 / 分布式共识协议

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

引用本文

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

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

正文

收起

操作系统和编译器等系统软件是现代计算机应用运行的基础，已广泛应用于医疗、工业、军事、航空航天和能源等关键领域以及人们的日常生活中。系统软件中一个微小的漏洞就可能会导致重大的生命财产损失，所以保障系统软件的高可靠性至关重要。传统的软件测试等方法只能证明系统软件中存在错误，而不能彻底消除错误^[1]。随着系统软件的功能越来越多、代码规模越来越大、内部逻辑越来越复杂，如何保障系统软件的高可靠性是一个非常重要又极具挑战性的问题。

作为目前唯一已知的保证系统不存在代码错误的方法，形式化方法（Formal Methods）在系统软件领域正越来越多地被学术界和工业界关注和应用^[2]，微软、亚马逊、华为等企业纷纷加大对形式化方法领域的投入。形式化方法的基本思想是基于逻辑系统对系统软件的行为进行严谨的建模，并证明这些行为均满足某种开发者期望的性质。随着相关理论与逻辑的突破和证明工具的逐步完善，形式化方法正逐步从理论走向实践，从学术界走向工业界，并被成功用于构建具有高可靠性的系统软件。

1 形式化方法概述

收起

形式化证明系统软件正确性的基本流程包括对系统语义进行建模、定义待证明的性质和执行证明3部分。首先，需要通过形式化建模系统语义来描述系统所有可能的行为，不同的系统需要不同的建模方法。例如，串行程序的语义可以通过状态机（State Machine）建模^[3]，状态机的状态包括程序中每个变量的值和当前需要执行的代码，每执行一行代码就会修改状态机的状态，串行程序的行为可以通过状态机可达的状态描述。其次，需要明确什么样的软件行为是正确的行为，这种对正确性的定义称为规约（Specification）^[3]。例如，程序员在代码里面为函数功能编写的注释就是一种规约，但是这种基于自然语言编写的规约往往具有歧义，难以用于形式化证明。因此，形式化方法中通常使用更加严谨的逻辑公式编写规约，称为形式化规约（Formal Specification）^[3]。最后，形式化方法的目标是要证明软件的具体实现符合形式化规约。常用的证明方法主要包括定理证明（Theorem Proving）^[4]和模型检验（Model Checking）^[5-6]。下面将分别介绍这两种方法。值得注意的是，这两种方法并不是互斥的，近年来已经有工作尝试将两种方法相结合^[7]。

定理证明的基本想法是把证明目标作为一个数学定理，基于一系列推理规则推导出定理成立。按照自动化程度从低到高的顺序，定理证明可以分为交互式验证（Interactive Verification）^{[8⇓⇓⇓⇓⇓-14]}、半自动验证（Auto-active Verification）^{[15⇓⇓⇓⇓-20]}和一键验证（Push-button Verification）^[21-26]3类。交互式验证要求用户手动编写全部的定理推导证明过程。例如，在交互式证明工具Isabelle/HOL^[4]中，用户需要手动编写代码引用相关定理推导出证明目标成立。半自动验证只需要用户提供一小部分证明过程，大部分证明过程可以由证明工具自动完成。例如，微软开发的工具Dafny^[20]就是一种常见的半自动验证工具。一键验证只需要程序员手动定义形式化规约，全部的证明过程都可以自动完成。符号执行（Symbolic Execution）是常见的一键验证方法之一^[26]，基本思想是把程序的输入看作可能取任意值的符号，这样可以表示所有可能的程序输入。然后用这些符号表示程序的运行结果，这样就能表示所有可能的程序运行结果。最后证明所有可能的运行结果都满足形式化规约。半自动和一键验证工具通常基于可满足性模理论（Satisfiability Modulo Theories, SMT）求解器等约束求解工具^[21]实现自动化。验证工具先把验证目标表示为一阶逻辑公式，然后再将公式输入SMT求解器，最后SMT求解器自动对公式进行验证并输出结果，如果验证不通过，SMT求解器还会给出反例。这3种形式化方法各有利弊，并不存在最优的形式化方法。对于自动化程度高的形式化方法，其优势在于人力成本低、易用性好，但是这类方法证明能力有限。对于自动化程度低的形式化方法，其优势在于证明能力更强，可以验证更多种类的程序和性质，但是手动编写证明过程的时间和人力成本随着系统软件代码量的增加而迅速增加。

模型检验的基本想法是自动遍历程序运行过程中所有可达的程序状态，检查程序运行过程中是否产生了违反规约的行为，如果有则输出反例，否则程序满足规约。如果需要检查的程序状态过多，模型检验可能无法在可接受的时间内终止，程序中的循环次数太大以及并发线程的数量过多等因素都有可能导致这种问题。因此，模型检验的主要挑战就在于如何处理程序状态爆炸的问题。限界模型检验（Bounded Model Checking）是处理该挑战的常用方式之一^[27]，其基本想法是针对可能造成状态爆炸的模型参数设置边界，包括限制循环最大迭代次数等，这样就可以有效避免状态爆炸问题。限界模型检验的主要缺点是不能保证发现程序中所有的错误，因为有些错误可能需要更多的并发线程数量或者更大的循环迭代次数等才能触发。限界模型检验的主要优点是在某些场景下仍然能够有效地发现错误，这是因为有些代码错误只需要较少的循环迭代次数和并发线程数量就会被触发。

2 国内外研究态势

收起

首先介绍国内外将形式化方法用于系统软件的部分代表性工作，包括前期一些里程碑式的工作，然后对国内外的研究现状进行对比分析。

seL4是第1个被完全形式化验证过的通用操作系统内核^[2]，澳大利亚新南威尔士大学等机构的研究人员使用交互式证明工具Isabelle/HOL^[4]开发验证。验证seL4的基本想法是先使用Isabelle/HOL形式化定义一个抽象的操作系统作为形式化规约，这个抽象操作系统简洁地描述了seL4应该实现的所有功能，然后再通过一系列定理推导证明seL4和抽象的操作系统功能相同，以此证明seL4的正确性。这个项目的主要缺点是研究人员没有给出验证细粒度并发系统的方案，只验证了串行操作系统，其中的同步原语等部分代码也没有被形式化验证过。

Certiucos项目^[9]对验证并发操作系统进行了探索，验证了一个商用抢占式操作系统µC/OS-II的核心模块，验证的重点是中断导致的程序并发执行，由中国科学技术大学的研究人员使用交互式证明工具验证。具体来说，研究人员对每个函数定义了对应的抽象函数作为形式化规约，这些抽象函数只描述函数功能，隐藏了具体实现细节。研究人员证明每个C语言实现的函数都和其对应的抽象函数功能相同，以此证明了操作系统正确性。在验证并发程序方面，研究人员通过验证单个线程执行行为的正确性推导出操作系统在并发执行情况下的正确性。这项工作的主要缺点是人力成本很高，整个项目编写了20万行以上的证明代码，耗费5.5人年^[9]。

Jitterbug^[23]是第1个能够对伯克利包过滤器（Berkeley Packet Filter, BPF）程序的编译器进行一键验证的框架，由美国华盛顿大学的研究人员基于符号执行工具Serval^[26]实现。具体来说，形式化规约被定义为编译器总是输出正确的编译结果，即输出的机器代码和输入编译器的BPF程序功能一致。Jitterbug通过证明每一条BPF程序指令的编译结果都是正确的，进而推导出整个BPF程序的编译结果是正确的。研究人员将Jitterbug用于多个已有编译器，成功找到并修复了16个前所未知的错误^[23]。Jitterbug的主要问题是只针对BPF程序的编译器，不能一键验证任意的其他语言的编译器。

国内和国外在研究方向和发展趋势方面基本相同。具体来说，证明手段从交互式验证逐步向半自动验证、一键验证发展，追求越来越低的验证成本和越来越快的验证速度。例如，seL4^[2]的验证使用的是交互式证明工具，而后来的操作系统验证工作Hyperkernel^[3]则实现了一键验证。证明的性质从简单的串行系统的功能正确性转为其他更加复杂的重要性质，包括并发系统的功能正确性、安全性等。例如，2015年美国麻省理工学院验证了一个串行文件系统FSCQ^[8]，其后的DaisyNFS^[19]等工作则是证明并发文件系统。在研究成果方面，国外由于从20世纪就开始研究如何将形式化方法应用于系统软件，近年来在操作系统、编译器、文件系统、分布式系统和分布式协议等方面都涌现出了丰硕的研究成果，包括第1个形式化验证过的崩溃安全（Crash-safe）的磁盘文件系统FSCQ^[8]、第1个能够半自动验证分布式系统功能正确性和活性（Liveness）的工具IronFleet^[15]、第1个一键验证BPF代码编译器的框架Jitterbug^[23]等。相比较而言，国内在这方面的研究工作起步较晚，目前相关的研究机构和人员数量也较少，但是近年来在部分系统软件的验证方面也取得了不俗的成绩。例如，南京大学和中国科学技术大学研究团队的工作CASCompCert^[14]针对并发程序编译器的形式化验证提出了新的理论并构建了验证框架，相关论文获得第40届程序设计语言设计与实现会议（ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019）杰出论文奖;华为公司和上海交通大学等机构的研究团队针对弱内存模型下同步原语的一键验证及优化提出了新的理论和工具^[28]，相关工作获得第26届编程语言和操作系统的体系结构支持国际会议（ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2021）杰出论文奖。

3 形式化方法在系统软件中的实践

收起

本节介绍上海交通大学并行与分布式系统研究所及相关合作者将形式化方法应用于系统软件的5个具体案例并进行总结，如图1所示。

研究人员自底向上对同步原语、文件系统、分布式共识协议和数据库这些系统软件栈中的一系列核心组成部分进行了形式化验证。摩尔定律失效后硬件架构向多核方向发展，使用于并发控制的同步原语的正确性和性能变得尤其重要，研究人员提出了自动验证和优化弱内存模型下同步原语^[28]以及自动合成并验证非均匀访存模型（Non Uniform Memory Access, NUMA）架构下锁的方法^[7]。基于同步原语，开发人员能够构建更加复杂的系统软件。作为上层应用运行的基础，系统软件的可靠性同样重要^[29]。因此，研究人员构建了第1个形式化验证过的细粒度并发文件系统AtomFS^[10]。除了单机系统软件之外，随着分布式计算的发展，基于分布式共识协议（Distributed Consensus Protocol）^[30]构建的分布式系统的可靠性也变得非常重要。于是，研究人员基于形式化验证工具TLA⁺（Temporal Logic of Actions⁺）^[31]对主流共识协议Paxos^[30]和Raft^[32]的原理进行了深入研究^[33]。基于规则的结构化查询语言（Structured Query Language, SQL）重写是优化数据库SQL查询性能的常用技术之一^[34]，不正确的规则会导致重写后的SQL语句返回错误的结果。研究人员基于形式化方法保障了规则的可靠性^[35]。

3.1 弱内存模型下同步原语的验证与优化

同步原语的正确性和性能对于弱内存模型下并发程序的正确性和性能非常重要，然而弱内存模型下同步原语的正确性和性能之间存在矛盾，难以兼顾，如何解决两者之间的跷跷板问题是一个非常重要且具有挑战性的研究方向。在正确性方面，同步原语出错的主要原因是弱内存模型下允许更多可能的内存访问乱序执行。为了避免错误，程序员需要在代码中的某些位置插入内存屏障（Memory Barrier）以避免某些乱序执行的发生^[28]。内存屏障越多，越有可能减少并发错误。在性能方面，有时只需要在部分代码处插入内存屏障就可以保障同步原语的正确性，增加不必要的内存屏障会带来不必要的性能开销。所以内存屏障的数量应该尽可能少。

VSync是第1个自动化验证并优化弱内存模型同步原语的系统^[28]，由华为公司、上海交通大学和德国马克斯·普朗克研究所的研究人员合作完成，使用状态机建模程序语义，基于模型检验实现一键验证。如图2所示，给定一个同步原语的源代码，VSync的基本想法是先通过搜索器自动搜索可能的插入内存屏障的方案，再基于形式化验证器从中筛选出能够保证同步原语正确性的方案，最后从这些能保证正确性的方案中选择内存屏障性能开销最小的方案作为VSync的输出。VSync在保证同步原语正确性的前提下尽可能减少不必要的内存屏障，兼顾了正确性和性能。

循环给同步原语的形式化验证带来了巨大的挑战。同步原语的代码中常常使用循环来实现等待其他线程释放锁等功能，这类循环的最大迭代次数往往没有上界，称为无界循环（Unbounded Loop）^[28]。证明同步原语的正确性需要检查并发下所有可能的执行情况，因为无界循环的迭代次数没有上界，所以不可能通过枚举所有可能的循环迭代次数来遍历所有可能的执行情况，否则验证将无法终止。为了应对这个挑战，VSync基于对同步原语中无界循环特点的观察提出了新的验证技术，避免了枚举所有可能的循环迭代次数。如果同步原语实现正确，那么VSync的验证器会在有限时间内输出验证通过，否则验证器会输出反例。

与已有只关注同步原语正确性的工作^[5,36]相比，VSync这一工作的重要意义之一在于，其证明了形式化方法不仅可以保证正确性，还能优化性能。另外，VSync实现了对含无界循环同步原语的一键验证，验证速度比已有的交互式^[36]或自动化验证工具^[5]也有明显提升。

3.2 NUMA架构下锁的生成和验证

在NUMA架构下实现高性能且正确的锁是一件非常重要又有挑战性的事情^[37-38]。一方面，NUMA架构下复杂的内存层级对程序的性能影响巨大^[7]。例如，同一个NUMA节点线程之间的数据访问速度往往快于不同NUMA节点线程之间的数据访问速度，而在同一个NUMA节点内部还有高速缓存（Cache）等更多内存层级。另一方面，针对不同体系结构下NUMA架构的不同层级，并不存在唯一一种性能最优的锁，不同NUMA架构下的不同层级应该使用不同的锁。因此，如何针对给定的NUMA架构自动合成性能较优的锁并保证正确性是一个很有价值的问题。

CLoF是第1个针对NUMA架构自动合成并验证锁的系统^[7]，由华为公司、德国德累斯顿工业大学和上海交通大学的研究人员合作完成，基于3.1节中介绍的VSync^[28]实现。具体流程如图3所示，首先CLoF会对给定的NUMA架构中的内存层级进行分析。然后给每个层级选择一种锁的实现，组合不同层级的锁自动合成针对NUMA架构的新的锁。最后，通过运行性能测试在众多不同的组合方案中选择一种性能最优的方案作为CLoF的输出。这样，CLoF系统就能充分利用NUMA架构的硬件特性实现高性能的锁。与此同时，CLoF基于前文VSync中提出的形式化方法保证合成的锁的正确性。

每个合成锁是由不同内存层级的锁共同组成的。CLoF在形式化验证方面面临的主要挑战是合成的锁较为复杂、代码量大，直接使用VSync验证会导致验证时间过长。为了应对这个挑战，CLoF基于数学归纳法的思想对合成的锁进行验证。首先，CLoF用VSync的验证器验证了每个内存层级可以选择使用的锁，如MCS锁和CLH锁等，这些锁的代码量不大，验证器会在可接受的时间内给出验证结果。然后，CLoF证明了任意给定两个已被证明正确性的锁，组合这两个锁合成的新锁也能保证正确性，从而进一步推导出整个合成的锁是正确的，解决了验证过程超时的问题。

3.3 并发文件系统的验证

AtomFS^[10]是第1个被形式化验证过的细粒度并发内存文件系统，由上海交通大学、华为公司和美国哥伦比亚大学的研究人员合作完成。AtomFS使用细粒度inode锁，为应用程序提供mkdir、rename等原子的操作接口。

AtomFS的证明目标是每个文件系统操作的可线性化（Linearizability）^[39]，即每个文件系统接口都提供原子的操作语义。可线性化要求对并发系统每个接口的调用都在调用开始到调用结束之间的某个时间点瞬间生效，这个时间点就被称作可线性化点（Linearization Point）^[10]。如果并发系统满足可线性化的要求，那么对于操作间任意的并发执行，都可以根据各个操作可线性化点的发生时间构造出一个操作间的顺序，按照这个顺序串行执行各个操作可以得到和并发执行完全相同的执行结果。如图4所示，如果文件系统满足可线性化的要求，那么给定一种unlink操作和mkdir操作并发执行的情况，可以基于unlink的可线性化点在mkdir可线性化点之前这一信息，构造出一个先执行unlink后执行mkdir的串行执行情况。在串行执行和并发执行下，都是unlink操作失败，mkdir操作成功，文件系统中新增加一个目录b。

验证AtomFS的基本步骤如下：①研究人员采用公理语义形式化建模文件系统的行为，即通过一系列的公理定义每条程序指令的行为，从而描述出整个程序的行为;②根据可线性化的定义，手动寻找每个操作内部实现中的可线性化点并进行证明。与FSCQ^[8]、Yggdrasil^[22]等已有的验证串行文件系统的工作相比，AtomFS的主要贡献在于证明了细粒度并发的文件系统。当文件系统代码存在错误时，会无法正常推导证明过程，但是AtomFS使用的交互式验证工具并不会给出反例，也不会告知具体哪行代码有错误，需要使用者自行定位错误位置。

3.4 分布式共识协议优化算法的移植与验证

分布式共识协议对于分布式系统的可用性来说非常重要。当分布式系统中有节点发生崩溃后，剩余节点需要快速针对系统对外应当表现出的行为达成共识，例如节点收到用户读请求后需要确定应当返回的值。这时就需要运行分布式共识协议，选出一个新的节点作为领导者（Leader），用于决定这些事情。

Paxos协议^[30]是历史悠久的经典分布式共识协议，然而由于其难以被人理解，近年来在工业界正逐渐被另一个分布式共识协议Raft^[32]所取代。Raft协议和Paxos协议有很多相似之处，例如它们的执行流程都可以分为两个对应的阶段，它们有着相似的协议状态。这种相似性引起人们思考两个问题：第一，这两个协议是否等价?第二，已有的针对Paxos协议的优化算法^[40-41]是否可以自动移植到Raft协议上?研究这两个问题有利于加深对这两个协议原理的理解，并且如果第2个问题的答案是肯定的，那么就可以轻易地复用Paxos协议有关的优化算法。

上海交通大学、美国纽约大学和美国纽约州立大学石溪分校的研究人员合作进行了研究，并首次回答了这两个重要的问题^[33]。针对上述第一个问题，虽然Raft协议和Paxos协议的具体运行流程有很多相似点，但是它们并不等价。研究人员首先通过状态机形式化建模协议的语义，协议的状态由分布式系统中每个节点的状态组成，包括每个节点是否已经被选为领导者等，执行协议就是修改每个节点的状态。然后基于协议状态定义协议之间的等价性，具体来说，在两个协议的运行过程中，应当可以将每个Raft的协议状态映射到Paxos的协议状态，这种映射称之为精化映射（Refinement Mapping）^[42]。之后研究人员证明了Paxos和Raft的协议状态之间不存在精化映射，所以Paxos和Raft不等价。

针对上述第2个问题，Paxos和Raft两个协议之间不等价，Paxos上的优化算法也难以自动移植到Raft上。但是研究人员设计了一个Raft协议的变种Raft*，并基于交互式的形式化验证工具TLA^+[31]手动编写证明过程，证明了每个Raft*的协议状态可以映射到Paxos的协议状态。研究人员还进一步提出了把Paxos协议的状态恒定优化算法自动移植到Raft*协议上的方法。状态恒定优化是指不会修改原有协议状态的优化算法，研究人员手动证明了这种移植方法的正确性。

3.5 数据库查询的自动化验证

基于规则的SQL语句重写是优化数据库查询性能的关键技术之一^[34]。给定一条SQL查询语句，数据库系统会尝试将其重写成另外一条语义等价但是性能更优的SQL语句。语义等价是指在任意的数据库状态上执行两条SQL查询语句，它们的返回结果总是相同的。例如，当dept.id是emp.deptid的外键时，“SELECT emp.id FROM emp LEFT JOIN dept ON emp.deptid = dept.id”可以重写为“SELECT emp.id FROM emp”，因为去掉了LEFT JOIN，所以查询的时延显著降低。数据库系统中往往集成了很多条不同的重写规则，用于重写不同形式的查询语句。具体来说，重写规则包含前提条件C、源逻辑查询计划Qsrc和目标逻辑查询计划Qdest，在C成立并且给定SQL语句的逻辑查询计划和Qsrc相匹配时，可以按照Qdest把给定的SQL语句重写为与Qdest匹配的另一条新的SQL语句。

数据库中现有的规则不足以优化网络应用中的查询语句。数据库系统中包含的重写规则是由经验丰富的专家手动设计，耗费了数十年时间积累，规则数量的增长速度非常缓慢，难以用于重写网络应用中复杂的查询语句。研究人员在GitHub上收集了50个与优化SQL查询性能相关的issue，目前重写能力最强大的数据库系统Microsoft SQL Server只能重写和优化其中23个^[35]。

WeTune是第1个基于形式化方法自动生成并验证重写规则的系统^[35]，由上海交通大学和美国纽约大学的研究人员合作完成。如图5所示，WeTune系统的基本想法是首先在一定的搜索空间内枚举潜在的重写规则，这可以通过枚举可能的前提条件和逻辑查询计划实现。然后，WeTune基于形式化验证筛选出其中正确的规则。最后，WeTune通过评估重写前后查询语句的性能，找到其中真正能够用于优化SQL查询性能的有效的重写规则。

WeTune系统面临的主要挑战是如何验证重写规则的正确性，其实现了一个重写规则验证器应对这个挑战。给定一条重写规则<Qsrc, Qdest, C>，其正确性定义为在前提条件C成立的情况下，改写前后的两个SQL查询语义等价。为了形式化建模一条SQL查询的语义，WeTune自动把SQL查询转为代数结构U半环表达式（U-semiring Expression）^[35]。具体来说，一个U半环表达式是一个函数f (t)，输入t是一个元组（Tuple），返回值是t在SQL查询结果中的数量。于是，证明两个SQL查询等价就变成了证明其U半环表达式等价。WeTune自动将U半环表达式等价问题转换成一阶逻辑表达式，利用现有的SMT求解器Z3^[21]自动证明这个公式是否成立。如果成立，那么重写规则就是正确的，否则该重写规则不正确。为了增强验证能力，WeTune还支持集成其他已有的验证工具^[43-44]。

3.6 实践经验总结

形式化方法在提高系统软件可靠性方面已经有了一些成功的实践。具体来说，形式化方法可以验证系统核心模块的关键性质，简化模块维护与重构;定义形式化规约可以精确定义系统需求，减少对软件功能理解上的歧义;形式化证明系统设计符合形式化规约并且代码实现和系统设计一致可以有效减少系统中的错误;除了检查软件是否有错误之外，形式化方法甚至可以进一步辅助部分代码实现的自动生成，并用于优化软件性能。

受到验证成本和工业界具体需求的影响，形式化方法在系统软件领域的应用呈现出如下特点：第一，程序员只针对某种特定的性质或者系统软件中的某个关键组成部分进行验证，而不是证明整个系统软件的正确性;第二，为了保障高可靠性，程序员会同时结合多种验证方法，分别验证系统软件的不同组成部分和不同性质;第三，程序员会倾向于使用轻量级的形式化方法和工具，降低形式化证明带来的人力和时间成本;第四，除了可靠性外，工业界对系统软件往往还有很高的性能诉求，不能为了降低形式化验证的难度而过度简化验证目标牺牲性能。

4 形式化方法在系统软件中的挑战与发展建议

收起

4.1 挑战

基于实践过程中遇到的问题，总结了将形式化方法用于系统软件面临的理论和工程两方面挑战。

理论方面：①为了形式化规约能够尽可能简洁，其定义通常建立在对底层机器的抽象上，而不会保留硬件特性的全部细节。这种抽象和真实的硬件之间存在差距，可能导致形式化规约不能描述程序在机器上实际运行时可能产生的全部行为，导致验证过的程序在执行时出错。②系统软件中某些性质的验证目前缺少实现自动化的理论基础，导致自动化证明工具的验证能力有限，难以证明复杂性质和大规模系统。而使用自动化程度较低的方法成本很高，可能无法接受。

工程方面：①软件的开发设计人员难以理解形式化规约的含义，从而也很难判断形式化方法专家编写的形式化规约是否正确。一方面，系统软件通常用C、C++或者汇编等语言实现，而形式化规约通常使用谓词逻辑公式等数学符号编写，两者之间的形式差距较大;另一方面，系统软件中的功能越来越复杂，难以抽象为简短的公式，导致编写出的形式化规约也较为复杂。②学术界的相关研究比较分散，涌现出了针对不同场景和不同性质的多种验证工具。这些工具可能基于不同的公理系统和符号定义等，导致它们相互之间无法复用彼此的证明代码。即使对于同一个形式化证明工具，证明代码仍然可能难以得到有效维护和更新，新版本的验证工具可能无法正常运行和检查使用旧版本工具编写的证明过程。③在验证不通过时，验证工具可能无法提供有效的调试信息。系统软件开发者和形式化方法专家需要手动定位错误的具体位置和原因，系统实现、证明过程甚至形式化规约都有可能出错。

4.2 发展建议

针对上述挑战，从理论和系统两方面对如何更好地使用形式化方法提高系统软件可靠性提出如下建议。

理论方面：①形式化验证方面的理论专家在建模系统行为时需要深入理解系统硬件方面的具体特性，需要更加严谨的理论对底层机器的行为进行建模，不能对系统行为过度简化。②针对超大规模的系统软件和一些复杂的性质进行严格的形式化证明是非常困难的，这时候可以考虑牺牲一部分可靠性或者完备性，使得形式化方法用于超大规模代码和复杂性质成为可能。

工程方面：①在工业界应用形式化方法时，应当在系统软件开发者和学术界的形式化验证专家之间建立更好的协作机制。系统软件开发者对于系统的性质和原理了解得更加透彻，形式化验证专家则对不同验证方法和相关理论更加熟悉，好的协作机制有利于让形式化验证专家编写的规约切实反映出系统开发者对系统行为正确性的预期。②形式化验证专家应当为编程语言进行统一的形式化建模，使得多种不同的形式化方法可以被集成到开发工具链中。验证工具能够自动生成相关引理并使用不同方法进行验证。此外集成方式应该具有较强的开放性，以便于引入学术界提出的新技术或者对已有工具进行组合。③形式化验证专家不仅要提供证明系统正确的方法，也要提供证明系统不正确的方法。当验证不通过的时候验证工具应当生成反例，提供更多有用的调试信息。

针对未来如何改善国内的研究现状，提出如下3点建议。

（1）工业界和学术界应当建立密切的合作关系，这有利于形式化验证专家深入理解系统特点，找到真实且有价值的研究问题，解决企业痛点。

（2）在研究理论问题的同时也要关注工程方面面临的挑战，这有利于开发出较为轻量级的验证工具，使得研究成果能够真正落地到大规模真实系统软件中。

（3）相关研究应该注意增强连续性，使得后续研究能够基于之前的研究成果和系统代码。

5 结束语

收起

随着系统软件在越来越多关键行业中得到深入应用且功能日趋复杂，如何保障其安全与可靠性变得越来越重要。因此，如何应用形式化方法协助构建具有高可靠性的系统软件将会是一个越来越重要的研究方向，这对于医疗、工业、军事、航空航天和能源等关键领域尤其重要。

形式化方法对于构建可信赖的系统软件有极大潜力，已经成功应用在操作系统、文件系统、分布式系统和数据库系统等关键系统软件模块中。目前形式化方法仍然面临诸多理论和工程等方面的挑战。更好地将形式化方法用于提高系统软件可靠性，需要学术界和工业界协同配合，建立一个学术界和工业界公共的研发平台;需要考虑将相关学术成果应用到工业界具体场景下的工程开发问题;需要更好的理论和工程实践以支持大规模形式化验证。

参考文献

收起

文献

收起

参考文献引证文献

排序方式：

[1]

王戟, 詹乃军, 冯新宇, 等. 形式化方法概貌[J]. 软件学报, 2019, 30(1): 33-61.

[2]

Klein

, Elphinstone

, Heiser

, 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

, Sigurbjarnarson

, 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

, Paulson

L C

, Wenzel

. Isabelle/HOL: A proof assistant for higher-order logic[M]. Berlin, Heidelberg: Springer, 2002.

[5]

Kokologiannakis

, Vafeiadis

. 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

. 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

, Behrens

, 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

, Chajed

, 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]

F W

, Fu

, 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

, Ding

H R

, Du

, 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]

R H

, Shao

, Chen

, 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

, Dall

, 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

, Tassarotti

, Theng

, 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

, Howell

, Kapritsos

, 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

, Hawblitzel

, Kapritsos

, 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

, 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

, Lattuada

, Hawblitzel

, 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

, Tassarotti

, Theng

, 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

, Bjørner

. 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

, Bornholt

, Torlak

, 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

, van Geffen

, Torlak

, 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

, Tao

, Gu

, 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

, Bodik

. 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

, Bornholt

, 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

, Cimatti

, Clarke

, 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

, De

Lima Chehab R L

, Behrens

, 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]

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

. The part-time parliament[J]. ACM Transactions on Computer Systems, 1998, 16(2): 133-169.

https://doi.org/10.1145/279227.279229

[31]

Lamport

, Matthews

, Tuttle

, 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

, Ousterhout

. 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

, 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

, Camacho-Rodríguez

, Hyde

, 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

, 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

, Sjöberg

, 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

, Fagan

, Mellor-Crummey

. High performance locks for multi-level NUMA systems[J]. ACM SIGPLAN Notices, 2015, 50(8): 215-226.

[38]

Dice

, Kogan

. 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.

https://doi.org/10.1145/78969.78972

[40]

Biely

, Milosevic

, Santos

, 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

, Schiper

, 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

, Lamport

. The existence of refinement mappings[J]. Theoretical Computer Science, 1991, 82(2): 253-284.

https://doi.org/10.1016/0304-3975(91)90224-P

[43]

Zhou

, Arulraj

, 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

, Cheung

, et al. HoTTSQL: Proving query rewrites with univalent SQL semantics[J]. ACM SIGPLAN Notices, 2017, 52(6): 510-524.

https://doi.org/10.1145/3140587.3062348

2023年第2卷第1期

PDF下载

2909

1473

引用本文

BibTeX

文章信息

doi: 10.3981/j.issn.2097-0781.2023.01.003

接收时间：2023-01-06
出版时间：2023-03-20
发布时间：2023-03-24

补充材料

相关文章

文章信息

作者

出版历史

收稿日期：2023-01-06
修回日期：2023-02-09

基金

作者信息

1.上海交通大学软件学院，上海 200240

2.华为德累斯顿研究所，德国德累斯顿 01069

通讯作者:

^†

参考文献

分享链接

https://castjournals.cast.org.cn/joweb/qzkj/CN/10.3981/j.issn.2097-0781.2023.01.003

分享至

全文二维码

扫描看全文

引用本文

BibTeX

本文的引用情况

表12种不同金属材料的力学参数

科 Family	属数 Number of genus	种数 Number of species	占总种数比例 Percentage of total species (%)	属 Genus	种数 Number of species	占总种数比例 Percentage of total species (%)
鹅膏菌科Amanitaceae	2	11	5.26	鹅膏菌属 Amanita	10	4.78
小菇科 Mycenaceae	2	12	5.74	丝盖伞属 Inocybe	5	2.39
多孔菌科 Polyporaceae	8	14	6.70	蜡蘑属 Laccaria	5	2.39
红菇科 Russulaceae	3	23	11.00	小皮伞属 Marasmius	6	2.87
				小菇属 Mycena	11	5.26
				光柄菇属 Pluteus	5	2.39
				红菇属 Russula	17	8.13
				栓菌属 Trametes	5	2.39

关闭全屏

BibTeX
EndNote
RefWorks
TxT

访问统计

友情链接

联系我们

官方微信公众号