×

zbMATH — the first resource for mathematics

Verification of concurrent systems with VerCors. (English) Zbl 1445.68131
Bernardo, Marco (ed.) et al., Formal methods for executable software models. 14th international school on formal methods for the design of computer, communication, and software systems, SFM 2014, Bertinoro, Italy, June 16–20, 2014. Advanced lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8483, 172-216 (2014).
Summary: 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.
For the entire collection see [Zbl 1305.68021].
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[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) · Zbl 1453.68042
[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) · doi:10.1109/PDP.2014.31
[3] Apt, K.R.: Ten years of Hoare’s logic: A survey – Part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981) · Zbl 0471.68006 · doi:10.1145/357146.357150
[4] Artho, C., Havelund, K., Biere, A.: High-level data races. Softw. Test., Verif. Reliab. 13(4), 207–227 (2003) · Zbl 05446596 · doi:10.1002/stvr.281
[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) · Zbl 05431131 · doi:10.5381/jot.2004.3.6.a2
[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) · doi:10.1007/978-3-540-30569-9_3
[7] Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
[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) · Zbl 05189668 · doi:10.1007/11804192_6
[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) · doi:10.1145/2384616.2384625
[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) · Zbl 06400667 · doi:10.1007/978-3-319-06410-9_9
[11] Blom, S., Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs. Accepted to appear in Science of Computer Programming (2013)
[12] Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003) · Zbl 1067.68537 · doi:10.1007/3-540-44898-5_4
[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) · doi:10.1007/s10009-004-0167-4
[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) · Zbl 05189663 · doi:10.1007/11804192_16
[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) · Zbl 05618496 · doi:10.1007/978-3-642-03359-9_2
[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) · Zbl 05772655 · doi:10.1007/978-3-642-14295-6_42
[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) · Zbl 05930549 · doi:10.1007/978-3-642-20398-5_35
[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)
[19] Dietl, W., Müller, P.: Universes: Lightweight ownership for JML. Journal of Object Technology 4(8), 5–32 (2005) · Zbl 05431212 · doi:10.5381/jot.2005.4.8.a1
[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) · Zbl 06326004 · doi:10.1007/978-3-642-36946-9_11
[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) · doi:10.1145/1449764.1449782
[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) · Zbl 05301161 · doi:10.1007/978-3-540-70592-5_18
[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) · doi:10.1109/32.908957
[24] Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19–31 (1967) · Zbl 0189.50204 · doi:10.1090/psapm/019/0235771
[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) · Zbl 1137.68354 · doi:10.1007/978-3-540-76637-7_3
[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) · Zbl 05488153 · doi:10.1007/978-3-540-89330-1_13
[27] Haack, C., Huisman, M., Hurlin, C., Amighi, A.: Permission-based separation logic for Java. Submitted to Logical Methods in Computer Science · Zbl 1448.68215
[28] Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[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) · Zbl 1326.68096 · doi:10.1007/978-3-642-19718-5_15
[30] Huisman, M., Mihelčić, M.: Specification and verification of GPGPU programs using permission-based separation logic. In: BYTECODE 2013 (2013)
[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) · doi:10.1007/3-540-46428-X_15
[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) · doi:10.1109/SEFM.2005.39
[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) · Zbl 05930518 · doi:10.1007/978-3-642-20398-5_4
[34] Jason Sanders, E.K.: CUDA by Example: An Introduction to General-Purpose GPU Programming. Addison-Wesley Professional (2010)
[35] Khronos OpenCL Working Group. The OpenCL specification (2008-2013)
[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] 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)
[38] Leino, K.R.M.: This is Boogie 2. Technical report, Microsoft Research (June 2008)
[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) · Zbl 1253.68095 · doi:10.1007/978-3-642-17511-4_20
[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) · doi:10.1145/1882291.1882320
[41] Liskov, B., Guttag, J.: Abstraction and specification in program development. MIT Press, Cambridge (1986) · Zbl 0644.68001
[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) · doi:10.1007/978-3-540-73589-2_11
[43] Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall (1997) · Zbl 0987.68516
[44] Müller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253–286 (2006) · Zbl 1100.68539 · doi:10.1016/j.scico.2006.03.001
[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)
[46] O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoretical Computer Science 375(1-3), 271–307 (2007) · Zbl 1111.68023 · doi:10.1016/j.tcs.2006.12.035
[47] The OpenCL 1.2 specification (2011)
[48] Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informatica Journal 6, 319–340 (1975) · Zbl 0312.68011 · doi:10.1007/BF00268134
[49] Parkinson, M.: Local reasoning for Java. Technical Report UCAM-CL-TR-654, University of Cambridge (2005)
[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) · Zbl 1369.68151 · doi:10.1145/1040305.1040326
[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) · Zbl 1256.03036
[52] Parr, T.: The Definitive ANTLR 4 Reference. Pragmatic Bookshelf (2013)
[53] Poetzsch-Heffter, A.: Specification and Verification of Object-Oriented Programs. PhD thesis, Habilitation thesis, Technical University of Munich (1997)
[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) · Zbl 0970.68149 · doi:10.1007/978-94-017-0435-9_1
[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) · doi:10.1109/LICS.2002.1029817
[56] Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1) (2012) · Zbl 1204.68131 · doi:10.1145/2160910.2160911
[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) · doi:10.1145/1366230.1366276
[58] VerCors project homepage (2014), http://www.utwente.nl/vercors/
[59] Weiß, B.: Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. PhD thesis, Karlsruhe Institute of Technology (2011)
[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) · Zbl 06400629 · doi:10.1007/978-3-642-54804-8_16
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.