Abstract
A verified compiler is an integral part of every security infrastructure. Previous work has come up with formal semantics for sequential and concurrent variants of Java and has proven the correctness of compilers for the sequential part. This paper presents a rigorous formalisation (in the proof assistant Isabelle/HOL) of concurrent Java source and byte code together with an executable compiler and its correctness proof. It guarantees that the generated byte code shows exactly the same observable behaviour as the semantics for the multithreaded source code.
This work is partially supported by DFG grant Sn 11/10-1.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Aceto, L., van Glabbeek, R.J., Fokkink, W., Ingólfsdóttir, A.: Axiomatizing prefix iteration with silent steps. Information and Computation 127(1), 26–40 (1996)
Alves-Foss, J. (ed.): Formal Syntax and Semantics of Java. LNCS, vol. 1523. Springer, Heidelberg (1999)
Aspinall, D., Ševčík, J.: Formalising Java’s data-race-free guarantee. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 22–37. Springer, Heidelberg (2007)
Belblidia, N., Debbabi, M.: A dynamic operational semantics for JVML. Journal of Object Technology 6(3), 71–100 (2007)
Bergstra, J.A., Klop, J.W., Olderog, E.R.: Failures without chaos: a new process semantics for fair abstraction. In: IFIP 1987, Formal Description of Programming Concepts III, pp. 77–103. Elsevier Science Publishing, Amsterdam (1987)
Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Software Engineering Notes 28(6), 2 (2003)
Flanagan, C., Freund, S.N., Lifshin, M., Qadeer, S.: Types for atomicity: Static checking and inference for Java. ACM TOPLAS 30(4), 1–53 (2008)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 3rd edn. Addison-Wesley, Reading (2005)
Hammer, C., Snelting, G.: Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs. International Journal of Information Security 8(6), 399–422 (2009)
Huisman, M., Petri, G.: BicolanoMT: a formalization of multi-threaded Java at bytecode level. In: BYTECODE 2008. ENTCS (2008)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS 28, 619–695 (2006)
Leinenbach, D.: Compiler Verification in the Context of Pervasive System Verification. PhD thesis, Saarland University (2008)
Leroy, X.: Formal certification of a compiler backend or: Programming a compiler with a proof assistant. In: POPL 2006, pp. 42–54. ACM, New York (2006)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363–446 (2009)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, Second Edition. Addison-Wesley, Reading (1999)
Liu, H., Moore, J.S.: Executable JVM Model for Analytical Reasoning: A Study. In: IVME 2003, pp. 15–23 (2003)
Lochbihler, A.: Type safe nondeterminism - a formal semantics of Java threads. In: FOOL 2008 (2008)
Lochbihler, A.: Jinja with threads. In: The Archive of Formal Proofs (2009), http://afp.sf.net/devel-entries/JinjaThreads.shtml (Formal proof development)
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, Heidelberg (1981)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Nipkow, T. (ed.): Special Issue on Java Bytecode Verification. Journal of Automated Reasoning, vol. 30(3-4). Springer, Heidelberg (2003)
Nipkow, T., Paulson, L.C., Wenzel, M.T. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Rittri, M.: Proving the correctness of a virtual machine by a bisimulation. Licentiate thesis, Göteborg University (1988)
Ševčík, J., Aspinall, D.: On validity of program transformations in the Java memory model. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 27–51. Springer, Heidelberg (2008)
Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine. Springer, Heidelberg (2001)
Wand, M.: Compiler correctness for parallel languages. In: FPCA 1995, pp. 120–134. ACM, New York (1995)
Wasserrab, D., Lohner, D., Snelting, G.: On PDG-based noninterference and its modular proof. In: PLAS 2009, pp. 31–44. ACM, New York (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lochbihler, A. (2010). Verifying a Compiler for Java Threads. In: Gordon, A.D. (eds) Programming Languages and Systems. ESOP 2010. Lecture Notes in Computer Science, vol 6012. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11957-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-11957-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11956-9
Online ISBN: 978-3-642-11957-6
eBook Packages: Computer ScienceComputer Science (R0)