×

zbMATH — the first resource for mathematics

Mobile objects as mobile processes. (English) Zbl 1093.68562
Inf. Comput. 177, No. 2, 195-241 (2002); erratum ibid. 179, No. 2, 384 (2002).
Summary: Obliq is a lexically scoped, distributed, object-based programming language. In Obliq, the migration of an object is proposed as creating a clone of the object at the target site, whereafter the original object is turned into an alias for the clone. Obliq has only an informal semantics, so there is no proof that this style of migration is safe, i.e., transparent to object clients. In previous work, we introduced Øjeblik, an abstraction of Obliq, where, by lexical scoping, sites have been abstracted away. We used Øjeblik in order to exhibit how the semantics behind Obliq’s implementation renders migration unsafe. We also suggested a modified semantics that we conjectured instead to be safe. In this paper, we rewrite our modified semantics of Øjeblik in terms of the \(\pi\)-calculus, and we use it to formally prove the correctness of object surrogation, the abstraction of object migration in Øjeblik.

MSC:
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M, and, Cardelli, L. 1996, A Theory of Objects, Monographs in Computer Science, Springer-Verlag, Berlin. · Zbl 0876.68014
[2] Amadio, R.M.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, Theoret. comput. sci., 195, 291-324, (1998) · Zbl 0915.68009
[3] Amadio, R. M., Castellani, I., and Sangiorgi, D.An extended abstract appeared in “Proceedings of CONCUR ’96”, Lecture Notes in Computer Science, Vol. 1119, pp. 147-162.
[4] Boudol, G. 1992, Asynchrony and the π-Calculus (note), Rapport de Recherche 1702, INRIA Sophia-Antipolis.
[5] Cardelli, L.1995, A language with distributed scope, Computing Systems8, 27-59. Short version in “Proceedings of POPL ’95”, a preliminary version appeared as Report 122, Digital Systems Research, June 1994.
[6] Di Blasio, P., and Fisher, K.1996, A concurrent object calculus, inProceedings of CONCUR ’96U. Montanari and V. Sassone, Eds., Lecture Notes in Computer Science, Vol. 1119, pp. 655-670, Springer-Verlag, Berlin. An extended version appeared as Stanford University Technical Note STAN-CS-TN-96-36, 1996.
[7] Fournet, C., and Gonthier, G.1996, The reflexive chemical abstract machine and the join-calculus, inProceedings of POPL ’96, January, pp. 372-385, Assoc. Comput. Mach. New York.
[8] Gordon, A. D., and Hankin, P. D.1998, A concurrent object calculus: Reduction and typing, inProceedings of HLCL ’98U. Nestmann and B. C. Pierce, Eds., Electronic Notes in Theoretical Computer Science, Vol. 16.3, Elsevier Science, Amsterdam. · Zbl 0917.68064
[9] Gordon, A. D., Hankin, P. D., and Lassen, S. B.1997, Compilation and equivalence of imperative objects, inProceedings of FSTTCS ’97S. Ramesh and G. Sivakumar, Eds., Lecture Notes in Computer Science, Vol. 1346, December, pp. 74-87, Springer-Verlag, Berlin. Full version available as Technical Report 429, University of Cambridge Computer Laboratory, June 1997.
[10] Honda, K. 1992, Two Bisimilarities for the ν-Calculus, Technical Report 92-002, Keio University.
[11] Honda, K., and Tokoro, M.1991, An object calculus for asynchronous communication, inProceedings of ECOOP ’91P. America, Ed., Lecture Notes in Computer Science, Vol. 512, July, pp. 133-147, Springer-Verlag, Berlin.
[12] Honda, K.; Yoshida, N., On reduction-based process semantics, Theoret. comput. sci., 152, 437-486, (1995) · Zbl 0871.68122
[13] Hüttel, H, and, Kleist, J. 1996, Objects as mobile processes, in, MPFS ’96, Research Series RS-96-38, BRICS. · Zbl 1014.68104
[14] Hüttel, H, Kleist, J, Merro, M, and, Nestmann, U. 1999, Migration \(=\) cloning; aliasing (preliminary version), in, Informal Proceedings of the Sixth International Workshop on Foundations of Object-Oriented Languages (FOOL 6, San Antonio, Texas, USA), Sponsored by ACM/SIGPLAN.
[15] Jul, E.; Levy, H.; Hutchinson, N.; Black, A., Fine-grained mobility in the emerald system, ACM trans. comput. systems, 6, 109-133, (1988)
[16] Kleist, J., and Sangiorgi, D.1998, Imperative objects and mobile processes, inProceedings of PROCOMET ’98D. Gries and W.-P. de Roever, Eds., pp. 285-303, International Federation for Information Processing (IFIP), Chapman & Hall, London.
[17] Kobayashi, N., Pierce, B. C., and Turner, D. N.1996, Linearity and the pi-calculus, inProceedings of POPL ’96, January, pp. 358-371, Assoc. Comput. Mach. New York.
[18] Merro, M.2000, Locality and polyadicity in asynchronous name-passing calculi, inProceedings of FoSSaCS 2000J. Tiuryn, Ed., Lecture Notes in Computer Science, Vol. 1784, pp. 238-251, Springer-Verlag, Berlin. · Zbl 0961.68091
[19] Merro, M. 2000, Locality in the π-Calculus and Applications to Distributed Objects, Ph.D. thesis, Ecole des Mines, France.
[20] Merro, M., and Sangiorgi, D.1998, On asynchrony in name-passing calculi, inProceedings of ICALP ’98K. G. Larsen, S. Skyum, and G. Winskel, Eds., Lecture Notes in Computer Science, Vol. 1443, July, pp. 856-867, Springer-Verlag, Berlin. · Zbl 0910.03019
[21] Milner, R.1993, The polyadic π-calculus: A tutorial, inLogic and Algebra of SpecificationF. L. Bauer, W. Brauer, and H. Schwichtenberg, Eds., Computer and System Sciences, Vol. 94, Series F, NATO Advanced Study Institute, Springer-Verlag, Berlin. Available as Technical Report ECS-LFCS-91-180, University of Edinburgh, October 1991.
[22] Milner, R., and Sangiorgi, D.1992, Barbed bisimulation, inProceedings of ICALP ’92W. Kuich, Ed., Lecture Notes in Computer Science, Vol. 623, pp. 685-695, Springer-Verlag, Berlin.
[23] Morris, J.-H. 1968, Lambda Calculus Models of Programming Languages, Ph.D. thesis, MIT.
[24] Nestmann, U., Hüttel, H., Kleist, J., and Merro, M., Aliasing models for mobile objects, Inform. and Comput.175, 3-33. Available athttp://www.cs.auc.dk/research/FS/ojeblik/. An extended abstract has appeared as Distinguished Paper in the 2000, “Proceedings of EUROPAR ’99”, Lecture Notes in Computer Science, Vol. 1685. · Zbl 1012.68114
[25] Philippou, A.; Walker, D., On transformations of concurrent object programs, An extended abstract appeared in “proceedings of CONCUR ’96”, Theoret. comput. sci., 195, 259-289, (1998) · Zbl 0915.68024
[26] Pierce, B.C.; Sangiorgi, D., Typing and subtyping for mobile processes, Mathematical structures in comput. sci., 6, 409-454, (1996) · Zbl 0861.68030
[27] Sangiorgi, D., Locality and non-interleaving semantics in calculi for mobile processes, Theoret. comput. sci., 155, 39-83, (1996) · Zbl 0874.68115
[28] Sangiorgi, D.1998, An interpretation of typed objects into typed π-calculus, Information and Computation143, 34-73. Earlier version published as Rapport de Recherche RR-3000, INRIA Sophia-Antipolis, August 1996.
[29] Sangiorgi, D., The name discipline of uniform receptiveness, Theoret. comput. sci., 221, 457-493, (1999) · Zbl 0930.68035
[30] Sangiorgi, D.1999, The typed π-calculus at work: A proof of Jones’s parallelisation theorem on concurrent objects, Theory and Practice of Object-Oriented Systems5, 25-33. An early version was included in the “Informal Proceedings of FOOL 4”, January 1997.
[31] Sangiorgi, D.2000, Lazy functions and mobile processes, inProof, Language and Interaction: Essays in Honour of Robin Milner, Foundations of ComputingG. Plotkin, C. Stirling, and M. Tofte, Eds., MIT Press, Cambridge, MA. Available as INRIA Sophia-Antipolis Rapport de Recherche RR-2515.
[32] Sangiorgi, D., and Milner, R.1992, The problem of “weak bisimulation up to”, inProceedings of CONCUR ’92R. Cleaveland, Ed., Lecture Notes in Computer Science, Vol. 630, pp. 32-46, Springer-Verlag, Berlin.
[33] Sangiorgi, D, and, Walker, D. 2001, The π-Calculus: A Theory of Mobile Processes, Cambridge University Press, Cambridge, UK. · Zbl 0981.68116
[34] Talcott, C. L. 1996, Obliq semantics notes, Unpublished note, available at, clt@cs.stanford.edu.
[35] Van Roy, P.; Haridi, S.; Brand, P.; Smolka, G.; Mehl, M.; Scheidhauer, R., Mobile objects in distributed oz, ACM trans. programming lang. systems, 19, 804-851, (1997)
[36] Walker, D., Objects in the π-calculus, Infor. and comput., 116, 253-271, (1995) · Zbl 0828.68043
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.