Commit 22ac7640 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Add a good failure state for allocation failure.

parent 3f472699
......@@ -41,7 +41,7 @@ Definition to_heap : heap → heapUR :=
Definition to_alloc (a : allocation) : allocR :=
to_agree a.
Definition to_allocs : gmap block_id allocation allocsUR :=
Definition to_allocs : gmap alloc_id allocation allocsUR :=
fmap to_alloc.
Definition to_fntbl : gmap loc function fntblUR :=
......@@ -52,7 +52,7 @@ Section definitions.
Implicit Types (st : lock_state) (l : loc) (q : Qp) (b : mbyte).
Definition allocs_entry_def (id : block_id) (a : allocation) : iProp Σ :=
Definition allocs_entry_def (id : alloc_id) (a : allocation) : iProp Σ :=
own heap_allocs_name ( {[ id := to_alloc a ]}).
Definition allocs_entry_aux : seal (@allocs_entry_def). by eexists. Qed.
Definition allocs_entry := unseal allocs_entry_aux.
......@@ -94,19 +94,19 @@ Section definitions.
Definition heap_ctx (h : heap) : iProp Σ :=
(own heap_name ( to_heap h))%I.
Definition allocs_ctx (ub : blocks) : iProp Σ :=
Definition allocs_ctx (ub : allocs) : iProp Σ :=
(own heap_allocs_name ( to_allocs ub))%I.
Definition fntbl_ctx (t : gmap loc function) : iProp Σ :=
(own heap_fntbl_name ( to_fntbl t))%I.
Definition blocks_used_agree (h : heap) (ub : blocks) : Prop :=
Definition blocks_used_agree (h : heap) (ub : allocs) : Prop :=
l, ub !! l.1 = None heap_block_free h l.
Definition state_ctx (σ:state) : iProp Σ :=
blocks_used_agree σ.(st_heap) σ.(st_used_blocks)
blocks_used_agree σ.(st_heap) σ.(st_allocs)
heap_ctx σ.(st_heap)
allocs_ctx σ.(st_used_blocks)
allocs_ctx σ.(st_allocs)
fntbl_ctx σ.(st_fntbl).
End definitions.
......@@ -146,7 +146,7 @@ Section to_heap.
End to_heap.
Section to_allocs.
Implicit Types b : blocks.
Implicit Types b : allocs.
Lemma to_allocs_valid b : to_allocs b.
Proof. intros id. rewrite lookup_fmap. by case (b !! id) => // -[[]?]. Qed.
......@@ -203,11 +203,11 @@ Section blocks_used_agree.
Qed.
Lemma blocks_used_agree_heap_upd_list_in ls vs f ub h:
list_to_set ls.*1 dom (gset block_id) ub
list_to_set ls.*1 dom (gset alloc_id) ub
blocks_used_agree h ub blocks_used_agree (heap_upd_list ls vs f h) ub.
Proof.
move => Hls Hb l Hl. apply heap_block_free_upd_list; first by apply Hb.
assert (l.1 dom (gset block_id) ub); last by set_solver.
assert (l.1 dom (gset alloc_id) ub); last by set_solver.
by rewrite elem_of_dom Hl.
Qed.
End blocks_used_agree.
......@@ -248,7 +248,7 @@ Section allocs.
iIntros (?) "?". rewrite loc_in_bounds_eq/loc_in_bounds_def. iExists _. by iFrame.
Qed.
Lemma allocs_alloc_list (ls : list loc) (vs : list val) (ub : blocks):
Lemma allocs_alloc_list (ls : list loc) (vs : list val) (ub : allocs):
NoDup ls.*1 ->
dom (gset _) ub ## (list_to_set ls.*1)
length vs = length ls
......
......@@ -208,9 +208,9 @@ Declare Scope loc_scope.
Delimit Scope loc_scope with L.
Open Scope loc_scope.
Definition block_id := Z.
Definition alloc_id := Z.
Definition loc : Set := block_id * Z.
Definition loc : Set := alloc_id * Z.
Bind Scope loc_scope with loc.
Inductive mbyte : Set :=
......@@ -231,7 +231,7 @@ Record allocation :=
alloc_end : Z; (* One-past-the-end address. *)
}.
Definition blocks := gmap block_id allocation.
Definition allocs := gmap alloc_id allocation.
......@@ -316,10 +316,15 @@ Record function := {
(* TODO: put both function and bytes in the same heap or make pointers disjoint (current version is wrong)*)
Record state := {
st_heap: heap;
st_used_blocks: blocks;
st_allocs: allocs;
st_fntbl: gmap loc function;
st_alloc_failure: bool;
}.
Definition st_set_alloc_failure (σ : state) : state :=
{| st_heap := σ.(st_heap); st_allocs := σ.(st_allocs);
st_fntbl := σ.(st_fntbl); st_alloc_failure := true; |}.
Record runtime_function := {
(* locations of args and local vars are substitued in the body *)
rf_fn : function;
......@@ -340,13 +345,21 @@ Record continuation := {
Record thread_state := {
ts_rfn: runtime_function;
ts_conts: list continuation;
ts_alloc_failure: bool;
}.
Definition set_alloc_failure (ts : thread_state) : thread_state :=
{| ts_rfn := ts.(ts_rfn); ts_conts := ts.(ts_conts); ts_alloc_failure := true; |}.
Inductive val_or_alloc_failure :=
| VOAF_val (v: val)
| VOAF_fail (s : stmt) (ks: list continuation).
(* values for statements *)
Record stmt_val := {
sv_fn : function;
sv_locs: list (loc * layout);
sv_val: val;
sv_val_or_alloc_failure: val_or_alloc_failure;
}.
Implicit Type (l : loc) (e : expr) (v : val) (sz : nat) (h : heap) (σ : state) (ly : layout) (s : stmt) (sgn : signed) (rf : runtime_function) (ts : thread_state) (co : continuation).
......@@ -556,7 +569,7 @@ Proof. apply Z.divide_add_r. Qed.
Lemma aligned_to_add l (n : nat) x:
(l + x * n) `aligned_to` n l `aligned_to` n.
Proof.
unfold aligned_to. destruct l as [? a] => /=. rewrite Z.add_comm.
unfold aligned_to. destruct l => /=. rewrite Z.add_comm.
split.
- apply: Z.divide_add_cancel_r. by apply Z.divide_mul_r.
- apply Z.divide_add_r. by apply Z.divide_mul_r.
......@@ -565,7 +578,7 @@ Qed.
Lemma aligned_to_mult_eq l n1 n2 off:
l `aligned_to` n2 (l + off) `aligned_to` (n1 * n2) (n2 | off).
Proof.
unfold aligned_to. destruct l as [? a] => /= ??. apply: Z.divide_add_cancel_r => //.
unfold aligned_to. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
apply: (Zdivide_mult_l _ n1). by rewrite Z.mul_comm -Nat2Z.inj_mul.
Qed.
......@@ -575,7 +588,7 @@ Qed.
allocation that contains [l]. Note that we consider the 1-past-the-end
pointer to be in range of an allocation. *)
Definition heap_loc_in_bounds (l : loc) (n : nat) (st : state) : Prop :=
alloc, st.(st_used_blocks) !! l.1 = Some alloc
alloc, st.(st_allocs) !! l.1 = Some alloc
alloc.(alloc_start) l.2
l.2 + n alloc.(alloc_end).
......@@ -617,12 +630,14 @@ Fixpoint heap_free_list ls h : heap :=
Definition update_stmt ts s := {|
ts_conts := ts.(ts_conts);
ts_rfn := {| rf_fn := ts.(ts_rfn).(rf_fn); rf_stmt := s; rf_locs := ts.(ts_rfn).(rf_locs) |};
ts_alloc_failure := ts.(ts_alloc_failure);
|}.
Definition heap_fmap f σ := {|
st_heap := f σ.(st_heap);
st_fntbl := σ.(st_fntbl);
st_used_blocks := σ.(st_used_blocks);
st_allocs := σ.(st_allocs);
st_alloc_failure := σ.(st_alloc_failure);
|}.
Definition to_val (e : expr) : option val :=
......@@ -632,20 +647,36 @@ Definition to_val (e : expr) : option val :=
end.
Definition stmt_to_val (ts : thread_state) : option stmt_val :=
match ts.(ts_rfn).(rf_stmt), ts.(ts_conts) with
| Return (Val v), [] => Some {| sv_fn := ts.(ts_rfn).(rf_fn); sv_locs := ts.(ts_rfn).(rf_locs); sv_val := v |}
| _,_ => None
if ts.(ts_alloc_failure) then
Some {| sv_fn := ts.(ts_rfn).(rf_fn);
sv_locs := ts.(ts_rfn).(rf_locs);
sv_val_or_alloc_failure := VOAF_fail ts.(ts_rfn).(rf_stmt) ts.(ts_conts) |}
else
match ts.(ts_rfn).(rf_stmt), ts.(ts_conts) with
| Return (Val v), [] => Some {| sv_fn := ts.(ts_rfn).(rf_fn);
sv_locs := ts.(ts_rfn).(rf_locs);
sv_val_or_alloc_failure := VOAF_val v |}
| _ , _ => None
end.
Definition stmt_of_val (sv : stmt_val) : thread_state :=
match sv.(sv_val_or_alloc_failure) with
| VOAF_val v => {|
ts_rfn := {| rf_stmt := Return (Val v);
rf_locs := sv.(sv_locs);
rf_fn := sv.(sv_fn); |};
ts_conts := [];
ts_alloc_failure := false;
|}
| VOAF_fail s ks => {|
ts_rfn := {| rf_stmt := s;
rf_locs := sv.(sv_locs);
rf_fn := sv.(sv_fn); |};
ts_conts := ks;
ts_alloc_failure := true;
|}
end.
Definition stmt_of_val (sv : stmt_val) : thread_state := {|
ts_rfn := {| rf_stmt := Return (Val sv.(sv_val));
rf_locs := sv.(sv_locs);
rf_fn := sv.(sv_fn); |};
ts_conts := [];
|}.
(*** Evaluation of operations *)
(** Checks that the location [l] is allocated on the heap [h] *)
Definition valid_ptr l h : Prop :=
......@@ -980,11 +1011,11 @@ Definition to_allocation (off : Z) (len : nat) : allocation :=
Allocation off (off + len).
(*** Evaluation of statements *)
Inductive stmt_step : thread_state state list Empty_set thread_state state list thread_state Prop :=
Inductive simple_stmt_step : thread_state state list Empty_set thread_state state list thread_state Prop :=
| StmtExprS ts σ σ' Ks e e' os efs:
ts.(ts_rfn).(rf_stmt) = stmt_fill Ks e
prim_step e σ os e' σ' efs
stmt_step ts σ os (update_stmt ts (stmt_fill Ks e')) σ' []
simple_stmt_step ts σ os (update_stmt ts (stmt_fill Ks e')) σ' []
| AssignS (o : order) ts σ s v1 v2 l v' ly:
let start_st st := st = if o is Na2Ord then WSt else RSt 0%nat in
let end_st _ := if o is Na1Ord then WSt else RSt 0%nat in
......@@ -994,22 +1025,22 @@ Inductive stmt_step : thread_state → state → list Empty_set → thread_state
val_to_loc v1 = Some l
v2 `has_layout_val` ly
heap_at l ly v' start_st σ.(st_heap)
stmt_step ts σ [] (update_stmt ts end_stmt) (heap_fmap (heap_upd l end_val end_st) σ) []
simple_stmt_step ts σ [] (update_stmt ts end_stmt) (heap_fmap (heap_upd l end_val end_st) σ) []
| SwitchS ts σ v n m bs s def it :
ts.(ts_rfn).(rf_stmt) = Switch it (Val v) m bs def
val_to_int v it = Some n
( i : nat, m !! n = Some i is_Some (bs !! i))
stmt_step ts σ [] (update_stmt ts $ default def (i m !! n; bs !! i)) σ []
simple_stmt_step ts σ [] (update_stmt ts $ default def (i m !! n; bs !! i)) σ []
| GotoS ts σ b s :
ts.(ts_rfn).(rf_stmt) = Goto b
ts.(ts_rfn).(rf_fn).(f_code) !! b = Some s
stmt_step ts σ [] (update_stmt ts s) σ []
simple_stmt_step ts σ [] (update_stmt ts s) σ []
| ReturnS ts σ v co cs:
ts.(ts_rfn).(rf_stmt) = Return (Val v)
ts.(ts_conts) = co :: cs
stmt_step ts σ []
simple_stmt_step ts σ []
(* substitute the return value for rvar *)
(update_stmt {| ts_conts := cs; ts_rfn := co.(c_rfn) |} (subst_stmt [co.(c_rvar)] [v] co.(c_rfn).(rf_stmt)))
(update_stmt {| ts_conts := cs; ts_rfn := co.(c_rfn); ts_alloc_failure := false; |} (subst_stmt [co.(c_rvar)] [v] co.(c_rfn).(rf_stmt)))
(* deallocate the stack *)
(heap_fmap (heap_free_list ts.(ts_rfn).(rf_locs)) σ) []
| CallS lsa lsv ts σ vf vs s co f rf fn fn' h' h'' ret ub':
......@@ -1026,8 +1057,8 @@ Inductive stmt_step : thread_state → state → list Empty_set → thread_state
Forall (heap_block_free σ.(st_heap)) lsa
Forall (heap_block_free σ.(st_heap)) lsv
(* ensure that ls blocks are unused *)
Forall (λ l, σ.(st_used_blocks) !! l.1 = None) lsa
Forall (λ l, σ.(st_used_blocks) !! l.1 = None) lsv
Forall (λ l, σ.(st_allocs) !! l.1 = None) lsa
Forall (λ l, σ.(st_allocs) !! l.1 = None) lsv
(* ensure that locations are aligned *)
Forall2 has_layout_loc lsa fn.(f_args).*2
Forall2 has_layout_loc lsv fn.(f_local_vars).*2
......@@ -1038,35 +1069,56 @@ Inductive stmt_step : thread_state → state → list Empty_set → thread_state
(* initialize the arguments with the supplied values *)
heap_upd_list lsa vs (λ _, RSt 0%nat) h' = h''
(* add used blocks allocations *)
list_to_map (zip (lsa.*1 ++ lsv.*1) (zip_with to_allocation (lsa.*2 ++ lsv.*2) (ly_size <$> (fn.(f_args).*2 ++ fn.(f_local_vars).*2)))) σ.(st_used_blocks) = ub'
list_to_map (zip (lsa.*1 ++ lsv.*1) (zip_with to_allocation (lsa.*2 ++ lsv.*2) (ly_size <$> (fn.(f_args).*2 ++ fn.(f_local_vars).*2)))) σ.(st_allocs) = ub'
rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; rf_stmt := Goto fn'.(f_init); |}
co = {| c_rfn := (update_stmt ts s).(ts_rfn); c_rvar := ret |}
stmt_step ts σ [] {| ts_conts := co::ts.(ts_conts); ts_rfn := rf |}
{| st_heap:= h''; st_fntbl := σ.(st_fntbl); st_used_blocks := ub' |} []
simple_stmt_step ts σ []
{| ts_conts := co::ts.(ts_conts); ts_rfn := rf; ts_alloc_failure := ts.(ts_alloc_failure); |}
{| st_heap:= h''; st_fntbl := σ.(st_fntbl); st_allocs := ub'; st_alloc_failure := σ.(st_alloc_failure); |} []
| CallFailS ts σ vf vs s f fn ret:
ts.(ts_rfn).(rf_stmt) = Call ret (Val vf) (Val <$> vs) s
val_to_loc vf = Some f
σ.(st_fntbl) !! f = Some fn
Forall2 has_layout_val vs fn.(f_args).*2
simple_stmt_step ts σ [] (set_alloc_failure ts) (st_set_alloc_failure σ) []
| SkipSS ts σ s :
ts.(ts_rfn).(rf_stmt) = SkipS s
stmt_step ts σ [] (update_stmt ts s) σ []
simple_stmt_step ts σ [] (update_stmt ts s) σ []
| ExprSS ts σ s v:
ts.(ts_rfn).(rf_stmt) = ExprS (Val v) s
stmt_step ts σ [] (update_stmt ts s) σ []
simple_stmt_step ts σ [] (update_stmt ts s) σ []
(* no rule for StuckS *)
.
Inductive stmt_step : thread_state state list Empty_set thread_state state list thread_state Prop :=
| SStep_ok ts σ os ts' σ' tsl :
ts.(ts_alloc_failure) = false
σ.(st_alloc_failure) = false
simple_stmt_step ts σ os ts' σ' tsl
stmt_step ts σ os ts' σ' tsl
| SStep_fail ts σ os ts' σ' tsl :
σ.(st_alloc_failure) = true
ts.(ts_alloc_failure) = false
simple_stmt_step ts σ os ts' σ' tsl
σ'.(st_alloc_failure) = true
stmt_step ts σ os (set_alloc_failure ts') σ' [].
(*** Language instance for statements *)
Lemma stmt_to_of_val sv : stmt_to_val (stmt_of_val sv) = Some sv.
Proof. move: sv => [???]. by cbn. Qed.
Proof. by move: sv => [??[]]. Qed.
Lemma stmt_of_to_val ts sv : stmt_to_val ts = Some sv stmt_of_val sv = ts.
Proof.
destruct ts as [rf [|??]]; destruct rf as [?? s]; destruct s as [|[] | | | | | |]; cbn => //?.
by simplify_eq.
destruct ts as [rf [|??] []]; destruct rf as [?? s];
destruct s as [|[] | | | | | |]; cbn => //?; by simplify_eq.
Qed.
Lemma stmt_val_stuck ts σ κ ts' σ' efs : stmt_step ts σ κ ts' σ' efs stmt_to_val ts = None.
Proof.
move sv: (stmt_to_val ts) => [] // /stmt_of_to_val <-;
inversion_clear 1; cbn in * => //. destruct Ks => //; simpl in *. simplify_eq.
exfalso. apply: val_irreducible H1. by eexists.
move sv: (stmt_to_val ts) => [] // /stmt_of_to_val <- H. exfalso.
inversion_clear H; destruct sv as [??[]] => //; cbn in *; simplify_eq;
inversion_clear H2; cbn in * => //; destruct Ks => //; simpl in *; simplify_eq;
[ apply: val_irreducible H0 | apply: val_irreducible H1 ]; by eexists.
Qed.
Lemma stmt_lang_mixin : LanguageMixin stmt_of_val stmt_to_val stmt_step.
......@@ -1118,11 +1170,12 @@ Proof. rewrite /offset_loc/shift_loc/=. destruct l => /=. f_equal. lia. Qed.
Lemma offset_loc_sz1 ly l n : ly.(ly_size) = 1%nat l offset{ly} n = l + n.
Proof. rewrite /offset_loc => ->. f_equal. lia. Qed.
(*
Lemma stmt_to_val_non_ret ts s :
(if s is Return (Val v) then False else True) →
stmt_to_val (update_stmt ts s) = None.
Proof. destruct s as [ |e| | | | | |] => //. by destruct e. Qed.
Proof. destruct s as [|e| | | | | |] => //. by destruct e. Qed.
*)
Lemma stmt_fill_inj Ks1 Ks2 e1 e2 :
to_val e1 = None to_val e2 = None stmt_fill Ks1 e1 = stmt_fill Ks2 e2
......@@ -1160,19 +1213,6 @@ Lemma heap_at_inj_val l ly h v v' flk1 flk2:
heap_at l ly v flk1 h heap_at l ly v' flk2 h v = v'.
Proof. move => [_ [Hv1 H1]] [_ [Hv2 H2]]. apply: heap_at_go_inj_val => //. congruence. Qed.
Lemma heap_fresh_blocks n (ub : blocks) lys :
length lys = n
ls, length ls = n Forall (λ l : loc, ub !! l.1 = None) ls NoDup ls.*1 Forall2 has_layout_loc ls lys.
Proof.
eexists ((λ x, (x, 0)) <$> fresh_list n (dom (gset block_id) ub)). split_and!.
- rewrite fmap_length fresh_list_length //.
- apply Forall_forall => l. move => /elem_of_list_fmap[?[->He]]/=.
by apply fresh_list_is_fresh, not_elem_of_dom in He.
- rewrite -list_fmap_compose NoDup_fmap. by apply NoDup_fresh_list.
- rewrite Forall2_fmap_l. apply Forall2_true; last by rewrite fresh_list_length.
move => ?? /=. by apply Z.divide_0_r.
Qed.
Lemma heap_upd_ext h l v f1 f2:
( x, f1 x = f2 x)
heap_upd l v f1 h = heap_upd l v f2 h.
......
This diff is collapsed.
......@@ -564,7 +564,7 @@ Qed.
Ltac inv_stmt_step :=
match goal with
| H : stmt_step (update_stmt _ ?st) _ _ _ _ _ |- _ =>
| H : simple_stmt_step (update_stmt _ ?st) _ _ _ _ _ |- _ =>
inversion H; subst; clear H; simplify_map_eq/=;
match goal with
| H2 : st = ?e2 |- _ =>
......
......@@ -30,12 +30,14 @@ Definition initial_thread_state (main : loc) : thread_state := {|
rf_fn := {| f_args := []; f_local_vars := []; f_init := ""; f_code := |}
|};
ts_conts := [];
ts_alloc_failure := false;
|}.
Definition initial_state (fns : gmap loc function) (gs : gmap loc mbyte) (bs : blocks) :=
Definition initial_state (fns : gmap loc function) (gs : gmap loc mbyte) (bs : allocs) :=
{| st_heap := (λ b, (RSt 0%nat, b) ) <$> gs;
st_fntbl := fns;
st_used_blocks := bs |}.
st_allocs := bs;
st_alloc_failure := false; |}.
Lemma wp_to_typed_stmt `{!typeG Σ} (ts : thread_state) v':
f_code (rf_fn (ts_rfn ts)) =
......@@ -45,16 +47,19 @@ Lemma wp_to_typed_stmt `{!typeG Σ} (ts : thread_state) v':
WP ts {{ v, True }}.
Proof.
rewrite /typed_stmt stmt_wp_unfold -{9}(update_stmt_id ts) => ? Happ /of_to_val Hv. iIntros "Hs".
iApply "Hs" => //. by rewrite Happ. iIntros (v).
iDestruct 1 as ([]) "[% _]". destruct v => //. rewrite -Hv. by iApply wp_value'.
destruct ts.(ts_alloc_failure) eqn:Heq.
- iApply (wp_value _ _ _ _ {| sv_fn := _; sv_locs := _; sv_val_or_alloc_failure := VOAF_fail _ _; |}); last done.
rewrite /update_stmt Heq. done.
- iApply "Hs" => //. by rewrite Happ. iIntros (v).
iDestruct 1 as ([]) "[% _]". destruct v => //. rewrite -Hv. by iApply wp_value'.
Qed.
Definition main_type `{!typeG Σ} (P : iProp Σ) :=
fn( () : (); P) () : (), int i32; True.
(** * The main adequacy lemma *)
Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap loc function) (gs : gmap loc mbyte) (bs : blocks) n t2 σ2 κs:
blocks_used_agree (initial_state fns gs bs).(st_heap) (initial_state fns gs bs).(st_used_blocks)
Lemma refinedc_adequacy Σ `{!typePreG Σ} (thread_mains : list loc) (fns : gmap loc function) (gs : gmap loc mbyte) (bs : allocs) n t2 σ2 κs:
blocks_used_agree (initial_state fns gs bs).(st_heap) (initial_state fns gs bs).(st_allocs)
( {HtypeG : typeG Σ}, gl gt,
let Hglobals : globalG Σ := {| global_locs := gl; global_initialized_types := gt; |} in
([ map] kqsgs, heap_mapsto_mbyte k 1 qs) -
......@@ -120,9 +125,9 @@ Proof.
Qed.
(** * Helper functions for using the adequacy lemma *)
Definition block_to_loc (l: block_id): loc := (l, 0%Z).
Definition block_to_loc (l: alloc_id): loc := (l, 0%Z).
Definition block_list_to_loc (l: block_id): list mbyte gmap loc mbyte :=
Definition block_list_to_loc (l: alloc_id): list mbyte gmap loc mbyte :=
list_to_map imap (λ i b, (block_to_loc l + i, b)).
Lemma block_list_to_loc_nil l :
......@@ -149,19 +154,19 @@ Proof.
apply not_elem_of_list_to_map_1 => /= Hin2. set_solver.
Qed.
Definition heap_list_to_heap : gmap block_id (list mbyte) gmap loc mbyte :=
Definition heap_list_to_heap : gmap alloc_id (list mbyte) gmap loc mbyte :=
map_fold (λ b ls m, block_list_to_loc b ls m) .
Definition heap_list_to_used_blocks : gmap block_id (list mbyte) blocks :=
Definition heap_list_to_allocs : gmap alloc_id (list mbyte) allocs :=
fmap (λ l, to_allocation 0 (length l)).
Lemma heap_list_to_heap_insert `{!refinedcG Σ} l v h :
h !! l = None
([ map] kqs heap_list_to_heap (<[l := v]> h), heap_mapsto_mbyte k 1 qs) -
([ map] kqs heap_list_to_used_blocks (<[l := v]> h), allocs_entry k qs) -
([ map] kqs heap_list_to_allocs (<[l := v]> h), allocs_entry k qs) -
block_to_loc l v
([ map] kqs heap_list_to_heap h, heap_mapsto_mbyte k 1 qs)
([ map] kqs heap_list_to_used_blocks h, allocs_entry k qs).
([ map] kqs heap_list_to_allocs h, allocs_entry k qs).
Proof.
iIntros (HNone) "Hm Ha".
rewrite /heap_list_to_heap map_fold_insert_L //; last by move => *; apply block_list_to_loc_comm.
......@@ -174,7 +179,7 @@ Proof.
apply not_elem_of_list_to_map_1. set_solver.
}
iDestruct "Hm" as "[Hv $]".
rewrite /heap_list_to_used_blocks fmap_insert big_sepM_insert; last by rewrite lookup_fmap HNone.
rewrite /heap_list_to_allocs fmap_insert big_sepM_insert; last by rewrite lookup_fmap HNone.
iDestruct "Ha" as "[Ha $]".
rewrite heap_mapsto_eq/heap_mapsto_def.
iSplitL "Ha". { iApply allocs_entry_to_loc_in_bounds => //. simpl. lia. }
......@@ -186,9 +191,9 @@ Proof.
Qed.
Lemma heap_list_blocks_agree fns gs:
blocks_used_agree (initial_state fns (heap_list_to_heap gs) (heap_list_to_used_blocks gs)).(st_heap) (initial_state fns (heap_list_to_heap gs) (heap_list_to_used_blocks gs)).(st_used_blocks).
blocks_used_agree (initial_state fns (heap_list_to_heap gs) (heap_list_to_allocs gs)).(st_heap) (initial_state fns (heap_list_to_heap gs) (heap_list_to_allocs gs)).(st_allocs).
Proof.
move => /= l. rewrite /heap_list_to_used_blocks lookup_fmap fmap_None. move => Hgs i.
move => /= l. rewrite /heap_list_to_allocs lookup_fmap fmap_None. move => Hgs i.
rewrite lookup_fmap fmap_None /heap_list_to_heap. move: Hgs.
induction gs as [|] using map_ind. { by rewrite map_fold_empty. }
rewrite map_fold_insert_L //; last by move => *; apply block_list_to_loc_comm.
......
......@@ -57,7 +57,7 @@ Section adequate.
loc_main; loc_main2
].
Definition initial_heap : gmap block_id (list mbyte) :=
Definition initial_heap : gmap alloc_id (list mbyte) :=
<[block_allocator_data := replicate (Z.to_nat 10000) MPoison ]> $
<[block_allocator_state := replicate (struct_alloc_state).(ly_size) MPoison ]> $
<[block_initialized := LATCH_INIT ]> $
......@@ -80,7 +80,7 @@ Section adequate.
nsteps (Λ := stmt_lang) n (initial_thread_state <$> [loc_main; loc_main2],
initial_state (fn_lists_to_fns function_locs functions)
(heap_list_to_heap initial_heap)
(heap_list_to_used_blocks initial_heap)) κs (t2, σ2)
(heap_list_to_allocs initial_heap)) κs (t2, σ2)
e2, e2 t2 not_stuck e2 σ2.
Proof.
move => HNDblocks HNDfns.
......
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