Alexander Ahern
ABSTRACT
This paper presents a Java-like core language with primitives for object-oriented distribution 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.
- Acute home page. www.cl.cam.ac.uk/users/pes20/acute.Google Scholar
- M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996. Google ScholarDigital Library
- A. Ahern and N. Yoshida. Full version of this paper. www.doc.ic.ac.uk/~aja/dcbl.html.Google Scholar
- A. Ahern and N. Yoshida. Formal Analysis of a Distributed Object-Oriented Language and Runtime. Technical Report 2005/01, Department of Computing, Imperial College London: Available at: www.doc.ic.ac.uk/~aja/dcbl.html, 2005.Google Scholar
- D. Ancona, G. Lagorio, and E. Zucca. Simplifying types in a calculus for Java exceptions. Technical report, DISI - Univ. di Genova, 2002.Google Scholar
- S. Arun-Kumar and M. Hennessy. An efficiency preorder for processes. Acta Inf., 29(8):737--760, 1992. Google ScholarDigital Library
- G. Bierman, M. Parkinson, and A. Pitts. MJ: An imperative core calculus for Java and Java with effects. Technical Report 563, Univ. of Cambridge Computer Laboratory, April 2003.Google Scholar
- P. Bogle and B. Liskov. Reducing cross domain call overhead using batched futures. In OOPSLA'94, pages 341--354. ACM Press, 1994. Google ScholarDigital Library
- S. Briais and U. Nestmann. Mobile objects "must" move safely. In FMOODS'02, pages 129--146. Kluwer, 2002. Google ScholarDigital Library
- L. Cardelli. Obliq: A language with distributed scope. Technical Report 122, Systems Research Center, Digital Equipment Corporation, 1994.Google Scholar
- R. Christ. SanFrancisco Performance: A case study in performance of large-scale Java applications. IBM Systems Journal, 39(1), 2000. Google ScholarDigital Library
- S. Drossopoulou and S. Eisenbach. Manifestations of Dynamic Linking. In USE 2002, Málaga, Spain, June 2002.Google Scholar
- S. Drossopoulou, G. Lagorio, and S. Eisenbach. Flexible Models for Dynamic Linking. In P. Degano, editor, ESOP'03, volume 2618 of LNCS, pages 38--53. Springer-Verlag, April 2003. Google ScholarDigital Library
- D. Flanagan. Java Examples in a Nutshell. O'Reilly UK, 2000. Google ScholarDigital Library
- A. D. Gordon and P. D. Hankin. A concurrent object calculus: Reduction and typing. Technical Report 457, Univ. of Cambridge Computer Laboratory, February 1999.Google Scholar
- A. D. Gordon and D. Syme. Typing a multi-language intermediate code. In POPL'01, pages 248--260. ACM Press, 2001. Google ScholarDigital Library
- T. Greanier. Discover the secrets of the Java Serialization API. java.sun.com/developer/technicalArticles/Programming/serialization/.Google Scholar
- K. Honda. Composing processes. In POPL'96, pages 344--357, 1996. Google ScholarDigital Library
- K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedings of ECOOP'91, volume 512, pages 133--147, 1991. Google ScholarDigital Library
- K. Honda, V. T. Vasconcelos, and M. Kubo. Language primitives and type disciplines for structured communication-based programming. In ESOP'98, volume 1381 of LNCS, pages 22--138. Springer-Verlag, 1998. Google ScholarDigital Library
- K. Honda and N. Yoshida. On reduction-based process semantics. TCS, 151(2):385--435, 1995. Google ScholarDigital Library
- A. Igarashi, B. C. Pierce, and P. Wadler. Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. and Sys., 23(3):396--450, 2001. Google ScholarDigital Library
- A. Jeffrey. A Distributed Object Calculus. In FOOL. ACM Press, 2000.Google Scholar
- C. Jones. Constraining interference in an object-based design method. In TAPSOFT'93, volume 668 of LNCS, pages 136--150. Springer-Verlag, 1993. Google ScholarDigital Library
- E. Jul, H. Levy, N. Hutchinson, and A. Black. Fine-grained mobility in the emerald system. ACM Trans. Comput. Syst., 6(1):109--133, 1988. Google ScholarDigital Library
- S. Kamin, L. Clausen, and A. Jarvis. Jumbo:run-time code generation for java and its applications. In CGO'03. IEEE, 2003. Google ScholarDigital Library
- N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst., 21(5):914--947, 1999. Google ScholarDigital Library
- C. Krintz, B. Calder, and U. Hölzle. Reducing transfer delay using Java class file splitting and prefetching. In OOPSLA'99, pages 276--291. ACM Press, 1999. Google ScholarDigital Library
- S. Liang and G. Bracha. Dynamic class loading in the Java virtual machine. In OOPSLA'98, pages 36--44. ACM Press, 1998. Google ScholarDigital Library
- G. McGraw and G. Morrisett. Attacking malicious code: a report to the infosec research council. IEEE Software, 17(5):33--44, 2000. Google ScholarDigital Library
- M. Merro, J. Kleist, and U. Nestmann. Mobile objects as mobile processes. Inf. & Comp., 177(2):195--241, 2002. Google ScholarDigital Library
- R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, parts I and II. Inf. & Comp., 100(1), 1992. Google ScholarDigital Library
- U. Nestmann, H. Hüttel, J. Kleist, and M. Merro. Aliasing models for mobile objects. Inf. & Comp., 177(2):195--241, 2002. Google ScholarDigital Library
- A. Ohori and K. Kato. Semantics for communication primitives in a polymorphic language. In POPL'93, pages 99--112. ACM Press, 1993. Google ScholarDigital Library
- B. C. Pierce. Types and Programming Languages. MIT Press, 2002. Google ScholarDigital Library
- Z. Qian, A. Goldberg, and A. Coglio. A formal specification of Java class loading. In OOPSLA'00, pages 325--336. ACM Press, 2000. Google ScholarDigital Library
- J. C. Reynolds. Syntactic control of interference. In POPL'78, pages 39--46. ACM Press, 1978. Google ScholarDigital Library
- D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher Order Paradigms. PhD thesis, Univ. of Edinburgh, 1992.Google Scholar
- J. W. Stamos and D. K. Gifford. Implementing remote evaluation. IEEE Trans. Softw. Eng., 16(7):710--722, 1990. Google ScholarDigital Library
- Sun Microsystems Inc. Java Remote Method Invocation (RMI). java.sun.com/products/jdk/rmi/.Google Scholar
- W. Taha and T. Sheard. Multi-stage programming with explicit annotations. In PEPM'97, pages 203--217. ACM Press, 1997. Google ScholarDigital Library
- F. Tejani. Implementation of a distributed mobile Java. Master's thesis, Imperial College London, 2005.Google Scholar
- V. T. Vasconcelos, A. Ravara, and S. Gay. Session types for functional multithreading. In CONCUR'04, volume 3170 of LNCS, pages 497--511. Springer-Verlag, 2004.Google Scholar
- J. Vitek, C. Bryce, and W. Binder. Designing JavaSeal or how to make Java safe for agents. Electronic Commerce Objects, 1998.Google Scholar
- D. S. Wallach, D. Balfanz, D. Dean, and E. W. Felten. Extensible security architectures for Java. In SOSP'97, pages 116--128. ACM Press, 1997. Google ScholarDigital Library
- K. Yeung. Dynamic performance optimisation of distributed Java applications. PhD thesis, Imperial College London, 2004.Google Scholar
- K. Yeung and P. Kelly. Optimizing Java RMI programs by communication restructuring. In Middleware'03, volume 2672 of LNCS, pages 324--343. Springer-Verlag, 2003. Google ScholarDigital Library
- N. Yoshida. Channel dependency types for higher-order mobile processes. In POPL'04, pages 147--160. ACM Press, 2004. Full version available at www.doc.ic.ac.uk/~yoshida. Google ScholarDigital Library
- N. Yoshida, M. Berger, and K. Honda. Strong Normalisation in the π-Calculus. In LICS'01, pages 311--322. IEEE, 2001. The full version in Journal of Inf. & Comp., 191 (2004) 145--202, Elsevier. Google ScholarDigital Library
- D. Yu, A. Kennedy, and D. Syme. Formalization of generics for the .NET common language runtime. In POPL'04, pages 39--51. ACM Press, 2004. Google ScholarDigital Library
- T. Zhao, J. Noble, and J. Vitek. Scoped types for real-time Java. In RTSS'04, 2004. Google ScholarDigital Library
- D. Zook, S. S. Huang, and Y. Smaragdakis. Generating AspectJ Programs with Meta-AspectJ. In GPCE'04, volume 3286 of LNCS, pages 1--19. Springer-Verlag, 2004.Google Scholar
Index Terms
- Formalising Java RMI with explicit code mobility
Recommendations
Formalising Java RMI with explicit code mobility
Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming systems languages and applicationsThis paper presents a Java-like core language with primitives for object-oriented distribution and explicit code mobility. We apply our formulation to prove the correctness of several optimisations for distributed programs. Our language captures crucial ...
Formalising Java RMI with explicit code mobility
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 ...
Experiments with multi-protocol RMI in Java
JGI '02: Proceedings of the 2002 joint ACM-ISCOPE conference on Java GrandeRemote Method Invocation is an adaptation of the remote procedure call paradigm for object-oriented environments. RMI allows clients to seamlessly invoke methods of objects within remote servers. Communication between the client and server is based upon ...
Reviews
Maulik A Dave
Remote method invocation (RMI) is a frequently used technique in distributed processing. This paper proposes some optimizations related to RMI. A new Java-like language, called DJ, is proposed. The language has constructs facilitating the optimizations. RMI and code mobility are introduced in the first section. The second section informally explains the optimizations, which reduce communication times among processors. Instead of calling methods of the same remote object one after another, calls bundled into a freeze block can be sent to the remote processor. Strategies for optimized class downloading can be programmed using serialize and deserialize constructs. The grammar describing the syntax of DJ is presented in the third section. In DJ, networking constructs with class tables appear only at runtime. The operational semantics of DJ is discussed in the fourth section. DJ's typing system is given special treatment, and is described separately in the next two sections. Types for channels, threads, and networks are described. Invariants for class availability, linearity, locality, and progress are constructed. The correctness proofs of the optimizations are given in the seventh section. Some reduction rules for DJ are also presented in an appendix. A detailed survey of related works and conclusions are presented in the last two sections. One of the first impressions created by the paper is that lower level programming is required to achieve some of the optimizations in distributed processing. The properties, and the theoretical analysis developed, can be useful in other, similar situations. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments