Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs

  • Conference paper
  • First Online:
Formal Methods (FM 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14000))

Included in the following conference series:

Abstract

We present VeyMont: a deductive verification tool that aims to make reasoning about functional correctness and deadlock freedom of parallel programs (relatively complex) as easy as that of sequential programs (relatively simple). The novelty of VeyMont is that it “inverts the workflow”: it supports a new method to parallelise verified programs, in contrast to existing methods to verify parallel programs. Inspired by methods for distributed systems, VeyMont targets coarse-grained parallelism among threads (i.e., whole-program parallelisation) instead of fine-grained parallelism among tasks (e.g., loop parallelisation).

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

References

  1. https://benchmarksgame-team.pages.debian.net/benchmarksgame/index.html

  2. Aiken, A., Nicolau, A.: Optimal loop parallelization. In: PLDI, pp. 308–317. ACM (1988)

    Google Scholar 

  3. Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett. 22(6), 307–309 (1986)

    Article  MathSciNet  Google Scholar 

  4. Apt, K.R., Olderog, E.-R.: Fifty years of Hoare’s logic. Formal Aspects Comput. 31(6), 751–807 (2019). https://doi.org/10.1007/s00165-019-00501-3

    Article  MathSciNet  MATH  Google Scholar 

  5. Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56–68 (2021)

    Article  Google Scholar 

  6. Berman, P., Garay, J.A., Perry, K.J.: Towards optimal distributed consensus (extended abstract). In: FOCS, pp. 410–415. IEEE Computer Society (1989)

    Google Scholar 

  7. Bloem, R., et al.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers, San Rafael (2015)

    Book  MATH  Google Scholar 

  8. Bloem, R., et al.: Decidability in parameterized verification. SIGACT News 47(2), 53–64 (2016)

    Article  MathSciNet  Google Scholar 

  9. 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 

  10. Blom, S., Darabi, S., Huisman, M., Safari, M.: Correct program parallelisations. Int. J. Softw. Tools Technol. Transf. 23(5), 741–763 (2021). https://doi.org/10.1007/s10009-020-00601-z

    Article  Google Scholar 

  11. Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_9

    Chapter  Google Scholar 

  12. Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259–270. ACM (2005)

    Google Scholar 

  13. Boulet, P., Darte, A., Silber, G.-A., Vivien, F.: Loop parallelization algorithms: from parallelism extraction to code generation. Parallel Comput. 24(3–4), 421–444 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  14. 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 

  15. Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1–3), 227–270 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  16. Burke, M., Cytron, R.: Interprocedural dependence analysis and parallelization. In: SIGPLAN Symposium on Compiler Construction, pp. 162–175. ACM (1986)

    Google Scholar 

  17. Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL, pp. 263–274. ACM (2013)

    Google Scholar 

  18. Carbone, M., Montesi, F., Schürmann, C.: Choreographies, logically. Distributed Comput. 31(1), 51–67 (2018)

    Article  MathSciNet  MATH  Google Scholar 

  19. Castro, D., Hu, R., Jongmans, S.S., Ng, N., Yoshida, N.: Distributed programming using role-parametric session types in Go: statically-typed endpoint APIs for dynamically-instantiated communication structures. PACMPL, 3(POPL), 29:1–29:30 (2019)

    Google Scholar 

  20. Din, C.C., Tapia Tarifa, S.L., Hähnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 217–233. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25423-4_14

    Chapter  Google Scholar 

  21. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  22. Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276–296. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_15

    Chapter  Google Scholar 

  23. Hobor, A., Gherghina, C.: Barriers in concurrent separation logic: now with tool support! Log. Methods Comput. Sci., 8(2) (2012)

    Google Scholar 

  24. Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM (2008)

    Google Scholar 

  25. Hu, R., Yoshida, N.: Hybrid session verification through endpoint API generation. In: Stevens, P., Wasowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 401–418. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_24

    Chapter  Google Scholar 

  26. Itai, A., Rodeh, M.: Symmetry breaking in distributive networks. In: FOCS, pp. 150–158. IEEE Computer Society (1981)

    Google Scholar 

  27. Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_4

    Chapter  Google Scholar 

  28. Jacobs, S., Reynolds, A.: TACAS 22 Artifact Evaluation VM - Ubuntu 20.04 LTS (2021). https://doi.org/10.5281/zenodo.5562597

  29. Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)

    Article  MATH  Google Scholar 

  30. Jongmans, S., van den Bos, P.: A predicate transformer for choreographies. In: ESOP 2022. LNCS, vol. 13240, pp. 520–547. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-99336-8_19

    Chapter  Google Scholar 

  31. Lamport, L.: The parallel execution of DO loops. Commun. ACM 17(2), 83–93 (1974)

    Article  MATH  Google Scholar 

  32. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)

    Article  Google Scholar 

  33. Lim, A.W., Lam, M.S.: Maximizing parallelism and minimizing synchronization with affine transforms. In: POPL, pp. 201–214. ACM Press (1997)

    Google Scholar 

  34. López, H.A., et al.: Protocol-based verification of message-passing parallel programs. In: OOPSLA, pp. 280–298. ACM (2015)

    Google Scholar 

  35. Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in F#. In: CC, pp. 128–138. ACM (2018)

    Google Scholar 

  36. Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC, pp. 98–108. ACM (2017)

    Google Scholar 

  37. Ng, N., Yoshida, N.: Pabble: parameterised scribble. Serv. Oriented Comput. Appl. 9(3–4), 269–284 (2015)

    Article  Google Scholar 

  38. Oancea, C.E., Rauchwerger, L.: Logical inference techniques for loop parallelization. In PLDI, pp. 509–520. ACM (2012)

    Google Scholar 

  39. O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  40. O’Hearn, P.: Separation logic. Commun. ACM 62(2), 86–95 (2019)

    Article  Google Scholar 

  41. Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319–340 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  42. Owicki, S.S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  43. Peleg, D.: Time-optimal leader election in general networks. J. Parallel Distrib. Comput. 8(1), 96–99 (1990)

    Article  Google Scholar 

  44. Raza, M., Calcagno, C., Gardner, P.: Automatic parallelization with separation logic. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 348–362. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00590-9_25

    Chapter  Google Scholar 

  45. Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55–74. IEEE Computer Society (2002)

    Google Scholar 

  46. Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: ECOOP, volume 74 of LIPIcs, pp. 24:1–24:31. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2017)

    Google Scholar 

  47. Skeen, D.: Nonblocking commit protocols. In: SIGMOD Conference, pp. 133–142. ACM Press (1981)

    Google Scholar 

  48. Suzuki, I.: Proving properties of a ring of finite-state machines. Inf. Process. Lett. 28(4), 213–214 (1988)

    Article  MathSciNet  MATH  Google Scholar 

  49. Tournavitis, G., Wang, Z., Franke, B., O’Boyle, M.F.: Towards a holistic approach to auto-parallelization: integrating profile-driven parallelism detection and machine-learning based mapping. In: PLDI, pp. 177–187. ACM (2009)

    Google Scholar 

  50. VerCors Wiki. https://github.com/utwente-fmt/vercors/wiki

  51. VeyMont Artifact. https://doi.org/10.5281/zenodo.7410640

  52. Wolf, F.A., Arquint, L., Clochard, M., Oortwijn, W., Pereira, J.C., Müller, P.: Gobra: modular specification and verification of Go programs. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 367–379. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81685-8_17

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Petra van den Bos

  2. Department of Computer Science, Open University, Heerlen, The Netherlands

    Sung-Shik Jongmans

  3. CWI, Amsterdam, The Netherlands

    Sung-Shik Jongmans

