Distributed call-by-value machines

TL;DR

This paper introduces DCESH, a new distributed abstract machine for higher-order programs that supports remote higher-order function calls without code transfer, with formal correctness proofs and a prototype compiler.

Contribution

It presents the design and formal verification of DCESH, a distributed machine supporting higher-order remote procedure calls, extending the CES and CESH machines.

Findings

DCESH supports higher-order remote calls without code transfer.

Formal proofs of correctness for each extension in Agda.

Prototype compiler demonstrating practical implementation.

Abstract

We present a new abstract machine, called DCESH, which describes the execution of higher-order programs running in distributed architectures. DCESH implements a generalised form of Remote Procedure Call that supports calling higher-order functions across node boundaries, without sending actual code. Our starting point is a variant of the SECD machine that we call the CES machine, which implements reduction for untyped call-by-value PCF. We successively add the features that we need for distributed execution and show the correctness of each addition. First we add heaps, forming the CESH machine, which provides features necessary for more efficient execution, and show that there is a bisimulation between the CES and the CESH machine. Then we construct a two-level operational semantics, where the high level is a network of communicating machines, and the low level is given by local machine transitions. Using these networks, we arrive at our final system, the distributed CESH machine (DCESH). We show that there is a bisimulation relation also between the CESH machine and the DCESH machine. All the technical results have been formalised and proved correct in Agda, and a prototype compiler has been developed.