Advertisement

Verification of Concurrent Systems with VerCors

  • Afshin Amighi
  • Stefan Blom
  • Saeed Darabi
  • Marieke Huisman
  • Wojciech Mostowski
  • Marina Zaharieva-Stojanovski
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8483)

Abstract

This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separation logic to reason about multithreaded Java programs. We discuss in particular how we use the logic to use different implementations of synchronisers in verification, and how we reason about class invariance properties in a concurrent setting. Further, we also show how the approach is suited to reason about programs using a different concurrency paradigm, namely kernel programs using the Single Instruction Multiple Data paradigm. Concretely, we illustrate how permission-based separation logic is suitable to verify functional correctness properties of OpenCL kernels. All verification techniques discussed in this paper are supported by the VerCors tool set.

Keywords

Global Memory Concurrent Program Concurrent System Java Modeling Language Class Invariant 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Amighi, A., Blom, S., Huisman, M.: Resource protection using atomics: Patterns and verifications. Technical Report TR-CTIT-13-10, CTIT, University of Twente (2013)Google Scholar
  2. 2.
    Amighi, A., Blom, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Formal specifications for Java’s synchronisation classes. In: Lafuente, A.L., Tuosto, E. (eds.) 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, pp. 725–733. IEEE Computer Society (2014)Google Scholar
  3. 3.
    Apt, K.R.: Ten years of Hoare’s logic: A survey – Part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)CrossRefzbMATHGoogle Scholar
  4. 4.
    Artho, C., Havelund, K., Biere, A.: High-level data races. Softw. Test., Verif. Reliab. 13(4), 207–227 (2003)CrossRefGoogle Scholar
  5. 5.
    Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology 3(6), 27–56 (2004)CrossRefGoogle Scholar
  6. 6.
    Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)Google Scholar
  8. 8.
    Berdine, J., Calcagno, C., O’Hearn, P.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: A verifier for GPU kernels. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2012, pp. 113–132. ACM, New York (2012)CrossRefGoogle Scholar
  10. 10.
    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, Heidelberg (2014)CrossRefGoogle Scholar
  11. 11.
    Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Accepted to appear in Science of Computer Programming (2013)Google Scholar
  12. 12.
    Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  13. 13.
    Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Software Tools for Technology Transfer 7, 212–232 (2005)CrossRefGoogle Scholar
  14. 14.
    Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Cohen, E., Moskal, M., Schulte, W., Tobies, S.: Local verification of global invariants in concurrent programs. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 480–494. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  17. 17.
    Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  18. 18.
    Cowan, B., Kapralos, B.: GPU-based acoustical occlusion modeling with acoustical texture maps. In: Proceedings of the 6th Audio Mostly Conference: A Conference on Interaction with Sound, AM 2011, pp. 55–61. ACM, New York (2011)Google Scholar
  19. 19.
    Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology 4(8), 5–32 (2005)CrossRefGoogle Scholar
  20. 20.
    Dietl, W., Müller, P.: Object ownership in program verification. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. LNCS, vol. 7850, pp. 289–318. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  21. 21.
    DiStefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 213–226. ACM (2008)Google Scholar
  22. 22.
    Drossopoulou, S., Francalanza, A., Müller, P., Summers, A.J.: A unified framework for verification techniques for object invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 412–437. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Transactions on Software Engineering 27(2), 99–123 (2001)CrossRefGoogle Scholar
  24. 24.
    Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19–31 (1967)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    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)CrossRefGoogle Scholar
  26. 26.
    Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java’s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 171–187. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  27. 27.
    Haack, C., Huisman, M., Hurlin, C., Amighi, A.: Permission-based separation logic for Java. Submitted to Logical Methods in Computer ScienceGoogle Scholar
  28. 28.
    Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)CrossRefzbMATHGoogle Scholar
  29. 29.
    Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276–296. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  30. 30.
    Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs using permission-based separation logic. In: BYTECODE 2013 (2013)Google Scholar
  31. 31.
    Huizing, K., Kuiper, R.: Verification of object oriented programs using class invariants. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 208–221. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  32. 32.
    Jacobs, B., Piessens, F., Leino, K.R.M., Schulte, W.: Safe concurrency for aggregate objects with invariants. In: Software Engineering and Formal Methods, pp. 137–147 (2005)Google Scholar
  33. 33.
    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)CrossRefGoogle Scholar
  34. 34.
    Jason Sanders, E.K.: CUDA by Example: An Introduction to General-Purpose GPU Programming. Addison-Wesley Professional (2010)Google Scholar
  35. 35.
    Khronos OpenCL Working Group. The OpenCL specification (2008-2013)Google Scholar
  36. 36.
    Leavens, G., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., Müller, P., Kiniry, J., Chalin, P.: JML Reference Manual. Dept. of Computer Science, Iowa State University (February 2007), http://www.jmlspecs.org
  37. 37.
    Leino, K., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2009. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009)Google Scholar
  38. 38.
    Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (June 2008)Google Scholar
  39. 39.
    Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  40. 40.
    Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: SIGSOFT FSE 2010, Santa Fe, NM, USA, pp. 187–196. ACM (2010)Google Scholar
  41. 41.
    Liskov, B., Guttag, J.: Abstraction and specification in program development. MIT Press, Cambridge (1986)zbMATHGoogle Scholar
  42. 42.
    Lu, Y., Potter, J., Xue, J.: Validity invariants and effects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 202–226. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  43. 43.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall (1997)Google Scholar
  44. 44.
    Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253–286 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  45. 45.
    Mulligan, J.B.: A GPU-accelerated software eye tracking system. In: Proceedings of the Symposium on Eye Tracking Research and Applications, ETRA 2012, pp. 265–268. ACM, New York (2012)Google Scholar
  46. 46.
    O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  47. 47.
    The OpenCL 1.2 specification (2011)Google Scholar
  48. 48.
    Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica Journal 6, 319–340 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  49. 49.
    Parkinson, M.: Local reasoning for Java. Technical Report UCAM-CL-TR-654, University of Cambridge (2005)Google Scholar
  50. 50.
    Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 247–258. ACM (2005)Google Scholar
  51. 51.
    Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Logical Methods in Computer Science 8(3:01), 1–54 (2012)MathSciNetzbMATHGoogle Scholar
  52. 52.
    Parr, T.: The Definitive ANTLR 4 Reference. Pragmatic Bookshelf (2013)Google Scholar
  53. 53.
    Poetzsch-Heffter, A.: Specification and Verification of Object-Oriented Programs. PhD thesis, Habilitation thesis, Technical University of Munich (1997)Google Scholar
  54. 54.
    Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, vol. II.1, pp. 13–39. Kluwer (1998)Google Scholar
  55. 55.
    Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74. IEEE Computer Society (2002)Google Scholar
  56. 56.
    Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1) (2012)Google Scholar
  57. 57.
    Stone, S.S., Haldar, J.P., Tsao, S.C., Hwu, W.-M.W., Liang, Z.-P., Sutton, B.P.: Accelerating advanced MRI reconstructions on GPU-s. In: Proceedings of the 5th Conference on Computing Frontiers, CF 2008, pp. 261–272. ACM, New York (2008)CrossRefGoogle Scholar
  58. 58.
    VerCors project homepage (2014), http://www.utwente.nl/vercors/
  59. 59.
    Weiß, B.: Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. PhD thesis, Karlsruhe Institute of Technology (2011)Google Scholar
  60. 60.
    Zaharieva-Stojanovski, M., Huisman, M.: Verifying class invariants in concurrent programs. In: Gnesi, S., Rensink, A. (eds.) FASE 2014 (ETAPS). LNCS, vol. 8411, pp. 230–245. Springer, Heidelberg (2014)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Afshin Amighi
    • 1
  • Stefan Blom
    • 1
  • Saeed Darabi
    • 1
  • Marieke Huisman
    • 1
  • Wojciech Mostowski
    • 1
  • Marina Zaharieva-Stojanovski
    • 1
  1. 1.University of TwenteThe Netherlands

Personalised recommendations