Authors
  1. Petra van den Bos
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sung-Shik Jongmans
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Petra van den Bos .

Editor information

Editors and Affiliations

  1. University of Toronto, Toronto, ON, Canada

    Marsha Chechik

  2. RWTH Aachen University, Aachen, Germany

    Joost-Pieter Katoen

  3. University of Lübeck, Lübeck, Germany

    Martin Leucker

A Appendix: Parallelisation of Tic-Tac-Toe

A Appendix: Parallelisation of Tic-Tac-Toe

The following listing shows the two threads for top-level fields p1 and p2 in the parallelisation of the sequential-ish program in Fig. 4, generated by VeyMont (functionally correct and deadlock-free). We note that p1Thread and p2Thread have “opposite” behaviour in their methods turn1 and turn2.

figure bh

The remaining classes that are part of the parallelisation are:

  • ParProgram: This class is responsible for creating channels and starting the threads. It is very similar to class ParProgram in Fig. 3b

  • Player, Move: These classes are straightforward Java versions of the \(\upmu \)PVL versions in Fig. 4.

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

van den Bos, P., Jongmans, SS. (2023). VeyMont: Parallelising Verified Programs Instead of Verifying Parallel Programs. In: Chechik, M., Katoen, JP., Leucker, M. (eds) Formal Methods. FM 2023. Lecture Notes in Computer Science, vol 14000. Springer, Cham. https://doi.org/10.1007/978-3-031-27481-7_19

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-27481-7_19

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-27480-0

  • Online ISBN: 978-3-031-27481-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation