CRII: SHF: Distributed Systems With Verified Complexity By Design

分布式系统协调多台联网计算机以实现共同目标，对国家的数字基础设施至关重要。然而，他们也是出了名的难以得到正确的，特别是在面对计算机和网络故障。以前的研究工作使用的工具，从正式的方法，如定理证明，建立分布式系统的正式验证的正确性保证。该项目通过攻击可表示为游戏的一类分布式系统（分布式路由器，负载均衡器等）的正式验证性能保证的补充问题来推进最先进的技术。这样的性能保证在从实时系统到低延迟Web应用程序的各种设置中都很有用。该项目还支持本科生和研究生水平的课程开发，以及研究者的"Coq Bootcamp"等活动，这是一个每周两次的针对本科生的形式验证夏季研讨会。研究者的技术方法结合了编程语言的工具，例如用于Coq中的正确构造编程的特定领域语言（DSL），以及最近在算法博弈论方面的工作：拉夫加登？的光滑游戏和游戏的实现称为乘法权重。通过组成一个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.