Formalising Java RMI with explicit code mobility. (English) Zbl 1132.68020

Summary: This paper presents an object-oriented, Java-like core language with primitives for distributed programming and explicit code mobility. We apply our formulation to prove the correctness of several optimisations for distributed programs. Our language captures crucial but often hidden aspects of distributed object-oriented programming, including object serialisation, dynamic class downloading and remote method invocation. It is defined in terms of an operational semantics that concisely models the behaviour of distributed programs using machinery from calculi of mobile processes. Type safety is established using invariant properties for distributed runtime configurations. We argue that primitives for explicit code mobility offer a programmer fine-grained control of type-safe code distribution, which is crucial for improving the performance and safety of distributed object-oriented applications.


68N15 Theory of programming languages
Full Text: DOI Link


[1] Abadi, Martin; Cardelli, Luca, A theory of objects, (1996), Springer-Verlag · Zbl 0876.68014
[2] Acute. Acute home page. http://www.cl.cam.ac.uk/users/pes20/acute, 2005
[3] Alexander Ahern, Code mobility and Java RMI, Ph.D. Thesis, Department of Computing, Imperial College London, July 2007
[4] Alexander Ahern, Nobuko Yoshida, Formal analysis of a distributed object-oriented language and runtime, Technical Report 2005/01, Department of Computing, Imperial College London. Available at: http://www.doc.ic.ac.uk/ aja/dcbl.html, 2005 · Zbl 1151.68347
[5] Ahern, Alexander; Yoshida, Nobuko, Formalising Java RMI with explicit code mobility, (), 211-230 · Zbl 1132.68020
[6] Davide Ancona, Giovanni Lagorio, Elena Zucca, Simplifying types in a calculus for Java exceptions, Technical Report, DISI - Università di Genova, 2002 · Zbl 1049.68746
[7] Andrews, Gregory R., Foundations of multithreaded, parallel, and distributed programming, (2000), Addison Wesley
[8] Arun-Kumar, S.; Hennessy, Matthew, An efficiency preorder for processes, Acta inform., 29, 8, 737-760, (1992) · Zbl 0790.68039
[9] Gavin Bierman, Matthew Parkinson, Andrew Pitts, MJ: An imperative core calculus for Java and Java with effects, Technical Report 563, University of Cambridge Computer Laboratory, April 2003
[10] Bogle, Phillip; Liskov, Barbara, Reducing cross domain call overhead using batched futures, (), 341-354
[11] Briais, Sébastien; Nestmann, Uwe, Mobile objects must move safely, (), 129-146 · Zbl 1048.68026
[12] Luca Cardelli, Obliq: A language with distributed scope, Technical Report 122, Systems Research Center, Digital Equipment Corporation, 1994
[13] Christ, R., Sanfrancisco performance: A case study in performance of large-scale Java applications, IBM systems J., 39, 1, (2000)
[14] Drossopoulou, Sophia; Eisenbach, Susan, Manifestations of dynamic linking, () · Zbl 1032.68039
[15] Drossopoulou, Sophia; Lagorio, Giovanni; Eisenbach, Susan, Flexible models for dynamic linking, (), 38-53 · Zbl 1032.68039
[16] Flanagan, David, Java examples in a nutshell, (2000), O’Reilly UK · Zbl 0978.68032
[17] Andrew D. Gordon, Paul D. Hankin, A concurrent object calculus: Reduction and typing, Technical Report 457, University of Cambridge Computer Laboratory, February 1999 · Zbl 0917.68064
[18] Gordon, Andrew D.; Syme, Don, Typing a multi-language intermediate code, (), 248-260 · Zbl 1323.68209
[19] Todd Greanier, Discover the secrets of the Java Serialization API. http://java.sun.com/developer/technicalArticles/Programming/serialization/, 2005
[20] Kohei Honda, Composing processes, in: Proceedings of POPL’96, 1996, pp. 344-357
[21] Honda, Kohei; Tokoro, Mario, An object calculus for asynchronous communication, (), 133-147
[22] Honda, Kohei; Vasconcelos, Vasco T.; Kubo, Makoto, Language primitives and type disciplines for structured communication-based programming, (), 22-138
[23] Honda, Kohei; Yoshida, Nobuko, On reduction-based process semantics, Theoret. comput. sci., 151, 2, 385-435, (1995) · Zbl 0871.68122
[24] Norman C. Hutchinson, Rajendra K. Raj, Andrew P. Black, Henry M. Levy, Eric Jul, The Emerald programming language, Technical Report, Department of Computer Science, University of British Columbia, Vancouver BC, Canada V6T 1Z2, October 1991
[25] Igarashi, Atsushi; Pierce, Benjamin C.; Wadler, Philip, Featherweight Java: A minimal core calculus for Java and GJ, ACM trans. programming languages systems, 23, 3, 396-450, (2001)
[26] Jeffrey, Alan, A distributed object calculus, ()
[27] Jones, Cliff, Constraining interference in an object-based design method, (), 136-150
[28] Kamin, Sam; Clausen, Lars; Jarvis, Ava, Jumbo: run-time code generation for Java and its applications, ()
[29] Naoki Kobayashi, Benjamin Pierce, David Turner, Linear types and \(\pi\)-calculus, in: Proceedings of POPL’96, 1996, pp. 358-371
[30] Krintz, Chandra; Calder, Brad; Hölzle, Urs, Reducing transfer delay using Java class file splitting and prefetching, (), 276-291
[31] Liang, Sheng; Bracha, Gilad, Dynamic class loading in the Java virtual machine, (), 36-44
[32] McGraw, Gary; Morrisett, Greg, Attacking malicious code: A report to the infosec research council, IEEE software, 17, 5, 33-44, (2000)
[33] Merro, Massimo; Kleist, Josva; Nestmann, Uwe, Mobile objects as mobile processes, Inform. and comput., 177, 2, 195-241, (2002) · Zbl 1093.68562
[34] Sun Microsystems Inc. Java Remote Method Invocation (RMI). http://java.sun.com/products/jdk/rmi/, 2005
[35] Milner, Robin; Parrow, Joachim; Walker, David, A calculus of mobile processes, parts I and II, Inform. and comput., 100, 1, (1992) · Zbl 0752.68037
[36] Milner, Robin; Sangiorgi, Davide, Barbed bisimulation, (), 685-695
[37] Nestmann, Uwe; Hüttel, Hans; Kleist, Josva; Merro, Massimo, Aliasing models for mobile objects, Inform. and comput., 177, 2, 195-241, (2002) · Zbl 1012.68114
[38] Ohori, Atsushi; Kato, Kazuhiko, Semantics for communication primitives in a polymorphic language, (), 99-112
[39] Karen Osmond, Alexander Ahern, Nobuko Yoshida, DJ SourceForge Homepage. http://dj-project.sourceforge.net/
[40] Pierce, Benjamin C., Types and programming languages, (2002), MIT Press · Zbl 0995.68018
[41] Qian, Zhenyu; Goldberg, Allen; Coglio, Alessandro, A formal specification of Java class loading, (), 325-336
[42] Reynolds, John C., Syntactic control of interference, (), 39-46
[43] Davide Sangiorgi, Expressing mobility in process algebras: First-order and higher order paradigms, Ph.D. Thesis, University of Edinburgh, 1992
[44] Stamos, James W.; Gifford, David K., Implementing remote evaluation, IEEE trans. softw. eng., 16, 7, 710-722, (1990)
[45] Taha, Walid; Sheard, Tim, Multi-stage programming with explicit annotations, (), 203-217
[46] Farzana Tejani, Implementation of a distributed mobile Java, Master’s Thesis, Imperial College London, MEng. Computing Final Year Project, Imperial College London, 2005
[47] Vasconcelos, Vasco T.; Ravara, António; Gay, Simon, Session types for functional multithreading, (), 497-511 · Zbl 1099.68677
[48] Vitek, Jan; Bryce, Ciarán; Binder, Walter, Designing javaseal or how to make Java safe for agents, Electronic commerce objects, (1998)
[49] Wallach, Dan S.; Balfanz, Dirk; Dean, Drew; Felten, Edward W., Extensible security architectures for Java, (), 116-128
[50] Kwok Yeung, Dynamic performance optimisation of distributed Java applications, Ph.D. Thesis, Imperial College London, 2004
[51] Yeung, Kwok; Kelly, Paul, Optimizing Java RMI programs by communication restructuring, (), 324-343
[52] Yoshida, Nobuko, Graph types for monadic mobile processes, (), 211-230, Full version as Edinburgh LFCS Technical Report, ECS-LFCS-96-350, 1996
[53] Yoshida, Nobuko, Channel dependency types for higher-order mobile processes, (), 147-160, Full version available at: www.doc.ic.ac.uk/ yoshida · Zbl 1325.68162
[54] Yoshida, Nobuko; Berger, Martin; Honda, Kohei, Strong normalisation in the \(\pi\)-calculus, (), 311-322, The full version in Journal of Inform. and Comput., 191 (2004) 145-202, Elsevier · Zbl 1101.68705
[55] Yu, Dachuan; Kennedy, Andrew; Syme, Don, Formalization of generics for the.net common language runtime, (), 39-51 · Zbl 1325.68053
[56] Tian Zhao, James Noble, Jan Vitek, Scoped types for real-time Java, in: Proceedings of the 25th Annual IEEE Symposium on Real-Time Systems, 2004 · Zbl 1127.68015
[57] Zook, David; Huang, Shan Shan; Smaragdakis, Yannis, Generating aspectj programs with meta-aspectj, (), 1-19 · Zbl 1215.68054
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.