Event Structures and Causal-Consistent Reversibility

Source: doi:10.1007/3-540-17906-2_31, url:https://github.com/vikraman/event-structures Authors: Vikraman Choudhury Status: verified Main declarations: EventStructures.EventStructure, EventStructures.Conf Tags: concurrency, order-theory, reversible-computation, event-structures MSC: 68Q85, 06A06

Mathematical overview

Formalizes event structures (sets of events with a causal partial order and a binary conflict relation) and several facts about causal-consistent reversibility on them. The development defines configurations, computations, traces and the trace monoid, paths between configurations, rollbacks (maximal configurations omitting a chosen event), and replay (minimal and maximal reconstructions of a configuration compatible with a log), and proves their correctness, uniqueness and causal-safety properties.

References

Prime event structures with binary conflict and their configurations originate in M. Nielsen, G. Plotkin and G. Winskel, Petri nets, event structures and domains, part I, Theoretical Computer Science 13 (1981), 85-108, doi:10.1016/0304-3975(81)90112-2, and are developed further in G. Winskel, Event structures, Advances in Petri Nets 1986, LNCS 255, Springer, 1987, 325-392, doi:10.1007/3-540-17906-2_31. The trace monoid (lists of events up to the congruence generated by swapping adjacent concurrent events) is the free partially commutative monoid of A. Mazurkiewicz, Trace theory, Advances in Petri Nets 1986, LNCS 255, Springer, 1987, 278-324, doi:10.1007/3-540-17906-2_30. The rollback and replay development follows the causal-consistent approach to reversibility introduced by V. Danos and J. Krivine, Reversible communicating systems, CONCUR 2004, LNCS 3170, Springer, 2004, 292-307, doi:10.1007/978-3-540-28644-8_19.

Provenance

Imported from https://github.com/vikraman/event-structures. Upstream is Apache-2.0 licensed and contains no sorrys.