"Confluence"

[Aqissiaq]

Einar's dream is a specific result about reordering of steps between critical points

• decide on a sufficiently interesting subset of ABS with Einar
• find the statement of of the dream theorem
• formalize a notion of execution/traces
• prove theorem

[Aqissiaq]

The theorem is on page 10 of this paper and reads:

Let G1,G2,G3 be stable configurations and τ1, τ2 traces such that G1 =τ1=> G2 and G1 =τ2=> G3.
If τ2 is in [τ1], then G2 = G3

Where:

• A stable configuration is one where all objects are either blocked or idle.
• Traces consist of events for new objects, remote calls, scheduling, and reading/writing futures.
• [τ1] denotes the set of global traces whose local projection is equal to τ1 for all objects

The paper has a coarse-grained labelled semantics in Fig. 6.

[palmskog]

Great, and I think we can assume this is about finite traces, so we can express them in Coq as regular list event.

[ebjohnsen]

Yes I agree with that! Einar

…

On 7 Feb 2024, at 17:46, Karl Palmskog ***@***.***> wrote: Great, and I think we can assume this is about finite traces, so we can express them in Coq as regular list event. — Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>