Library langs.L2.GCsemantics

A version of L2 semantics that safely drops frames on a non-deterministic basis.

Inductive Error :=

Attempting to apply a null value
Getting stuck
| Wrong : Error
.

Values
Inductive V :=
| NumV : Z V
| BoolV : bool V
| ClosV : list D exp FrameId V
| DefFunV : V V
| RecordV : FrameId V
| NullV : V
| AbortV : Error V
.

Outcomes of auxiliary computations:
Inductive AuxV :=
| UnitAV
| FrameAV : FrameId AuxV
| AbortAV : Error AuxV
| AddrAV : Addr AuxV
.

Definition abort (v: V) :=
  match v with
  | AbortV eAbortV e
  | _AbortV Wrong
  end.

Definition aborta (v: V) :=
  match v with
  | AbortV eAbortAV e
  | _AbortAV Wrong
  end.

Definition good (v: V) :=
  match v with
  | AbortV _False
  | _True
  end.

Checks if a value refers to a frame:
Inductive vrefers' : V FrameId Prop :=
| vr_clos : v xs e f,
              v = ClosV xs e f
              vrefers' v f
| vr_deffun : v v' f,
              v = DefFunV v'
              vrefers' v' f
              vrefers' v f
| vr_record : v f,
              v = RecordV f
              vrefers' v f
.

Instance VR : @VRefers V :=
{ vrefers := vrefers'
}.

Dynamic Semantics


Section DynamicSemantics.

  Context `{G: Graph (@AT T)} `{DVT: DefaultVTyp T V} .

In this version, the "machine state" is augmented with an auxiliary stack of roots that must be preserved by GC.
Inductive eval_exp : H FrameId list FrameId exp V H Prop :=
  | eval_gc_ :
      
