Top

Published in:

2021 | OriginalPaper | Chapter

Selectively-Amortized Resource Bounding

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

Published in: Static Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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 Wissensvorsprung sichern!

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 Wissensvorsprung sichern!

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 Wissensvorsprung sichern!

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_12CrossRef

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_5CrossRef

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_27CrossRef

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_6CrossRef

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_10CrossRef

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_4CrossRef

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_39CrossRef

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_24CrossRef

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_19CrossRef

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_13CrossRef

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-YCrossRefMATH

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_57CrossRef

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_50CrossRef

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-4MathSciNetCrossRefMATH

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.5010248CrossRefMATH

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_22CrossRef

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

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"