We present a generalized committed choice construct for concurrent programs that interact with a shared store. The generalized committed choice (GCC) allows multiple computations from different alternatives to occur concurrently and later commit to one of them. This generalizes the traditional committed choice in Dijkstra’s Guarded Command Language beyond don’t care nondeterminism to also handle don’t know non-determinism. The contribution of the paper is the semantics framework for formalizing GCC. The key challenge is how to handle the notion of commit given that GCC evolves a computation from a single state into many possible co-existing states.
Joxan Jaffar, Roland H. C. Yap, Kenny Qili Zhu