Probabilistically accurate program transformations

Sasa Misailovic, Daniel M. Roy, Martin C. Rinard

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

Abstract

The standard approach to program transformation involves the use of discrete logical reasoning to prove that the transformation does not change the observable semantics of the program. We propose a new approach that, in contrast, uses probabilistic reasoning to justify the application of transformations that may change, within probabilistic accuracy bounds, the result that the program produces. Our new approach produces probabilistic guarantees of the form ℙ(|D|≥ B) ≤ε, ε ∈ (0, 1), where D is the difference between the results that the transformed and original programs produce, B is an acceptability bound on the absolute value of D, and ε is the maximum acceptable probability of observing large |D|. We show how to use our approach to justify the application of loop perforation (which transforms loops to execute fewer iterations) to a set of computational patterns.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 18th International Symposium, SAS 2011, Proceedings
Pages316-333
Number of pages18
DOIs
StatePublished - Sep 28 2011
Externally publishedYes
Event18th International Static Analysis Symposium, SAS 2011 - Venice, Italy
Duration: Sep 14 2010Sep 16 2010

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6887 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other18th International Static Analysis Symposium, SAS 2011
CountryItaly
CityVenice
Period9/14/109/16/10

Fingerprint

Program Transformation
Justify
Probabilistic Reasoning
Semantics
Probabilistic Approach
Absolute value
Reasoning
Transform
Iteration

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Misailovic, S., Roy, D. M., & Rinard, M. C. (2011). Probabilistically accurate program transformations. In Static Analysis - 18th International Symposium, SAS 2011, Proceedings (pp. 316-333). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6887 LNCS). https://doi.org/10.1007/978-3-642-23702-7_24

Probabilistically accurate program transformations. / Misailovic, Sasa; Roy, Daniel M.; Rinard, Martin C.

Static Analysis - 18th International Symposium, SAS 2011, Proceedings. 2011. p. 316-333 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6887 LNCS).

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

Misailovic, S, Roy, DM & Rinard, MC 2011, Probabilistically accurate program transformations. in Static Analysis - 18th International Symposium, SAS 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6887 LNCS, pp. 316-333, 18th International Static Analysis Symposium, SAS 2011, Venice, Italy, 9/14/10. https://doi.org/10.1007/978-3-642-23702-7_24
Misailovic S, Roy DM, Rinard MC. Probabilistically accurate program transformations. In Static Analysis - 18th International Symposium, SAS 2011, Proceedings. 2011. p. 316-333. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-23702-7_24
Misailovic, Sasa ; Roy, Daniel M. ; Rinard, Martin C. / Probabilistically accurate program transformations. Static Analysis - 18th International Symposium, SAS 2011, Proceedings. 2011. pp. 316-333 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f5b622dcdf2240ffb3db438be4124cbb,
title = "Probabilistically accurate program transformations",
abstract = "The standard approach to program transformation involves the use of discrete logical reasoning to prove that the transformation does not change the observable semantics of the program. We propose a new approach that, in contrast, uses probabilistic reasoning to justify the application of transformations that may change, within probabilistic accuracy bounds, the result that the program produces. Our new approach produces probabilistic guarantees of the form ℙ(|D|≥ B) ≤ε, ε ∈ (0, 1), where D is the difference between the results that the transformed and original programs produce, B is an acceptability bound on the absolute value of D, and ε is the maximum acceptable probability of observing large |D|. We show how to use our approach to justify the application of loop perforation (which transforms loops to execute fewer iterations) to a set of computational patterns.",
author = "Sasa Misailovic and Roy, {Daniel M.} and Rinard, {Martin C.}",
year = "2011",
month = "9",
day = "28",
doi = "10.1007/978-3-642-23702-7_24",
language = "English (US)",
isbn = "9783642237010",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "316--333",
booktitle = "Static Analysis - 18th International Symposium, SAS 2011, Proceedings",

}

TY - GEN

T1 - Probabilistically accurate program transformations

AU - Misailovic, Sasa

AU - Roy, Daniel M.

AU - Rinard, Martin C.

PY - 2011/9/28

Y1 - 2011/9/28

N2 - The standard approach to program transformation involves the use of discrete logical reasoning to prove that the transformation does not change the observable semantics of the program. We propose a new approach that, in contrast, uses probabilistic reasoning to justify the application of transformations that may change, within probabilistic accuracy bounds, the result that the program produces. Our new approach produces probabilistic guarantees of the form ℙ(|D|≥ B) ≤ε, ε ∈ (0, 1), where D is the difference between the results that the transformed and original programs produce, B is an acceptability bound on the absolute value of D, and ε is the maximum acceptable probability of observing large |D|. We show how to use our approach to justify the application of loop perforation (which transforms loops to execute fewer iterations) to a set of computational patterns.

AB - The standard approach to program transformation involves the use of discrete logical reasoning to prove that the transformation does not change the observable semantics of the program. We propose a new approach that, in contrast, uses probabilistic reasoning to justify the application of transformations that may change, within probabilistic accuracy bounds, the result that the program produces. Our new approach produces probabilistic guarantees of the form ℙ(|D|≥ B) ≤ε, ε ∈ (0, 1), where D is the difference between the results that the transformed and original programs produce, B is an acceptability bound on the absolute value of D, and ε is the maximum acceptable probability of observing large |D|. We show how to use our approach to justify the application of loop perforation (which transforms loops to execute fewer iterations) to a set of computational patterns.

UR - http://www.scopus.com/inward/record.url?scp=80053107668&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=80053107668&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-23702-7_24

DO - 10.1007/978-3-642-23702-7_24

M3 - Conference contribution

AN - SCOPUS:80053107668

SN - 9783642237010

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 316

EP - 333

BT - Static Analysis - 18th International Symposium, SAS 2011, Proceedings

ER -