PSM: Policy Synchronised Deterministic Memory
Abstract
Concurrency and determinacy do not go well with each other when resources must be shared. Haskell provides parallel programming abstractions such as IVar and LVar in the Par monad and concurrent abstractions such as MVar and TVar in the in IO and STM monads, respectively. The former are determinate but have no destructive updates and the latter have destructive updates but do not guarantee determinacy. Programming patterns that are both concurrent and determinate, such as those provided by Kahn or Berry require memory abstractions at a higher level than is currently available. In this paper we describe a new type context PSM for policy synchronised memory in Haskell. Like STM and IO, the computations in PSM can access persistent state and, as a side-effect, update the memory in imperative style. Like the Par and IO monads, PSM supports concurrent threads and shared state. However, in contrast to IO, our PSM contexts are race-free since concurrent accesses are policy coordinated which guarantees determinacy.Well-typed transactions in the PSM context can accommodate abstract data structures that are imperative, concurrently shareable and still behave deterministically, by construction.
Keywords
Cite
@article{arxiv.2506.15424,
title = {PSM: Policy Synchronised Deterministic Memory},
author = {Michael Mendler and Marc Pouzet},
journal= {arXiv preprint arXiv:2506.15424},
year = {2025}
}
Comments
This report summarises work on coding the theory of policy-synchronised memory (see https://rdcu.be/erBwl) in Haskell. This was developed for a graduate level course on Functional Reactive Programming taught at Bamberg University by the first author during 2020-2023. An early version of the PSM library had been presented at the SYNCHRON Workshop (Aussois, France), November 2019