CAREER: Building Reliable Distributed Systems with Refinement Types

职业：构建具有细化类型的可靠分布式系统

• 批准号: 2145367
• 负责人: Lindsey Kuper
• 金额: $ 61.97万
• 依托单位: University of California-Santa Cruz
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-07-01 至 2027-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2145367&HistoricalAwards=false
• 关键词: CAREER; Building; Reliable; Distributed; Systems

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.

该奖项是根据2021年《美国救援计划法》的全部或部分资助的（公共法117-2）。托迪最重要的计算机系统是分布式系统：由通过网络发送消息传达的多台机器组成的系统，单个机器或网络连接可能独立失败。 由于消息被重新排序或延迟以及机器和网络连接失败的可能性，因此众所周知，此类系统非常困难且容易出错。 广泛使用的协议旨在确保给定的消息传递订单或给定的数据一致性策略，但是由机器检查的证明确保了这些协议可执行实现的正确性。 该项目的目的是使用内置在通用编程语言中的强大工具机械地验证分布式系统的真实，可执行的实现。 该项目的新颖性重点是立即执行实现，并在其模块化验证方法中，将低级消息传递关注与高级应用程序语义分开。该项目的影响将是改善分布式软件系统的整体可信度和可靠性。 该项目进一步旨在通过将有关分布式系统验证的Zines和视频整合到研究人员和项目团队的教学和研究实践中，并在线免费提供，并使项目验证的方法围绕更细节的限制类型，使项目验证的方法允许Progriptation Permecors progripations：通过SMT求解器在编译时间检查。该项目使用Liquid Haskell，它扩展了Haskell编程语言并支持改进类型，并且可以进一步用于外部验证，即定义函数以陈述和证明定理。研究人员和团队将使用Liquid Haskell来开发经过机械验证的模块化库来实施分布式系统。 一个新的经过验证的消息传递库将构成其他经过验证的组件的基础，例如提供复制数据类型和分布式数据存储的库。此外，该项目研究了将液体haskell的优势与AGDA等交互式证明助手的优势相结合。这些调查最终在对这种混合自动化/互动验证工具的全面调查中，并对设计空间提供了整体科学理解。该奖项反映了NSF的法定任务，并认为值得通过基金会的知识分子优点和更广泛的影响审查标准通过评估来进行评估。

项目成果

Verified Causal Broadcast with Liquid Haskell

使用 Liquid Haskell 验证因果广播

• DOI: 10.1145/3587216.3587222
• 发表时间: 2023
• 期刊: IFL '22: Proceedings of the 34th Symposium on Implementation and Application of Functional Languages
• 作者: Redmond, Patrick;Shen, Gan;Vazou, Niki;Kuper, Lindsey
• 通讯作者: Kuper, Lindsey