The only different transition in this version: safely drop any set of frames outside of the current frame and the auxiliary root stack.
       h0 h1 h2 frm roots s t e v fs,
        safeRemoval h0 fs h1
        ( f, In f fs ¬ In f (frm::roots))
        eval_exp h1 frm roots (E s t e) v h2
        eval_exp h0 frm roots (E s t e) v h2
  | eval_cnum_ :
      
        frm roots z h s t,
        eval_exp h frm roots (E s t (CNum z)) (NumV z) h
  | eval_true_ :
      
        frm roots h s t,
        eval_exp h frm roots (E s t CTrue) (BoolV true) h
  | eval_false_:
      
        frm roots h s t,
        eval_exp h frm roots (E s t CFalse) (BoolV false) h
  | eval_plus_:
      
        frm roots e1 e2 z1 z2 h0 h1 h2 s t
        (EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
        (EVALR: eval_exp h1 frm roots e2 (NumV z2) h2),
        eval_exp h0 frm roots (E s t (Plus e1 e2)) (NumV (z1+z2)%Z) h2
  | eval_plus_b1 :
      
        frm roots e1 e2 h0 v1 h1 s t
        (EVALL: eval_exp h0 frm roots e1 v1 h1)
        (ABORTL: z1, v1 NumV z1),
        eval_exp h0 frm roots (E s t (Plus e1 e2)) (abort v1) h1
  | eval_plus_b2 :
      
        frm roots e1 e2 h0 z1 v2 h1 h2 s t
        (EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
        (EVALR: eval_exp h1 frm roots e2 v2 h2)
        (ABORTR: z2, v2 NumV z2),
        eval_exp h0 frm roots (E s t (Plus e1 e2)) (abort v2) h2
  | eval_gt_:
      
        frm roots e1 e2 z1 z2 h0 h1 h2 s t
        (EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
        (EVALR: eval_exp h1 frm roots e2 (NumV z2) h2),
        eval_exp h0 frm roots (E s t (Gt e1 e2)) (BoolV (Z.gtb z1 z2)) h2
  | eval_gt_b1 :
      
        frm roots e1 e2 h0 v1 h1 s t
        (EVALL: eval_exp h0 frm roots e1 v1 h1)
        (ABORTL: z1, v1 NumV z1),
        eval_exp h0 frm roots (E s t (Gt e1 e2)) (abort v1) h1
  | eval_gt_b2 :
      
        frm roots e1 e2 h0 z1 v2 h1 h2 s t
        (EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
        (EVALR: eval_exp h1 frm roots e2 v2 h2)
        (ABORTR: z2, v2 NumV z2),
        eval_exp h0 frm roots (E s t (Gt e1 e2)) (abort v2) h2
  | eval_lhs_:
      
        frm roots s t lhs h0 h1 ff d v
        (EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
        (GET: getSlot h1 ff d v),
        eval_exp h0 frm roots (E s t (Lhs lhs)) v h1
  | eval_lhs_b1 :
      
        frm roots lhs h0 s t h1 q
        (EVLHS: eval_lhs h0 frm roots lhs (AbortAV q) h1),
        eval_exp h0 frm roots (E s t (Lhs lhs)) (AbortV q) h1
  | eval_lhs_b2 :
      
        frm roots s t lhs h0 h1 ff d
        (EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
        (GET: v, ¬ getSlot h1 ff d v),
        eval_exp h0 frm roots (E s t (Lhs lhs)) (AbortV Wrong) h1
  | eval_fn_ :
      
        frm roots h s t ds e,
        eval_exp h frm roots (E s t (Fn ds e)) (ClosV ds e frm) h
  | eval_app :
      
        frm roots h0 h1 h2 h3 h4 e1 e2s s t vb ff sf f e ds
        (EVAL1: eval_exp h0 frm roots e1 (ClosV ds e ff) h1)
        (SF: scopeofFrame h1 ff sf)
        (NF: initDefault h1 (expScope e) [(P, [(sf, ff)])] f h2)
        (EVAL2: fill_slots_par h2 frm (f::roots) f ds e2s UnitAV h3)
        (EVALBODY: eval_exp h3 f (frm::roots) e vb h4),
        eval_exp h0 frm roots (E s t (App e1 e2s)) vb h4
  | eval_app_dfun :
      
        h0 frm roots h1 s t e1 e2s v
        (EVAL1: eval_exp h0 frm roots e1 (DefFunV v) h1),
        eval_exp h0 frm roots (E s t (App e1 e2s)) v h1
  | eval_app_b1 :
      
        h0 frm roots v1 h1 s t e1 e2s
        (EVAL1: eval_exp h0 frm roots e1 v1 h1)
        (ABORT1: match v1 with
                 | ClosV _ _ _False
                 | DefFunV _False
                 | _True
                 end),
        eval_exp h0 frm roots (E s t (App e1 e2s)) (abort v1) h1
  | eval_app_b2 :
      
        h0 frm roots e1 h1 e2s h2 h3 s t ds e ff sf f q
        (EVAL1: eval_exp h0 frm roots e1 (ClosV ds e ff) h1)
        (SF: scopeofFrame h1 ff sf)
        (NF: initDefault h1 (expScope e) [(P, [(sf, ff)])] f h2)
        (ABORT2: fill_slots_par h2 frm (f::roots) f ds e2s (AbortAV q) h3),
        eval_exp h0 frm roots (E s t (App e1 e2s)) (AbortV q) h3
  
  | eval_letpar_ :
      
        frm roots h0 h1 h2 h3 lb ds es e2 v2 ff sf s t
        (UNZIP: unzipb lb = (ds,es))
        (SF: scopeofFrame h1 frm sf)
        (NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
        (EVAL1: fill_slots_par h1 frm (ff::roots) ff ds es UnitAV h2)
        (EVAL2: eval_exp h2 ff (frm::roots) e2 v2 h3),
        eval_exp h0 frm roots (E s t (LetPar lb e2)) v2 h3
  | eval_letpar_b1 :
      
        frm roots h0 h1 h2 lb ds es e2 s t ff sf q
        (UNZIP : unzipb lb = (ds,es))
        (SF: scopeofFrame h1 frm sf)
        (NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
        (ABORT1: fill_slots_par h1 frm (ff::roots) ff ds es (AbortAV q) h2),
        eval_exp h0 frm roots (E s t (LetPar lb e2)) (AbortV q) h2
  
  | eval_letseq_ :
      
        frm roots h0 h1 h2 lb ds es e2 v2 s t fi
        (UNZIP: unzipb lb = (ds, es))
        
        (EVAL1: fill_slots_seq h0 frm roots ds es (FrameAV fi) h1)
        (EVAL2: eval_exp h1 fi (frm::roots) e2 v2 h2),
        eval_exp h0 frm roots (E s t (LetSeq lb e2)) v2 h2
  | eval_letseq_b1 :
      
        frm roots h0 h1 lb ds es e2 s t q
        (UNZIP: unzipb lb = (ds, es))
        
        (ABORT1 : fill_slots_seq h0 frm roots ds es (AbortAV q) h1),
        eval_exp h0 frm roots (E s t (LetSeq lb e2)) (AbortV q) h1
  
  | eval_letrec_ :
      
        frm roots h0 h1 h2 h3 lvb ds evs e2 v2 ff sf s t
        (UNZIP: unzipb lvb = (ds,evs))
        (SF: scopeofFrame h1 frm sf)
        (NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
        (EVAL1: fill_slots_rec h1 ff (frm::roots) ds evs UnitAV h2)
        (EVAL2: eval_exp h2 ff (frm::roots) e2 v2 h3),
        eval_exp h0 frm roots (E s t (LetRec lvb e2)) v2 h3
  | eval_letrec_b1 :
      
        frm roots h0 h1 h2 lb ds es e2 s t ff sf q
        (UNZIP: unzipb lb = (ds,es))
        (SF: scopeofFrame h1 frm sf)
        (NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
        (ABORT1: fill_slots_rec h1 ff (frm::roots) ds es (AbortAV q) h2),
        eval_exp h0 frm roots (E s t (LetRec lb e2)) (AbortV q) h2
  
  | eval_asgn_ :
      
        h0 frm roots s t lhs e h1 h2 ff d v h3
        (EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
        (EVAL: eval_exp h1 frm (ff::roots) e v h2)
        (SET: setSlot h2 ff d v h3),
        eval_exp h0 frm roots (E s t (Asgn lhs e)) v h3
  | eval_asgn_b1 :
      
        h0 frm roots s t lhs e h1 q
        (EVAL: eval_lhs h0 frm roots lhs (AbortAV q) h1),
        eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV q) h1
  | eval_asgn_b2 :
      
        h0 frm roots s t lhs e h1 ff d q h2
        (EVAL: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
        (ABORT: eval_exp h1 frm (ff::roots) e (AbortV q) h2),
        eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV q) h2
  | eval_asgn_b3 :
      
        h0 frm roots s t lhs e h1 h2 ff d v
        (EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
        (EVAL: eval_exp h1 frm (ff::roots) e v h2)
        (SET: h3, ¬ setSlot h2 ff d v h3),
        eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV Wrong) h2
  | eval_if_t :
      
        frm roots e1 e2 e3 v h0 h1 h2 s t
        (EVAL1: eval_exp h0 frm roots e1 (BoolV true) h1)
        (EVAL2: eval_exp h1 frm roots e2 v h2),
        eval_exp h0 frm roots (E s t (If e1 e2 e3)) v h2
  | eval_if_f :
      
        frm roots e1 e2 e3 v h0 h1 h2 s t
        (EVAL1: eval_exp h0 frm roots e1 (BoolV false) h1)
        (EVAL3: eval_exp h1 frm roots e3 v h2),
        eval_exp h0 frm roots (E s t (If e1 e2 e3)) v h2
  | eval_if_b1:
      
        frm roots e1 e2 e3 h0 h1 v1 s t
        (EVAL1: eval_exp h0 frm roots e1 v1 h1)
        (ABORT1: b, v1 BoolV b),
        eval_exp h0 frm roots (E s t (If e1 e2 e3)) (abort v1) h1
  
  | eval_seq_ :
      
        frm roots e1 e2 v1 v2 h0 h1 h2 s t
        (EVAL1: eval_exp h0 frm roots e1 v1 h1)
        (GOOD1: good v1)
        (EVAL2: eval_exp h1 frm roots e2 v2 h2),
        eval_exp h0 frm roots (E s t (Seq e1 e2)) v2 h2
  | eval_seq_b1 :
      
        frm roots e1 e2 h0 h1 s t q
        (EVAL1: eval_exp h0 frm roots e1 (AbortV q) h1),
        eval_exp h0 frm roots (E s t (Seq e1 e2)) (AbortV q) h1
  
  | eval_new_ :
      
        frm roots r h0 h1 rf s t s0 p s' d'
        (RLOOK: rlookup r p s' d')
        (ASC: assocScope d' s0)
        (RECF: initDefault h0 s0 [] rf h1),
        eval_exp h0 frm roots (E s t (New r)) (RecordV rf) h1
  | eval_new_b1 :
      
        frm roots r h0 s t
        (RLOOK: p s' d' s0, ¬ (rlookup r p s' d' assocScope d' s0)),
        eval_exp h0 frm roots (E s t (New r)) (AbortV Wrong) h0

  with eval_lhs : H FrameId list FrameId lhs AuxV H Prop :=
  | eval_lhs_var_ :
      
        h frm roots r a
        (ADDR: getAddr h frm r a),
        eval_lhs h frm roots (Var r) (AddrAV a) h
  | eval_lhs_var_b :
      
        h frm roots r
        (ADDR: a, ¬ getAddr h frm r a),
        eval_lhs h frm roots (Var r) (AbortAV Wrong) h
  | eval_lhs_field :
      
        h0 frm roots e r s rf scf h1 h2 a sf
        (EVAL: eval_exp h0 frm roots e (RecordV rf) h1)
        (SF: scopeofFrame h1 rf sf)
        (SCF: initDefault h1 s [(I, [(sf, rf)])] scf h2)
        (SCR: scopeofRefP r s)
        (ADDR: getAddr h2 scf r a),
        eval_lhs h0 frm roots (Field e r) (AddrAV a) h2
  | eval_lhs_field_null :
      
        h0 frm roots e r h1
        (EVAL: eval_exp h0 frm roots e NullV h1),
        eval_lhs h0 frm roots (Field e r) (AbortAV NullPointer) h1
  | eval_lhs_field_b1:
      
        h0 frm roots e r h1 v
        (EVAL: eval_exp h0 frm roots e v h1)
        (BAD: match v with
              | RecordV _False
              | NullVFalse
              | _True
              end),
        eval_lhs h0 frm roots (Field e r) (aborta v) h1
  | eval_lhs_field_b2:
      
        h0 frm roots e r s rf scf h1 h2 sf
        (EVAL: eval_exp h0 frm roots e (RecordV rf) h1)
        (SCR: scopeofRefP r s)
        (SF: scopeofFrame h1 rf sf)
        (SCF: initDefault h1 s [(I, [(sf, rf)])] scf h2)
        (ADDR: a, ¬ getAddr h2 scf r a),
        eval_lhs h0 frm roots (Field e r) (AbortAV Wrong) h2

  with fill_slots_par : H FrameId list FrameId FrameId list D list exp AuxV H Prop :=
  | fill_par_nil :
      
        h frm roots fc,
        fill_slots_par h frm roots fc nil nil UnitAV h
  | fill_par_b1 :
      
        h frm roots fc ld,
        ld nil
        fill_slots_par h frm roots fc ld nil (AbortAV Wrong) h
  | fill_par_b2 :
      
        h frm roots fc le,
        le nil
        fill_slots_par h frm roots fc nil le (AbortAV Wrong) h
  | fill_par_cons :
      
        h0 frm roots e d es ds fc v h1 h2 h3 v1
        (EVAL: eval_exp h0 frm roots e v h1)
        (GOOD: good v)
        (SS: setSlot h1 fc d v h2)
        (TAIL: fill_slots_par h2 frm roots fc ds es v1 h3),
        fill_slots_par h0 frm roots fc (d::ds) (e::es) v1 h3
  | fill_par_cons_b1 :
      
        h0 frm roots e es d ds fc h1 q
        (EVAL: eval_exp h0 frm roots e (AbortV q) h1),
        fill_slots_par h0 frm roots fc (d :: ds) (e :: es) (AbortAV q) h1
  | fill_par_cons_b2 :
      
        h0 frm roots e d es ds fc v h1
        (EVAL: eval_exp h0 frm roots e v h1)
        (GOOD: good v)
        (SS: h2, ¬ setSlot h1 fc d v h2),
        fill_slots_par h0 frm roots fc (d::ds) (e::es) (AbortAV Wrong) h1
  

  with fill_slots_seq : H FrameId list FrameId list D list exp AuxV H Prop :=

       

  | fill_seq_nil :
      
        h frm roots,
        fill_slots_seq h frm roots nil nil (FrameAV frm) h
  | fill_seq_b1 :
      
        h frm roots ld,
        ld nil
        fill_slots_seq h frm roots ld nil (AbortAV Wrong) h
  | fill_seq_b2 :
      
        h frm roots le,
        le nil
        fill_slots_seq h frm roots nil le (AbortAV Wrong) h
  | fill_seq_cons :
      
        h0 frm roots e es d ds fc v h1 h2 h3 h4 v1 sd sf
        (SD: scopeofDecl d = Some sd)
        (SF: scopeofFrame h0 frm sf)
        (NF: initDefault h0 sd [(P, [(sf, frm)])] fc h1)
        (EVAL: eval_exp h1 frm (fc::roots) e v h2)
        (GOOD: good v)
        (SS: setSlot h2 fc d v h3)
        (TAIL: fill_slots_seq h3 fc (frm::roots) ds es v1 h4),
        fill_slots_seq h0 frm roots (d :: ds) (e :: es) v1 h4
  | fill_seq_cons_b1 :
      
        h0 frm roots e es d ds h1 sd fc h2 q sf
        (SD: scopeofDecl d = Some sd)
        (SF: scopeofFrame h0 frm sf)
        (NF: initDefault h0 sd [(P, [(sf, frm)])] fc h1)
        (EVAL: eval_exp h1 frm (fc::roots) e (AbortV q) h2),
        fill_slots_seq h0 frm roots (d :: ds) (e :: es) (AbortAV q) h2
  | fill_seq_cons_b2 :
      
        h0 frm roots e es d ds fc v h1 h2 sd sf
        (SD: scopeofDecl d = Some sd)
        (SF: scopeofFrame h0 frm sf)
        (NF: initDefault h0 sd [(P, [(sf, frm)])] fc h1)
        (EVAL: eval_exp h1 frm (fc::roots) e v h2)
        (GOOD: good v)
        (SS: h3, ¬ setSlot h2 fc d v h3),
        fill_slots_seq h0 frm roots (d :: ds) (e :: es) (AbortAV Wrong) h2
  

  with fill_slots_rec : H FrameId list FrameId list D list exp AuxV H Prop :=

       

  | fill_rec_nil :
      
        h frm roots,
        fill_slots_rec h frm roots nil nil UnitAV h
  | fill_rec_b1 :
      
        h frm roots ld,
        ld nil
        fill_slots_rec h frm roots ld nil (AbortAV Wrong) h
  | fill_rec_b2 :
      
        h frm roots le,
        le nil
        fill_slots_rec h frm roots nil le (AbortAV Wrong) h
  | fill_rec_cons :
      
        h0 frm roots e d es ds v h1 h2 h3 v1
        (EVAL: eval_exp h0 frm roots e v h1)
        (GOOD: good v)
        (SS: setSlot h1 frm d v h2)
        (TAIL: fill_slots_rec h2 frm roots ds es v1 h3),
        fill_slots_rec h0 frm roots (d::ds) (e::es) v1 h3
  | fill_rec_cons_b1 :
      
        h0 frm roots e es d ds h1 q
        (EVAL: eval_exp h0 frm roots e (AbortV q) h1),
        fill_slots_rec h0 frm roots (d :: ds) (e :: es) (AbortAV q) h1
  | fill_rec_cons_b2 :
      
        h0 frm roots e d es ds v h1 v1
        (EVAL: eval_exp h0 frm roots e v h1)
        (GOOD: good v)
        (SS: h2, ¬ setSlot h1 frm d v h2),
        fill_slots_rec h0 frm roots (d::ds) (e::es) v1 h1
  
  .

  Scheme eval_exp_ind2 := Minimality for eval_exp Sort Prop
  with eval_lhs_ind2 := Minimality for eval_lhs Sort Prop
  with fill_par_ind2 := Minimality for fill_slots_par Sort Prop
  with fill_seq_ind2 := Minimality for fill_slots_seq Sort Prop
  with fill_rec_ind2 := Minimality for fill_slots_rec Sort Prop.
  Combined Scheme eval_exp_ind3
           from eval_exp_ind2, eval_lhs_ind2, fill_par_ind2, fill_seq_ind2, fill_rec_ind2.

  Inductive eval_prog : prog V Prop :=
  | eval_prog_ :
      e v f h0 h1 rds
      (TOPFRM: initDefault (emptyHeap) (expScope e) [] f h0)
      (EVALB: eval_exp h0 f nil e v h1),
      eval_prog (Prog rds e) v
  .

End DynamicSemantics.