Library Copland.Trace

Traces and their relation to event systems.

Require Import List.
Import List.ListNotations.
Open Scope list_scope.
Require Import Omega Preamble More_lists Term Event_system Term_system.

Shuffles

A trace is a list of events. shuffle merges two traces as is done by parallel execution. The order of events in the traces to be merged does not change, but all other interleavings are allowed.

Inductive shuffle: list Ev → list Ev → list Ev → Prop :=
| shuffle_nil_left: ∀ es, shuffle [] es es
| shuffle_nil_right: ∀ es, shuffle es [] es
| shuffle_left:
    ∀ e es0 es1 es2,
      shuffle es0 es1 es2 →
      shuffle (e :: es0) es1 (e :: es2)
| shuffle_right:
    ∀ e es0 es1 es2,
      shuffle es0 es1 es2 →
      shuffle es0 (e :: es1) (e :: es2).
Hint Constructors shuffle.

Lemma shuffle_length:
  ∀ es0 es1 es2,
    shuffle es0 es1 es2 →
    length es0 + length es1 = length es2.

Lemma shuffle_in_left:
  ∀ e es0 es1 es2,
    shuffle es0 es1 es2 →
    In e es0 →
    In e es2.

Lemma shuffle_in_right:
  ∀ e es0 es1 es2,
    shuffle es0 es1 es2 →
    In e es1 →
    In e es2.

Lemma shuffle_in:
  ∀ e es0 es1 es2,
    shuffle es0 es1 es2 →
    In e es2 ↔ In e es0 ∨ In e es1.

Lemma shuffle_in_skipn_left:
  ∀ i e es0 es1 es2,
    shuffle es0 es1 es2 →
    In e (skipn i es0) →
    In e (skipn i es2).

Lemma shuffle_in_skipn_right:
  ∀ i e es0 es1 es2,
    shuffle es0 es1 es2 →
    In e (skipn i es1) →
    In e (skipn i es2).

Lemma shuffle_earlier_left:
  ∀ es0 es1 es2 e0 e1,
    earlier es0 e0 e1 →
    shuffle es0 es1 es2 →
    earlier es2 e0 e1.

Lemma shuffle_earlier_right:
  ∀ es0 es1 es2 e0 e1,
    earlier es1 e0 e1 →
    shuffle es0 es1 es2 →
    earlier es2 e0 e1.

Lemma shuffle_nodup_append:
  ∀ tr0 tr1 tr2,
    NoDup tr0 → NoDup tr1 →
    disjoint_lists tr0 tr1 →
    shuffle tr0 tr1 tr2 →
    NoDup tr2.

Big-Step Semantics

The traces associated with an annotated term are defined inductively.

Inductive trace: AnnoTerm → Plc → Evidence →
                 list Ev → Prop :=
| tasp: ∀ r x p e,
    trace (aasp r x) p e [(asp_event (fst r) x p e )]
| tatt: ∀ r x p e q tr1,
    trace x q e tr1 →
    trace (aatt r q x) p e
          ((req (fst r) p q e )
             :: tr1 ++
             [(rpy (pred (snd r)) p q (aeval x q e))])
| tlseq: ∀ r x y p e tr0 tr1,
    trace x p e tr0 →
    trace y p (aeval x p e) tr1 →
    trace (alseq r x y) p e (tr0 ++ tr1)
| tbseq: ∀ r s x y p e tr0 tr1,
    trace x p (sp (fst s) e) tr0 →
    trace y p (sp (snd s) e) tr1 →
    trace (abseq r s x y) p e
          ((split (fst r) p e
                  (sp (fst s) e)
                  (sp (snd s) e))
             :: tr0 ++ tr1 ++
             [(join (pred (snd r)) p (aeval x p (sp (fst s) e)) (aeval y p (sp (snd s) e)) (ss (aeval x p (sp (fst s) e)) (aeval y p (sp (snd s) e))))])
| tbpar: ∀ r s x y p e tr0 tr1 tr2,
    trace x p (sp (fst s) e) tr0 →
    trace y p (sp (snd s) e) tr1 →
    shuffle tr0 tr1 tr2 →
    trace (abpar r s x y) p e
          ((split (fst r) p e
                  (sp (fst s) e)
                  (sp (snd s) e))
             :: tr2 ++
             [(join (pred (snd r)) p (aeval x p (sp (fst s) e)) (aeval y p (sp (snd s) e)) (pp (aeval x p (sp (fst s) e)) (aeval y p (sp (snd s) e))))]).
Hint Resolve tasp.

Lemma trace_length:
  ∀ t p e tr,
    trace t p e tr → esize t = length tr.

The events in a trace correspond to the events associated with an annotated term, a place, and some evidence.

Lemma trace_events:
  ∀ t p e tr v,
    well_formed t →
    trace t p e tr →
    In v tr ↔ events t p e v.

Lemma trace_range:
  ∀ t p e tr v,
    well_formed t →
    trace t p e tr →
    In v tr →
    fst (range t) ≤ ev v < snd (range t).

Lemma trace_range_event:
  ∀ t p e tr i,
    well_formed t →
    trace t p e tr →
    fst (range t) ≤ i < snd (range t) →
    ∃ v, In v tr ∧ ev v = i.

Lemma trace_injective_events:
  ∀ t p e tr v0 v1,
    well_formed t →
    trace t p e tr →
    In v0 tr → In v1 tr →
    ev v0 = ev v1 →
    v0 = v1.

Lemma nodup_trace:
  ∀ t p e tr,
    well_formed t →
    trace t p e tr →
    NoDup tr.

Event Systems and Traces

Lemma evsys_tr_in:
  ∀ t p e tr ev0,
    well_formed t →
    trace t p e tr →
    ev_in ev0 (ev_sys t p e) →
    In ev0 tr.

The traces associated with an annotated term are compatible with its event system.

Theorem trace_order:
  ∀ t p e tr ev0 ev1,
    well_formed t →
    trace t p e tr →
    prec (ev_sys t p e) ev0 ev1 →
    earlier tr ev0 ev1.