Advertisement

An Abstraction Technique for Describing Concurrent Program Behaviour

  • Wytse Oortwijn
  • Stefan Blom
  • Dilian Gurov
  • Marieke HuismanEmail author
  • Marina Zaharieva-Stojanovski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.

Notes

Acknowledgements

This work is partially supported by the ERC grant 258405 for the VerCors project and by the NWO TOP 612.001.403 project VerDi.

References

  1. 1.
    Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1), 1–66 (2015)MathSciNetzbMATHGoogle Scholar
  2. 2.
    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 CrossRefGoogle Scholar
  3. 3.
    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 CrossRefGoogle Scholar
  4. 4.
    Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84–98. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-22969-0_6 CrossRefGoogle Scholar
  5. 5.
    Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)Google Scholar
  6. 6.
    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 CrossRefGoogle Scholar
  7. 7.
    da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207–231. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44202-9_9 Google Scholar
  8. 8.
    da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: Steps in modular specifications for concurrent modules. In: MFPS, EPTCS, pp. 3–18 (2015).  https://doi.org/10.1016/j.entcs.2015.12.002
  9. 9.
    Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14107-2_24 CrossRefGoogle Scholar
  10. 10.
    Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 363–377. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00590-9_26 CrossRefGoogle Scholar
  11. 11.
    Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19–37. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-76637-7_3 CrossRefGoogle Scholar
  12. 12.
    Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)zbMATHGoogle Scholar
  13. 13.
    Groote, J.F., Ponse, A.: The syntax and semantics of \(\mu \)CRL. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds.) Algebra of Communicating Processes, pp. 26–62. Springer, London (1995).  https://doi.org/10.1007/978-1-4471-2120-6_2 CrossRefGoogle Scholar
  14. 14.
    Honda, K., Marques, E.R.B., Martins, F., Ng, N., Vasconcelos, V.T., Yoshida, N.: Verification of MPI programs using session types. In: Träff, J.L., Benkner, S., Dongarra, J.J. (eds.) EuroMPI 2012. LNCS, vol. 7490, pp. 291–293. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33518-1_37 CrossRefGoogle Scholar
  15. 15.
    Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM (2008)Google Scholar
  16. 16.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)CrossRefzbMATHGoogle Scholar
  17. 17.
    Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: POPL, pp. 637–650. ACM (2015)Google Scholar
  18. 18.
    Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 696–723. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54434-1_26 CrossRefGoogle Scholar
  19. 19.
    O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoret. Comput. Sci. 375(1–3), 271–307 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Pang, J., van de Pol, J., Espada, M.: Abstraction of parallel uniform processes with data. In: SEFM, pp. 14–23. IEEE (2004)Google Scholar
  21. 21.
    Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 237–251. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_17 CrossRefGoogle Scholar
  22. 22.
    Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science, pp. 55–74. IEEE Computer Society (2002).  https://doi.org/10.1109/LICS.2002.1029817
  23. 23.
    Sergey, I., Nanevski, A., Banerjee, A.: Mechanized verification of fine-grained concurrent programs. In: PLDI, pp. 77–87. ACM (2015)Google Scholar
  24. 24.
    Sergey, I., Nanevski, A., Banerjee, A.: Specifying and verifying concurrent algorithms with histories and subjectivity. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 333–358. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46669-8_14 CrossRefGoogle Scholar
  25. 25.
    Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 149–168. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54833-8_9 CrossRefGoogle Scholar
  26. 26.
    Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377–390 (2013)Google Scholar
  27. 27.
    Zaharieva-Stojanovski, M.: Closer to reliable software: verifying functional behaviour of concurrent programs. Ph.D. thesis, University of Twente (2015).  https://doi.org/10.3990/1.9789036539241

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Wytse Oortwijn
    • 1
  • Stefan Blom
    • 1
  • Dilian Gurov
    • 2
  • Marieke Huisman
    • 1
    Email author
  • Marina Zaharieva-Stojanovski
    • 1
  1. 1.University of TwenteEnschedeThe Netherlands
  2. 2.KTH Royal Institute of TechnologyStockholmSweden

Personalised recommendations