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.

Conference Day
Fri 9 Nov

Displayed time zone: Guadalajara, Mexico City, Monterrey change

13:30 - 14:15
VerificationOOPSLA at Studio 1
Chair(s): Tony HoskingAustralian National University / Data61
13:30
22m
Talk
Leto: Verifying Application-Specific Fault Tolerance through Parameterized Execution Models
OOPSLA
Brett BostonMassachusetts Institute of Technology, Zoe GongMassachusetts Institute of Technology, Michael CarbinMassachusetts Institute of Technology
13:52
22m
Talk
Safe Replication through Bounded Concurrency Verification
OOPSLA
Gowtham KakiPurdue University, Kapil EarankyPurdue University, KC SivaramakrishnanUniversity of Cambridge, Suresh JagannathanPurdue University