We present an approach for implementing language-level primitives for whole-process migration and speculative execution in a compiler and associated runtime environment. These primitives are exposed to the user through simple language constructs that do not require the user to manage process state explicitly. With migration and speculation we show how the user can quickly add persistent checkpoints to any large-scale distributed application that requires longevity in a faulty environment. We demonstrate the use of migration and speculation primitives for checkpointing in a canonical grid computation application, and analyze the results of this implementation.

Transactions are a simple and powerful mechanism for establishing fault-tolerance. To allow multiple processes to cooperate in a transaction we relax the isolation property and use message passing for communication. We call the new abstraction a speculation.

We investigate the development of a general-purpose framework for mechanized reasoning about the meta-theory of programming languages. In order to provide a standard, uniform account of a programming language, we propose to define it as a logic in a logical framework, using the same mechanisms for definition, reasoning, and automation that are available to other logics. Then, in order to reason about the language's meta-theory, we use reflection to inject the programming language into (usually richer and more expressive) meta-theory.One of the key features of our approach is that structure of the language is preserved when it is reflected, including variables, meta-variables, and binding structure. This allows the structure of proofs to be preserved as well, and there is a one-to-one map from proof steps in the original programming logic to proof steps in the reflected logic. The act of reflecting a language is automated; all definitions, theorems, and proofs are preserved by the transformation and all the key lemmas (such as proof and structural induction) are automatically derived.The principal representation used by the reflected logic is higher-order abstract syntax (HOAS). However, reasoning about terms in HOAS can be awkward in some cases, especially for variables. For this reason, we define a computationally equivalent variable-free de Bruijn representation that is interchangeable with the HOAS in all contexts. The de Bruijn representation inherits the properties of substitution and alpha-equality from the logical framework, and it is not complicated by administrative issues like variable renumbering.We further develop the concepts and principles of proofs, provability, and structural and proof induction. This work is fully implemented in the MetaPRL theorem prover. We illustrate with an application to F<: as defined in the POPLmark challenge.

This paper presents MojaveFS, a distributed file system with support for sequential consistency. It provides location transparency and makes use of replication for reliability and fault tolerance. We employ a hybrid hash-based and tree-based lookup mechanism for files that, combined with an efficient caching scheme, provides fast access to files in the system. MojaveFS uses a novel data storage strategy where files are split into smaller objects to increase data availability. It also uses a group communication protocol with guarantees for a total order on messages sent within the system, enabling MojaveFS to support the traditional sequential consistency model for concurrent access

This paper presents a kernel level distributed interprocess communication library (KDIPC) with support for distributed shared memory and distributed semaphores. KDIPC uses the System V inter-process communication programming interface and enhances it to provide functionality in distributed environments. A key feature of KDIPC, inherited from System VIPC API, is providing an interface allowing atomic operations on semaphore sets. This permits application developers to perform locking of multiple resources in an atomic manner, simplifies the code and reduces the risk of deadlocks. The implementation is done at the Linux kernel level to reduce the overhead induced by the strict consistency model.

Although building systems from components has attractions, this approach also has problems. Can we be sure that a certain configuration of components is correct? Can it perform as well as a monolithic system? Our paper answers these questions for the Ensemble communication architecture by showing how, with help of the Nuprl formal system, configurations may be checked against specifications, and how optimized code can be synthesized from these configurations. The performance results show that we can substantially reduce end-to-end latency in the already optimized Ensemble system. Finally, we discuss whether the techniques we used are general enough for systems other than communication systems.