Advertisement

Causal Termination of Multi-threaded Programs

  • Andrey Kupriyanov
  • Bernd Finkbeiner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

We present a new model checking procedure for the termination analysis of multi-threaded programs. Current termination provers scale badly in the number of threads; our new approach easily handles 100 threads on multi-threaded benchmarks like Producer-Consumer. In our procedure, we characterize the existence of non-terminating executions as Mazurkiewicz-style concurrent traces and apply causality-based transformation rules to refine them until a contradiction can be shown. The termination proof is organized into a tableau, where the case splits represent a novel type of modular reasoning according to different causal explanations of a hypothetical error. We report on experimental results obtained with a tool implementation of the new procedure, called Arctor, on previously intractable multi-threaded benchmarks.

Keywords

Ranking Function Covered Vertex Graph Transformation Proof Rule Transition Predicate 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491–504. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  2. 2.
    Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413–429. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent c programs. Formal Methods in System Design 25(2-3), 129–166 (2004)CrossRefzbMATHGoogle Scholar
  5. 5.
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  6. 6.
    Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. SIGPLAN Not. 41(6), 415–426 (2006)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. ACM SIGPLAN Notices 42(6), 320 (2007)CrossRefGoogle Scholar
  8. 8.
    Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 47–61. Springer, Heidelberg (2013)Google Scholar
  9. 9.
    Corradini, A., Montanari, U., Rossi, F., Ehrig, H., Heckel, R., Löwe, M.: Algebraic approaches to graph transformation - part i: Basic concepts and double pushout approach. In: Rozenberg [25], pp. 163–246Google Scholar
  10. 10.
    Dräger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: Slab: A certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 271–274. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  11. 11.
    Ehrig, H., Heckel, R., Korff, M., Löwe, M., Ribeiro, L., Wagner, A., Corradini, A.: Algebraic approaches to graph transformation - part ii: Single pushout approach and comparison with double pushout approach. In: Rozenberg [25], pp. 247–312Google Scholar
  12. 12.
    Ganty, P., Genaim, S.: Proving Termination Starting from the End. Computer Aided Verification (10), 397–412 (2013)Google Scholar
  13. 13.
    Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Automated termination proofs with aProVE. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 210–220. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  14. 14.
    Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer-Verlag Inc., New York (1996)Google Scholar
  15. 15.
    Kupriyanov, A., Finkbeiner, B.: Causality-based verification of multi-threaded programs. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 257–272. Springer, Heidelberg (2013)Google Scholar
  16. 16.
    Manna, Z.: Introduction to Mathematical Theory of Computation. McGraw-Hill, Inc., New York (1974)Google Scholar
  17. 17.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems - safety. Springer (1995)Google Scholar
  18. 18.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: Response. In: Manna, Z., Peled, D.A. (eds.) Pnueli Festschrift. LNCS, vol. 6200, pp. 279–361. Springer, Heidelberg (2010)Google Scholar
  19. 19.
    Mazurkiewicz, A.: Concurrent program schemes and their interpretations. Technical Report DAIMI PB 78. Aarhus University (1977)Google Scholar
  20. 20.
    Olderog, E.-R., Apt, K.R.: Fairness in parallel programs: The transformational approach. ACM Trans. Program. Lang. Syst. 10(3), 420–455 (1988)CrossRefGoogle Scholar
  21. 21.
    Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 32–41 (July 2004)Google Scholar
  22. 22.
    Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  23. 23.
    Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol. 4354, pp. 245–259. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  24. 24.
    Reisig, W.: Petri Nets – An Introduction. Springer (1985)Google Scholar
  25. 25.
    Rozenberg, G.: Handbook of Graph Grammars and Computing by Graph Transformations. Foundations, vol. 1. World Scientific (1997)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Andrey Kupriyanov
    • 1
  • Bernd Finkbeiner
    • 1
  1. 1.Universität des SaarlandesSaarbrückenGermany

Personalised recommendations