Paper Info
Title
Leto: verifying application-specific hardware fault tolerance with programmable execution models
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 an 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
Year
DOI
Venue
2018
10.1145/3276533
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
Approximate Computing
Journal
2
Issue
ISSN
Citations 
OOPSLA
2475-1421
1
PageRank 
References 
Authors
0.35
0
3
Name
Order
Citations
PageRank
Brett Boston110.35
Zoe Gong210.35
Michael Carbin378238.09