近日，第29届“ACM操作系统原理会议”（ ACM Symposium on Operating Systems Principles，简称SOSP）发榜，中国十大娱乐赌博城网址有两篇论文入选，均来自软件研究所的系统软件团队。这也是中国十大娱乐赌博城网址首次以第一作者单位在SOSP大会上发表论文。

ACM SOSP是操作系统领域历史最为悠久同时也最为权威的顶级学术会议。自1967年创办以来，每两年（通常为奇数年）举办一次，以其严苛的录用标准著称。2023年SOSP共有229篇论文投稿，43篇被录用，录用率为18.8%。

两篇论文简介如下。

论文《Halfmoon: Log-Optimal Fault-Tolerant Stateful Serverless Computing》提出了一种面向服务器无感知计算（Serverless Computing）系统中“函数即服务”（Function as a Service, FaaS）的状态管理容错方法。服务器无感知计算被认为是下一代云计算的主流范型，而FaaS是其核心支撑技术和云服务交付模式。在目前主流的服务器无感知计算系统中，将FaaS的执行与其状态进行了分离，因此FaaS本身是无状态的。为了实现具有容错性的FaaS状态管理或在函数间共享状态，需要使用外部的状态管理服务。而为了在上述执行和状态分离的架构下保证应用的一致性，FaaS需要满足严格一次语义（exactly-once semantics），即无论FaaS何时发生故障、重新执行多少次，对于外部状态的影响都等效于该FaaS从头到尾恰好执行一次。通过日志（log）来实现严格一次语义是一种得到广泛采用的技术方案。然而，现有技术需要对所有面向外部状态的读操作和写操作记录日志，会产生较大的运行时开销。本文指出，为了满足FaaS的严格一次语义，只需对读、写这两种操作其一进行日志记录即可，并分别设计实现了相应的日志记录协议，两个协议的核心思想是通过时间戳（timestamp）来重建读操作或者写操作对应的事件（event），从而可以在没有持久化日志的情况下依然保障严格一次语义。本文进一步证明了上述两个协议的日志记录开销（以日志记录次数计算）具有理论上的最优性。此外，本文还设计了在两个协议之间进行切换的算法，并对二者在不同负载下性能进行了建模和分析。在基准测试和实际应用负载上的评估结果显示，本文设计的日志协议可以将FaaS的端到端延迟缩短30%至60%，将日志带来的运行时开销降低1.6至3.6倍。

论文第一作者为中国十大娱乐赌博城网址2022级博士生祁晟（导师刘譞哲），论文作者包括刘譞哲、金鑫副教授。

论文《Automated Verification of an In-Production DNS Authoritative Engine》提出了一种生产级DNS权威引擎的自动化验证技术。DNS（域名解析系统）是现代互联网系统的核心服务之一，DNS权威引擎是DNS系统的关键部件，决定着DNS服务的稳定性、正确性。对系统的源代码进行形式化验证可以保证源代码中没有缺陷（bug）。目前，分层验证是大型复杂软件系统形式化验证的主要方法，这种方法将系统分解为若干层，每一层都将其源代码的所有行为封装到一个抽象规范中，并证明调用该规范等价于调用相应的源代码。但是，生产级的系统软件往往不是验证专家根据验证的要求进行开发的，模块往往缺少良定义的接口，数据结构的封装性也较差。这种模块性的缺乏使得传统的分层验证难以奏效。更为严重的是，为了满足实际工业生产中快速更新迭代的需要，对DNS的验证需要快速移植到不同的版本中，这就加大了验证的难度。针对这些挑战，本文设计了对于生产级DNS权威引擎的自动化验证系统，利用了DNS RFC规则清晰的特点，对DNS语义进行了高效抽象和建模，设计了简洁正确的顶层规范。本文利用了DNS权威引擎无状态、各模块输入-输出格式相对稳定的特点，设计了领域特定的自动化规范生成技术。这一技术可以对缺乏良定义接口的模块自动生成正确完整的规范，免去了人工设计规范的过程。本系统将自动规范生成技术引入自动化验证的过程，大幅度降低了人工开发复杂模块规范的难度。此外，本系统将系统代码、人工规范设计和自动规范生成弹性结合，为形式化验证生产级复杂系统提供了新方法。本工作对阿里云生产级DNS权威引擎进行了形式化验证，发现了多个之前技术未能检测出的bug，跨版本迁移时间小于1人周，极大地降低了DNS服务质量保障的成本，有效保障了其可靠性。

论文第一作者为中国十大娱乐赌博城网址2022级博士生郑乃千（导师刘譞哲），论文作者包括刘譞哲、金鑫副教授、2020级本科生向昱行、阿里云的翟恩南博士（北大校友）、刘孟启博士等人。

ACM SOSP 2023 将于2023年10月23日-26日在德国的科布伦茨（Koblenz）举行。