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.
|