Top

Journal of Automated Reasoning

Published in:

17-12-2016

Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings

Authors: Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin

Published in: Journal of Automated Reasoning | Issue 1/2017

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

search-config

AI-assisted search

Off

Abstract

By following a rely-guarantee style of reasoning, we present novel termination and cost analyses for concurrent programs that, in order to prove termination or infer the cost of a considered loop: (1) infer the termination/cost of each loop as if it were a sequential one, imposing assertions on how shared-data is modified concurrently; and then (2) prove that these assertions cannot be violated infinitely many times and, for cost analysis, infer how many times they are violated. At the core of the analysis, we use a may-happen-in-parallel analysis to restrict the set of program points whose execution can interleave. Interestingly, the same kind of reasoning can be applied to prove termination and infer upper bounds on the number of iterations of loops with concurrent interleavings. To the best of our knowledge, this is the first method to automatically bound the cost of such kind of loops. We have implemented our analysis for an actor-based language, and showed its accuracy and efficiency by applying it on several typical applications for concurrent programs and on an industrial case study.

previous article Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints

next article Type-Based Cost Analysis for Lazy Functional Languages

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

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

Available only for authorised users

For simplicity of the presentation, we have not included (nor used in the examples) an additional instruction to get the return value of an asynchronous call. This instruction exists in the ABS language [27] and it is called y.get, where

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-016-9400-6/MediaObjects/10817_2016_9400_IEq54_HTML.gif

is the future variable, but it does not introduce any challenge to the analysis.

Lines of code exclude comments and blanks.

http://costa.ls.fi.upm.es/comparator.

For every comparable method, we computed 200 ratios and compute their average.

At this point we assume a specific shape of \({tr^{ no-rst }}\) that starts and ends with a \({tr^{w}}\) subtrace. However, the same reasoning can be applied assuming \({tr^{ no-rst }}\) starts or ends with \({tr^{ inc }}\).

Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)

Albert, E., Arenas, P., Correas, J., Genaim, S., Gómez-Zamalloa, M., Román-Díez, G.P., Puebla, G.: Object-sensitive cost analysis for concurrent objects. Softw. Test. Verif. Reliab. 25(3), 218–271 (2015). doi:10.1002/stvr.1569 CrossRef

Albert, E., Arenas, P., Flores-Montoya, A., Genaim, S., Gómez-Zamalloa, M., Martin-Martin, E., Puebla, G., Román-Díez, G.: SACO: Static analyzer for concurrent objects. In: Ábrahám, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—20th International Conference, TACAS 2014. Lecture Notes in Computer Science, vol. 8413, pp. 562–567. Springer (2014). doi:10.1007/978-3-642-54862-8_46

Albert, E., Arenas, P., Genaim, S., Gómez-Zamalloa, M., Puebla, G.: Cost analysis of concurrent OO programs. In: Yang, H. (ed.) Programming Languages and Systems-9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5–7, 2011. Proceedings, Lecture Notes in Computer Science, vol. 7078, pp. 238–254. Springer (2011). doi:10.1007/978-3-642-25318-8_19

Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46(2), 161–203 (2011). doi:10.1007/s10817-010-9174-1 MathSciNetCrossRefMATH

Albert, E., Arenas, P., Genaim, S., Puebla, G.: A practical comparator of cost functions and its applications. Sci. Comput. Progr. 111(3), 483–504 (2015). doi:10.1016/j.scico.2014.12.001 CrossRef

Albert, E., Correas, J., Johnsen, E.B., Román-Díez, G.: Parallel cost analysis of distributed systems. In: Static Analysis-22nd International Symposium, SAS 2015. Proceedings, Lecture Notes in Computer Science, vol. 9291, pp. 275–292. Springer (2015). doi:10.1007/978-3-662-48288-9_16

Albert, E., Correas, J., Puebla, G., Román-Díez, G.: Quantified abstract configurations of distributed systems. Form. Asp. Comput. 27(4), 665–699 (2015). doi:10.1007/s00165-014-0321-z MathSciNetCrossRefMATH

Albert, E., Correas, J., Román-Díez, G.: Non-cumulative resource analysis. In: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Lecture Notes in Computer Science, vol. 9035, pp. 85–100. Springer (2015). doi:10.1007/978-3-662-46681-0_6

10.

Albert, E., Flores-Montoya, A., Genaim, S.: Analysis of may-happen-in-parallel in concurrent objects. In: Giese, H., Rosu, G. (eds.) Formal Techniques for Distributed Systems-Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13–16, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7273, pp. 35–51. Springer (2012). doi:10.1007/978-3-642-30793-5_3

11.

Albert, E., Flores-Montoya, A., Genaim, S., Martin-Martin, E.: Termination and cost analysis of loops with concurrent interleavings. In: Hung, D.V., Ogawa, M. (eds.) Automated Technology for Verification and Analysis-11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15–18, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8172, pp. 349–364. Springer (2013). doi:10.1007/978-3-319-02444-8_25

