Top

Hint

Swipe to navigate through the chapters of this book

Published in:

Read chapter Read first chapter

2021 | OriginalPaper | Chapter

Selectively-Amortized Resource Bounding

Authors : Tianhan Lu, Bor-Yuh Evan Chang, Ashutosh Trivedi

Published in: Static Analysis

Publisher: Springer International Publishing

Abstract

We consider the problem of automatically proving resource bounds. That is, we study how to prove that an integer-valued resource variable is bounded by a given program expression. Automatic resource-bound analysis has recently received significant attention because of a number of important applications (e.g., detecting performance bugs, preventing algorithmic-complexity attacks, identifying side-channel vulnerabilities), where the focus has often been on developing precise amortized reasoning techniques to infer the most exact resource usage. While such innovations remain critical, we observe that fully precise amortization is not always necessary to prove a bound of interest. And in fact, by amortizing selectively, the needed supporting invariants can be simpler, making the invariant inference task more feasible and predictable. We present a framework for selectively-amortized analysis that mixes worst-case and amortized reasoning via a property decomposition and a program transformation. We show that proving bounds in any such decomposition yields a sound resource bound in the original program, and we give an algorithm for selecting a reasonable decomposition.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

inform now

previous chapter Selective Context-Sensitivity for k-CFA with CFL-Reachability

next chapter Reduced Products of Abstract Domains for Fairness Certification of Neural Networks

Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: Principles of Programming Languages (POPL), pp. 147–160 (1999). https://doi.org/10.1145/292540.292555

Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71316-6_12 CrossRef

Albert, E., Genaim, S., Gómez-Zamalloa, M.: Heap space analysis for Java bytecode. In: International Symposium on Memory Management (ISMM), pp. 105–116 (2007). https://doi.org/10.1145/1296907.1296922

Albert, E., Genaim, S., Gómez-Zamalloa, M.: Live heap space analysis for languages with garbage collection. In: International Symposium on Memory Management (ISMM), pp. 129–138 (2009). https://doi.org/10.1145/1542431.1542450

Albert, E., Genaim, S., Masud, A.N.: More precise yet widely applicable cost analysis. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 38–53. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-18275-4_5 CrossRef

Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 405–421. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33125-1_27 CrossRef

Atkey, R.: Amortised resource analysis with separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 85–103. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_6 CrossRef

Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Alternating runtime and size complexity analysis of integer programs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 140–155. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_10 CrossRef

Cadek, P., Danninger, C., Sinn, M., Zuleger, F.: Using loop bound analysis for invariant generation. In: Formal Methods in Computer Aided Design (FMCAD), pp. 1–9 (2018). https://doi.org/10.23919/FMCAD.2018.8603005

10.

Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Programming Language Design and Implementation (PLDI), pp. 467–478 (2015). https://doi.org/10.1145/2737924.2737955

11.

Carbonneaux, Q., Hoffmann, J., Reps, T., Shao, Z.: Automated resource analysis with Coq proof objects. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 64–85. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_4 CrossRef

12.

Chatterjee, K., Fu, H., Goharshady, A.K., Goharshady, E.K.: Polynomial invariant generation for non-deterministic recursive programs. In: Programming Language Design and Implementation (PLDI), pp. 672–687 (2020). https://doi.org/10.1145/3385412.3385969

13.

Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_39 CrossRef

14.

de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24 CrossRef

15.

Defense Advanced Research Projects Agency (DARPA): Space/time analysis for cybersecurity (STAC) (2019). https://www.darpa.mil/program/space-time-analysis-for-cybersecurity

16.

Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), pp. 443–456 (2013). https://doi.org/10.1145/2509136.2509511

17.

Guéneau, A., Charguéraud, A., Pottier, F.: A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 533–560. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_19 CrossRef

18.

Guéneau, A., Jourdan, J.-H., Charguéraud, A., Pottier, F.: Formal proof and analysis of an incremental cycle detection algorithm. In: Interactive Theorem Proving (ITP), vol. 141, pp. 18:1–18:20 (2019). https://doi.org/10.4230/LIPIcs.ITP.2019.18

