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.
Cites work
- An algebra of synchronous atomic steps
- Bisimulation from open maps
- Contextuality in distributed systems
- Developments in concurrent Kleene algebra
- Directed algebraic topology and concurrency. With a foreword by Maurice Herlihy and a preface by Samuel Mimram
- Full abstraction for a shared-variable parallel language
- Generic figures and their glueings. A constructive approach to functor categories
- Generic inference. A unifying theory for automated reasoning
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- scientific article; zbMATH DE number 1945067 (Why is no real title available?)
- scientific article; zbMATH DE number 3796014 (Why is no real title available?)
- scientific article; zbMATH DE number 3297895 (Why is no real title available?)
- Non-locality, contextuality and valuation algebras: a general theory of disagreement
- Ordered valuation algebras: A generic framework for approximating inference
- Sheaf semantics for concurrent interacting objects
- Sheaves in geometry and logic: a first introduction to topos theory
- Time, clocks, and the ordering of events in a distributed system
- Topological signal processing
Cited in
(3)
This page was built for publication: Contextuality in distributed systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6174413)
