Toward Denotational Semantics

[eupp]

The aim of this issue is to present the plan to construct a denotational concurrency semantics based on the formalism of stable event structures, and to track the progress in achieving this goal.

I'll present the current vision of this plan in a series of steps. Each major step then will be accompanied by a separate issue where we'll be able to discuss technical details of a specific problem.

• [ ] Stable Event Structures. Define stable event structures and their configurations. Define the binary causality relation on configuration and prove its properties. This is the most straightforward task since we only need to mechanize existing simple theory in Coq [1,2].

• [ ] Synchronization Algebra. The parallel product on labeled stable event structures is defined with respect to synchronization algebra. This algebra decides which events from the parallel process should synchronize. We need to define the synchronization algebra and prove its properties. At this point, we'll need to adjust the theory given in the textbooks for our needs (more details will be posted in the separate issue).

• [ ] Combinators on Stable Event Structures. Define the following combinators on stable event structures: empty structure, unit structure, sum (conflict), sequential product, parallel product. Prove their properties (e.g. associativity, commutativity, etc). Again, we'll need to adjust the theory here.

• [ ] Correspondance between Prime and Stable Event Structures. Use the standard theory [2] to construct an isomorphism between configurations of prime and stable event structures.

• [ ] Denotation Semantics of a simple concurrent language. Define simple imperative language with the parallel composition (IMP) which has the following constructs: atomic instructions (read/writes/updates), conditional (if), sequential composition (;), parallel composition (||). Give a denotational semantics in terms of stable event structures.

Bonus Track!

• [ ] Refinement Relation and Observational Equivalence. Define refinement relation on stable event structures. Define observational refinement on program syntax (via operational semantics). Prove full abstraction (i.e. equivalence of two refinement relations). Use the refinement relation to prove soundness of several program transformations [3].

• [ ] Fixpoint constructions on Stable Event Structures. Prove that stabel event structures form cpo (chain-complete partial order). Use it to define fixpoint operator on stable event structures. Use the fixpoint to give semantics to loops and recursion in the programming language. In the process, we will have to also mechanize the theory of cpos and Kleene fixed-point theorem [4] (or try to find ready to use Coq library).

RFC @volodeyka @dmitromikh @anton-trunov @anlun

[1] Winskel G. Event structures //Advanced Course on Petri Nets. – Springer, Berlin, Heidelberg, 1986. – С. 325-392. link

[2] Winskel G. Event structure semantics for CCS and related languages //International Colloquium on Automata, Languages, and Programming. – Springer, Berlin, Heidelberg, 1982. – С. 561-576. link

[3] Dodds M., Batty M., Gotsman A. Compositional verification of compiler optimisations on relaxed memory //European Symposium on Programming. – Springer, Cham, 2018. – С. 1027-1055. link

[4] Bertot Y., Komendantsky V. Fixed point semantics and partial recursion in Coq //Proceedings of the 10th international ACM SIGPLAN conference on Principles and practice of declarative programming. – 2008. – С. 89-96. link

[eupp]

I've published an RFC w.r.t. synchronization algebras #59

[eupp]

An RFC w.r.t. to stable event structures encoding #60