Verified integrity properties for safe approximate program transformations

Michael Carbin, Deokhwan Kim, Sasa Misailovic, Martin C. Rinard

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationPEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013
Pages63-66
Number of pages4
DOIs
StatePublished - Feb 12 2013
Externally publishedYes
EventACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013 - Rome, Italy
Duration: Jan 21 2013Jan 22 2013

Publication series

NamePEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013

Other

OtherACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013
CountryItaly
CityRome
Period1/21/131/22/13

Keywords

  • Approximate computing
  • Integrity properties
  • Loop perforation
  • Relaxed programs

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Software

Fingerprint Dive into the research topics of 'Verified integrity properties for safe approximate program transformations'. Together they form a unique fingerprint.

  • Cite this

    Carbin, M., Kim, D., Misailovic, S., & Rinard, M. C. (2013). Verified integrity properties for safe approximate program transformations. In PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013 (pp. 63-66). (PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013). https://doi.org/10.1145/2426890.2426901