先进数据系统实验室

北京时间2023年9月12日，EuroSys 2024 公布了论文入选结果，我实验室一篇论文“Noctua: Towards Practical and Automated Fine-grained Consistency Analysis”成功入选 EuroSys 2024 会议！本届会议共收到244篇投稿，最终接受39篇，录用率16.0%。向各位参与研究工作的老师、同学、合作者表示祝贺！

论文简介：

放宽强一致性在实现geo-replicated网络应用程序的可伸缩性和可用性中起关键性作用。然而，尽管现有众多分析工具，但在现代应用程序中确保宽松一致性的正确性仍然是一项挑战，这是因为这些应用程序通常是用动态语言编写的，并使用了高级的面向对象数据库抽象，而传统分析工具无法处理这类应用程序。

本工作中，我们设计了一个完全自动化的验证框架Noctua，用于理解这类网络应用程序中的细粒度一致性语义。框架的核心是一种简单的可验证语言SOIR，以弥合由高级语言逻辑和数据库交互组成的应用代码库和SMT求解器可验证的指令之间的语义差距。此外，我们提出了一个轻量级的程序分析器作为前端，该分析器利用应用开发框架的能力将一致性相关的副作用和应用不变式从源代码中提取为SOIR代码。最后，利用SMT求解器Z3构建验证后端，该后端使用一种新的SMT编码将SOIR代码直接而高效地映射到Z3代码，新编码将对象间的顺序信息和对象数据分离出来，从而增加了数据库语义的覆盖率。

借助Noctua，我们成功在真实的Python应用程序上执行了全自动的细粒度一致性分析，相比人工验证显著减少了人工验证成本，且验证结果符合预期。若集成一致性分析结果到运行时环境中，则有望显著提高受分析应用程序在分布式部署时的性能表现。

该项工作是由我实验室硕士生马凯、UC Irvine在读硕士生朱恩左（2021-2022，ADSL实验室实习生），李诚副教授，以及贝尔实验室的陈瑞川老师、休斯顿大学的颜枫老师、清华大学的陈康老师联合完成的。该论文的研究得到国家自然科学基金“泛在操作系统”专项支持。