CAREER: Verifying Distributed System Implementations

职业：验证分布式系统实施

• 批准号: 1749570
• 负责人: Zachary Tatlock
• 金额: $ 55万
• 依托单位: University of Washington
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-04-01 至 2025-03-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1749570&HistoricalAwards=false
• 关键词: CAREER; Verifying; Distributed; System; Implementations

Billions of people depend on distributed systems every day for health care, banking, transportation, and more. Despite costly testing efforts, these complex services still fail in practice, leading to data loss and major service outages that threaten everyone's convenience, finances, and safety. This project is developing the tools and techniques necessary to verify (mathematically prove) safety and reliability for distributed systems implementations under any combination of network and machine misbehaviors. The intellectual merits are to develop compositional verification techniques where the programmer can independently prove correctness for applications and reliability for fault-tolerance components. The broader significance and importance are to provide rigorous reliability guarantees for the core computational infrastructure society depends on and to train a new generation of engineers who will create high-performance, verified distributed systems implementations.This project aims to make verification tractable by developing verified system transformers which automatically wrap simple systems with fault tolerance mechanisms guaranteed to preserve equivalence. This approach separates concerns of application correctness from fault tolerance which eases proof effort and enables greater code reuse. Industrial practitioners are already using an early prototype verified system transformer as a guide in exploring designs and alternate implementations. An outcome of this project is an extensive library of such transformers covering a broad range of critical distributed system features including reconfiguration, ring maintenance, and software update.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

每天有数十亿人依赖分布式系统来获得医疗保健、银行、交通等服务。 尽管进行了昂贵的测试，但这些复杂的服务在实践中仍然失败，导致数据丢失和重大服务中断，威胁到每个人的便利性，财务和安全。该项目正在开发必要的工具和技术，以验证（数学证明）在网络和机器错误行为的任何组合下分布式系统实现的安全性和可靠性。智力的优点是开发组合验证技术，程序员可以独立地证明应用程序的正确性和容错组件的可靠性。更广泛的意义和重要性是为社会所依赖的核心计算基础设施提供严格的可靠性保证，并培养新一代的工程师，他们将创建高性能，验证分布式系统implementation.This项目的目的是使验证易于处理的开发验证系统transformers自动包装简单的系统与容错机制，保证保持等价性。这种方法将对应用程序正确性的关注与容错分离开来，从而简化了证明工作，并实现了更高的代码重用。行业从业者已经在使用早期原型验证系统Transformer作为探索设计和替代实现的指南。该项目的一个成果是一个广泛的此类变压器库，涵盖了广泛的关键分布式系统功能，包括重新配置、环维护和软件更新。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Relational e-matching

关系电子匹配

• 发表时间: 2022
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Yihong Zhang;Yisu Remy Wang;Max Willsey;Zachary Tatlock
• 通讯作者: Zachary Tatlock

egg: Fast and extensible equality saturation

Egg：快速且可扩展的平等饱和

• DOI: 10.1145/3434304
• 发表时间: 2021
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Willsey, Max;Nandi, Chandrakana;Wang, Yisu Remy;Flatt, Oliver;Tatlock, Zachary;Panchekha, Pavel
• 通讯作者: Panchekha, Pavel

QED at Large: A Survey of Engineering of Formally Verified Software

• DOI: 10.1561/2500000045
• 发表时间: 2019-09
• 期刊: ArXiv
• 作者: T. Ringer;Karl Palmskog;Ilya Sergey;Miloš Gligorić;Zachary Tatlock

Rewrite rule inference using equality saturation

• DOI: 10.1145/3485496
• 发表时间: 2021-08
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Chandrakana Nandi;Max Willsey;Amy Zhu;Y. Wang;Brett Saiki;Adam Anderson;Adriana Schulz;D. Grossman;Zach Tatlock

Small Proofs from Congruence Closure

同余闭包的小证明

• 发表时间: 2022
• 期刊: 2022 Formal Methods in Computer-Aided Design (FMCAD
• 作者: Oliver Flatt;Samuel Coward;Max Willsey;Zachary Tatlock;Pavel Panchekha
• 通讯作者: Pavel Panchekha