Abstract machines for game semantics, revisited

TL;DR

This paper introduces new abstract machines based on game semantics, enabling structured compilation for distributed systems, supporting state and concurrency, and demonstrated through a toy distributed compiler for ICA.

Contribution

It defines HRAM and GAM models for game semantics, enabling composition and distributed compilation of languages with state and concurrency.

Findings

HRAMs can represent complex language features

GAMs require HRAM combinators for composition

Distributed ICA compiler is sound and memory-safe

Abstract

We define new abstract machines for game semantics which correspond to networks of conventional computers, and can be used as an intermediate representation for compilation targeting distributed systems. This is achieved in two steps. First we introduce the HRAM, a Heap and Register Abstract Machine, an abstraction of a conventional computer, which can be structured into HRAM nets, an abstract point-to-point network model. HRAMs are multi-threaded and subsume communication by tokens (cf. IAM) or jumps. Game Abstract Machines (GAM), are HRAMs with additional structure at the interface level, but no special operational capabilities. We show that GAMs cannot be naively composed, but composition must be mediated using appropriate HRAM combinators. HRAMs are flexible enough to allow the representation of game models for languages with state (non-innocent games) or concurrency (non-alternating games). We illustrate the potential of this technique by implementing a toy distributed compiler for ICA, a higher-order programming language with shared state concurrency, thus significantly extending our previous distributed PCF compiler. We show that compilation is sound and memory-safe, i.e. no (distributed or local) garbage collection is necessary.