Program Logics for Compositional Specification and Verification of Distributed Systems

分布式服务在现代生活的许多方面，如医疗保健、在线商务、交通、娱乐和基于云的应用程序，其重要性和无处不在，怎么强调都不为过。考虑到分布式软件的重要性及其复杂性，源于其并发性和容忍重新排序和数据包丢失的必要性，如今在工业中，有一个严格的验证方法来建立其正确性属性，确保一旦分布式系统启动并运行，它永远不会出错，并最终完成其目标，这被认为是至关重要的。现实世界的应用程序，包括分布式应用程序，并不是作为独立的、整体的代码块开发的：它们是由多个组件构建的，通过组合在不同模块中实现的程序机制，独立开发，然后链接在一起。因此，这种组合方法的好处是关注点分离，这使得开发过程模块化：为了使用分布式协议的实现作为库，人们应该知道它是做什么的，而不必费心去理解它是如何工作的。唉，在模块化软件开发中被认为是一种良好实践的潜力，在关于分布式软件的形式化推理领域还没有完全实现。现有的规范和验证分布式应用程序的方法主要集中在对独立协议的系统进行推理，这些协议的行为是使用其执行历史的不变量来描述的，然后使用协议的抽象模型来检查。由于没有统一的方式来指定和验证分布式协议及其客户端（可能本身就是协议实现）的实现，因此在形式化推理的垂直组合性中引入了一个缺口：为了证明分布式库的客户端程序的正确性，应该依赖于根据库的模型而不是其实际实现建立的正确性结果。此外，指定分布式协议的方式可能会采用特定的正确性条件，固定其历史不变量，例如线性性、最终一致性或因果一致性，从而迫使人们采用相应的验证方法，以便对协议的客户端进行推理。这种多样性对水平组合性提出了挑战，使得对组合了多个协议的非玩具应用程序进行推理变得非常重要。该项目建议开发一种统一的模块化方法，用于在机器检查的框架中正式指定和验证分布式应用程序的实现，解决垂直和水平组合性的问题。建议的方法建立在hoare风格的程序逻辑的思想之上，用于有效的并发程序及其使用依赖类型的机械化。因此，建议的方法将在分布式计算领域的模块化软件开发的良好实践和关于程序的组合推理的思想之间建立连接，作为正式验证它们的方法，因此，提供对其正确性的最强保证。

It is hard to overstate the significance and ubiquity of distributed services in many aspects of the modern life, such as health care, online commerce, transportation, entertainment and cloud-based applications. Given the importance of distributed software and its complexity, stemming from its concurrent nature and the necessity to tolerate reordering and loss of packets, it is nowadays considered vital in industry to have a rigorous verification methodology for establishing its correctness properties, ensuring that, once a distributed system is up and running, it will never go wrong and will eventually complete its goals.Real-world applications, including distributed ones, are not developed as standalone, monolithic pieces of code: they are rather built from multiple components, by composing the program machinery implemented in different modules, developed independently and then linked together. The benefit of such a compositional approach is thus the separation of concerns, which makes the development process modular: in order to use an implementation of a distributed protocol as a library, one should know what it does without bothering to understand how it works.Alas, the potential of what is considered to be a good practice in modular software development, is not yet fully realised in the area of formal reasoning about distributed software. The existing approaches for specification and verification of distributed applications are predominantly focused on reasoning about systems as of standalone protocols, whose behavior is described using invariants of their execution histories, which are then checked using the protocols' abstract models. The absence of a uniform way of specifying and verifying implementations of distributed protocols and their clients (which might be themselves protocol implementations) introduces a gap in vertical compositionality of the formal reasoning: in order to prove correctness of a distributed library's client program, one should rely on the correctness result, established with respect to the library's model rather than its actual implementation. Furthermore, the way a distributed protocol is specified might employ a particular correctness condition, fixing its history invariants, such as linearizability, eventual or causal consistency, forcing one to adopt the corresponding verification methodology for the sake of reasoning about the protocol's clients. This diversity poses challenges with respect to horizontal compositionality, making it non-trivial to reason about non-toy applications that combine several protocols.This project proposes to develop a uniform and modular approach for formally specifying and verifying implementations of distributed applications, in a machine-checked framework, addressing both issues of vertical and horizontal compositionality. The suggested methodology builds on the ideas of Hoare-style program logics for effectful concurrent programs and their mechanisation using dependent types. The proposed approach will thus establish a connecting link between the good practices of modular software development in the area of distributed computing and ideas of compositional reasoning about programs, as a way to formally verify them, therefore, delivering the strongest guarantees of their correctness.