Ignore:
Timestamp:
May 8, 2013, 4:53:31 PM (7 years ago)
Author:
tranquil
Message:
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Interference.ma

    r3014 r3255  
    55  | decision_colour: Register → decision.
    66
     7definition DeqRegister : DeqSet ≝
     8mk_DeqSet Register eq_Register ?.
     9#x #y % [2: #EQ destruct cases y % ]
     10cases x -x try (cases y -y normalize #EQ destruct %)
     11qed.
     12
     13unification hint 0 ≔ ⊢ Register ≡ carr DeqRegister.
     14
     15definition is_src_of_move :
     16∀globals.joint_statement ERTL globals → vertex → bool ≝
     17λglobals,s,v.
     18match s with
     19[ sequential s _ ⇒
     20  match s with
     21  [ step_seq s ⇒
     22    match s with
     23    [ MOVE pr ⇒
     24      match \snd pr with
     25      [ Reg r ⇒
     26        match r with
     27        [ PSD r ⇒ match v with [ inl r' ⇒ eq_identifier … r r' | _ ⇒ false ]
     28        | HDW r ⇒ match v with [ inr r' ⇒ eq_Register r r' | _ ⇒ false ]
     29        ]
     30      | _ ⇒ false
     31      ]
     32    | _ ⇒ false
     33    ]
     34  | _ ⇒ false
     35  ]
     36| _ ⇒ false
     37].
     38
     39definition interferes_asym :
     40  ∀globals.joint_internal_function ERTL globals →
     41  valuation register_lattice →
     42  label → vertex → vertex → bool ≝
     43λglobals,fn,liveafter,l,v1,v2.
     44match v1 with
     45[ inr R ⇒
     46  match v2 with [ inl _ ⇒ R ∈ RegistersForbidden | _ ⇒ false ]
     47| _ ⇒ false ]
     48
     49match stmt_at … (joint_if_code … fn) l with
     50[ None ⇒ false
     51| Some s ⇒
     52  in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧
     53  ¬is_src_of_move … s v2
     54].
     55
     56definition interferes ≝ λglobals,fn,liveafter,label,v1,v2.
     57interferes_asym globals fn liveafter label v1 v2 ∨
     58interferes_asym globals fn liveafter label v2 v1.
     59
    760(* prop_colouring is the non interferece
    861   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
    962   registers *)
    10 record coloured_graph (before: valuation register_lattice): Type[1] ≝
     63record coloured_graph (interferes : label → vertex → vertex → bool) : Type[1] ≝
    1164{ colouring: vertex → decision
    1265; spilled_no: nat
    13 ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 →
    14   lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2
    15 ; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
    16    ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
     66; prop_colouring: ∀l. ∀v1, v2: vertex.
     67  interferes l v1 v2 → colouring v1 = colouring v2 → v1 = v2
     68; prop_spilled_no: ∀v1:vertex.∀i.colouring v1 = decision_spill i → i < spilled_no
     69; hdw_same_colouring : ∀R.colouring (inr … R) = decision_colour R
    1770}.
    1871
     
    2174  ∀fn:joint_internal_function ERTL globals.
    2275   ∀liveafter.
    23     coloured_graph (livebefore globals fn liveafter).
     76    coloured_graph (interferes … fn liveafter).
Note: See TracChangeset for help on using the changeset viewer.