Fri 9 Nov 2018 13:30 - 13:52 at Studio 1 - Verification Chair(s): Tony Hosking

Due to the aggressive scaling of technology sizes in modern computer processor fabrication, modern processors have become less reliable and more prone to exposing hardware errors to software. In response, 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 in the underlying hardware.

To this end we present Leto, a verification system that enables developers to verify their applications with respect to a first-class fault model specification. Namely, Leto enables software and platform developers to programmatically specify the faulty semantics of the underlying hardware system as well as verify assertions about the behavior of the application’s resulting execution. A key aspect of verifying these implementations is that applications that leverage application-specific fault tolerance mechanisms often require assertions that relate the behavior of the implementation’s execution in the presence of errors to a fault-free execution. To support this, Leto specifically supports relational verification in that its assertion language enables a developer to specify and verify assertions that relate the two semantics of the program. 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.

Fri 9 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:30 - 14:15
VerificationOOPSLA at Studio 1
Chair(s): Tony Hosking Australian National University / Data61
Leto: Verifying Application-Specific Fault Tolerance through Parameterized Execution Models
Brett Boston Massachusetts Institute of Technology, Zoe Gong Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
Safe Replication through Bounded Concurrency Verification
Gowtham Kaki Purdue University, Kapil Earanky Purdue University, KC Sivaramakrishnan University of Cambridge, Suresh Jagannathan Purdue University