Skip to main content
SpringerLink
Log in

Probabilistically Accurate Program Transformations

  • Conference paper
Static Analysis (SAS 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6887))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ansel, J., Chan, C., Wong, Y., Olszewski, M., Zhao, Q., Edelman, A., Amara-singhe, S.: Petabricks: A language and compiler for algorithmic choice. In: PLDI 2010 (2010)

    Google Scholar 

  2. Arnold, B., Balakrishnan, N., Nagaraja, H.: A first course in order statistics. Society for Industrial Mathematics, Philadelphia (2008)

    Google Scholar 

  3. Baek, W., Chilimbi, T.: Green: A framework for supporting energy-conscious programming using controlled approximation. In: PLDI 2010 (2010)

    Google Scholar 

  4. Bienia, C., Kumar, S., Singh, J.P., Li, K.: The PARSEC benchmark suite: Characterization and architectural implications. In: PACT 2008 (2008)

    Google Scholar 

  5. Carbin, M., Rinard, M.: Automatically Identifying Critical Input Regions and Code in Applications. In: ISSTA 2010 (2010)

    Google Scholar 

  6. Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: POPL 2010 (2010)

    Google Scholar 

  7. Chaudhuri, S., Gulwani, S., Lublinerman, R., Navidpour, S.: Proving Programs Robust. In: FSE 2011 (2011)

    Google Scholar 

  8. Chaudhuri, S., Solar-Lezama, A.: Smooth interpretation. In: PLDI 2010 (2010)

    Google Scholar 

  9. Cochran, W.G.: Sampling techniques. John Wiley & Sons, Chichester (1977)

    MATH  Google Scholar 

  10. Di Pierro, A., Hankin, C., Wiklicky, H.: A systematic approach to probabilistic pointer analysis. In: ASPLAS 2007 (2007)

    Google Scholar 

  11. Di Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic λ-calculus and quantitative program analysis. Journal of Logic and Computation (2005)

    Google Scholar 

  12. Di Pierro, A., Wiklicky, H.: Concurrent constraint programming: Towards probabilistic abstract interpretation. In: PPDP 2000 (2000)

    Google Scholar 

  13. Goodman, N., Mansinghka, V., Roy, D., Bonawitz, K., Tenenbaum, J.: Church: a language for generative models. In: UAI 2008 (2008)

    Google Scholar 

  14. Gulwani, S., Necula, G.C.: Precise interprocedural analysis using random interpretation. In: POPL 2005 (2005)

    Google Scholar 

  15. Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI 2010 (2010)

    Google Scholar 

  16. Hall, M., Murphy, B., Amarasinghe, S., Liao, S., Lam, M.: Interprocedural analysis for parallelization. In: Languages and Compilers for Parallel Computing (1996)

    Google Scholar 

  17. Hoffman, H., Sidiroglou, S., Carbin, M., Misailovic, S., Agarwal, A., Rinard, M.: Dynamic knobs for power-aware computing. In: ASPLOS 2011 (2011)

    Google Scholar 

  18. Hoffmann, H., Misailovic, S., Sidiroglou, S., Agarwal, A., Rinard, M.: Using Code Perforation to Improve Performance, Reduce Energy Consumption, and Respond to Failures. Technical Report MIT-CSAIL-TR-2009-042 (2009)

    Google Scholar 

  19. Hurd, J.: A formal approach to probabilistic termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, p. 230. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Kennedy, K., Allen, J.R.: Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann, San Francisco (2002)

    Google Scholar 

  21. Klir, G.: Uncertainty and information. John Wiley & Sons, Chichester (2006)

    Google Scholar 

  22. Kozen, D.: Semantics of probabilistic programs. Journal of Computer and System Sciences (1981)

    Google Scholar 

  23. Kwiatkowska, M., Norman, G., Parker, D.: Prism: Probabilistic symbolic model checker. In: Computer Performance Evaluation: Modelling Techniques and Tools (2002)

    Google Scholar 

  24. Misailovic, S., Roy, D., Rinard, M.: Probabilistic and Statistical Analysis of Per-forated Patterns. Technical Report MIT-CSAIL-TR-2011-003, MIT (2011)

    Google Scholar 

  25. Misailovic, S., Sidiroglou, S., Hoffmann, H., Rinard, M.: Quality of service profiling. In: ICSE 2010 (2010)

    Google Scholar 

  26. Monniaux, D.: Abstract interpretation of probabilistic semantics. In: SAS 2000. LNCS, vol. 1824, pp. 322–340. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  27. Monniaux, D.: An abstract monte-carlo method for the analysis of probabilistic programs. In: POPL 2001 (2001)

    Google Scholar 

  28. Moore, R.E.: Interval analysis. Prentice-Hall, Englewood Cliffs (1966)

    MATH  Google Scholar 

  29. Morgan, C., McIver, A.: pGCL: formal reasoning for random algorithms. South African Computer Journal 22 (1999)

    Google Scholar 

  30. Park, S., Pfenning, F., Thrun, S.: A probabilistic language based upon sampling functions. In: POPL 2005 (2005)

    Google Scholar 

  31. Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL 2002 (2002)

    Google Scholar 

  32. Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: ICFP 2010 (2010)

    Google Scholar 

  33. Rinard, M.: Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. In: ICS 2006 (2006)

    Google Scholar 

  34. Rinard, M.: Using early phase termination to eliminate load imbalances at barrier synchronization points. In: OOPSLA 2007 (2007)

    Google Scholar 

  35. Rinard, M., Hoffmann, H., Misailovic, S., Sidiroglou, S.: Patterns and statistical analysis for understanding reduced resource computing. In: Onward! 2010 (2010)

    Google Scholar 

  36. Saheb-Djahromi, N.: Probabilistic LCF. In: MFCS 1978 (1978)

    Google Scholar 

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

    Google Scholar 

  38. Sidiroglou, S., Misailovic, S., Hoffmann, H., Rinard, M.: Managing Performance vs. Accuracy Trade-offs With Loop Perforation. In: FSE 2011 (2011)

    Google Scholar 

  39. Smith, M.: Probabilistic abstract interpretation of imperative programs using truncated normal distributions. Electronic Notes in Theoretical Computer Science (2008)

    Google Scholar 

  40. Sorber, J., Kostadinov, A., Garber, M., Brennan, M., Corner, M.D., Berger, E.D.: Eon: a language and runtime system for perpetual systems. In: SenSys 2007 (2007)

    Google Scholar 

  41. Springer, M.: The algebra of random variables. John Wiley & Sons, Chichester (1979)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MIT CSAIL, USA

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

Authors
  1. Sasa Misailovic
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Daniel M. Roy
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin C. Rinard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Science Deptartement, Technion, 32000, Technion City, Haifa, Israel

    Eran Yahav

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Misailovic, S., Roy, D.M., Rinard, M.C. (2011). Probabilistically Accurate Program Transformations. In: Yahav, E. (eds) Static Analysis. SAS 2011. Lecture Notes in Computer Science, vol 6887. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23702-7_24

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-23702-7_24

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-23701-0

  • Online ISBN: 978-3-642-23702-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation