Efficient and proven verification of unreliable hardware executions of classic algorithms

Lowering voltage and frequency guardbands of CPU, DRAM, cache, or interconnect lowers power and latency, but increases the risk of silent data corruptions in even formally verified hardware and software. Researchers have been developing systems that use unreliable hardware, combined with software checkers executed on reliable hardware, to gain high performance with no risk. Deterministic checkers for many important algorithms are asymptotically and practically more efficient than the original problem solvers, e.g. for systems of linear equations, satisfiability, linear programming, sorting, 3SUM, graph matching and others. Writing a correct checker is hard, since often intricate corner cases get overlooked. Our system, SOUNDCHECK, helps reduce burden on programmers by automatically proving soundness and completeness of checkers with bounded verification in the Sketch program synthesis language. Verified checkers are emitted as efficient C++ code and shown to have low overhead which results in a net performance improvement with no risk.

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

2015

Author dc:creator

• Gyurova, Yoana G

Advisor dc:contributor.advisor

• Saman Amarasinghe.

• Electrical Engineering and Computer Science.

Statement dc:rights

• M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about 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/100599

OAI identifier oai:identifier

oai:dspace.mit.edu:1721.1/100599