"Confluence" - Githubissues

kth-step / abs-metatheory

https://kth-step.github.io/abs-metatheory

MIT License

0 stars 0 forks source link

"Confluence" #5

Open Aqissiaq opened 8 months ago

Aqissiaq commented 8 months ago

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

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

Aqissiaq commented 7 months ago

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 commented 7 months ago

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

ebjohnsen commented 7 months ago

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: @.***>