Leto : verifying application-specific fault tolerance via first-class execution models

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 during the application's execution. To this end I present Leto, a 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. A key aspect of verifying these implementations is that applications leveraging 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 thesis, I present the Leto programming language and its corresponding verification system. I also demonstrate Leto on several applications that leverage application-specific fault tolerance mechanisms.

Department dc:contributor.department

Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science.

Grantor dc:publisher

Massachusetts Institute of Technology

Year dc:date.issued

2018

Author dc:creator

• Boston, Brett (Brett Cyrus)

Advisor dc:contributor.advisor

• Michael Carbin.

• Electrical Engineering and Computer Science.

Statement dc:rights

• MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission.

Licence dc:rights.uri

• http://dspace.mit.edu/handle/1721.1/7582

Language dc:language.iso

eng

Handle dc:identifier.uri

http://hdl.handle.net/1721.1/115751

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/115751