CAREER: Building Reliable Distributed Systems with Refinement Types

该奖项的全部或部分资金来自《2021年美国救援计划法案》(公法117-2)。当今最重要的计算机系统是分布式系统：由多台机器通过在网络上发送消息进行通信，单个机器或网络连接可能独立发生故障的系统。由于消息被重新排序或延迟，以及机器和网络连接发生故障的可能性，对此类系统进行编程是出了名的困难和容易出错。例如，广泛使用的协议旨在确保给定的消息传递顺序或给定的数据一致性策略，但确保这些协议的可执行实现的正确性的机器检查的证明很少。这个项目的目标是使用内置到通用编程语言中的强大工具，机械地验证分布式系统的真实、可执行的实现。该项目的新奇之处在于它专注于可立即执行的实现，以及它的模块化验证方法，该方法将较低级别的消息传递问题与较高级别的应用程序语义分开。该项目的影响将是提高分布式软件系统的整体可信性和可靠性。该项目还旨在通过将有关分布式系统验证的杂志和视频的创建整合到研究人员和项目团队的教学和研究实践中，并将生成的材料在网上免费提供，从而创建可接近的研究入口点，并发展学生的科学交流技能。该项目的语言级别分布式系统验证的方法以细化类型为中心：数据类型允许程序员指定逻辑谓词，以限制由类型描述的值的集合，并且可以在编译时由SMT求解器进行检查。该项目使用Liquid Haskell，它扩展了Haskell编程语言，支持精化类型，并可进一步用于外部验证，即定义函数来陈述和证明定理。研究人员和团队将使用Liquid Haskell开发机械验证的模块化程序库，以实现分布式系统。新的经过验证的消息传递库将构成其他经过验证的组件的基础，例如提供复制数据类型和分布式数据存储的库。此外，该项目还研究如何将Liquid Haskell的优点与AGDA等交互证明助手的优点结合起来。这些调查的最终结果是对这种混合的自动化/交互验证工具进行全面调查，并提供对设计空间的整体科学理解。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

This award is funded in whole or in part under the American Rescue Plan Act of 2021 (Public Law 117-2).Today's most important computer systems are distributed systems: those that consist of multiple machines that communicate by sending messages over a network, and where individual machines or network connections may fail independently. Programming such systems is notoriously difficult and error-prone due to messages being reordered or delayed and the possibility of machines and network connections failing. Widely-used protocols are meant to ensure, for instance, a given message delivery order or a given data consistency policy, but machine-checked proofs ensuring the correctness of executable implementations of these protocols are rare. The goal of this project is to mechanically verify real, executable implementations of distributed systems, using powerful tools built into a general-purpose programming language. The project's novelties are in its focus on immediately executable implementations, and in its modular verification approach that separates lower-level message delivery concerns from higher-level application semantics. The project's impacts will be in improving the overall trustworthiness and reliability of distributed software systems. The project further aims to create approachable entry points to research, and to develop students' scientific communication skills, by integrating the creation of zines and videos about distributed systems verification into the investigator and project team's teaching and research practices, and making the resulting materials freely available online.The project's approach to language-level distributed systems verification centers around refinement types: data types that let programmers specify logical predicates that restrict the set of values described by a type, and that can be checked at compile time by an SMT solver. The project uses Liquid Haskell, which extends the Haskell programming language with support for refinement types, and which can further be used for extrinsic verification, that is, defining functions to state and prove theorems. The investigator and team will use Liquid Haskell to develop mechanically verified, modular libraries for implementing distributed systems. A novel verified message delivery library will form the foundation for additional verified components, such as libraries providing replicated data types and distributed data stores. Furthermore, the project investigates combining the strengths of Liquid Haskell with those of interactive proof assistants such as Agda. These investigations culminate in a comprehensive survey of such hybrid automated/interactive verification tools, and provide a holistic scientific understanding of the design space.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.