Acute: high-level programming language design for distributed computation

ABSTRACT

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programminglanguage support for such systems, focussing on their typing and naming issues.We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. The main features are: (1) type-safe marshalling of arbitrary values; (2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system; (3) expression-level names generated to ensure that name equality tests suffice for type-safety of associated values, e.g. values carried on named channels; (4) controlled dynamic rebinding of marshalled values to local resources; and (5) thunkification of threads and mutexes to support computation mobility.These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of ML, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language runtime from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.

REFERENCES

• 1: Joe Armstrong , Robert Virding , Claes Wikström , Mike Williams, Concurrent programming in ERLANG (2nd ed.), Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1996
• 2: Nick Benton , Luca Cardelli , Cédric Fournet, Modern Concurrency Abstractions for C#, Proceedings of the 16th European Conference on Object-Oriented Programming, p.415-440, June 10-14, 2002
• 3: Gavin Bierman , Michael Hicks , Peter Sewell , Gareth Stoyle , Keith Wansbrough, Dynamic rebinding for marshalling and update, with destruct-time ?, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.99-110, August 25-29, 2003, Uppsala, Sweden
• 4: Alex Buckley, Michelle Murray, Susan Eisenbach, and Sophia Drossopoulou. Flexible bytecode for linking in .NET. In Proc. BYTECODE 2005, April 2005.
• 5: D. Le Botlan, A. Rossberg, C. Schulte, G. Smolka, and G. Tack, 2005. www.ps.uni-sb.de/alice/.
• 6: Luca Cardelli, A language with distributed scope, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.286-297, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199516]
• 7: Luca Cardelli , Andrew D. Gordon, Mobile Ambients, Proceedings of the First International Conference on Foundations of Software Science and Computation Structure, p.140-155, March 28-April 04, 1998
• 8: Sophia Drossopoulou , Susan Eisenbach , David Wragg, A Fragment Calculus Towards a Model of Separate Compilation, Linking and Binary Compatibility, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.147, July 02-05, 1999
• 9: Packacking and deploying .Net framework applications (.Net framework tutorials, msdn), 2003.
• 10: Cédric Fournet , Georges Gonthier , Jean-Jacques Lévy , Luc Maranget , Didier Rémy, A Calculus of Mobile Agents, Proceedings of the 7th International Conference on Concurrency Theory, p.406-421, August 26-29, 1996
• 11: Jun Furuse and Pierre Weis. Entrées/sorties de valeurs en Caml. In J. Francophones des Langages Applicatifs, 2000.
• 12: Dan Grossman , Greg Morrisett , Steve Zdancewic, Syntactic type abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.6, p.1037-1080, Nov. 2000 [doi>10.1145/371880.371887]
• 13: Robert Harper , Mark Lillibridge, A type-theoretic approach to higher-order modules with sharing, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.123-137, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176927]
• 14: R. Harper and B. C. Pierce. Design issues in advanced module systems, 2005. Chapter in Advanced Topics in Types and Programming Languages, B. C. Pierce, editor.
• 15: M. Hennessy, J. Rathke, and N. Yoshida. Safedpi: A language for controlling mobile code. In Proc. FOSSACS, LNCS 2987, 2004.
• 16: Robert Harper , Christopher Stone, A type-theoretic interpretation of standard ML, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 17: JoCaml. http://pauillac.inria.fr/jocaml/.
• 18: Xavier Leroy, Manifest types, modules, and separate compilation, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.109-122, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.176926]
• 19: James J. Leifer , Gilles Peskine , Peter Sewell , Keith Wansbrough, Global abstraction-safe marshalling with hash types, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.87-98, August 25-29, 2003, Uppsala, Sweden
• 20: Tom Murphy VII , Karl Crary , Robert Harper , Frank Pfenning, A Symmetric Modal Lambda Calculus for Distributed Computing, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.286-295, July 13-17, 2004 [doi>10.1109/LICS.2004.7]
• 21: Benjamin C. Pierce , David N. Turner, Pict: a programming language based on the Pi-Calculus, Proof, language, and interaction: essays in honour of Robin Milner, MIT Press, Cambridge, MA, 2000
• 22: John H. Reppy, Concurrent programming in ML, Cambridge University Press, New York, NY, 1999
• 23: Andreas Rossberg, Generativity and dynamic opacity for abstract types, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.241-252, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888274]
• 24: Peter Sewell, Modules, abstract types, and distributed versioning, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.236-247, January 2001, London, United Kingdom
• 25: M. R. Shinwell. The Fresh Approach: functional programming with names and binders. Technical Report UCAM-CLTR-618, University of Cambridge, Computer Laboratory, 2005.
• 26: P. Sewell, J. J. Leifer, K. Wansbrough, M. Allen-Williams, Francesco Z. Nardelli, P. Habouzit, and V. Vafeiadis. Acute: High-level programming language design for distributed computation. design rationale and language definition. Technical Report 605, University of Cambridge Computer Laboratory, October 2004. Also published as INRIA RR-5329. 193pp.
• 27: P. Sewell, J. J. Leifer, K. Wansbrough, M. Allen-Williams, F. Zappa Nardelli, P. Habouzit, and V. Vafeiadis. Source release of the Acute system, January 2005. Available from http://www.cl.cam.ac.uk/users/pes20/acute/.
• 28: Mark R. Shinwell , Andrew M. Pitts , Murdoch J. Gabbay, FreshML: programming with binders made simple, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.263-274, August 25-29, 2003, Uppsala, Sweden
• 29: Peter Sewell , Pawel T. Wojciechowski , Benjamin C. Pierce, Location-Independent Communication for Mobile Agents: A Two-Level Architecture, Workshop on Internet Programming Languages, p.1-31, May 13, 1998
• 30: Bent Thomsen , Lone Leth , Tsung-Min Kuo, A Facile Tutorial, Proceedings of the 7th International Conference on Concurrency Theory, p.278-298, August 26-29, 1996
• 31: Asis Unyapoth , Peter Sewell, Nomadic pict: correct communication infrastructure for mobile computation, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.116-127, January 2001, London, United Kingdom
• 32: Vesta. http://www.vestasys.org/.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features

General Terms:
Design, Languages

Keywords:
ML, abstract types, distributed programming, marshalling, modules, programming languages, rebinding, serialisation, type theory, version control