CAREER: Distributed System Synthesis on Certified Middleware

分布式系统是现代计算的支柱。然而，由于其组合的大状态空间以及节点和网络故障，它们是复杂的，并且容易出现错误。最近发生的数据、货币和服务损失表明，分布式系统的可靠性仍然难以捉摸。不仅提供接口的协议和系统设计人员，甚至使用这些接口的分布式应用程序编程人员都面临着固有的复杂性。该项目致力于解决跨客户端应用程序和支持分布式中间件的分布式系统的程序员生产力和可靠性。该项目包括新的客户端应用程序自动合成技术和新的分布式中间件验证技术。分布式存储提供了一系列一致性选择，这让客户在正确性、响应性和可用性之间左右为难。鉴于应用程序的高级完整性属性，该项目自动确定确保完整性和收敛所需的最低协调，并自动合成复制对象的协议。这些应用程序的可靠性在很大程度上取决于广播和共识等微妙协议的底层中间件的正确性。传统上，中间件被设计为层的堆栈，其正确性通常被组合为关于在每一层及其子层之间交换的事件的时间优先级的直观论证。本项目在一个证明助手中构建了一个开发和验证框架，以设计一个机械验证的中间件栈。该框架基于组成和时间计划逻辑，以使证据与直观的论证相匹配。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Distributed systems are the backbone of modern computing. However, they are complicated and prone to bugs due to their combinatorially large state-spaces, and node and network failures. Recent occurrences of data, currency and service loss have shown that reliability of distributed systems remains elusive. The inherent complication is faced by not only protocol and system designers that provide interfaces but even distributed application programmers that use these interfaces. This project addresses programmer productivity and reliability of distributed systems that spans both the client applications and the supporting distributed middleware. This project includes both novel automatic synthesis techniques for client applications and novel verification techniques for distributed middleware. Distributed stores provide a spectrum of consistency choices that impose a dilemma for clients between correctness, responsiveness and availability. Given the high-level integrity properties of the application, this project automatically decides the minimum required coordination that guarantees integrity and convergence and automatically synthesizes protocols for replicated objects. The reliability of these applications is crucially dependent on the correctness of the underlying middleware of subtle protocols such as broadcast and consensus. The middleware is classically designed as stacks of layers, and its correctness is often stated compositionally as intuitive arguments on temporal precedence of the events exchanged between each layer and its sub-layers. This project builds a development and verification framework in a proof assistant to design a mechanically verified middleware stack. The framework is based on a compositional and temporal program logic so that the proofs match the intuitive arguments.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.