Verifying Programs Under Custom Application-Specific Execution Models

TL;DR

Leto is an SMT-based verification system that allows developers to specify and verify application behavior under custom, application-specific execution models, particularly for fault-tolerant systems.

Contribution

This paper introduces Leto, a novel programming language and verification system for specifying and verifying execution models in fault-tolerant applications.

Findings

Successfully verified fault-tolerance mechanisms in multiple applications

Demonstrated Leto's effectiveness in ensuring correctness under custom models

Enabled precise specification of hardware and application behavior

Abstract

Researchers have recently designed a number of application-specific fault tolerance mechanisms that enable applications to either be naturally resilient to errors or include additional detection and correction steps that can bring the overall execution of an application back into an envelope for which an acceptable execution is eventually guaranteed. A major challenge to building an application that leverages these mechanisms, however, is to verify that the implementation satisfies the basic invariants that these mechanisms require--given a model of how faults may manifest during the application's execution. To this end we present Leto, an SMT based automatic verification system that enables developers to verify their applications with respect to a first-class execution model specification. Namely, Leto enables software and platform developers to programmatically specify the execution semantics of the underlying hardware system as well as verify assertions about the behavior of the application's resulting execution. In this paper, we present the Leto programming language and its corresponding verification system. We also demonstrate Leto on several applications that leverage application-specific fault tolerance mechanisms.