research-article

Verified integrity properties for safe approximate program transformations

Authors:

Michael Carbin,

Sasa Misailovic,

Martin C. RinardAuthors Info & Claims

PEPM '13: Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation

Pages 63 - 66

https://doi.org/10.1145/2426890.2426901

Published: 21 January 2013 Publication History

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.

References

[1]

Frama-C. http://frama-c.com/.

[2]

pycparser. http://code.google.com/p/pycparser/.

[3]

J. Ansel, C. Chan, Y. L. Wong, M. Olszewski, Q. Zhao, A. Edelman, and S. Amarasinghe. PetaBricks: A language and compiler for algorithmic choice. PLDI, 2009.

Digital Library

[4]

W. Baek and T. M. Chilimbi. Green: A framework for supporting energy-conscious programming using controlled approximation. PLDI, 2010.

Digital Library

[5]

C. Bienia, S. Kumar, J. Pal Singh, and K. Li. The PARSEC benchmark suite: Characterization and architectural implications. PACT, 2008.

Digital Library

[6]

M. Carbin, D. Kim, S. Misailovic, and M. Rinard. Proving acceptability properties of relaxed nondeterministic approximate programs. PLDI, 2012.

Digital Library

[7]

S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. Navidpour. Proving programs robust. FSE, 2011.

Digital Library

[8]

H. Hoffmann, S. Misailovic, S. Sidiroglou, A. Agarwal, and M. Rinard. Using code perforation to improve performance, reduce energy consumption, and respond to failures. Technical Report MIT-CSAIL-TR-2009-042, MIT, 2009.

[9]

H. Hoffmann, Sidiroglou S., Carbin M., Misailovic S., Agarwal A., and M. Rinard. Dynamic knobs for responsive power-aware computing. ASPLOS, 2011.

Digital Library

[10]

S. Misailovic, D. Kim, and M. Rinard. Parallelizing sequential programs with statistical accuracy tests. Technical Report MIT-CSAIL-TR-2010-038, MIT, 2010.

[11]

S. Misailovic, S. Sidiroglou, H. Hoffmann, and M. Rinard. Quality of service profiling. ICSE, 2010.

Digital Library

[12]

S. Misailovic, D. Roy, and M. Rinard. Probabilistically accurate program transformations. SAS, 2011.

Digital Library

[13]

G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. CC, 2002.

Digital Library

[14]

M. Rinard. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. ICS, 2006.

Digital Library

[15]

M. Rinard. Using early phase termination to eliminate load imbalances at barrier synchronization points. OOPSLA, 2007.

Digital Library

[16]

A. Sampson, W. Dietl, E. Fortuna, D. Gnanapragasam, L. Ceze, and D. Grossman. EnerJ: Approximate data types for safe and general low-power computation. PLDI, 2011.

Digital Library

[17]

S. Sidiroglou, S. Misailovic, H. Hoffmann, and M. Rinard. Managing performance vs. accuracy trade-offs with loop perforation. FSE, 2011.

Digital Library

[18]

Z. Zhu, S. Misailovic, J. Kelner, and M. Rinard. Randomized accuracy-aware program transformations for efficient approximate computations. POPL, 2012.

Digital Library

Cited By

Misailovic S(2022)Accuracy-Aware CompilersApproximate Computing Techniques10.1007/978-3-030-94705-7_7(177-214)Online publication date: 3-Jan-2022
https://doi.org/10.1007/978-3-030-94705-7_7
Fernando VJoshi KLaurel JMisailovic S(2021)Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous ProgramsRuntime Verification10.1007/978-3-030-88494-9_10(184-206)Online publication date: 6-Oct-2021
https://doi.org/10.1007/978-3-030-88494-9_10
Joshi KFernando VMisailovic SMars JTang LXue JWu P(2020)Aloe: verifying reliability of approximate programs in the presence of recovery mechanismsProceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3368826.3377924(56-67)Online publication date: 22-Feb-2020
https://dl.acm.org/doi/10.1145/3368826.3377924
Show More Cited By

Index Terms

Verified integrity properties for safe approximate program transformations

Recommendations

Proving acceptability properties of relaxed nondeterministic approximate programs
PLDI '12: Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation

