×

zbMATH — the first resource for mathematics

Mechanising a type-safe model of multithreaded Java with a verified compiler. (English) Zbl 1451.68178
Summary: This article presents JinjaThreads, a unified, type-safe model of multithreaded Java source code and bytecode formalised in the proof assistant Isabelle/HOL. The semantics strictly separates sequential aspects from multithreading features like locks, forks and joins, interrupts, and the wait-notify mechanism. This separation yields an interleaving framework and a notion of deadlocks that are independent of the language, and makes the type safety proofs modular. JinjaThreads’s non-optimising compiler translates source code into bytecode. Its correctness proof guarantees that the generated bytecode exhibits exactly the same observable behaviours as the source code, even for infinite executions and under the Java memory model. The semantics and the compiler are executable. JinjaThreads builds on and reuses the Java formalisations Jinja, Bali, \(\mu\)Java, and Java\(^{\ell\mathit{ight}}\) by Nipkow’s group. Being the result of more than fifteen years of studying Java in Isabelle/HOL, it constitutes a large and long-lasting case study. It shows that fairly standard formalisation techniques scale well and highlights the challenges, benefits, and drawbacks of formalisation reuse.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N15 Theory of programming languages
68N20 Theory of compilers and interpreters
68Q55 Semantics in the theory of computing
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aceto, L; Glabbeek, RJ; Fokkink, W; Ingólfsdóttir, A, Axiomatizing prefix iteration with silent steps, Inf. Comput., 127, 26-40, (1996) · Zbl 0855.68030
[2] Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java, LNCS, vol. 1523. Springer (1999). https://doi.org/10.1007/3-540-48737-9 · Zbl 0938.68559
[3] Backes, M., Busenius, A., Hriţcu, C.: On the development and formalization of an extensible code generator for real life security protocols. In: Goodloe, A.E., Person, S. (eds.) NFM 2012, LNCS, vol. 7226, pp. 371-387. Springer (2012). https://doi.org/10.1007/978-3-642-28891-3_34
[4] Ballarin, C, Locales: a module system for mathematical theories, J. Autom. Reason., 52, 123-153, (2014) · Zbl 1315.68218
[5] Barthe, G., Crégut, P., Grégoire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de Boer, F., Bonsangue, M., Graf, S., de Roever, W.P. (eds.) Formal Methods for Components and Objects, LNCS, vol. 5382, pp. 1-24. Springer (2008). https://doi.org/10.1007/978-3-540-92188-2_1
[6] Batty, M., Memarian, K., Nienhuis, K., Pichon-Pharabod, J., Sewell, P.: The problem of programming language concurrency semantics. In: Vitek, J. (ed.) ESOP 2015, LNCS, vol. 9032, pp. 283-307. Springer (2015). https://doi.org/10.1007/978-3-662-46669-8_12
[7] Belblidia, N; Debbabi, M, A dynamic operational semantics for JVML, J. Object Technol., 6, 71-100, (2007)
[8] Berghofer, S., Strecker, M.: Extracting a formally verified, fully executable compiler from a proof assistant. In: COCV 2003, ENTCS, vol. 82(2), pp. 377-394 (2003). https://doi.org/10.1016/S1571-0661(05)82598-8
[9] Bergstra, J.A., Klop, J.W., Olderog, E.R.: Failures without chaos: a new process semantics for fair abstraction. In: Formal Description of Programming Concepts III (IFIP 1987), pp. 77-103. Elsevier Science Publishing (1987)
[10] Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010, LNCS, vol. 6172, pp. 131-146. Springer (2010). https://doi.org/10.1007/978-3-642-14052-5_11 · Zbl 1291.68326
[11] Bogdănaş, D., Roşu, G.: K-Java: A complete semantics of Java. In: POPL 2015, pp. 445-456. ACM (2015). https://doi.org/10.1145/2676726.2676982 · Zbl 1281.68072
[12] Breitner, J., Graf, J., Hecker, M., Mohr, M., Snelting, G.: On improvements of low-deterministic security. In: Piessens, F., Viganò, L. (eds.) POST 2016, LNCS, vol. 9635, pp. 68-88. Springer, Berlin (2016). https://doi.org/10.1007/978-3-662-49635-0_4
[13] Connected limited device configuration (CLDC) specification 1.1. http://jcp.org/aboutJava/communityprocess/final/jsr139/index.html
[14] Czarnik, P., Schubert, A.: Extending operational semantics of the Java bytecode. In: Barthe, G., Fournet, C. (eds.) TGC 2008, LNCS, vol. 4912, pp. 57-72. Springer (2008)
[15] Dave, MA, Compiler verification: a bibliography, SIGSOFT Softw. Eng. Notes, 28, 2-2, (2003)
[16] Drossopoulou, S., Eisenbach, S.: Describing the semantics of Java and proving type soundness. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java, LNCS, vol. 1523, pp. 542-542. Springer (1999). https://doi.org/10.1007/3-540-48737-9_2
[17] Farzan, A., Chen, F., Meseguer, J., Roşu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D. (eds.) CAV 2004, LNCS, vol. 3114, pp. 501-505. Springer (2004). https://doi.org/10.1007/978-3-540-27813-9_46 · Zbl 1103.68611
[18] Farzan, A., Meseguer, J., Roşu, G.: Formal JVM code analysis in Java FAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004, LNCS, vol. 3116, pp. 132-147. Springer (2004). https://doi.org/10.1007/978-3-540-27815-3_14 · Zbl 1214.68188
[19] Flanagan, C; Freund, SN; Lifshin, M; Qadeer, S, Types for atomicity: static checking and inference for Java, ACM Trans. Program. Lang. Syst., 30, 1-53, (2008)
[20] Giffhorn, D.: Slicing of concurrent programs and its application to information flow control. Ph.D. thesis, Fakultät für Informatik, Karlsruher Institut für Technologie (2012)
[21] Gosling, J., Joy, B., Steele, G., Bracha, G., Buckley, A.: The Java Language Specification: Java SE 8 Edition. Oracle America, Inc. (2015)
[22] Goto, M., Jagadeesan, R., Pitcher, C., Riely, J.: Types for relaxed memory models. In: TLDI 2012, pp. 25-38. ACM (2012). https://doi.org/10.1145/2103786.2103791
[23] Grossman, D.: Type-safe multithreading in Cyclone. In: TLDI 2003, pp. 13-25. ACM (2003). https://doi.org/10.1145/604174.604177
[24] Hartel, PH; Moreau, L, Formalizing the safety of Java, the Java virtual machine, and Java card, ACM Comput. Surv., 33, 517-558, (2001)
[25] Huisman, M., Petri, G.: BicolanoMT: a formalization of multi-threaded Java at bytecode level. In: BYTECODE 2008, Electronic Notes in Theoretical Computer Science (2008)
[26] Java platform, standard edition 8 API specification (2014). http://docs.oracle.com/javase/8/docs/api/
[27] Kildall, G.A.: A unified approach to global program optimization. In: POPL 1973, pp. 194-206. ACM (1973). https://doi.org/10.1145/512927.512945 · Zbl 0309.68020
[28] Klein, G.: Verified Java bytecode verification. Ph.D. thesis, Institut für Informatik, Technische Universität München (2003)
[29] Klein, G; Nipkow, T, Verified lightweight bytecode verification, Concurr. Comput. Pract. Exp., 13, 1133-1151, (2001) · Zbl 0997.68018
[30] Klein, G; Nipkow, T, Verified bytecode verifiers, Theor. Comput. Sci., 298, 583-626, (2002) · Zbl 1038.68109
[31] Klein, G., Nipkow, T.: Jinja is not Java. In: Klein, G., Nipkow, T., Paulson, L.C. (eds.) The Archive of Formal Proofs. http://www.isa-afp.org/entries/Jinja.shtml (2005). Formal proof development. Accessed 31 Jan 2018
[32] Klein, G; Nipkow, T, A machine-checked model for a Java-like language, virtual machine and compiler, ACM Trans. Program. Lang. Syst., 28, 619-695, (2006)
[33] Klein, G., Nipkow, T., von Oheimb, D., Nieto, L.P., Schirmer, N., Strecker, M.: Java source and bytecode formalizations in Isabelle: Bali. Isabelle sources in Isabelle/HOL/Bali (2002)
[34] Klein, G; Strecker, M, Verified bytecode verification and type-certifying compilation, J. Log. Algebraic Program., 58, 27-60, (2004) · Zbl 1067.68039
[35] Klein, G; Wildmoser, M, Verified bytecode subroutines, J. Autom. Reason., 30, 363-398, (2003) · Zbl 1031.68040
[36] Krebbers, R.: The C standard formalized in Coq. Ph.D. thesis, Radboud University Nijmegen (2015)
[37] Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: POPL 2014, pp. 179-191. ACM, New York (2014). https://doi.org/10.1145/2535838.2535841 · Zbl 1284.68405
[38] Lamport, L, How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Trans. Comput., 28, 690-691, (1979) · Zbl 0419.68045
[39] Leroy, X.: Formal certification of a compiler backend or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42-54. ACM (2006). https://doi.org/10.1145/1111037.1111042 · Zbl 1369.68124
[40] Leroy, X, A formally verified compiler back-end, J. Autom. Reason., 43, 363-446, (2009) · Zbl 1185.68215
[41] Leroy, X; Blazy, S, Formal verification of a C-like memory model and its uses for verifying program transformations, J. Autom. Reason., 41, 1-31, (2008) · Zbl 1154.68039
[42] Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)
[43] Liu, H., Moore, J.S.: Executable JVM model for analytical reasoning: a study. In: IVME 2003, pp. 15-23. ACM (2003). https://doi.org/10.1145/858570.858572
[44] Liu, H., Moore, J.S.: Java program verification via a JVM deep embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) TPHOLs 2004, LNCS, vol. 3223, pp. 117-125. Springer (2004). https://doi.org/10.1007/978-3-540-30142-4_14 · Zbl 1099.68731
[45] Lochbihler, A.: Jinja with threads. In: Klein, G., Nipkow, T., Paulson, L.C. (eds.) The Archive of Formal Proofs. http://www.isa-afp.org/entries/JinjaThreads.shtml (2007). Formal proof development
[46] Lochbihler, A.: Type safe nondeterminism—a formal semantics of Java threads. In: Proceedings of the 2008 International Workshop on Foundations of Object-Oriented Languages (FOOL 2008) (2008)
[47] Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010, LNCS, vol. 6012, pp. 427-447. Springer (2010). https://doi.org/10.1007/978-3-642-11957-6_23 · Zbl 1260.68080
[48] Lochbihler, A.: Java and the Java memory model-a unified, machine-checked formalisation. In: Seidl, H. (ed.) ESOP 2012, LNCS, vol. 7211, pp. 497-517. Springer (2012) · Zbl 1352.68034
[49] Lochbihler, A.: A machine-checked, type-safe model of Java concurrency: language, virtual machine, memory model, and verified compiler. Ph.D. thesis, Karlsruher Institut für Technologie, Fakultät für Informatik (2012). https://doi.org/10.5445/KSP/1000028867 · Zbl 1352.68034
[50] Lochbihler, A, Making the Java memory model safe, ACM Trans. Program. Lang. Syst., 35, 12:1-12:65, (2014)
[51] Lochbihler, A., Bulwahn, L.: Animating the formalised semantics of a Java-like language. In: van Eekelen, M., Geuvers, H., Schmalz, J., Wiedijk, F. (eds.) ITP 2011, LNCS, vol. 6898, pp. 216-232. Springer (2011). https://doi.org/10.1007/978-3-642-22863-6_17 · Zbl 1342.68294
[52] McLean, J, A general theory of composition for a class of “possibilistic” properties, IEEE Trans. Softw. Eng., 22, 53-67, (1996)
[53] Milner, R.: A modal characterisation of observable machine-behaviour. In: Astesiano, E., Böhm, C. (eds.) CAAP 1981, LNCS, vol. 112, pp. 25-34. Springer (1981). https://doi.org/10.1007/3-540-10828-9_52 · Zbl 0474.68074
[54] Milner, R.: Communication and Concurrency. Prentice Hall, New York (1989) · Zbl 0683.68008
[55] Mobius consortium. Deliverable D3.1. Byte code level specification language and program logic (2006)
[56] Moore, JS; Porter, G, The apprentice challenge, ACM Trans. Program. Lang. Syst., 24, 193-216, (2002)
[57] Moser, G., Schaper, M.: From Jinja bytecode to term rewriting: a complexity reflecting transformation. Inf. Comput. (to appear). http://cbr.uibk.ac.at/publications/ic16.pdf · Zbl 1395.68160
[58] Nipkow, T.: Verified bytecode verifiers. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001, LNCS, vol. 2030, pp. 347-363. Springer (2001). https://doi.org/10.1007/3-540-45315-6_23 · Zbl 0978.68512
[59] Nipkow, T., von Oheimb, D.: Java\(_{{ℓ }ight}\) is type-safe—definitely. In: POPL 1998, pp. 161-170. ACM (1998). https://doi.org/10.1145/268946.268960 · Zbl 0997.68018
[60] Nipkow, T., von Oheimb, D., Pusch, C.: \(μ \)Java: embedding a programming language in a theorem prover. In: Bauer, F.L., Steinbrüggen, R. (eds.) Foundations of Secure Computation, NATO Science Series F: Computer and Systems Sciences, vol. 175, pp. 117-144. IOS Press (2000) · Zbl 0995.68019
[61] Norrish, M.: A formal semantics for C++. Tech. rep., NICTA (2008). Available from http://nicta.com.au/people/norrishm/attachments/bibliographies_and_papers/C-TR.pdf
[62] Oheimb, D.v.: Analyzing Java in Isabelle/HOL. formalization, type safety and hoare logic. Ph.D. thesis, Fakultät für Informatik, Technische Universität München (2000). http://tumb1.biblio.tu-muenchen.de/publ/diss/in/2001/oheimb.html
[63] Oheimb, D.v.: Hoare logic for Java in Isabelle/HOL. Concurr. Comput. Pract. Exp. 13(13), 1173-1214 (2001). · Zbl 0997.68019
[64] Oheimb, D.v., Nipkow, T.: Machine-checking the Java specification: proving type-safety. In: Alves-Foss, J. (ed.) Formal Syntax and Semantics of Java, LNCS, vol. 1523, pp. 119-156. Springer (1999)
[65] Oheimb, D.v., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In: Eriksson, L.H., Lindsay, P. (eds.) FME 2002, LNCS, vol. 2391, pp. 89-105. Springer (2002). https://doi.org/10.1007/3-540-45614-7_6 · Zbl 1064.68543
[66] Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016, LNCS, vol. 9632, pp. 589-615. Springer (2016). https://doi.org/10.1007/978-3-662-49498-1_23
[67] Pusch, C.: Proving the soundness of a Java bytecode verifier specification in Isabelle/HOL. In: Cleaveland, R. (ed.) TACAS 1999, LNCS, vol. 1579, pp. 89-103. Springer (1999). https://doi.org/10.1007/3-540-49059-0_7
[68] Quis custodiet—machine-checked software security analyses. https://pp.info.uni-karlsruhe.de/projects/quis-custodiet/
[69] Ramananandro, T., Dos Reis, G., Leroy, X.: Formal verification of object layout for C++ multiple inheritance. In: POPL 2011, pp. 67-80. ACM (2011). https://doi.org/10.1145/1926385.1926395 · Zbl 1284.68197
[70] Rittri, M.: Proving the correctness of a virtual machine by a bisimulation. Licentiate thesis, Göteborg University (1988)
[71] Roşu, G; Şerbănuţă, TF, An overview of the K semantic framework, J. Log. Algebraic Program., 79, 397-434, (2010) · Zbl 1214.68188
[72] Rushby, J.: Formal methods and the certification of critical systems. Tech. Rep. SRI-CSL-93-7, Computer Science Laboratory, SRI International (1993). http://www.csl.sri.com/papers/csl-93-7/
[73] Sampson, J., Boehm, H., Otenko, O., Levart, P., Holmes, D., Haley, A., Buchholz, M., Lea, D., Davidovich, V., Terekhov, A., Diestelhorst, S.: Varieties of CAS semantics (another doc fix request). Thread the on concurrency-interest mailing list, first post at http://altair.cs.oswego.edu/pipermail/concurrency-interest/2015-January/013613.html (2015). Accessed 17 Oct 2017
[74] Schirmer, N.: Java definite assignment in Isabelle/HOL. In: Proceedings of ECOOP Workshop on Formal Techniques for Java-like Programs. Technical Report 408, ETH Zurich (2003)
[75] Schirmer, N, Analysing the Java package/access concepts in isabelle/HOL, Concurr. Comput. Pract. Exp-Form. Tech. Java Program., 16, 689-706, (2004)
[76] Schirmer, N.: A verification environment for sequential imperative programs in Isabelle/HOL. In: Baader, F., Voronkov, A. (eds.) LPAR 2004, Lecture Notes in Artificial Intelligence, vol. 3452, pp. 398-414. Springer (2005) · Zbl 1108.68410
[77] Schirmer, N.: Verification of sequential imperative programs in Isabelle/HOL. Ph.D. thesis, Technische Universität München (2006) · Zbl 1108.68410
[78] Ševčík, J; Vafeiadis, V; Zappa Nardelli, F; Jagannathan, S; Sewell, P, Compcerttso: a verified compiler for relaxed-memory concurrency, J. ACM, 60, 22:1-22:50, (2013) · Zbl 1281.68072
[79] Stärk, R., Schmid, J., Börger, E.: Java and the Java Virtual Machine. Springer, Berlin (2001) · Zbl 0978.68033
[80] Strecker, M.: Formal verification of a Java compiler in Isabelle. In: CADE 2002, LNCS, vol. 2392, pp. 63-77. Springer (2002) · Zbl 1072.68593
[81] Strecker, M.: Investigating type-certifying compilation with Isabelle. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002, LNCS, vol. 2514, pp. 403-417. Springer (2002). https://doi.org/10.1007/3-540-36078-6_27 · Zbl 1023.68521
[82] Tool-assisted specification and verification of javacard programmes: Verificard. http://cordis.europa.eu/project/rcn/53643_en.html
[83] Wagner, D., et al. (eds.): Ausgezeichnete Informatik. Dissertation (2003), LNI, vol. D-3. Köllen Verlag (2003)
[84] Wand, M.: Compiler correctness for parallel languages. In: FPCA 1995, pp. 120-134. ACM (1995) · Zbl 1315.68218
[85] Wasserrab, D.: From formal semantics to verified slicing—a modular framework with applications in language based security. Ph.D. thesis, Karlsruher Institut für Technologie, Fakultät für Informatik (2010)
[86] Wasserrab, D., Lohner, D.: Proving information flow noninterference by reusing a machine-checked correctness proof for slicing. In: 6th International Verification Workshop (VERIFY 2010), 2010
[87] Wright, AK; Felleisen, M, A syntactic approach to type soundness, Inf. Comput., 115, 38-94, (1994) · Zbl 0938.68559
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.