12.

Albert, E., Genaim, S., Gordillo, P.: May-happen-in-parallel analysis for asynchronous programs with inter-procedural synchronization. In: Static Analysis-22nd International Symposium, SAS 2015. Proceedings, Lecture Notes in Computer Science, vol. 9291, pp. 72–89. Springer (2015). doi:10.1007/978-3-662-48288-9_5

13.

Albert, E., Gómez-Zamalloa, M., Isabel, M.: Combining static analysis and testing for deadlock detection. In: Integrated Formal Methods-12th International Conference, IFM 2016, Reykjavik, Iceland, June 1–5, 2016. Proceedings, Lecture Notes in Computer Science, vol. 9681, pp. 409–424. Springer (2016)

14.

Albert, E., Gómez-Zamalloa, M., Isabel, M.: Syco: A systematic testing tool for concurrent objects. In: Zaks, A., Hermenegildo, M.V. (eds.) Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12–18 2016, pp. 269–270. ACM (2016)

15.

Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Proceedings of the SAS’10, LNCS, vol. 6337, pp. 117–133. Springer (2010)

16.

Armstrong, J., Virding, R., Wistrom, C., Williams, M.: Concurrent Programming in Erlang. Prentice Hall, Upper Saddle River (1996)MATH

17.

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.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). Lecture Notes in Computer Science, vol. 8413, pp. 140–155. Springer (2014)

18.

Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 467–478. ACM, New York (2015). doi:10.1145/2737924.2737955

19.

Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’07, pp. 320–330. ACM, New York (2007). doi:10.1145/1250734.1250771

20.

Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011)CrossRef

21.

de Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: de Nicola, R. (ed.) Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24–April 1, 2007. Proceedings, Lecture Notes in Computer Science, vol. 4421, pp. 316–330. Springer (2007)

22.

Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: ESOP, Lecture Notes in Computer Science, vol. 2305, pp. 262–277. Springer (2002)

23.

Flores-Montoya, A., Hähnle, R.: Resource analysis of complex programs with cost equations. In: Programming Languages and Systems-12th Asian Symposium, APLAS 2014, Singapore, November 17–19, 2014. Proceedings, LNCS, vol. 8858, pp. 275–295. Springer (2014)

24.

Garcia, A., Laneve, C., Lienhardt, M.: Static analysis of cloud elasticity. In: Falaschi, M., Albert, E. (eds.) Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14–16, 2015, pp. 125–136. ACM (2015). doi:10.1145/2790449.2790524

25.

Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don’t block. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 16–28. ACM (2009). doi:10.1145/1480881.1480886

26.

Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2–3), 202–220 (2009). doi:10.1016/j.tcs.2008.09.019 MathSciNetCrossRefMATH

27.

Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.C., de Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects-9th International Symposium, FMCO 2010, Graz, Austria, November 29–December 1, 2010. Revised Papers, Lecture Notes in Computer Science, vol. 6957, pp. 142–164. Springer (2012)

28.

Kupriyanov, A., Finkbeiner, B.: Causal termination of multi-threaded programs. In: Biere, A., Bloem, R. (eds.) 26th International Conference on Computer Aided Verification (CAV 2014). Lecture Notes in Computer Science, vol. 8559, pp. 814–830. Springer (2014)

29.

Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’12, pp. 237–251. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28756-5_17

30.

Schäfer, J., Poetzsch-Heffter, A.: JCobox: Generalizing active objects to concurrent components. In: D’Hondt, T. (ed.) ECOOP 2010-Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21–25, 2010. Proceedings, LNCS, vol. 6183, pp. 275–299. Springer (2010)

31.

Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Proceeding of Computer Aided Verification 2014, vol. 8559, pp. 745–761. Springer (2014)

32.

Sinn, M., Zuleger, F., Veith, H.: Difference constraints: an adequate abstraction for complexity analysis of imperative programs. CoRR abs/1508.04958 (2015). http://arxiv.org/abs/1508.04958

33.

Srinivasan, S., Mycroft, A.: Kilim: Isolation-typed actors for Java. In: Vitek, J. (ed.) ECOOP 2008-Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7–11, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5142, pp. 104–128. Springer (2008)

34.

Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS, Lecture Notes in Computer Science, vol. 6887, pp. 280–297. Springer (2011)

Title: Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings
Authors: Elvira Albert
Antonio Flores-Montoya
Samir Genaim
Enrique Martin-Martin
Publication date: 17-12-2016
Publisher: Springer Netherlands
Published in: Journal of Automated Reasoning / Issue 1/2017
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-016-9400-6

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 "Wirtschaft"

Springer Professional "Technik"

Other articles of this Issue 1/2017

Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints

Lower Bounds for Runtime Complexity of Term Rewriting

Type-Based Cost Analysis for Lazy Functional Languages

Preface: Special Issue on Automatic Resource Bound Analysis

Premium Partner