19.

Gulwani, S., Zuleger, F.: The reachability-bound problem. In: Programming Language Design and Implementation (PLDI), pp. 292–304 (2010). https://doi.org/10.1145/1806596.1806630

20.

Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: Programming Language Design and Implementation (PLDI), pp. 375–385 (2009a). https://doi.org/10.1145/1542476.1542518

21.

Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: precise and efficient static estimation of program computational complexity. In: Principles of Programming Languages (POPL), pp. 127–139 (2009). https://doi.org/10.1145/1480881.1480898

22.

Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. In: Principles of Programming Languages (POPL), pp. 357–370 (2011). https://doi.org/10.1145/1926385.1926427

23.

Hoffmann, J., Das, A., Weng, S.-C.: Towards automatic resource bound analysis for OCaml. In: Principles of Programming Languages (POPL), pp. 359–373 (2017). https://doi.org/10.1145/3009837.3009842

24.

Hrushovski, E., Ouaknine, J., Pouly, A., Worrell, J.: Polynomial invariants for affine programs. In: Logic in Computer Science (LICS), pp. 530–539 (2018). https://doi.org/10.1145/3209108.3209142

25.

Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Compositional recurrence analysis revisited. In: Programming Language Design and Implementation (PLDI), pp. 248–262 (2017). https://doi.org/10.1145/3062341.3062373

26.

Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. 2(POPL), 54:1–54:33 (2018). https://doi.org/10.1145/3158142

27.

Kincaid, Z., Breck, J., Cyphert, J., Reps, T.W.: Closed forms for numerical loops. Proc. ACM Program. Lang. 3(POPL), 55:1–55:29 (2019). https://doi.org/10.1145/3290368

28.

Lu, T., Černý, P., Chang, B.-Y.E., Trivedi, A.: Type-directed bounding of collections in reactive programs. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 275–296. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-11245-5_13 CrossRef

29.

Lu, T., Chang, B.-Y.E., Trivedi, A.: Selectively-amortized resource bounding (extended version) (2021). https://arxiv.org/abs/2108.08263

30.

Lu, T., Chang, B.-Y.E., Trivedi, A.: Selectively-amortized resource bounding (artifact) (2021). https://zenodo.org/record/5140586

31.

Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 91–130 (1991). https://doi.org/10.1016/0304-3975(91)90041-Y CrossRefMATH

32.

Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703–719. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_57 CrossRef

33.

Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745–761. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_50 CrossRef

34.

Sinn, M., Zuleger, F., Veith, H.: Difference constraints: an adequate abstraction for complexity analysis of imperative programs. In: Formal Methods in Computer Aided Design (FMCAD), pp. 144–151 (2015)

35.

Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason. 59(1), 3–45 (2017). https://doi.org/10.1007/s10817-016-9402-4 MathSciNetCrossRefMATH

36.

Tarjan, R.E.: Amortized computational complexity. SIAM J. Alg. Discrete Methods 6(2), 306–318 (1985) MathSciNetCrossRef

37.

Weiser, M.: Program slicing. IEEE Trans. Software Eng. 10(4), 352–357 (1984). https://doi.org/10.1109/TSE.1984.5010248 CrossRefMATH

38.

Wilhelm, R., et al.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7(3):36:1–36:53 (2008). https://doi.org/10.1145/1347375.1347389

39.

Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 280–297. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23702-7_22 CrossRef

Title: Selectively-Amortized Resource Bounding
Authors: Tianhan Lu
Bor-Yuh Evan Chang
Ashutosh Trivedi
Publisher: Springer International Publishing
Book: Static Analysis
Print ISBN: 978-3-030-88805-3

Electronic ISBN: 978-3-030-88806-0

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-88806-0_14

Springer Professional

Hint

Swipe to navigate through the chapters of this book

Abstract

Please log in to get access to this content

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner