Commit 82a9279b authored by Hai Dang's avatar Hai Dang
Browse files

statement for allocating locals

parent 9e4d5d8c
......@@ -124,10 +124,11 @@ Definition access1 (stk: stack) (access: access_kind) (tg: tag) cids
end.
(* Initialize [l, l + n) with singleton stacks of `tg` *)
Definition init_stack (t: tag) : stack := [mkItem Unique t None].
Fixpoint init_stacks α (l:loc) (n:nat) (tg: tag) : stacks :=
match n with
| O => α
| S n => <[l:= [mkItem Unique tg None]]>(init_stacks α (l + 1) n tg)
| S n => <[l:= init_stack tg]>(init_stacks α (l + 1) n tg)
end.
Fixpoint for_each α (l:loc) (n:nat) (dealloc: bool) (f: stack option stack)
......
......@@ -28,14 +28,14 @@ Proof. by rewrite -free_mem_foldr' shift_loc_0. Qed.
Lemma init_stacks_foldr' α l n si (m: nat):
init_stacks α (l + m) n si =
fold_right (λ (i: nat) hi, <[(l + i):=[mkItem Unique si None]]> hi) α (seq m n).
fold_right (λ (i: nat) hi, <[(l + i):= init_stack si]> hi) α (seq m n).
Proof.
revert m. induction n as [|n IHn]; intros m; [done|]. simpl. f_equal.
by rewrite shift_loc_assoc -(Nat2Z.inj_add m 1) Nat.add_1_r IHn.
Qed.
Lemma init_stacks_foldr α l n si:
init_stacks α l n si =
fold_right (λ (i: nat) hi, <[(l + i):=[mkItem Unique si None]]> hi) α (seq 0 n).
fold_right (λ (i: nat) hi, <[(l + i):= init_stack si]> hi) α (seq 0 n).
Proof. by rewrite -init_stacks_foldr' shift_loc_0. Qed.
......@@ -149,7 +149,7 @@ Proof. move => l' s' /init_mem_lookup_case [[//]|//]. Qed.
Lemma init_stacks_lookup α l n t :
( (i: nat), (i < n)%nat
init_stacks α l n t !! (l + i) = Some [mkItem Unique t None])
init_stacks α l n t !! (l + i) = Some (init_stack t))
( (l': loc), ( (i: nat), (i < n)%nat l' l + i)
init_stacks α l n t !! l' = α !! l').
Proof.
......@@ -201,7 +201,7 @@ Lemma init_stacks_lookup_case_2 α l n t :
l' s', α !! l' = Some s'
init_stacks α l n t !! l' = Some s' ( i : nat, (i < n)%nat l' l + i)
i, (0 i < n) l' = l + i
init_stacks α l n t !! l' = Some [mkItem Unique t None].
init_stacks α l n t !! l' = Some $ init_stack t.
Proof.
destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
intros l1 s1 Eq'.
......
......@@ -7,6 +7,24 @@ Set Default Proof Using "Type".
(** MEM STEP -----------------------------------------------------------------*)
Definition res_alloc_local l s stk : resUR :=
(ε, {[ l := to_locStateR (lsLocal s stk)]}).
Lemma sim_body_alloc_local fs ft r n T σs σt Φ :
let l := (fresh_block σt.(shp), 0) in
let t := (Tagged σt.(snp)) in
let σs' := mkState (init_mem l (tsize T) σs.(shp))
(init_stacks σs.(sst) l (tsize T) t) σs.(scs)
(S σs.(snp)) σs.(snc) in
let σt' := mkState (init_mem l (tsize T) σt.(shp))
(init_stacks σt.(sst) l (tsize T) t) σt.(scs)
(S σt.(snp)) σt.(snc) in
let r' : resUR := res_alloc_local l ScPoison (init_stack t) in
Φ (r r') n (PlaceR l t T) σs' (PlaceR l t T) σt' : Prop
r {n,fs,ft} (Alloc T, σs) (Alloc T, σt) : Φ.
Proof.
Admitted.
(** Alloc *)
(*
Lemma sim_body_alloc_shared fs ft r n T σs σt Φ :
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment