A Type-Based Locality Analysis for a Functional Distributed Language

In this thesis we give a type-based analysis for an ML-like distributed language that detects references certain not to escape from one processor to another. We assume a model of distribution based on distributed shared memory. From the programmer's viewpoint, the same reference on different machines refers to the same data object in a single logical store, but data is in fact distributed among the machines. A coherent protocol is then responsible for determining for each operation with references whether the associated data is available on the current machine, and if not, retrieving it over the network. The costs of calling a coherency protocol for each store access can be reduced if a locality analysis can determine which references refer to local data only. Assignment and dereference operations using these local references can then be compiled to specialised versions, usually comprising a few machine instructions to manipulate data in the store. The locality analysis we propose takes the form of a conservative extension of the Hindley-Milner polymorphic type discipline where reference types are tagged with locality information. We prove type soundness of the type system with respect to an operational semantics, and we also show that the type system soundly describes the locality of references in the sense that a local reference is certain not to escape according to the operational semantics. This result means that a compiler can safely use the locality information provided by the types to replace assignment and dereferencing operations performed on local references with specialised variants, which are less costly than the originals. In order to illustrate how this can be done we define a target language and we give an operational semantics for it at a level of abstraction that differentiates between local and global versions of operations with the store. We define a translation from well typed source expressions to expressions in the target language induced by the locality information on types, and we prove that this translation preserves the original behaviour. We then give a sound type reconstruction algorithm and we discuss a restricted form of best locality property that we conjecture the algorithm possesses. We also report on experiments showing that detecting local references has a significant impact on the performance of programs