CRII: SHF: Distributed Systems With Verified Complexity By Design

分布式系统协调多台联网计算机以实现共同目标，对国家的数字基础设施至关重要。然而，它们也是出了名的难以纠正，特别是在面对计算机和网络故障的情况下。以前的研究工作使用了形式化方法中的工具，例如定理证明器，来构建具有正式验证的正确性保证的分布式系统。这个项目通过解决形式上验证一类可表示为游戏的分布式系统的性能保证的补充问题来推进最先进的技术：分布式路由器、负载均衡器等。这样的性能保证在从实时系统到低延迟Web应用程序的各种环境中都很有用。该项目还支持本科生和研究生的课程开发，以及一些活动，如调查者的“Coq训练营”，一周两次的本科生正式验证夏季研讨会。调查者的技术方法结合了编程语言中的工具，如用于Coq中按结构更正编程的领域特定语言(DSL)，以及最近在算法博弈论方面的工作：RoughGarden？S流畅游戏和一个名为乘法权重的游戏的实现。通过将用于平滑游戏的DSL与经过验证的乘性权重的实现相结合，该项目正式地限定了平滑游戏收敛的时间以及所产生的状态WRT的质量。最好的。为了恢复对允许故障的网络模型的保证，该项目使用Verdi系统经过验证的系统转换器的量化版本，在常见分布式设计模式(如序列号)的实现中包装流畅的游戏。

Distributed systems, which coordinate multiple networked computers to meet a shared goal, are critical to the nation's digital infrastructure. Yet they are also notoriously difficult to get right, especially in the face of computer and network faults. Previous research efforts have used tools from formal methods, such as theorem provers, to build distributed systems with formally verified correctness guarantees. This project advances the state-of-the-art by attacking the complementary problem of formally verifying performance guarantees for a class of distributed systems representable as games: distributed routers, load balancers, and others. Such performance guarantees are useful in a wide variety of settings, from real-time systems to low-latency web applications. The project additionally supports curricular development at both the undergraduate and graduate levels, as well as activities such as the investigator's "Coq Bootcamp", a twice-weekly summer seminar on formal verification for undergraduates.The investigator's technical methodology combines tools from programming languages, such as domain-specific languages (DSLs) for correct-by-construction programming in Coq, with recent work in algorithmic game theory: Roughgarden?s smooth games and an implementation of games called multiplicative weights. By composing a DSL for smooth games with a verified implementation of multiplicative weights, this project formally bounds the time within which a smooth game converges, and the quality of the resulting state wrt. optimal. To recover guarantees against a network model that permits faults, the project uses a quantified version of the Verdi system's verified system transformers to wrap smooth games in implementations of common distributed design patterns such as sequence numbering.