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.