Sound Loop Superoptimization for Google Native Client
Abstract
Software fault isolation (SFI) is an important technique for the construction of secure operating systems, web browsers, and other extensible software. We demonstrate that superoptimization can dramatically improve the performance of Google Native Client, a SFI system that ships inside the Google Chrome Browser. Key to our results are new techniques for superoptimization of loops: we propose a new architecture for superoptimization tools that incorporates both a fully sound verification technique to ensure correctness and a bounded verification technique to guide the search to optimized code. In our evaluation we optimize 13 libc string functions, formally verify the correctness of the optimizations and report a median and average speedup of 25% over the libraries shipped by Google.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Apr 04, 2017
- Source ID
- 10.1145/3093337.3037754
Entities
People
- Alex Aiken
- Berkeley Churchill
- Jf Bastien
- Rahul Sharma
Organizations
- Defense Advanced Research Projects Agency
- Microsoft
- National Science Foundation
- Stanford University