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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Arnold, B., Balakrishnan, N., Nagaraja, H.: A first course in order statistics. Society for Industrial Mathematics, Philadelphia (2008)
Baek, W., Chilimbi, T.: Green: A framework for supporting energy-conscious programming using controlled approximation. In: PLDI 2010 (2010)
Bienia, C., Kumar, S., Singh, J.P., Li, K.: The PARSEC benchmark suite: Characterization and architectural implications. In: PACT 2008 (2008)
Carbin, M., Rinard, M.: Automatically Identifying Critical Input Regions and Code in Applications. In: ISSTA 2010 (2010)
Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: POPL 2010 (2010)
Chaudhuri, S., Gulwani, S., Lublinerman, R., Navidpour, S.: Proving Programs Robust. In: FSE 2011 (2011)
Chaudhuri, S., Solar-Lezama, A.: Smooth interpretation. In: PLDI 2010 (2010)
Cochran, W.G.: Sampling techniques. John Wiley & Sons, Chichester (1977)
Di Pierro, A., Hankin, C., Wiklicky, H.: A systematic approach to probabilistic pointer analysis. In: ASPLAS 2007 (2007)
Di Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic λ-calculus and quantitative program analysis. Journal of Logic and Computation (2005)
Di Pierro, A., Wiklicky, H.: Concurrent constraint programming: Towards probabilistic abstract interpretation. In: PPDP 2000 (2000)
Goodman, N., Mansinghka, V., Roy, D., Bonawitz, K., Tenenbaum, J.: Church: a language for generative models. In: UAI 2008 (2008)
Gulwani, S., Necula, G.C.: Precise interprocedural analysis using random interpretation. In: POPL 2005 (2005)
Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI 2010 (2010)
Hall, M., Murphy, B., Amarasinghe, S., Liao, S., Lam, M.: Interprocedural analysis for parallelization. In: Languages and Compilers for Parallel Computing (1996)
Hoffman, H., Sidiroglou, S., Carbin, M., Misailovic, S., Agarwal, A., Rinard, M.: Dynamic knobs for power-aware computing. In: ASPLOS 2011 (2011)
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)
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)
Kennedy, K., Allen, J.R.: Optimizing compilers for modern architectures: a dependence-based approach. Morgan Kaufmann, San Francisco (2002)
Klir, G.: Uncertainty and information. John Wiley & Sons, Chichester (2006)
Kozen, D.: Semantics of probabilistic programs. Journal of Computer and System Sciences (1981)
Kwiatkowska, M., Norman, G., Parker, D.: Prism: Probabilistic symbolic model checker. In: Computer Performance Evaluation: Modelling Techniques and Tools (2002)
Misailovic, S., Roy, D., Rinard, M.: Probabilistic and Statistical Analysis of Per-forated Patterns. Technical Report MIT-CSAIL-TR-2011-003, MIT (2011)
Misailovic, S., Sidiroglou, S., Hoffmann, H., Rinard, M.: Quality of service profiling. In: ICSE 2010 (2010)
Monniaux, D.: Abstract interpretation of probabilistic semantics. In: SAS 2000. LNCS, vol. 1824, pp. 322–340. Springer, Heidelberg (2000)
Monniaux, D.: An abstract monte-carlo method for the analysis of probabilistic programs. In: POPL 2001 (2001)
Moore, R.E.: Interval analysis. Prentice-Hall, Englewood Cliffs (1966)
Morgan, C., McIver, A.: pGCL: formal reasoning for random algorithms. South African Computer Journal 22 (1999)
Park, S., Pfenning, F., Thrun, S.: A probabilistic language based upon sampling functions. In: POPL 2005 (2005)
Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL 2002 (2002)
Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: ICFP 2010 (2010)
Rinard, M.: Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. In: ICS 2006 (2006)
Rinard, M.: Using early phase termination to eliminate load imbalances at barrier synchronization points. In: OOPSLA 2007 (2007)
Rinard, M., Hoffmann, H., Misailovic, S., Sidiroglou, S.: Patterns and statistical analysis for understanding reduced resource computing. In: Onward! 2010 (2010)
Saheb-Djahromi, N.: Probabilistic LCF. In: MFCS 1978 (1978)
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)
Sidiroglou, S., Misailovic, S., Hoffmann, H., Rinard, M.: Managing Performance vs. Accuracy Trade-offs With Loop Perforation. In: FSE 2011 (2011)
Smith, M.: Probabilistic abstract interpretation of imperative programs using truncated normal distributions. Electronic Notes in Theoretical Computer Science (2008)
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)
Springer, M.: The algebra of random variables. John Wiley & Sons, Chichester (1979)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)