PSM: Policy Synchronised Deterministic Memory

TL;DR

The paper introduces PSM, a new Haskell memory abstraction that enables deterministic, concurrent programming with shared state, combining the benefits of existing paradigms while ensuring race-free, policy-coordinated access.

Contribution

It presents PSM, a novel memory context in Haskell that guarantees determinacy and race-free concurrent access through policy synchronization.

Findings

PSM supports deterministic concurrent shared memory in Haskell.

It guarantees race-free access via policy coordination.

PSM accommodates imperative, shareable data structures.

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.