iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.1007/978-3-030-88806-0_17
Automated Verification of the Parallel Bellman–Ford Algorithm | SpringerLink
Skip to main content
Springer Nature Link
Log in

Automated Verification of the Parallel Bellman–Ford Algorithm

  • Conference paper
  • First Online:
Static Analysis (SAS 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12913))

Included in the following conference series:

Abstract

Many real-world problems such as internet routing are actually graph problems. To develop efficient solutions to such problems, more and more parallel graph algorithms are proposed. This paper discusses the mechanized verification of a commonly used parallel graph algorithm, namely the Bellman–Ford algorithm, which provides an inherently parallel solution to the Single-Source Shortest Path problem.

Concretely, we verify an unoptimized GPU version of the Bellman–Ford algorithm, using the VerCors verifier. The main challenge that we had to address was to find suitable global invariants of the graph-based properties for automated verification. This case study is the first deductive verification to prove functional correctness of the parallel Bellman–Ford algorithm. It provides the basis to verify other, optimized implementations of the algorithm. Moreover, it may also provide a good starting point to verify other parallel graph-based algorithms.

The first and third author are supported by the NWO VICI 639.023.710 Mercedes project.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Various details have been omitted for presentational clarity. We highlight only the most interesting aspects of the specification. The full specification is available at [31].

  2. 2.

    The keyword context is an abbreviation for both requires and ensures.

  3. 3.

    To specify permissions over a specific location \( idx \) of an array S we use \(\backslash \)pointer_index\((S, idx , \pi )\), where \( idx \) is a proper index in S.

  4. 4.

    atomicMin() is a built-in GPU function that compares its two arguments and assigns the minimum one to the first argument.

