Denotational Semantics for Probabilistic and Concurrent Programs

Abstract

We develop a denotational model for probabilistic and concurrent imperative programs , a class of programs with standard control flow via conditionals and while-loops, as well as probabilistic actions and parallel composition. Whereas the semantics of concurrent programs and of randomized programs are each well studied in isolation, their combination remains poorly understood. The crux of the problem is that interactions between control flow, probabilistic actions, and concurrent execution are not captured by straightforward generalizations of pomsets or convex languages—the prominent models for each effect on its own. Our work introduces the first denotational model for probabilistic concurrent programs with unbounded looping, a major step towards verification of these programs. We prove that the model has good domain-theoretic properties, important for semantics of unbounded loops, as well as two adequacy theorems, showing that the model subsumes typical powerdomain semantics for concurrency and convex powerdomain semantics for probabilistic nondeterminism. We illustrate the reasoning power of the new model with an analysis of the randomized solution to Dijkstra's Dining Philosophers problem, adapted from Lehmann and Rabin.