TY - GEN
T1 - Verified integrity properties for safe approximate program transformations
AU - Carbin, Michael
AU - Kim, Deokhwan
AU - Misailovic, Sasa
AU - Rinard, Martin C.
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
KW - Approximate computing
KW - Integrity properties
KW - Loop perforation
KW - Relaxed programs
UR - http://www.scopus.com/inward/record.url?scp=84873437273&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84873437273&partnerID=8YFLogxK
U2 - 10.1145/2426890.2426901
DO - 10.1145/2426890.2426901
M3 - Conference contribution
AN - SCOPUS:84873437273
SN - 9781450318426
T3 - PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013
SP - 63
EP - 66
BT - PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013
T2 - ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013
Y2 - 21 January 2013 through 22 January 2013
ER -