Ezgi Çiçek
ABSTRACT
Establishing quantitative bounds on the execution cost of programs is essential in many areas of computer science such as complexity analysis, compiler optimizations, security and privacy. Techniques based on program analysis, type systems and abstract interpretation are well-studied, but methods for analyzing how the execution costs of two programs compare to each other have not received attention. Naively combining the worst and best case execution costs of the two programs does not work well in many cases because such analysis forgets the similarities between the programs or the inputs.
In this work, we propose a relational cost analysis technique that is capable of establishing precise bounds on the difference in the execution cost of two programs by making use of relational properties of programs and inputs. We develop , a refinement type and effect system for a higher-order functional language with recursion and subtyping. The key novelty of our technique is the combination of relational refinements with two modes of typing-relational typing for reasoning about similar computations/inputs and unary typing for reasoning about unrelated computations/inputs. This combination allows us to analyze the execution cost difference of two programs more precisely than a naive non-relational approach.
We prove our type system sound using a semantic model based on step-indexed unary and binary logical relations accounting for non-relational and relational reasoning principles with their respective costs. We demonstrate the precision and generality of our technique through examples.
- A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In Proceedings of the 15th European Conference on Programming Languages and Systems, ESOP’06, pages 69–83, 2006. Google Scholar
Digital Library
- E. Albert, P. Arenas, S. Genaim, M. G´omez-Zamalloa, G. Puebla, D. Ram´ırez, G. Román, and D. Zanardini. Termination and Cost Analysis with COSTA and its User Interfaces. Electr. Notes Theor. Comput. Sci., 258(1):109–121, 2009. Google ScholarDigital Library
- T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object-oriented programs. In J. G. Morrisett and S. L. P. Jones, editors, Proceedings of the 33th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’06, pages 91–102, 2006. Google ScholarDigital Library
- A. W. Appel and D. A. McAllester. An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst., 23(5):657–683, 2001. Google ScholarDigital Library
- R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th Euro. Symp. on Prog. (ESOP’10), pages 85–103, 2010. Google ScholarDigital Library
- G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In M. J. Butler and W. Schulte, editors, Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 200–214, 2011. Google ScholarDigital Library
- G. Barthe, C. Fournet, B. Grégoire, P. Strub, N. Swamy, and S. Z. Béguelin. Probabilistic relational verification for cryptographic implementations. In S. Jagannathan and P. Sewell, editors, Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’14, pages 193–206, 2014. Google ScholarDigital Library
- G. Barthe, M. Gaboardi, E. J. Gallego Arias, J. Hsu, A. Roth, and P.-Y. Strub. Higher-order approximate relational refinement types for mechanism design and differential privacy. In S. K. Rajamani and D. Walker, editors, Proceedings of the 42nd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, pages 55–68, 2015. Google ScholarDigital Library
- N. Benton. Simple relational correctness proofs for static analyses and program transformations. In N. D. Jones and X. Leroy, editors, Proceedings of the 31th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’04, pages 14–25, 2004. Google ScholarDigital Library
- G. Bonfante, J. Marion, and J. Moyen. Quasi-interpretations a way to control resources. Theor. Comput. Sci., 412(25):2776–2796, 2011. Google ScholarDigital Library
- M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating Runtime and Size Complexity Analysis of Integer Programs. In Tools and Alg. for the Constr. and Anal. of Systems - 20th Int. Conf. (TACAS’14), pages 140–155, 2014.Google Scholar
- J. Burnim and K. Sen. Asserting and checking determinism for multithreaded programs. In H. van Vliet and V. Issarny, editors, Proceedings of the 7th joint meeting of the European Software Engineering Conference and the ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2009, Amsterdam, The Netherlands, August 24-28, 2009, pages 3–12, 2009. Google ScholarDigital Library
- M. Carbin, D. Kim, S. Misailovic, and M. C. Rinard. Proving acceptability properties of relaxed nondeterministic approximate programs. In J. Vitek, H. Lin, and F. Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, Beijing, China - June 11 - 16, 2012, pages 169–180, 2012. Google ScholarDigital Library
- M. Carbin, S. Misailovic, and M. C. Rinard. Verifying quantitative reliability for programs that execute on unreliable hardware. In A. L. Hosking, P. T. Eugster, and C. V. Lopes, editors, Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2013, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pages 33–52, 2013. Google ScholarDigital Library
- Q. Carbonneaux, J. Hoffmann, and Z. Shao. Compositional Certified Resource Bounds. In 36th Conference on Programming Language Design and Implementation (PLDI’15), 2015. Artifact submitted and approved. Google ScholarDigital Library
- S. Chaudhuri, S. Gulwani, and R. Lublinerman. Continuity analysis of programs. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’10, pages 57–70, 2010.. Google ScholarDigital Library
- E. C ¸ ic¸ek, D. Garg, and U. A. Acar. Refinement types for incremental computational complexity. In Programming Languages and Systems - 24th European Symposium on Programming, ESOP 2015, London, UK, April 11-18, 2015. Proceedings, pages 406–431, 2015.Google Scholar
- E. C ¸ ic¸ek, Z. Paraskevopoulou, and D. Garg. A type theory for incremental computational complexity with control flow changes. In Proceedings of the 21st International Conference on Functional Programming, ICFP ’16, 2016. Google ScholarDigital Library
- M. R. Clarkson and F. B. Schneider. Hyperproperties. In Proceedings of CSF’08, pages 51–65, 2008. Google ScholarDigital Library
- U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science, LICS ’11, pages 133–142, 2011. Google ScholarDigital Library
- U. Dal lago and B. Petit. The geometry of types. In Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL ’13, pages 167–178, 2013. Google ScholarDigital Library
- N. Danner, D. R. Licata, and R. Ramyaa. Denotational cost semantics for functional languages with inductive types. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 140–151, 2015. Google ScholarDigital Library
- D. Felsing, S. Grebing, V. Klebanov, P. Rümmer, and M. Ulbrich. Automating regression verification. In I. Crnkovic, M. Chechik, and P. Grünbacher, editors, ACM/IEEE International Conference on Automated Software Engineering, ASE ’14, Vasteras, Sweden - September 15 - 19, 2014, pages 349–360, 2014.. Google ScholarDigital Library
- M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy. In Proceedings of the 40th Annual Symposium on Principles of Programming Languages, POPL ’13, pages 357–370, 2013. Google ScholarDigital Library
- B. Godlin and O. Strichman. Regression verification: proving the equivalence of similar programs. Softw. Test., Verif. Reliab., 23(3): 241–258, 2013.Google ScholarCross Ref
- S. Gulwani, K. K. Mehra, and T. Chilimbi. Speed: Precise and efficient static estimation of program computational complexity. In Proceedings of the 36th Annual Symposium on Principles of Programming Languages, POPL ’09, pages 127–139, 2009. Google ScholarDigital Library
- C. Hawblitzel, S. K. Lahiri, K. Pawar, H. Hashmi, S. Gokbulut, L. Fernando, D. Detlefs, and S. Wadsworth. Will you still compile me tomorrow? static cross-version compiler validation. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, pages 191–201, 2013. Google ScholarDigital Library
- J. Hoffmann and Z. Shao. Automatic Static Cost Analysis for Parallel Programs. In 24th European Symposium on Programming (ESOP’15), 2015. Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. In Proceedings of the 38th Annual Symposium on Principles of Programming Languages, POPL ’11, pages 357–370, 2011. Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. ACM Trans. Program. Lang. Syst., 2012. Google ScholarDigital Library
- S. K. Lahiri, K. Vaswani, and C. A. R. Hoare. Differential static analysis: opportunities, applications, and challenges. In G. Roman and K. J. Sullivan, editors, Proceedings of the Workshop on Future of Software Engineering Research, FoSER 2010, at the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010, Santa Fe, NM, USA, November 7-11, 2010, pages 201–204, 2010.. Google ScholarDigital Library
- S. K. Lahiri, C. Hawblitzel, M. Kawaguchi, and H. Rebˆelo. SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In P. Madhusudan and S. A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, volume 7358 of Lecture Notes in Computer Science, pages 712–717, 2012. Google ScholarDigital Library
- S. K. Lahiri, K. L. McMillan, R. Sharma, and C. Hawblitzel. Differential assertion checking. In B. Meyer, L. Baresi, and M. Mezini, editors, Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC/FSE’13, pages 345–355, 2013. Google ScholarDigital Library
- F. Logozzo, S. K. Lahiri, M. Fähndrich, and S. Blackshear. Verification modulo versions: towards usable verification. In M. F. P. O’Boyle and K. Pingali, editors, Proceedings of 2014 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’14, page 32, 2014. Google ScholarDigital Library
- A. Nanevski, A. Banerjee, and D. Garg. Verification of information flow and access control policies with dependent types. In 32nd IEEE Symposium on Security and Privacy, S&P 2011, 22-25 May 2011, Berkeley, California, USA, pages 165–179, 2011. Google ScholarDigital Library
- F. Nielson and H. Nielson. Type and effect systems. In Correct System Design, volume 1710 of Lecture Notes in Computer Science, pages 114–136. 1999. Google ScholarDigital Library
- N. Partush and E. Yahav. Abstract semantic differencing via speculative correlation. In A. P. Black and T. D. Millstein, editors, Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA 2014, part of SPLASH 2014, Portland, OR, USA, October 20-24, 2014, pages 811–828, 2014. Google ScholarDigital Library
- S. Person, M. B. Dwyer, S. G. Elbaum, and C. S. Pasareanu. Differential symbolic execution. In M. J. Harrold and G. C. Murphy, editors, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2008, Atlanta, Georgia, USA, November 9-14, 2008, pages 226–237, 2008. Google ScholarDigital Library
- S. Person, G. Yang, N. Rungta, and S. Khurshid. Directed incremental symbolic execution. In M. W. Hall and D. A. Padua, editors, Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8, 2011, pages 504–515, 2011. Google ScholarDigital Library
- F. Pottier and V. Simonet. Information flow inference for ML. ACM Trans. Prog. Lang. Sys., 25(1):117–158, Jan. 2003. Google ScholarDigital Library
- J. Reed and B. C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Proceeding of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010, pages 157– 168, 2010. Google ScholarDigital Library
- B. Reistad and D. K. Gifford. Static dependent costs for estimating execution time. In Proceedings of the 1994 ACM Conference on LISP and Functional Programming, LFP ’94, pages 65–78, 1994. Google ScholarDigital Library
- D. Sands. Total correctness by local improvement in program transformation. In Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 221–232, 1995. Google ScholarDigital Library
- M. Sinn, F. Zuleger, and H. Veith. A Simple and Scalable Approach to Bound Analysis and Amortized Complexity Analysis. In Computer Aided Verification - 26th Int. Conf. (CAV’14), page 743–759, 2014. Google ScholarDigital Library
- T. Terauchi and A. Aiken. Secure information flow as a safety problem. In C. Hankin and I. Siveroni, editors, Static Analysis Symposium, volume 3672, pages 352–367, 2005. Google ScholarDigital Library
- G. Yang, M. B. Dwyer, and G. Rothermel. Regression model checking. In 25th IEEE International Conference on Software Maintenance (ICSM 2009), September 20-26, 2009, Edmonton, Alberta, Canada, pages 115–124, 2009.Google ScholarCross Ref
- H. Yang. Relational separation logic. Theoretical Comput. Sci., 375 (1-3):308–334, 2007. Google ScholarDigital Library
- A. Zaks and A. Pnueli. CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In J. Cuéllar, T. S. E. Maibaum, and K. Sere, editors, Formal Methods, volume 5014 of Lecture Notes in Computer Science, pages 35–51, 2008. Google ScholarDigital Library
Index Terms
- Relational cost analysis
Recommendations
Relational cost analysis
POPL '17Establishing quantitative bounds on the execution cost of programs is essential in many areas of computer science such as complexity analysis, compiler optimizations, security and privacy. Techniques based on program analysis, type systems and abstract ...
Relational cost analysis for functional-imperative programs
Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost analysis to establish bounds on the difference in the evaluation cost of the ...
Monadic refinements for relational cost analysis
Formal frameworks for cost analysis of programs have been widely studied in the unary setting and, to a limited extent, in the relational setting. However, many of these frameworks focus only on the cost aspect, largely side-lining functional properties ...
Comments