ABSTRACT
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 function memoization [11],and approximate data types [34] produce programs that can execute at a variety of points in an underlying performance versus accuracy tradeoff space. These transformed programs have the ability to trade accuracy of their results for increased performance by dynamically and nondeterministically modifying variables that control their execution.
We call such transformed programs relaxed programs because they have been extended with additional nondeterminism to relax their semantics and enable greater flexibility in their execution.
We present language constructs for developing and specifying relaxed programs. We also present proof rules for reasoning about properties [28] which the program must satisfy to be acceptable. Our proof rules work with two kinds of acceptability properties: acceptability properties [28], which characterize desired relationships between the values of variables in the original and relaxed programs, and unary acceptability properties, which involve values only from a single (original or relaxed) program. The proof rules support a staged reasoning approach in which the majority of the reasoning effort works with the original program. Exploiting the common structure that the original and relaxed programs share, relational reasoning transfers reasoning effort from the original program to prove properties of the relaxed program.
We have formalized the dynamic semantics of our target programming language and the proof rules in Coq and verified that the proof rules are sound with respect to the dynamic semantics. Our Coq implementation enables developers to obtain fully machine-checked verifications of their relaxed programs.
Supplemental Material
Available for Download
This supplementary material contains the formalization of convergent program points.
- The Coq Proof Assistant. http://coq.inria.fr.Google Scholar
- Scimark 2.0. http://math.nist.gov/scimark2.Google Scholar
- 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. Google ScholarDigital Library
- W. Baek and T. M. Chilimbi. Green: a framework for supporting energy-conscious programming using controlled approximation. PLDI, 2010. Google ScholarDigital Library
- G. Barthe, J. Crespo, and C. Kunz. Relational verification using product programs. FM, 2011. Google ScholarDigital Library
- G. Barthe, B. Köpf, F. Olmedo, and S. Zanella Béguelin. Probabilistic reasoning for differential privacy. POPL, 2012. Google ScholarDigital Library
- N. Benton. Simple relational correctness proofs for static analyses and program transformations. POPL, 2004. Google ScholarDigital Library
- W. Blume and R. Eigenmann. Performance analysis of parallelizing compilers on the Perfect Benchmarks programs. Transactions on Parallel and Distributed Systems, 3(6), 1992. Google ScholarDigital Library
- M. Carbin, D. Kim, S. Misailovic, and M. Rinard. Reasoning about Relaxed Programs. Technical Report MIT-CSAIL-TR-2011-050, MIT, 2011.Google Scholar
- M. Carbin and M. Rinard. Automatically Identifying Critical Input Regions and Code in Applications. ISSTA, 2010. Google ScholarDigital Library
- S. Chaudhuri, S. Gulwani, R. Lublinerman, and S. Navidpour. Proving Programs Robust. FSE, 2011. Google ScholarDigital Library
- J.M. Crespo and C. Kunz. A machine-checked framework for relational separation logic. SEFM, 2011. Google ScholarDigital Library
- B. Demsky and M. Rinard. Data structure repair using goal-directed reasoning. ICSE, 2005. Google ScholarDigital Library
- R. W. Floyd. Assigning meanings to programs. Mathematical aspects of computer science, 19(19--32), 1967.Google Scholar
- C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10), October 1969. Google ScholarDigital Library
- H. Hoffman, S. Sidiroglou, M. Carbin, S. Misailovic, A. Agarwal, and M. Rinard. Dynamic knobs for responsive power-aware computing. ASPLOS, 2011. Google ScholarDigital Library
- 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.Google Scholar
- S. Liu, K. Pattabiraman, T. Moscibroda, and B. Zorn. Flikker: Saving dram refresh-power through critical data partitioning. ASPLOS, 2011. Google ScholarDigital Library
- A. Milicevic, D. Rayside, K. Yessenov, and D. Jackson. Unifying execution of imperative and declarative code. ICSE, 2011. Google ScholarDigital Library
- S. Misailovic, D. Kim, and M. Rinard. Parallelizing sequential programs with statistical accuracy tests. Technical Report MIT-CSAIL-TR-2010-038, MIT, 2010.Google Scholar
- S. Misailovic, D. Roy, and M. Rinard. Probabilistically Accurate Program Transformations. SAS, 2011. Google ScholarDigital Library
- S. Misailovic, S. Sidiroglou, H. Hoffmann, and M. Rinard. Quality of service profiling. ICSE, 2010. Google ScholarDigital Library
- C. Morgan. The specification statement. Transactions on Programming Languages and Systems, 10(3), 1988. Google ScholarDigital Library
- A. Nanevski, A. Banerjee, and D. Garg. Verification of information flow and access control policies with dependent types. SP, 2011. Google ScholarDigital Library
- J. Nelson, A. Sampson, and L. Ceze. Dense approximate storage in phase-change memory. ASPLOS-WACI, 2011.Google Scholar
- A. Pnueli, M. Siegel, and E. Singerman. Translation validation. TACAS, 1998. Google ScholarDigital Library
- D. Rayside, A. Milicevic, K. Yessenov, G. Dennis, and D. Jackson. Agile specifications. OOPSLA, 2009. Google ScholarDigital Library
- M. Rinard. Acceptability-oriented computing. OOPSLA Onwards '03. Google ScholarDigital Library
- M. Rinard. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. ICS, 2006. Google ScholarDigital Library
- M. Rinard. Using early phase termination to eliminate load imbalances at barrier synchronization points. OOPSLA, 2007. Google ScholarDigital Library
- M. C. Rinard and D. Marinov. Credible compilation with pointers. RTRV, 1999.Google Scholar
- Martin Rinard. A lossy, synchronization-free, race-full, but still acceptably accurate parallel space-subdivision tree construction algorithm. Technical Report MIT-CSAIL-TR-2012-005, MIT, 2012.Google Scholar
- H. Samimi, E. Aung, and T. Millstein. Falling back on executable specifications. ECOOP, 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- S. Sidiroglou, S. Misailovic, H. Hoffmann, and M. Rinard. Managing Performance vs. Accuracy Trade-offs With Loop Perforation. FSE '11.Google Scholar
- H Yang. Relational separation logic. Theoretical Computer Science, 375(1--3), May 2007. Google ScholarDigital Library
- J. Yang, K. Yessenov, and A. Solar-Lezama. A language for automatically enforcing privacy policies. POPL, 2012. Google ScholarDigital Library
- Z. Zhu, S. Misailovic, J. Kelner, and M. Rinard. Randomized accuracy-aware program transformations for efficient approximate computations. POPL, 2012. Google ScholarDigital Library
- L. Zuck, A. Pnueli, and R. Leviathan. Validation of optimizing compilers. Technical report, Weizmann Institute of Science, 2001. Google ScholarDigital Library
Index Terms
- Proving acceptability properties of relaxed nondeterministic approximate programs
Recommendations
Proving acceptability properties of relaxed nondeterministic approximate programs
PLDI '12Approximate 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 ...
Completeness and decidability of converse PDL in the constructive type theory of Coq
CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and ProofsThe completeness proofs for Propositional Dynamic Logic (PDL) in the literature are non-constructive and usually presented in an informal manner. We obtain a formal and constructive completeness proof for Converse PDL by recasting a completeness proof ...
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and ProofsCall-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...
Comments