A compositional theory for STM Haskell

9 years 4 months ago
A compositional theory for STM Haskell
We address the problem of reasoning about Haskell programs that use Software Transactional Memory (STM). As a motivating example, we consider Haskell code for a concurrent non-deterministic tree rewriting algorithm implementing the operational semantics of the ambient calculus. The core of our theory is a uniform model, in the spirit of process calculi, of the run-time state of multi-threaded STM Haskell programs. The model was designed to simplify both local and compositional reasoning about STM programs. A single reduction relation captures both pure functional computations and also effectful computations in the STM and I/O monads. We state and prove liveness, soundness, completeness, safety, and termination properties relating source processes and their Haskell implementation. Our proof exploits various ideas from concurrency theory, such as the bisimulation technique, but in the setting of a sed programming language rather than an abstract process calculus. Additionally, we develo...
Johannes Borgström, Karthikeyan Bhargavan, An
Added 28 May 2010
Updated 28 May 2010
Type Conference
Year 2009
Authors Johannes Borgström, Karthikeyan Bhargavan, Andrew D. Gordon
Comments (0)