A straightforward approach to reasoning about concurrent programs is to define their behavior as a set of all possible interleavings of atomic actions of individual threads. However, reasoning in terms of interleavings proves to be too difficult both for humans and computers, because the number of possible interleavings grows rapidly.

Non-interleaving models of concurrency, such as pomset languages and event structures, try to tackle this problem by proposing more compact representations for the set of program behaviors. In recent years there has been renewed interest in non-interleaving concurrency models, for example, in the context of relaxed memory models, model-checking of concurrent programs, and model-based mutation testing.

The goal of this project is to develop a mechanized theory of non-interleaving concurrency models in the Coq Proof Assistant. The library should help interested researchers to formally prove properties of these models and develop new applications of the theory.

Project repository