A type system for JVM threads. (English) Zbl 1019.68013
Summary: The current definition of the Java bytecode verifier, as well as the proposals to formalize it, does not include any check about the structured use of locks by monitorenter and monitorexit instructions. So code is run, even if critical sections are corrupted. In this paper, we isolate a sublanguage of the Java virtual machine with thread creation and mutual exclusion. For this subset, we define a semantics and a formal verifier that enforces basic properties of threads and lock and unlock operations. The verifier integrates well with previous formalizations of the Java bytecode verifier. Our analysis of structured use of locks reveals the presence of bugs in the current compilers from Sun, IBM and Microsoft.
MSC:
| 68N15 | Theory of programming languages |
Keywords:
Java virtual machineReferences:
| [1] | Arnold, K.; Gosling, J., The java Programming Language (1996), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0876.68015 |
| [2] | P. Bertelsen, Semantics of java byte code, Technical Report, Department of Information Technology, Technical University of Denmark, March 1997.; P. Bertelsen, Semantics of java byte code, Technical Report, Department of Information Technology, Technical University of Denmark, March 1997. |
| [3] | G. Bigliardi, C. Laneve, A type system for JVM threads, in: Third ACM SIGPLAN Workshop on Types in Compilation (TIC 2000), Montreal, September 2000.; G. Bigliardi, C. Laneve, A type system for JVM threads, in: Third ACM SIGPLAN Workshop on Types in Compilation (TIC 2000), Montreal, September 2000. |
| [4] | G. Bigliardi, C. Laneve, The java bytecode verifier with structured locking checks, Software and documentation available from www.cs.unibo.it/ laneve/html/software.html; G. Bigliardi, C. Laneve, The java bytecode verifier with structured locking checks, Software and documentation available from www.cs.unibo.it/ laneve/html/software.html |
| [5] | Börger, E.; Schulte, W., Defining the java Virtual Machine as Platform for Provably Correct java Compilation, (Brim, L.; Gruska, J.; Zlatuska, J., Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS’98, Brno, Czech Republic. Mathematical Foundations of Computer Science 1998, 23rd International Symposium, MFCS’98, Brno, Czech Republic, Lecture Notes in Computer Science, Vol. 1450 (August 1998), Springer: Springer Berlin) |
| [6] | S. Drossopoulou, S. Eisenbach, java is type safe—probably, in: ECOOP ’97—Object-Oriented Programming 11th European Conference, Jyväskylä, Finland, Lecture Notes in Computer Science, Vol. 1241, Springer-Verlag, Berlin, 1997, pp. 389-418.; S. Drossopoulou, S. Eisenbach, java is type safe—probably, in: ECOOP ’97—Object-Oriented Programming 11th European Conference, Jyväskylä, Finland, Lecture Notes in Computer Science, Vol. 1241, Springer-Verlag, Berlin, 1997, pp. 389-418. |
| [7] | S.N. Freund, J.C. Mitchell, A type system for object initialization in the java bytecode language, in: OOPSLA ’98 Conference Proceedings, ACM SIGPLAN Notices, Vol. 33, No. 10, 1998, pp. 310-328.; S.N. Freund, J.C. Mitchell, A type system for object initialization in the java bytecode language, in: OOPSLA ’98 Conference Proceedings, ACM SIGPLAN Notices, Vol. 33, No. 10, 1998, pp. 310-328. |
| [8] | S.N. Freund, J.C. Mitchell, A formal framework for the java bytecode language and verifier, in: Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications, 1999, pp. 147-166.; S.N. Freund, J.C. Mitchell, A formal framework for the java bytecode language and verifier, in: Proceedings of the Conference on Object-Oriented Programming, Systems, Languages, and Applications, 1999, pp. 147-166. |
| [9] | S.N. Freund, J.C. Mitchell, A type system for java bytecode subroutines and exceptions, Technical Report STAN-CS-TN-99-91, Stanford Computer Science Technical Note, August 1999.; S.N. Freund, J.C. Mitchell, A type system for java bytecode subroutines and exceptions, Technical Report STAN-CS-TN-99-91, Stanford Computer Science Technical Note, August 1999. |
| [10] | M. Hagiya, A. Tozawa, On a new method for dataflow analysis of java Virtual Machine subroutines, Lecture Notes in Computer Science, Vol. 1503, Springer, Berlin, 1998, pp. 17-32.; M. Hagiya, A. Tozawa, On a new method for dataflow analysis of java Virtual Machine subroutines, Lecture Notes in Computer Science, Vol. 1503, Springer, Berlin, 1998, pp. 17-32. |
| [11] | Lea, D., Concurrent Programming in java: Design Principles and Patterns, The java Series (1996), Addison-Wesley: Addison-Wesley Reading, MA |
| [12] | T. Lindholm, F. Yellin, The java Virtual Machine Specification, The java Series, Addison-Wesley, Longman, Inc., 2nd Edition, 1999.; T. Lindholm, F. Yellin, The java Virtual Machine Specification, The java Series, Addison-Wesley, Longman, Inc., 2nd Edition, 1999. |
| [13] | T. Nipkow, D. von Oheimb, \( javalight\); T. Nipkow, D. von Oheimb, \( javalight\) |
| [14] | R. O’Callahan, A simple, comprehensive type system for java bytecode subroutines, in: Conference Record of POPL’99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, 1999, pp. 70-78.; R. O’Callahan, A simple, comprehensive type system for java bytecode subroutines, in: Conference Record of POPL’99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, New York, 1999, pp. 70-78. |
| [15] | Z. Qian, Formal specification of a large subset of java virtual machine instructions for objects, methods and subroutines, in: Formal Syntax and Semantics of java, Lecture Notes in Computer Science, Springer-Verlag, Berlin Germany, 1998.; Z. Qian, Formal specification of a large subset of java virtual machine instructions for objects, methods and subroutines, in: Formal Syntax and Semantics of java, Lecture Notes in Computer Science, Springer-Verlag, Berlin Germany, 1998. |
| [16] | Z. Qian, A. Goldberg, A. Goglio, A formal specification of java class loading, Technical Report Kestrel Institute, Palo Alto, March 2000.; Z. Qian, A. Goldberg, A. Goglio, A formal specification of java class loading, Technical Report Kestrel Institute, Palo Alto, March 2000. |
| [17] | Stata, R.; Abadi, M., A type system for java bytecode subroutines, ACM Trans. Programming Languages Systems, 21, 1, 90-137 (1999) |
| [18] | D. Syme, Proving java type soundness, Technical Report No. 427, University of Cambridge Computer Laboratory, June 1997.; D. Syme, Proving java type soundness, Technical Report No. 427, University of Cambridge Computer Laboratory, June 1997. |
| [19] | P.M. Yelland, A compositional account of the java virtual machine, in: Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, 1999, pp. 57-69.; P.M. Yelland, A compositional account of the java virtual machine, in: Conference Record of POPL 99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, 1999, pp. 57-69. |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