Approximate program transformations such as skipping tasks [29, 30], loop perforation [21, 22, 35], reduction sampling [38], multiple selectable implementations [3, 4, 16, 38], dynamic knobs [16], synchronization elimination [20, 32], approximate ...
Managing performance vs. accuracy trade-offs with loop perforation
ESEC/FSE '11: Proceedings of the 19th ACM SIGSOFT symposium and the 13th European conference on Foundations of software engineering

Many modern computations (such as video and audio encoders, Monte Carlo simulations, and machine learning algorithms) are designed to trade off accuracy in return for increased performance. To date, such computations typically use ad-hoc, domain-...
Approximate loop unrolling
CF '19: Proceedings of the 16th ACM International Conference on Computing Frontiers

We introduce Approximate Unrolling, a compiler loop optimization that reduces execution time and energy consumption, exploiting code regions that can endure some approximation and still produce acceptable results. Specifically, this work focuses on ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PEPM '13: Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation

January 2013

162 pages

ISBN:9781450318426

DOI:10.1145/2426890

Program Chairs:
Elvira Albert
Complutense University of Madrid, Spain
,
Shin-Cheng Mu
Academia Sinica, Taiwan

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '13

Sponsor:

SIGPLAN

POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 21, 2013

Rome, Italy

Acceptance Rates

PEPM '13 Paper Acceptance Rate 13 of 29 submissions, 45%;

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

18
Total Citations
View Citations
225
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Misailovic S(2022)Accuracy-Aware CompilersApproximate Computing Techniques10.1007/978-3-030-94705-7_7(177-214)Online publication date: 3-Jan-2022
https://doi.org/10.1007/978-3-030-94705-7_7
Fernando VJoshi KLaurel JMisailovic S(2021)Diamont: Dynamic Monitoring of Uncertainty for Distributed Asynchronous ProgramsRuntime Verification10.1007/978-3-030-88494-9_10(184-206)Online publication date: 6-Oct-2021
https://doi.org/10.1007/978-3-030-88494-9_10
Joshi KFernando VMisailovic SMars JTang LXue JWu P(2020)Aloe: verifying reliability of approximate programs in the presence of recovery mechanismsProceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3368826.3377924(56-67)Online publication date: 22-Feb-2020
https://dl.acm.org/doi/10.1145/3368826.3377924
Fernando VJoshi KMisailovic S(2019)Verifying safety and accuracy of approximate parallel programs via canonical sequentializationProceedings of the ACM on Programming Languages10.1145/33605453:OOPSLA(1-29)Online publication date: 10-Oct-2019
https://dl.acm.org/doi/10.1145/3360545
Stitt GCampbell DChen JShrivastava A(2019)PANDORA: a parallelizing approximation-discovery framework (WIP paper)Proceedings of the 20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems10.1145/3316482.3326345(198-202)Online publication date: 23-Jun-2019
https://dl.acm.org/doi/10.1145/3316482.3326345
De Silva HSantosa AHo NWong WChen JShrivastava A(2019)ApproxSymate: path sensitive program approximation using symbolic executionProceedings of the 20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems10.1145/3316482.3326341(148-162)Online publication date: 23-Jun-2019
https://dl.acm.org/doi/10.1145/3316482.3326341
Isenberg TJakobs MPauck FWehrheim H(2019)When Are Software Verification Results Valid for Approximate Hardware?Tests and Proofs10.1007/978-3-030-31157-5_1(3-20)Online publication date: 23-Sep-2019
https://doi.org/10.1007/978-3-030-31157-5_1
Boston BGong ZCarbin M(2018)Leto: verifying application-specific hardware fault tolerance with programmable execution modelsProceedings of the ACM on Programming Languages10.1145/32765332:OOPSLA(1-30)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276533
Isenberg TJakobs MPauck FWehrheim H(2018)Validity of Software Verification Results on Approximate HardwareIEEE Embedded Systems Letters10.1109/LES.2017.275820010:1(22-25)Online publication date: 1-Mar-2018
https://dl.acm.org/doi/10.1109/LES.2017.2758200
Albarghouthi A(2017)Probabilistic Horn Clause VerificationStatic Analysis10.1007/978-3-319-66706-5_1(1-22)Online publication date: 19-Aug-2017
https://doi.org/10.1007/978-3-319-66706-5_1
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten