Ein einfacher Ansatz, um über nebenläufige Programme nachzudenken, ist die Definition ihres Verhaltens als eine Menge aller möglichen Verschränkungen von atomaren Aktionen einzelner Threads. Allerdings erweist sich das Denken in Form von Verschränkungen sowohl für Menschen als auch für Computer als zu schwierig, da die Zahl der möglichen Verschränkungen schnell wächst.

Nicht-verschränkende Modelle der Gleichzeitigkeit, wie Pomset-Sprachen und Ereignisstrukturen, versuchen dieses Problem zu lösen, indem sie kompaktere Darstellungen für die Menge der Programmverhaltensweisen vorschlagen. In den letzten Jahren hat das Interesse an nicht-verschränkenden Gleichzeitigkeitsmodellen wieder zugenommen, z. B. im Zusammenhang mit entspannten Speichermodellen, der Modellüberprüfung von Gleichzeitigkeitsprogrammen und modellbasierten Mutationstests.

Das Ziel dieses Projekts ist die Entwicklung einer mechanisierten Theorie von nicht-verschränkenden Gleichzeitigkeitsmodellen im Coq Proof Assistant. Die Bibliothek soll interessierten Forscher*innen dabei helfen, Eigenschaften dieser Modelle formal zu beweisen und neue Anwendungen der Theorie zu entwickeln.

Projekt-Repository