Building reliable, high-performance networks with the Nuprl proof development system

Abstract

Proof systems for expressive type theories provide a foundation for the verification and synthesis of programs. But despite their successful application to numerous programming problems there remains an issue with scalability. Are proof environments capable of reasoning about large software systems? Can the support they offer be useful in practice? In this article we answer this question by showing how the N UPRL proof development system and its rich type theory have contributed to the design of reliable, high-performance networks by synthesizing optimized code for application configurations of the E NSEMBLE group communication toolkit. We present a type-theoretical semantics of OC AML , the implementation language of E NSEMBLE , and tools for automatically importing system code into the N UPRL system. We describe reasoning strategies for generating verifiably correct fast-path optimizations of application configurations that substantially reduce end-to-end latency in E NSEMBLE . We also discuss briefly how to use N UPRL for checking configurations against specifications and for the design of reliable adaptive network protocols.