Acute

Acute: high-level programming language design for distributed computation

This work is exploring the design space of high-level languages for distributed computation, focussing on typing, naming, and version change. We have designed, formally specified and implemented an experimental language, Acute. This extends an OCaml core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. It is 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 primitives, disentangling the language runtime from communication.

This requires a synthesis of novel and existing features:

type-safe interaction between programs, with marshal and unmarshal primitives;
dynamic loading and controlled rebinding to local resources;
modules and abstract types with abstraction boundaries that are respected by interaction;
global names, generated either freshly or based on module hashes: at the type level, as runtime names for abstract types; and at the term level, as channel names and other interaction handles;
versions and version constraints, integrated with type identity;
local concurrency and thread thunkification; and
second-order polymorphism with a namecase construct.

The language design deals with the interplay among these features and the core. The semantic definition tracks abstraction boundaries, global names, and hashes throughout compilation and execution, but still admits an efficient implementation strategy.

Papers

Acute: high-level programming language design for distributed computation Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis. Also in pdf.
To appear in Journal of Functional Programming. This gives a full discussion of the language design and an overview of the key aspects of the semantics.
Acute: high-level programming language design for distributed computation Peter Sewell, James J. Leifer, Keith Wansbrough, Francesco Zappa Nardelli, Mair Allen-Williams, Pierre Habouzit, Viktor Vafeiadis. In ICFP 2005. Also in pdf.
This short paper gives an overview of the main design choices.
Acute: high-level programming language design for distributed computation. Design rationale and language definition. Peter Sewell, James J. Leifer, Keith Wansbrough, Mair Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, Viktor Vafeiadis. Draft. Also in pdf.
This contains an extended version of the design discussion in the above, together with an introduction to the semantics, examples illustrating the semantics, and the full language definition.
errata for the above

Code

Here are some examples of Acute code: the modules Tcp_connection_management and Tcp_string_messaging, Local_channel, Distributed_channel, and Npi, and the Ambient implementation, referred to in the papers.

Download

People

University of Cambridge Computer Laboratory and INRIA Rocquencourt (Moscova project)

Previous work

Acute draws on earlier work on abstraction-safe marshalling, dynamic rebinding, and module versioning, described in the ICFP 2003 and POPL 2001 papers here, and also on work on Nomadic Pict. The implementation is written in Fresh OCaml and Acute also incorporates fresh name generation and swap.

Acknowledgements

This work has been funded by a Royal Society University Research Fellowship (Sewell), a St Catharine's College Heller Research Fellowship (Wansbrough), an INRIA grant "post-doc a l'etranger" (Zappa Nardelli), EPSRC grants GRN24872 and GRT11715, EC FET-GC project IST-2001-33234 PEPITO, and APPSEM 2.

Peter.Sewell@cl.cam.ac.uk

[Validate this page.]