Changeset 2745


Ignore:
Timestamp:
Feb 27, 2013, 10:46:05 PM (7 years ago)
Author:
sacerdot
Message:
  1. Complexity of policy computation lowered from O(n2) to O(n)
  2. Computational daemon in compiler.ma implemented
Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2700 r2745  
    2222  match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with
    2323  [ O   ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉
    24   | S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in
     24  | S m ⇒ λp.
     25          let res ≝ pi1 ?? (jump_expansion_internal program m) in
     26          let 〈no_ch,z〉 as p1 ≝ res in
    2527          match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with
    2628          [ None    ⇒ λp2.〈false,None ?〉
    2729          | Some op ⇒ λp2.if no_ch
    28             then pi1 ?? (jump_expansion_internal program m)
     30            then res
    2931            else pi1 ?? (jump_expansion_step program (pi1 ?? labels) «op,?»)
    3032          ] (refl … z)
     
    5557    ]
    5658  ]
    57 | cases (jump_expansion_internal program m) in p1;
     59| whd in match res in p1;
     60  cases (jump_expansion_internal program m) in p1;
    5861  #p cases p -p #p #r cases r normalize nodelta
    5962  [ #_ >p2 #ABS destruct (ABS)
  • src/compiler.ma

    r2724 r2745  
    8282include "ASM/ASMCostsSplit.ma".
    8383
     84(*CSC: move the next definitions, e.g. in BitVectorTrie *)
     85definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
     86 λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.
     87
     88definition strong_decidable: Prop → Type[0] ≝
     89 λP:Prop. P + ¬ P.
     90
     91lemma strong_decidable_in_codomain:
     92 ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
     93  strong_decidable (in_codomain A n m a).
     94 #A #n #m elim m
     95 [ normalize #a' #a inversion (a' == a) #H
     96   [ %1 %{(VEmpty …)} >(\P H) %
     97   | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
     98 | -n #n #L #R #Hl #Hr #a
     99   cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
     100   cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
     101   %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
     102   normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
     103 | #n #A %2 % * #x normalize #abs destruct ]
     104qed.
     105
    84106definition compile : clight_program →
    85107  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
     
    96118    in
    97119  return 〈p, ❬p', k'❭〉.
    98   cases daemon
     120 [ @strong_decidable_in_codomain
     121 | cases daemon ]
    99122qed.
Note: See TracChangeset for help on using the changeset viewer.