Advertisement

Distributed Computation of Fixed Points on Dependency Graphs

  • Andreas Engelbredt Dalsgaard
  • Søren EnevoldsenEmail author
  • Kim Guldstrand Larsen
  • Jiří Srba
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)

Abstract

Dependency graph is an abstract mathematical structure for representing complex causal dependencies among its vertices. Several equivalence and model checking questions, boolean equation systems and other problems can be reduced to fixed-point computations on dependency graphs. We develop a novel distributed algorithm for computing such fixed points, prove its correctness and provide an efficient, open-source implementation of the algorithm. The algorithm works in an on-the-fly manner, eliminating the need to generate a priori the entire dependency graph. We evaluate the applicability of our approach by a number of experiments that verify weak simulation/bisimulation equivalences between CCS processes and we compare the performance with the well-known CWB tool. Even though the fixed-point computation, being a P-complete problem, is difficult to parallelize in theory, we achieve significant speed-ups in the performance as demonstrated on a Linux cluster with several hundreds of cores.

Keywords

Dependency Graph Task Graph Label Transition System Leader Election Model Check Problem 
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.

Notes

Acknowledgments

The present work was supported by the Danish e-Infrastructure Cooperation by co-funding acquisitions of the MCC Linux cluster at Aalborg University and received funding from the Sino-Danish Basic Research Center IDEA4CPS funded by the Danish National Research Foundation and the National Science Foundation, China, the Innovation Fund Denmark center DiCyPS, as well as the ERC Advanced Grant LASSO. The fourth author is partially affiliated with FI MU in Brno.

References

  1. 1.
    Liu, X., Ramakrishnan, C.R., Smolka, S.A.: Fully local and efficient evaluation of alternating fixed points. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 5–19. Springer, Heidelberg (1998). doi: 10.1007/BFb0054161 CrossRefGoogle Scholar
  2. 2.
    Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998). doi: 10.1007/BFb0055040 CrossRefGoogle Scholar
  3. 3.
    Balcázar, L.J., Gabarró, J., Santha, M.: Deciding bisimilarity is p-complete. Formal Asp. Comput. 4(6A), 638–648 (1992)CrossRefzbMATHGoogle Scholar
  4. 4.
    Cleaveland, R., Parrow, J., Steffen, B.: The concurrency workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36–72 (1993)CrossRefGoogle Scholar
  5. 5.
    Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Berlin (1980)zbMATHGoogle Scholar
  6. 6.
    Bollig, B., Leucker, M., Weber, M.: Local parallel model checking for the alternation-free \(\mu \)-calculus. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 128–147. Springer, Heidelberg (2002). doi: 10.1007/3-540-46017-9_11 CrossRefGoogle Scholar
  7. 7.
    Grumberg, O., Heyman, T., Schuster, A.: Distributed symbolic model checking for \(\mu \)-calculus. Formal Meth. Syst. Des. 26(2), 197–219 (2005)CrossRefzbMATHGoogle Scholar
  8. 8.
    Joubert, C., Mateescu, R.: Distributed on-the-fly model checking and test case generation. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 126–145. Springer, Heidelberg (2006). doi: 10.1007/11691617_8 CrossRefGoogle Scholar
  9. 9.
    Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54862-8_13 CrossRefGoogle Scholar
  10. 10.
    Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013)CrossRefzbMATHGoogle Scholar
  11. 11.
    Holzmann, G.: Spin Model Checker, the: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2003)Google Scholar
  12. 12.
    Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. The MIT Press, Cambridge (2014)zbMATHGoogle Scholar
  13. 13.
    Andersen, J.R., Andersen, N., Enevoldsen, S., Hansen, M.M., Larsen, K.G., Olesen, S.R., Srba, J., Wortmann, J.K.: CAAL: concurrency workbench, aalborg edition. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 573–582. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-25150-9_33 CrossRefGoogle Scholar
  14. 14.
    Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math 5(2), 285–309 (1955)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Glabbeek, R.J.: The linear time - branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990). doi: 10.1007/BFb0039066 CrossRefGoogle Scholar
  16. 16.
    Andersen, J.R., Hansen, M.M., Andersen, N.: CAAL 2.0: equivalences, preorders and games for CCS and TCCS. Master’s thesis, Aalborg University (2015)Google Scholar
  17. 17.
    Jensen, J.F., Larsen, K.G., Srba, J., Oestergaard, L.K.: Local model checking of weighted CTL with upper-bound constraints. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 178–195. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-39176-7_12 CrossRefGoogle Scholar
  18. 18.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). doi: 10.1007/11539452_9 CrossRefGoogle Scholar
  19. 19.
    Liu, X., Smolka, S.A.: Simple linear-time algorithms for minimal fixed points. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 53–66. Springer, Heidelberg (1998). doi: 10.1007/BFb0055040 CrossRefGoogle Scholar
  20. 20.
    Dijkstra, E.W.: Shmuel Safra’s version of termination detection. EWD Manuscript 998, (1987)Google Scholar
  21. 21.
    Chang, E., Roberts, R.: An improved algorithm for decentralized extrema-finding in circular configurations of processes. Commun. ACM 22(5), 281–283 (1979)CrossRefzbMATHGoogle Scholar
  22. 22.
    Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Commun. ACM 12(5), 260–261 (1969)CrossRefGoogle Scholar
  23. 23.
    Kwok, Y.-K., Ahmad, I.: Benchmarking and comparison of the task graph scheduling algorithms. J. Parallel Distrib. Comput. 59(3), 381–422 (1999)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Andreas Engelbredt Dalsgaard
    • 1
  • Søren Enevoldsen
    • 1
    Email author
  • Kim Guldstrand Larsen
    • 1
  • Jiří Srba
    • 1
  1. 1.Department of Computer ScienceAalborg UniversityAalborg EastDenmark

Personalised recommendations