Verified integrity properties for safe approximate program transformations

Verified integrity properties for safe approximate program transformations
复制标题

已验证安全近似程序转换的完整性属性

DOI：
10.1145/2426890.2426901
复制
发表时间：
2013
期刊：
2017 IEEE/ACM International Symposium on Code Generation and Optimization (CGO)
影响因子：
--
通讯作者：
M. Rinard
M. Rinard
中科院分区：
--
文献类型：
--
作者：
Michael Carbin;Deokhwan Kim;Sasa Misailovic;M. Rinard

文献摘要

被引文献

相似文献

近似计算（例如，视频、音频和图像处理、机器学习和许多科学计算）可以自由地生成一系列可接受的结果。近似程序转换（例如，任务跳过和循环穿孔）利用这种自由度来生成可以在底层精度与性能权衡空间中的各个点执行的计算。一个潜在的担忧是，这些转换可能会改变程序的语义，从而导致程序崩溃、执行非法操作或以其他方式违反其完整性。 我们研究验证完整性属性（转换后的计算必须遵守的关键正确性属性）如何能够安全应用近似程序转换。我们提供了编译器的实验结果，该编译器验证穿孔循环的完整性属性，以实现循环穿孔的安全应用。
Approximate computations (for example, video, audio, and image processing, machine learning, and many scientific computations) have the freedom to generate a range of acceptable results. Approximate program transformations (for example, task skipping and loop perforation) exploit this freedom to produce computations that can execute at a variety of points in an underlying accuracy versus performance trade-off space. One potential concern is that these transformations may change the semantics of the program and therefore cause the program to crash, perform an illegal operation, or otherwise violate its integrity. We investigate how verifying integrity properties -- key correctness properties that the transformed computation must respect -- can enable the safe application of approximate program transformations. We present experimental results from a compiler that verifies integrity properties of perforated loops to enable the safe application of loop perforation.