Contextuality in distributed systems

TL;DR

This paper develops a mathematical framework for distributed system specifications using lattice structures, topological models, and information algebras, addressing synchronization issues and introducing a notion of contextuality in correctness.

Contribution

It introduces a new lattice-based model of distributed specifications using simplicial sets, presheaves, and information algebras, linking contextuality to program correctness.

Findings

Model of specifications using simplicial sets and presheaves

Identification of contextuality as a failure of a correctness criterion

Efficient algorithms for verification based on information algebras

Abstract

We present a lattice of distributed program specifications, whose ordering represents implementability/refinement. Specifications are modelled by families of subsets of relative execution traces, which encode the local orderings of state transitions, rather than their absolute timing according to a global clock. This is to overcome fundamental physical difficulties with synchronisation. The lattice of specifications is assembled and analysed with several established mathematical tools. Sets of nondegenerate cells of a simplicial set are used to model relative traces, presheaves model the parametrisation of these traces by a topological space of variables, and information algebras reveal novel constraints on program correctness. The latter aspect brings the enterprise of program specification under the widening umbrella of contextual semantics introduced by Abramsky et al. In this model of program specifications, contextuality manifests as a failure of a consistency criterion comparable to Lamport's definition of sequential consistency. The theory of information algebras also suggests efficient local computation algorithms for the verification of this criterion. The novel constructions in this paper have been verified in the proof assistant Isabelle/HOL.