References

  1. Agarwal, P., Dutta, M.: New approach of Bellman Ford algorithm on GPU using compute unified design architecture (CUDA). Int. J. Comput. Appl. 110(13) (2015)

    Google Scholar 

  2. Amighi, A., Darabi, S., Blom, S., Huisman, M.: Specification and verification of atomic operations in GPGPU programs. In: SEFM, vol. 9276 (2015)

    Google Scholar 

  3. Bellman, R.: On a routing problem. Q. Appl. Math. 16, 87–90 (1958)

    Google Scholar 

  4. Bender, M.A., Fineman, J.T., Gilbert, S., Tarjan, R.E.: A new approach to incremental cycle detection and related problems. ACM Trans. Algorith. (TALG) 12(2), 1–22 (2015)

    MathSciNet  MATH  Google Scholar 

  5. Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA, pp. 113–132. ACM (2012)

    Google Scholar 

  6. Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102–110. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66845-1_7

    Chapter  Google Scholar 

  7. Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Sci. Comput. Prog. 95, 376–388 (2014)

    Article  Google Scholar 

  8. Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44898-5_4

    Chapter  Google Scholar 

  9. Busato, F., Bombieri, N.: An efficient implementation of the Bellman-Ford algorithm for Kepler GPU architectures. IEEE Trans. Parall. Distrib. Syst. 27(8), 2222–2233 (2016)

    Article  Google Scholar 

  10. Chen, R., Cohen, C., Lévy, J.J., Merz, S., Théry, L.: Formal proofs of Tarjan’s algorithm in Why3, Coq, and Isabelle. arXiv preprint arXiv:1810.11979 (2018)

  11. Collingbourne, P., Cadar, C., Kelly, P.H.J.: Symbolic testing of openCL code. In: Eder, K., Lourenço, J., Shehory, O. (eds.) HVC 2011. LNCS, vol. 7261, pp. 203–218. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34188-5_18

    Chapter  Google Scholar 

  12. The Coq proof assistant. https://coq.inria.fr/

  13. Dafny program verifier, https://www.microsoft.com/en-us/research/project/dafny-a-language-and-program-verifier-for-functional-correctness/

  14. Dijkstra, E.W.: A note on two problems in connexion with graphs. Numerische mathematik 1(1), 269–271 (1959)

    Article  MathSciNet  Google Scholar 

  15. Ford, L.R., Jr.: Network flow theory. Tech. rep, DTIC Document (1956)

    Google Scholar 

  16. Grov, G., Tumas, V.: Tactics for the Dafny program verifier. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 36–53. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49674-9_3

    Chapter  Google Scholar 

  17. 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. No. 141, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019)

    Google Scholar 

  18. Hajela, G., Pandey, M.: Parallel implementations for solving shortest path problem using Bellman-Ford. Int. J. Comput. Appl. 95(15) (2014)

    Google Scholar 

  19. Isabelle interactive theorem prover. http://isabelle.in.tum.de/index.html

  20. Jeong, I.K., Uddin, J., Kang, M., Kim, C.H., Kim, J.M.: Accelerating a Bellman-Ford routing algorithm using GPU. In: Frontier and Innovation in Future Computing and Communications, pp. 153–160. Springer (2014)

    Google Scholar 

  21. Kleinberg, J., Tardos, E.: Algorithm design. Pearson Education India, New Delh (2006)

    Google Scholar 

  22. Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 321–335. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24372-1_23

    Chapter  Google Scholar 

  23. Lammich, P., Neumann, R.: A Framework for Verifying Depth-First Search Algorithms. In: CPP, pp. 137–146. ACM (2015)

    Google Scholar 

  24. Lammich, P., Wimmer, S.: IMP2-simple program verification in Isabelle/HOL. Archive of Formal Proofs (2019)

    Google Scholar 

  25. Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: SIGSOFT FSE 2010, Santa Fe, pp. 187–196. ACM (2010)

    Google Scholar 

  26. Li, G., Li, P., Sawaya, G., Gopalakrishnan, G., Ghosh, I., Rajan, S.P.: GKLEE: concolic verification and test generation for GPUs. In: ACM SIGPLAN Notices. vol. 47, pp. 215–224. ACM (2012)

    Google Scholar 

  27. Oortwijn, W.: Deductive techniques for model-based concurrency verification. Ph.D. thesis, University of Twente, Netherlands (2019). https://doi.org/10.3990/1.9789036548984

  28. Oortwijn, W., Huisman, M., Joosten, S.J.C., van de Pol, J.: Automated verification of parallel nested DFS. In: TACAS 2020. LNCS, vol. 12078, pp. 247–265. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45190-5_14

    Chapter  Google Scholar 

  29. van de Pol, J.C.: Automated verification of nested DFS. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 181–197. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19458-5_12

  30. Raad, A., Hobor, A., Villard, J., Gardner, P.: Verifying concurrent graph algorithms. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 314–334. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_17

    Chapter  Google Scholar 

  31. Safari, M., Oortwijn, W., Huisman, M.: Artifact for automated verification of the parallel bellman-ford algorithm. In: SAS (2021). https://github.com/Safari1991/SSSP-Verification

  32. Safari, M., Ebnenasir, A.: Locality-based relaxation: an efficient method for GPU-based computation of shortest paths. In: Mousavi, M.R., Sgall, J. (eds.) TTCS 2017. LNCS, vol. 10608, pp. 43–58. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68953-1_5

    Chapter  Google Scholar 

  33. Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77–87 (2015)

    Google Scholar 

  34. Surve, G.G., Shah, M.A.: Parallel implementation of bellman-ford algorithm using CUDA architecture. In: 2017 International conference of Electronics, Communication and Aerospace Technology (ICECA), vol. 2, pp. 16–22. IEEE (2017)

    Google Scholar 

  35. Volkov, G., Mandrykin, M., Efremov, D.: Lemma functions for Frama-c: C programs as proofs. In: 2018 Ivannikov Ispras Open Conference (ISPRAS), pp. 31–38. IEEE (2018)

    Google Scholar 

  36. A Theory of Bellman-Ford, in Isabelle. https://www.isa-afp.org/browser_info/current/AFP/Monad_Memo_DP/Bellman_Ford.html. Accessed Jan 2021

  37. Why3 gallery of formally verified programs. http://toccata.lri.fr/gallery/graph.en.html

  38. Why3 program verifier. http://why3.lri.fr/

  39. Wimmer, S., Hu, S., Nipkow, T.: Verified memoization and dynamic programming. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 579–596. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94821-8_34

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Formal Methods and Tools, University of Twente, Enschede, The Netherlands

    Mohsen Safari & Marieke Huisman

  2. ESI (TNO), Eindhoven, The Netherlands

    Wytse Oortwijn

Authors
  1. Mohsen Safari
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wytse Oortwijn
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marieke Huisman .

Editor information

Editors and Affiliations

  1. Informal Systems, Inria, ENS, DI - Ecole Normale Supérieure, Paris, France

    Cezara Drăgoi

  2. Microsoft Corporation, Redmond, WA, USA

    Suvam Mukherjee

  3. Nokia Bell Labs, Murray Hill, NJ, USA

    Kedar Namjoshi

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Safari, M., Oortwijn, W., Huisman, M. (2021). Automated Verification of the Parallel Bellman–Ford Algorithm. In: Drăgoi, C., Mukherjee, S., Namjoshi, K. (eds) Static Analysis. SAS 2021. Lecture Notes in Computer Science(), vol 12913. Springer, Cham. https://doi.org/10.1007/978-3-030-88806-0_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-88806-0_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-88805-3

  • Online ISBN: 978-3-030-88806-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation