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

Fingerprint

Learning systems
Image processing
Semantics

Keywords

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

ASJC Scopus subject areas

  • Computer Graphics and Computer-Aided Design
  • Software

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

Verified integrity properties for safe approximate program transformations. / Carbin, Michael; Kim, Deokhwan; Misailovic, Sasa; Rinard, Martin C.

PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013. 2013. p. 63-66 (PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013).

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

Carbin, M, Kim, D, Misailovic, S & Rinard, MC 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. PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013, pp. 63-66, ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation, PEPM 2013 - Co-located with POPL 2013, Rome, Italy, 1/21/13. https://doi.org/10.1145/2426890.2426901
Carbin M, Kim D, Misailovic S, Rinard MC. 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. 2013. p. 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
Carbin, Michael ; Kim, Deokhwan ; Misailovic, Sasa ; Rinard, Martin C. / Verified integrity properties for safe approximate program transformations. PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013. 2013. pp. 63-66 (PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013).
@inproceedings{a6fb34f925044b0c9e17858ad2570c19,
title = "Verified integrity properties for safe approximate program transformations",
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.",
keywords = "Approximate computing, Integrity properties, Loop perforation, Relaxed programs",
author = "Michael Carbin and Deokhwan Kim and Sasa Misailovic and Rinard, {Martin C.}",
year = "2013",
month = "2",
day = "12",
doi = "10.1145/2426890.2426901",
language = "English (US)",
isbn = "9781450318426",
series = "PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013",
pages = "63--66",
booktitle = "PEPM 2013 - Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, Co-located with POPL 2013",

}

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/2/12

Y1 - 2013/2/12

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

ER -