Abstract:
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.
This report is available in the following formats:
Index | Next An error occured whilst processing this directive