一句话：提出健全的循环超优化架构，用完全健全验证与有界验证指导搜索，显著提升 NaCl libc 性能。
软件故障隔离（SFI）用于构建安全操作系统、浏览器等可扩展软件，但会带来性能开销。本文表明超优化可显著提升 Google Native Client（Chrome 内置的 SFI 系统）的性能。核心是面向循环的超优化新技术：提出一种新的超优化工具架构，同时包含完全健全的验证技术以保证优化正确性，以及有界验证技术来引导搜索得到优化代码。评估中优化了 13 个 libc 字符串函数，形式化验证了优化的正确性，并报告相对 Google 随附库的中位数和平均加速为 25%。
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.