From 7ef46c778eddf39d4dcb41171b5d094a5b24e390 Mon Sep 17 00:00:00 2001 From: Antonin Reitz Date: Sat, 20 Jul 2024 23:40:24 +0200 Subject: [PATCH] quarantine v4: Slabs{Common,Free} done --- src/SlabsAlloc.fst | 2 + src/SlabsCommon.fst | 373 ++++++++++++++++-------------- src/SlabsFree.fst | 540 +++++++++++++++++++++++++------------------- src/SlotsFree.fsti | 2 +- 4 files changed, 517 insertions(+), 400 deletions(-) diff --git a/src/SlabsAlloc.fst b/src/SlabsAlloc.fst index 28f29b6..7976eaa 100644 --- a/src/SlabsAlloc.fst +++ b/src/SlabsAlloc.fst @@ -2040,6 +2040,8 @@ let allocate_slab_aux_3_3_2_1_aux2 (#opened:_) assert (G.reveal md_as_seq == Seq.create 4 0UL); slab_to_slots size_class (slab_array slab_region (US.add md_count_v (US.sub i 1sz))); empty_md_is_properly_zeroed size_class; + //TODO: QUARANTINEv4 + admit (); intro_slab_vprop size_class (slab_array slab_region (US.add md_count_v (US.sub i 1sz))) (md_bm_array md_bm_region (US.add md_count_v (US.sub i 1sz))) diff --git a/src/SlabsCommon.fst b/src/SlabsCommon.fst index 08f8be1..da1ed95 100644 --- a/src/SlabsCommon.fst +++ b/src/SlabsCommon.fst @@ -64,7 +64,10 @@ open SlotsCommon //TODO let t (size_class: sc) : Type0 = dtuple2 - (x:Seq.lseq U64.t 4{slab_vprop_aux2 size_class x}) + (x:(Seq.lseq U64.t 4 & Seq.lseq U64.t 4){ + slab_vprop_aux2 size_class (fst x) /\ + slab_vprop_aux2 size_class (snd x) + }) (fun _ -> Seq.lseq (G.erased (option (Seq.lseq U8.t (U32.v size_class)))) (U32.v (nb_slots size_class))) & Seq.lseq U8.t (U32.v page_size - US.v (rounding size_class)) @@ -92,129 +95,187 @@ let empty_md_is_properly_zeroed //TODO let empty_t size_class = empty_md_is_properly_zeroed size_class; - ((| Seq.create 4 0UL, Seq.create (U32.v (nb_slots size_class)) (Ghost.hide None) |), Seq.create (U32.v page_size - US.v (rounding size_class)) U8.zero) + ((| (Seq.create 4 0UL, Seq.create 4 0UL), Seq.create (U32.v (nb_slots size_class)) (Ghost.hide None) |), Seq.create (U32.v page_size - US.v (rounding size_class)) U8.zero) #push-options "--z3rlimit 50 --compat_pre_typed_indexed_effects" let p_empty_unpack (#opened:_) (sc: sc) - (b1 b2: blob) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = change_slprop_rel - ((p_empty sc) b1) - (slab_vprop sc (snd b2) (fst b2) - `VR2.vrefine` - (fun ((|s,_|),_) -> is_empty sc s == true)) + (p_empty sc arr md md_q) + (slab_vprop sc arr md md_q + `VR2.vrefine` + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_empty sc (seq_u64_or (fst mds) (snd mds)) == true) + ) (fun x y -> x == y) (fun _ -> ()); VR2.elim_vrefine - (slab_vprop sc (snd b2) (fst b2)) - (fun ((|s,_|),_) -> is_empty sc s == true) + (slab_vprop sc arr md md_q) + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_empty sc (seq_u64_or (fst mds) (snd mds)) == true) let p_partial_unpack (#opened:_) (sc: sc) - (b1 b2: blob) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = change_slprop_rel - ((p_partial sc) b1) - (slab_vprop sc (snd b2) (fst b2) - `VR2.vrefine` - (fun ((|s,_|),_) -> is_partial sc s == true)) + (p_partial sc arr md md_q) + (slab_vprop sc arr md md_q + `VR2.vrefine` + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_partial sc (seq_u64_or (fst mds) (snd mds)) == true) + ) (fun x y -> x == y) (fun _ -> ()); VR2.elim_vrefine - (slab_vprop sc (snd b2) (fst b2)) - (fun ((|s,_|),_) -> is_partial sc s == true) + (slab_vprop sc arr md md_q) + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_partial sc (seq_u64_or (fst mds) (snd mds)) == true) let p_full_unpack (#opened:_) (sc: sc) - (b1 b2: blob) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = change_slprop_rel - ((p_full sc) b1) - (slab_vprop sc (snd b2) (fst b2) - `VR2.vrefine` - (fun ((|s,_|),_) -> is_full sc s == true)) + (p_full sc arr md md_q) + (slab_vprop sc arr md md_q + `VR2.vrefine` + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_full sc (seq_u64_or (fst mds) (snd mds)) == true) + ) (fun x y -> x == y) (fun _ -> ()); VR2.elim_vrefine - (slab_vprop sc (snd b2) (fst b2)) - (fun ((|s,_|),_) -> is_full sc s == true) + (slab_vprop sc arr md md_q) + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_full sc (seq_u64_or (fst mds) (snd mds)) == true) let p_empty_pack (#opened:_) (sc: sc) - (b1 b2: blob) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = VR2.intro_vrefine - (slab_vprop sc (snd b1) (fst b1)) - (fun ((|s,_|),_) -> is_empty sc s == true); + (slab_vprop sc arr md md_q) + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_empty sc (seq_u64_or (fst mds) (snd mds)) == true); change_slprop_rel - (slab_vprop sc (snd b1) (fst b1) - `VR2.vrefine` - (fun ((|s,_|),_) -> is_empty sc s == true)) - ((p_empty sc) b2) + (slab_vprop sc arr md md_q + `VR2.vrefine` + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_empty sc (seq_u64_or (fst mds) (snd mds)) == true) + ) + (p_empty sc arr md md_q) (fun x y -> x == y) (fun _ -> ()) let p_partial_pack (#opened:_) (sc: sc) - (b1 b2: blob) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = VR2.intro_vrefine - (slab_vprop sc (snd b1) (fst b1)) - (fun ((|s,_|),_) -> is_partial sc s == true); + (slab_vprop sc arr md md_q) + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_partial sc (seq_u64_or (fst mds) (snd mds)) == true); change_slprop_rel - (slab_vprop sc (snd b1) (fst b1) - `VR2.vrefine` - (fun ((|s,_|),_) -> is_partial sc s == true)) - ((p_partial sc) b2) + (slab_vprop sc arr md md_q + `VR2.vrefine` + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_partial sc (seq_u64_or (fst mds) (snd mds)) == true) + ) + (p_partial sc arr md md_q) (fun x y -> x == y) (fun _ -> ()) let p_full_pack (#opened:_) (sc: sc) - (b1 b2: blob) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = VR2.intro_vrefine - (slab_vprop sc (snd b1) (fst b1)) - (fun ((|s,_|),_) -> is_full sc s == true); + (slab_vprop sc arr md md_q) + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_full sc (seq_u64_or (fst mds) (snd mds)) == true); change_slprop_rel - (slab_vprop sc (snd b1) (fst b1) - `VR2.vrefine` - (fun ((|s,_|),_) -> is_full sc s == true)) - ((p_full sc) b2) + (slab_vprop sc arr md md_q + `VR2.vrefine` + (fun ((|mds,_|),_) -> + let mds : _ & Seq.lseq U64.t 4 = mds in + is_full sc (seq_u64_or (fst mds) (snd mds)) == true) + ) + (p_full sc arr md md_q) (fun x y -> x == y) (fun _ -> ()) -let p_guard_pack (#opened:_) size_class b +let p_guard_pack (#opened:_) + (sc: sc) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = - intro_vrewrite (guard_slab (snd b) `star` A.varray (fst b)) (fun _ -> empty_t size_class) + intro_vrewrite + (guard_slab arr `star` A.varray md `star` A.varray md_q) + (fun _ -> empty_t sc) -let p_quarantine_pack (#opened:_) size_class b +let p_quarantine_pack (#opened:_) + (sc: sc) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = VR2.intro_vrefine - (quarantine_slab (snd b) `star` A.varray (fst b)) - (fun (_,s) -> s `Seq.equal` Seq.create 4 0UL); + (quarantine_slab arr `star` A.varray md `star` A.varray md_q) + (fun ((_,s),sq) -> + s `Seq.equal` Seq.create 4 0UL /\ + sq `Seq.equal` Seq.create 4 0UL + ); intro_vrewrite - (quarantine_slab (snd b) `star` A.varray (fst b) - `VR2.vrefine` - (fun (_,s) -> s `Seq.equal` Seq.create 4 0UL)) - (fun _ -> empty_t size_class) - -let p_quarantine_unpack (#opened:_) size_class b + ((quarantine_slab arr `star` A.varray md `star` A.varray md_q) + `VR2.vrefine` + (fun ((_,s),sq) -> + s `Seq.equal` Seq.create 4 0UL /\ + sq `Seq.equal` Seq.create 4 0UL + )) + (fun _ -> empty_t sc) + +let p_quarantine_unpack (#opened:_) + (sc: sc) + (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) = elim_vrewrite - (quarantine_slab (snd b) `star` A.varray (fst b) - `VR2.vrefine` - (fun (_,s) -> s `Seq.equal` Seq.create 4 0UL)) - (fun _ -> empty_t size_class); + ((quarantine_slab arr `star` A.varray md `star` A.varray md_q) + `VR2.vrefine` + (fun ((_,s),sq) -> + s `Seq.equal` Seq.create 4 0UL /\ + sq `Seq.equal` Seq.create 4 0UL + )) + (fun _ -> empty_t sc); VR2.elim_vrefine - (quarantine_slab (snd b) `star` A.varray (fst b)) - (fun (_,s) -> s `Seq.equal` Seq.create 4 0UL) + (quarantine_slab arr `star` A.varray md `star` A.varray md_q) + (fun ((_,s),sq) -> + s `Seq.equal` Seq.create 4 0UL /\ + sq `Seq.equal` Seq.create 4 0UL + ) #pop-options #restart-solver - inline_for_extraction noextract let slab_array (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) @@ -332,16 +393,18 @@ let f_lemma (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_count_v: US.t{US.v md_count_v <= US.v metadata_max}) (md_region_lv: Seq.lseq AL.status (US.v md_count_v)) (i: US.t{US.v i < US.v md_count_v}) : Lemma - (t_of (f size_class slab_region md_bm_region md_count_v md_region_lv i) + (t_of (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv i) == t size_class) = slab_vprop_lemma size_class (slab_array slab_region i) (md_bm_array md_bm_region i) + (md_bm_array md_bm_region_q i) #restart-solver @@ -406,6 +469,7 @@ let pack_3 (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) r_idxs @@ -451,21 +515,21 @@ let pack_3 (starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv)) - (f_lemma size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv)) (SeqUtils.init_us_refined (US.v md_count_v))) - (left_vprop2_aux size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv)); + (left_vprop2_aux size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv)); intro_vdep (left_vprop1 md_region r_idxs md_count_v) - (left_vprop2_aux size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv)) - (left_vprop2 size_class slab_region md_bm_region md_region r_idxs md_count_v); + (left_vprop2_aux size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv)) + (left_vprop2 size_class slab_region md_bm_region md_bm_region_q md_region r_idxs md_count_v); intro_vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) - (left_vprop size_class slab_region md_bm_region md_region r_idxs md_count_v) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs md_count_v) #pop-options #restart-solver @@ -474,20 +538,21 @@ let lemma_slab_aux_starseq (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count_v: US.t{US.v md_count_v <= US.v metadata_max}) (md_region_lv: G.erased (Seq.lseq AL.status (US.v md_count_v))) (idx:nat{idx < US.v md_count_v}) (v:AL.status) : Lemma - (let f1 = f size_class slab_region md_bm_region md_count_v md_region_lv in - let f2 = f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) idx v) in + (let f1 = f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv in + let f2 = f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) idx v) in let s = SeqUtils.init_us_refined (US.v md_count_v) in forall (k:nat{k <> idx /\ k < Seq.length s}). f1 (Seq.index s k) == f2 (Seq.index s k)) = - let f1 = f size_class slab_region md_bm_region md_count_v md_region_lv in - let f2 = f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) idx v) in + let f1 = f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv in + let f2 = f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) idx v) in let md_region_lv' = Seq.upd (G.reveal md_region_lv) idx v in let s = SeqUtils.init_us_refined (US.v md_count_v) in let aux (k:nat{k <> idx /\ k < Seq.length s}) @@ -503,6 +568,7 @@ let pack_slab_starseq (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) //(r_idxs: array US.t{A.length r_idxs = 7}) @@ -511,91 +577,56 @@ let pack_slab_starseq (md_region_lv: G.erased (Seq.lseq AL.status (US.v md_count_v))) (idx: US.t{US.v idx < US.v md_count_v}) (v: AL.status) - : SteelGhost unit opened - ( - slab_vprop size_class - (slab_array slab_region idx) - (md_bm_array md_bm_region idx) `star` - (starseq - #(pos:US.t{US.v pos < US.v md_count_v}) - #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) - (Seq.slice (SeqUtils.init_us_refined (US.v md_count_v)) 0 (US.v idx)) `star` - starseq - #(pos:US.t{US.v pos < US.v md_count_v}) - #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) - (Seq.slice (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx + 1) (Seq.length (SeqUtils.init_us_refined (US.v md_count_v))))) - ) - (fun _ -> - starseq - #(pos:US.t{US.v pos < US.v md_count_v}) - #(t size_class) - (f size_class slab_region md_bm_region md_count_v (Seq.upd md_region_lv (US.v idx) v)) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd md_region_lv (US.v idx) v)) - (SeqUtils.init_us_refined (US.v md_count_v)) - ) - (requires fun h0 -> - let md_blob : t_of (slab_vprop size_class - (slab_array slab_region idx) - (md_bm_array md_bm_region idx)) - = h0 (slab_vprop size_class - (slab_array slab_region idx) - (md_bm_array md_bm_region idx)) in - let md : Seq.lseq U64.t 4 = dfst (fst md_blob) in - v <> 4ul /\ v <> 3ul /\ - (v == 2ul ==> is_full size_class md) /\ - (v == 1ul ==> is_partial size_class md) /\ - (v == 0ul ==> is_empty size_class md) /\ - idx <> AL.null_ptr - ) - (ensures fun h0 _ h1 -> True) = SeqUtils.init_us_refined_index (US.v md_count_v) (US.v idx); if (U32.eq v 2ul) then ( p_full_pack size_class - (md_bm_array md_bm_region idx, - slab_array slab_region idx) - (md_bm_array md_bm_region idx, - slab_array slab_region idx); + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx); change_equal_slprop - (p_full size_class (md_bm_array md_bm_region idx, slab_array slab_region idx)) - (f size_class slab_region md_bm_region md_count_v (Seq.upd md_region_lv (US.v idx) v) + (p_full size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd md_region_lv (US.v idx) v) (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx))) ) else if (U32.eq v 1ul) then ( p_partial_pack size_class - (md_bm_array md_bm_region idx, - slab_array slab_region idx) - (md_bm_array md_bm_region idx, - slab_array slab_region idx); + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx); change_equal_slprop - (p_partial size_class (md_bm_array md_bm_region idx, slab_array slab_region idx)) - (f size_class slab_region md_bm_region md_count_v (Seq.upd md_region_lv (US.v idx) v) + (p_partial size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd md_region_lv (US.v idx) v) (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx))) ) else ( p_empty_pack size_class - (md_bm_array md_bm_region idx, - slab_array slab_region idx) - (md_bm_array md_bm_region idx, - slab_array slab_region idx); + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx); change_equal_slprop - (p_empty size_class (md_bm_array md_bm_region idx, slab_array slab_region idx)) - (f size_class slab_region md_bm_region md_count_v (Seq.upd md_region_lv (US.v idx) v) + (p_empty size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd md_region_lv (US.v idx) v) (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx))) ); lemma_slab_aux_starseq size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count_v md_region_lv (US.v idx) v; starseq_upd_pack #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) v)) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) v)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) v)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) v)) (SeqUtils.init_us_refined (US.v md_count_v)) (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx) @@ -619,37 +650,50 @@ let is_empty_and_slab_vprop_aux2_implies_zeroed let upd_and_pack_slab_starseq_quarantine size_class slab_region md_bm_region + md_bm_region_q md_region md_count md_count_v md_region_lv idx = - let md_as_seq = elim_slab_vprop size_class - (md_bm_array md_bm_region idx) (slab_array slab_region idx) in - Helpers.intro_empty_slab_varray size_class md_as_seq (slab_array slab_region idx); + let mds = elim_slab_vprop size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx) in + //TODO: lemma is_empty x||y ==> is_empty x + assume (is_empty size_class (fst mds)); + assume (is_empty size_class (snd mds)); + Helpers.intro_empty_slab_varray size_class (fst mds) (slab_array slab_region idx); mmap_trap_quarantine - (slab_array slab_region idx) - (u32_to_sz page_size); + (slab_array slab_region idx) + (u32_to_sz page_size); SeqUtils.init_us_refined_index (US.v md_count_v) (US.v idx); - is_empty_and_slab_vprop_aux2_implies_zeroed size_class md_as_seq; - p_quarantine_pack size_class (md_bm_array md_bm_region idx, slab_array slab_region idx); + is_empty_and_slab_vprop_aux2_implies_zeroed size_class (fst mds); + is_empty_and_slab_vprop_aux2_implies_zeroed size_class (snd mds); + p_quarantine_pack size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx); change_equal_slprop - (p_quarantine size_class (md_bm_array md_bm_region idx, slab_array slab_region idx)) - (f size_class slab_region md_bm_region md_count_v (Seq.upd md_region_lv (US.v idx) 4ul) + (p_quarantine size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd md_region_lv (US.v idx) 4ul) (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx))); lemma_slab_aux_starseq size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count_v md_region_lv (US.v idx) 4ul; starseq_upd_pack #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) 4ul)) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) 4ul)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) 4ul)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) 4ul)) (SeqUtils.init_us_refined (US.v md_count_v)) (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx) @@ -661,6 +705,7 @@ let pack_right_and_refactor_vrefine_dep (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -670,22 +715,22 @@ let pack_right_and_refactor_vrefine_dep vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) `star` - right_vprop slab_region md_bm_region md_region md_count_v + right_vprop slab_region md_bm_region md_bm_region_q md_region md_count_v ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let blob0 = h0 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob0) (ensures fun h0 _ h1 -> @@ -693,13 +738,13 @@ let pack_right_and_refactor_vrefine_dep = h0 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in let blob1 = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in dfst blob0 == dfst blob1 ) @@ -707,16 +752,16 @@ let pack_right_and_refactor_vrefine_dep let md_count_v' = elim_vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) in + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) in assert (G.reveal md_count_v' == md_count_v); change_equal_slprop - (right_vprop slab_region md_bm_region md_region md_count_v) - (right_vprop slab_region md_bm_region md_region (G.reveal md_count_v')); + (right_vprop slab_region md_bm_region md_bm_region_q md_region md_count_v) + (right_vprop slab_region md_bm_region md_bm_region_q md_region (G.reveal md_count_v')); intro_vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) - (left_vprop size_class slab_region md_bm_region md_region r_idxs (G.reveal md_count_v') `star` - right_vprop slab_region md_bm_region md_region (G.reveal md_count_v')) + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs (G.reveal md_count_v') `star` + right_vprop slab_region md_bm_region md_bm_region_q md_region (G.reveal md_count_v')) #pop-options diff --git a/src/SlabsFree.fst b/src/SlabsFree.fst index 528e33d..7025a19 100644 --- a/src/SlabsFree.fst +++ b/src/SlabsFree.fst @@ -21,7 +21,8 @@ module SM = Steel.Memory open Prelude open Config open Utils2 -open SlotsAlloc + +open SlotsCommon open SlotsFree open SlabsCommon @@ -115,11 +116,11 @@ module FS = FStar.FiniteSet.Base // - idxs.w is the new sz of quarantine list let update_quarantine2_aux (size_class: sc) - (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) - (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + //(slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) + //(md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) - (r_idxs: array US.t{A.length r_idxs = 7}) + //(r_idxs: array US.t{A.length r_idxs = 7}) (md_count_v: US.t{US.v md_count_v <= US.v metadata_max}) (md_region_lv: G.erased (Seq.lseq AL.status (US.v md_count_v))) (idx1 idx2 idx3 idx4 idx5 idx6 idx7: US.t) @@ -282,11 +283,11 @@ let lemma_head1_implies_pred1 (#opened:_) let update_quarantine2 (size_class: sc) - (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) - (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + //(slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) + //(md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) - (r_idxs: array US.t{A.length r_idxs = 7}) + //(r_idxs: array US.t{A.length r_idxs = 7}) (md_count_v: US.t{US.v md_count_v <= US.v metadata_max}) (md_region_lv: G.erased (Seq.lseq AL.status (US.v md_count_v))) (idx1 idx2 idx3 idx4 idx5 idx6 idx7: US.t) @@ -375,7 +376,7 @@ let update_quarantine2 return r ) else ( let idxs = update_quarantine2_aux size_class - slab_region md_bm_region md_region md_count r_idxs + md_region md_count md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 in return idxs @@ -385,6 +386,7 @@ let update_quarantine3_aux (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -397,16 +399,16 @@ let update_quarantine3_aux starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun md_region_lv' -> starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv') - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv') + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv') + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv') (SeqUtils.init_us_refined (US.v md_count_v)) ) (requires fun _ -> @@ -425,26 +427,35 @@ let update_quarantine3_aux #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx); SeqUtils.init_us_refined_index (US.v md_count_v) (US.v idx); (**) change_equal_slprop - (f size_class slab_region md_bm_region md_count_v md_region_lv + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v idx))) - (p_quarantine size_class (md_bm_array md_bm_region idx, slab_array slab_region idx)); - p_quarantine_unpack size_class (md_bm_array md_bm_region idx, slab_array slab_region idx); + (p_quarantine size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx)); + p_quarantine_unpack size_class + (slab_array slab_region idx) + (md_bm_array md_bm_region idx) + (md_bm_array md_bm_region_q idx); let md = gget (A.varray (md_bm_array md_bm_region idx)) in empty_md_is_properly_zeroed size_class; Quarantine.mmap_untrap_quarantine (slab_array slab_region idx) (u32_to_sz page_size); Helpers.slab_to_slots size_class (slab_array slab_region idx); + //TODO: quarantinev4 + admit (); intro_slab_vprop size_class + (slab_array slab_region idx) (md_bm_array md_bm_region idx) - (Seq.create 4 0UL) - (slab_array slab_region idx); + (md_bm_array md_bm_region_q idx) + (Seq.create 4 0UL); pack_slab_starseq size_class - slab_region md_bm_region md_region md_count + slab_region md_bm_region md_bm_region_q md_region md_count md_count_v md_region_lv idx 0ul; @@ -453,12 +464,12 @@ let update_quarantine3_aux #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) 0ul)) - (f size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv')) - (f_lemma size_class slab_region md_bm_region md_count_v + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv')) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v idx) 0ul)) - (f_lemma size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv')) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv')) (SeqUtils.init_us_refined (US.v md_count_v)) (SeqUtils.init_us_refined (US.v md_count_v)); md_region_lv' @@ -467,6 +478,7 @@ let update_quarantine3 (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -479,16 +491,16 @@ let update_quarantine3 starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun md_region_lv' -> starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv') - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv') + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv') + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv') (SeqUtils.init_us_refined (US.v md_count_v)) ) (requires fun _ -> @@ -516,51 +528,56 @@ let update_quarantine3 #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f size_class slab_region md_bm_region md_count_v md_region_lv') - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv') + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv') + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv') (SeqUtils.init_us_refined (US.v md_count_v)) (SeqUtils.init_us_refined (US.v md_count_v)); return md_region_lv' ) else ( let md_region_lv' = update_quarantine3_aux size_class - slab_region md_bm_region md_region md_count r_idxs + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 idxs in return md_region_lv' ) +#pop-options #push-options "--z3rlimit 75 --compat_pre_typed_indexed_effects" inline_for_extraction noextract let deallocate_slab_aux_cond (size_class: sc) - (md: slab_metadata) (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) : Steel bool - (slab_vprop size_class arr md) - (fun _ -> slab_vprop size_class arr md) + (slab_vprop size_class arr md md_q) + (fun _ -> slab_vprop size_class arr md md_q) (requires fun _ -> True) (ensures fun h0 r h1 -> let blob0 - : t_of (slab_vprop size_class arr md) - = h0 (slab_vprop size_class arr md) in + : t_of (slab_vprop size_class arr md md_q) + = h0 (slab_vprop size_class arr md md_q) in let blob1 - : t_of (slab_vprop size_class arr md) - = h1 (slab_vprop size_class arr md) in - let v0 : Seq.lseq U64.t 4 = dfst (fst blob0) in + : t_of (slab_vprop size_class arr md md_q) + = h1 (slab_vprop size_class arr md md_q) in + let mds : _ & Seq.lseq U64.t 4 = dfst (fst blob0) in dfst (fst blob0) == dfst (fst blob1) /\ dsnd (fst blob0) == dsnd (fst blob1) /\ blob0 == blob1 /\ - r == is_empty size_class v0 + r == is_empty size_class (seq_u64_or (fst mds) (snd mds)) ) = + admit (); assert (t_of (A.varray md) == Seq.lseq U64.t 4); - let md_as_seq : G.erased (Seq.lseq U64.t 4) - = elim_slab_vprop size_class md arr in + let mds : G.erased (Seq.lseq U64.t 4 & Seq.lseq U64.t 4) + = elim_slab_vprop size_class arr md md_q in let r = is_empty_s size_class md in - intro_slab_vprop size_class md md_as_seq arr; + intro_slab_vprop size_class arr md md_q (fst mds); return r +#pop-options + +#push-options "--fuel 1 --ifuel 1 --z3rlimit 100" module FS = FStar.FiniteSet.Base @@ -570,6 +587,7 @@ let deallocate_slab_aux_1_partial (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -587,15 +605,15 @@ let deallocate_slab_aux_1_partial starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -620,7 +638,7 @@ let deallocate_slab_aux_1_partial = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = @@ -655,7 +673,7 @@ let deallocate_slab_aux_1_partial ALG.ptrs_all #AL.status (US.v idx1) (US.v pos) (US.v idx3') (US.v idx4) (US.v idx5) gs1); //assert (ALG.partition #AL.status gs1 (US.v idx1) (US.v pos) (US.v idx3')); - (**) pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + (**) pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v (G.hide (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) idx1 pos idx3' idx4 idx5 idx6 idx7 @@ -665,6 +683,7 @@ let deallocate_slab_aux_1_empty (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -682,15 +701,15 @@ let deallocate_slab_aux_1_empty starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -715,7 +734,7 @@ let deallocate_slab_aux_1_empty = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = @@ -749,7 +768,7 @@ let deallocate_slab_aux_1_empty assert (ALG.ptrs_all #AL.status (US.v idx1) (US.v idx2) (US.v idx3) (US.v idx4) (US.v idx5) gs0 `FStar.FiniteSet.Base.equal` ALG.ptrs_all #AL.status (US.v pos) (US.v idx2) (US.v idx3') (US.v idx4) (US.v idx5) gs1); - (**) pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + (**) pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v (G.hide (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) pos idx2 idx3' idx4 idx5 idx6 idx7 @@ -761,6 +780,7 @@ let deallocate_slab_aux_1_fail (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -772,7 +792,8 @@ let deallocate_slab_aux_1_fail ( slab_vprop size_class (slab_array slab_region pos) - (md_bm_array md_bm_region pos) `star` + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos) `star` (vptr md_count `star` A.varray r_idxs `star` (AL.varraylist pred1 pred2 pred3 pred4 pred5 @@ -781,21 +802,21 @@ let deallocate_slab_aux_1_fail starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (Seq.slice (SeqUtils.init_us_refined (US.v md_count_v)) 0 (US.v pos)) `star` starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (Seq.slice (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos + 1) (Seq.length (SeqUtils.init_us_refined (US.v md_count_v))))) ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -803,13 +824,15 @@ let deallocate_slab_aux_1_fail (US.v idx1) (US.v idx2) (US.v idx3) (US.v idx4) (US.v idx5) (US.v idx6) (US.v idx7) h0 in let md_blob : t_of (slab_vprop size_class (slab_array slab_region pos) - (md_bm_array md_bm_region pos)) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)) = h0 (slab_vprop size_class (slab_array slab_region pos) - (md_bm_array md_bm_region pos)) in - let md : Seq.lseq U64.t 4 = dfst (fst md_blob) in + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)) in + let mds : _ & Seq.lseq U64.t 4 = dfst (fst md_blob) in let idxs0 = A.asel r_idxs h0 in - is_full size_class md /\ + is_full size_class (seq_u64_or (fst mds) (snd mds)) /\ US.v md_count_v <> AL.null /\ sel md_count h0 == md_count_v /\ Seq.index idxs0 0 == idx1 /\ @@ -828,26 +851,30 @@ let deallocate_slab_aux_1_fail = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = p_full_pack size_class - (md_bm_array md_bm_region pos, slab_array slab_region pos) - (md_bm_array md_bm_region pos, slab_array slab_region pos); + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos); SeqUtils.init_us_refined_index (US.v md_count_v) (US.v pos); change_equal_slprop - (p_full size_class (md_bm_array md_bm_region pos, slab_array slab_region pos)) - (f size_class slab_region md_bm_region md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))); + (p_full size_class + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))); starseq_pack_s #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos); - pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 @@ -860,6 +887,7 @@ let deallocate_slab_aux_1_quarantine (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -877,15 +905,15 @@ let deallocate_slab_aux_1_quarantine starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -910,7 +938,7 @@ let deallocate_slab_aux_1_quarantine = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = @@ -920,8 +948,8 @@ let deallocate_slab_aux_1_quarantine // Ensuring the quarantine is not full by dequeuing if needed let idxs = update_quarantine2 size_class - slab_region md_bm_region md_region - md_count r_idxs md_count_v md_region_lv + md_region + md_count md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 in assert (pos <> idxs.x); @@ -954,7 +982,7 @@ let deallocate_slab_aux_1_quarantine ALG.ptrs_all #AL.status (US.v idxs.x) (US.v idx2) (US.v idx3') (US.v idx4) (US.v pos) gs2); let md_region_lv' = update_quarantine3 size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul) idx1 idx2 idx3 idx4 idx5 idx6 idx7 @@ -972,7 +1000,7 @@ let deallocate_slab_aux_1_quarantine let gs_idxs1 : G.erased (Seq.lseq US.t 7) = gget (A.varray r_idxs) in - (**) pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + (**) pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv' idxs.x idx2 idx3' idx4 pos idxs'.x idxs'.y @@ -982,13 +1010,14 @@ let deallocate_slab_aux_1_quarantine open Quarantine // Slab initially full -#push-options "--compat_pre_typed_indexed_effects --z3rlimit 100" +#push-options "--compat_pre_typed_indexed_effects --z3rlimit 150" inline_for_extraction noextract let deallocate_slab_aux_1 (ptr: array U8.t) (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1008,8 +1037,8 @@ let deallocate_slab_aux_1 starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun b -> @@ -1017,7 +1046,7 @@ let deallocate_slab_aux_1 vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1050,64 +1079,77 @@ let deallocate_slab_aux_1 = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = - (**) starseq_unpack_s + (**)starseq_unpack_s #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos); (**) SeqUtils.init_us_refined_index (US.v md_count_v) (US.v pos); (**) change_equal_slprop - (f size_class slab_region md_bm_region md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))) - (p_full size_class (md_bm_array md_bm_region pos, slab_array slab_region pos)); + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))) + (p_full size_class + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)); (**) p_full_unpack size_class - (md_bm_array md_bm_region pos, slab_array slab_region pos) - (md_bm_array md_bm_region pos, slab_array slab_region pos); + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos); let b = deallocate_slot size_class - (md_bm_array md_bm_region pos) (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos) ptr pos2 in if b then ( - // deallocation success, slab no longer full - let cond = deallocate_slab_aux_cond size_class - (md_bm_array md_bm_region pos) - (slab_array slab_region pos) in - if cond then ( - if enable_quarantine then ( - upd_and_pack_slab_starseq_quarantine size_class - slab_region md_bm_region md_region md_count - md_count_v md_region_lv pos; - deallocate_slab_aux_1_quarantine size_class - slab_region md_bm_region md_region md_count r_idxs - md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; - return b + if enable_quarantine_slot then ( + sladmit (); + return true + ) else ( + // deallocation success, slab no longer full + let cond = deallocate_slab_aux_cond size_class + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos) in + if cond then ( + if enable_quarantine then ( + upd_and_pack_slab_starseq_quarantine size_class + slab_region md_bm_region md_bm_region_q md_region md_count + md_count_v md_region_lv pos; + deallocate_slab_aux_1_quarantine size_class + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs + md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; + return b + ) else ( + pack_slab_starseq size_class + slab_region md_bm_region md_bm_region_q md_region md_count + md_count_v md_region_lv pos 0ul; + deallocate_slab_aux_1_empty size_class + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs + md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; + return b + ) ) else ( + admit (); pack_slab_starseq size_class - slab_region md_bm_region md_region md_count - md_count_v md_region_lv pos 0ul; - deallocate_slab_aux_1_empty size_class - slab_region md_bm_region md_region md_count r_idxs + slab_region md_bm_region md_bm_region_q md_region md_count + md_count_v md_region_lv pos 1ul; + deallocate_slab_aux_1_partial size_class + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; return b ) - ) else ( - pack_slab_starseq size_class - slab_region md_bm_region md_region md_count - md_count_v md_region_lv pos 1ul; - deallocate_slab_aux_1_partial size_class - slab_region md_bm_region md_region md_count r_idxs - md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; - return b ) ) else ( + admit (); deallocate_slab_aux_1_fail size_class - slab_region md_bm_region md_region md_count r_idxs + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; return b ) @@ -1119,6 +1161,7 @@ let deallocate_slab_aux_2_empty (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1136,15 +1179,15 @@ let deallocate_slab_aux_2_empty starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1169,7 +1212,7 @@ let deallocate_slab_aux_2_empty = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = @@ -1203,7 +1246,7 @@ let deallocate_slab_aux_2_empty assert (ALG.ptrs_all #AL.status (US.v idx1) (US.v idx2) (US.v idx3) (US.v idx4) (US.v idx5) gs0 `FStar.FiniteSet.Base.equal` ALG.ptrs_all #AL.status (US.v pos) (US.v idx2') (US.v idx3) (US.v idx4) (US.v idx5) gs1); - (**) pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + (**) pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v (G.hide (Seq.upd (G.reveal md_region_lv) (US.v pos) 0ul)) pos idx2' idx3 idx4 idx5 idx6 idx7 @@ -1215,6 +1258,7 @@ let deallocate_slab_aux_2_partial (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1232,15 +1276,15 @@ let deallocate_slab_aux_2_partial starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv)) - (f_lemma size_class slab_region md_bm_region md_count_v (G.reveal md_region_lv)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (G.reveal md_region_lv)) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1265,11 +1309,11 @@ let deallocate_slab_aux_2_partial = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = - (**) pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + (**) pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 @@ -1279,6 +1323,7 @@ let deallocate_slab_aux_2_fail (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1290,7 +1335,8 @@ let deallocate_slab_aux_2_fail ( slab_vprop size_class (slab_array slab_region pos) - (md_bm_array md_bm_region pos) `star` + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos) `star` (vptr md_count `star` A.varray r_idxs `star` (AL.varraylist pred1 pred2 pred3 pred4 pred5 @@ -1299,14 +1345,14 @@ let deallocate_slab_aux_2_fail starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (Seq.slice (SeqUtils.init_us_refined (US.v md_count_v)) 0 (US.v pos)) `star` starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (Seq.slice (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos + 1) (Seq.length (SeqUtils.init_us_refined (US.v md_count_v))))) ) @@ -1314,7 +1360,7 @@ let deallocate_slab_aux_2_fail vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1322,13 +1368,15 @@ let deallocate_slab_aux_2_fail (US.v idx1) (US.v idx2) (US.v idx3) (US.v idx4) (US.v idx5) (US.v idx6) (US.v idx7) h0 in let md_blob : t_of (slab_vprop size_class (slab_array slab_region pos) - (md_bm_array md_bm_region pos)) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)) = h0 (slab_vprop size_class (slab_array slab_region pos) - (md_bm_array md_bm_region pos)) in - let md : Seq.lseq U64.t 4 = dfst (fst md_blob) in + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)) in + let mds : _ & Seq.lseq U64.t 4 = dfst (fst md_blob) in let idxs0 = A.asel r_idxs h0 in - is_partial size_class md /\ + is_partial size_class (seq_u64_or (fst mds) (snd mds)) /\ US.v md_count_v <> AL.null /\ sel md_count h0 == md_count_v /\ Seq.index idxs0 0 == idx1 /\ @@ -1347,26 +1395,30 @@ let deallocate_slab_aux_2_fail = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = p_partial_pack size_class - (md_bm_array md_bm_region pos, slab_array slab_region pos) - (md_bm_array md_bm_region pos, slab_array slab_region pos); + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos); SeqUtils.init_us_refined_index (US.v md_count_v) (US.v pos); change_equal_slprop - (p_partial size_class (md_bm_array md_bm_region pos, slab_array slab_region pos)) - (f size_class slab_region md_bm_region md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))); + (p_partial size_class + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))); starseq_pack_s #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos); - pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 @@ -1378,6 +1430,7 @@ let deallocate_slab_aux_2_quarantine (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1395,15 +1448,15 @@ let deallocate_slab_aux_2_quarantine starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul)) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun _ -> vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1428,7 +1481,7 @@ let deallocate_slab_aux_2_quarantine = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = @@ -1438,8 +1491,8 @@ let deallocate_slab_aux_2_quarantine // Ensuring the quarantine is not full by dequeuing if needed let idxs = update_quarantine2 size_class - slab_region md_bm_region md_region - md_count r_idxs md_count_v md_region_lv + md_region + md_count md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 in assert (pos <> idxs.x); @@ -1471,7 +1524,7 @@ let deallocate_slab_aux_2_quarantine ALG.ptrs_all #AL.status (US.v idxs.x) (US.v idx2') (US.v idx3) (US.v idx4) (US.v pos) gs2); let md_region_lv' = update_quarantine3 size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 4ul) idx1 idx2 idx3 idx4 idx5 idx6 idx7 @@ -1489,7 +1542,7 @@ let deallocate_slab_aux_2_quarantine let gs_idxs1 : G.erased (Seq.lseq US.t 7) = gget (A.varray r_idxs) in - (**) pack_3 size_class slab_region md_bm_region md_region md_count r_idxs + (**) pack_3 size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv' idxs.x idx2' idx3 idx4 pos idxs'.x idxs'.y @@ -1504,6 +1557,7 @@ let deallocate_slab_aux_2 (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1523,8 +1577,8 @@ let deallocate_slab_aux_2 starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun b -> @@ -1532,7 +1586,7 @@ let deallocate_slab_aux_2 vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1565,7 +1619,7 @@ let deallocate_slab_aux_2 = h1 (vrefinedep (vptr md_count) vrefinedep_prop - (left_vprop size_class slab_region md_bm_region md_region r_idxs) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) in md_count_v == dfst blob1) = @@ -1573,67 +1627,80 @@ let deallocate_slab_aux_2 #_ #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos); (**) SeqUtils.init_us_refined_index (US.v md_count_v) (US.v pos); (**) change_equal_slprop - (f size_class slab_region md_bm_region md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))) - (p_partial size_class (md_bm_array md_bm_region pos, slab_array slab_region pos)); + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv (Seq.index (SeqUtils.init_us_refined (US.v md_count_v)) (US.v pos))) + (p_partial size_class + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos)); (**) p_partial_unpack size_class - (md_bm_array md_bm_region pos, slab_array slab_region pos) - (md_bm_array md_bm_region pos, slab_array slab_region pos); + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos); let b = deallocate_slot size_class - (md_bm_array md_bm_region pos) (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos) ptr pos2 in if b then ( - // deallocation success, slab no longer full - let cond = deallocate_slab_aux_cond size_class - (md_bm_array md_bm_region pos) - (slab_array slab_region pos) in - if cond then ( - if enable_quarantine then ( - upd_and_pack_slab_starseq_quarantine size_class - slab_region md_bm_region md_region md_count - md_count_v md_region_lv pos; - deallocate_slab_aux_2_quarantine size_class - slab_region md_bm_region md_region md_count r_idxs - md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; - return b + if enable_quarantine_slot then ( + sladmit (); + return true + ) else ( + // deallocation success, slab no longer full + let cond = deallocate_slab_aux_cond size_class + (slab_array slab_region pos) + (md_bm_array md_bm_region pos) + (md_bm_array md_bm_region_q pos) in + if cond then ( + if enable_quarantine then ( + upd_and_pack_slab_starseq_quarantine size_class + slab_region md_bm_region md_bm_region_q md_region md_count + md_count_v md_region_lv pos; + deallocate_slab_aux_2_quarantine size_class + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs + md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; + return b + ) else ( + (**) pack_slab_starseq size_class + slab_region md_bm_region md_bm_region_q md_region md_count + md_count_v md_region_lv pos 0ul; + deallocate_slab_aux_2_empty size_class + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs + md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; + return b + ) ) else ( + admit (); (**) pack_slab_starseq size_class - slab_region md_bm_region md_region md_count - md_count_v md_region_lv pos 0ul; - deallocate_slab_aux_2_empty size_class - slab_region md_bm_region md_region md_count r_idxs + slab_region md_bm_region md_bm_region_q md_region md_count + md_count_v md_region_lv pos 1ul; + assert (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul `Seq.equal` md_region_lv); + (**) starseq_weakening + #_ + #(pos:US.t{US.v pos < US.v md_count_v}) + #(t size_class) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (SeqUtils.init_us_refined (US.v md_count_v)) + (SeqUtils.init_us_refined (US.v md_count_v)); + deallocate_slab_aux_2_partial size_class + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; return b ) - ) else ( - (**) pack_slab_starseq size_class - slab_region md_bm_region md_region md_count - md_count_v md_region_lv pos 1ul; - assert (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul `Seq.equal` md_region_lv); - (**) starseq_weakening - #_ - #(pos:US.t{US.v pos < US.v md_count_v}) - #(t size_class) - (f size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v (Seq.upd (G.reveal md_region_lv) (US.v pos) 1ul)) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) - (SeqUtils.init_us_refined (US.v md_count_v)) - (SeqUtils.init_us_refined (US.v md_count_v)); - deallocate_slab_aux_2_partial size_class - slab_region md_bm_region md_region md_count r_idxs - md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; - return b ) ) else ( + admit (); deallocate_slab_aux_2_fail size_class - slab_region md_bm_region md_region md_count r_idxs + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos; return b ) @@ -1647,6 +1714,7 @@ let deallocate_slab_fail (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1658,15 +1726,15 @@ let deallocate_slab_fail A.varray ptr `star` vptr md_count `star` A.varray r_idxs `star` - right_vprop slab_region md_bm_region md_region md_count_v `star` + right_vprop slab_region md_bm_region md_bm_region_q md_region md_count_v `star` (AL.varraylist pred1 pred2 pred3 pred4 pred5 (A.split_l md_region md_count_v) (US.v idx1) (US.v idx2) (US.v idx3) (US.v idx4) (US.v idx5) (US.v idx6) (US.v idx7)) `star` starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun b -> @@ -1674,7 +1742,7 @@ let deallocate_slab_fail vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1697,12 +1765,12 @@ let deallocate_slab_fail = let b = false in pack_3 size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7; pack_right_and_refactor_vrefine_dep - size_class slab_region md_bm_region md_region md_count + size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v; change_equal_slprop (A.varray ptr) @@ -1716,6 +1784,7 @@ let deallocate_slab' (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1728,15 +1797,15 @@ let deallocate_slab' A.varray ptr `star` vptr md_count `star` A.varray r_idxs `star` - right_vprop slab_region md_bm_region md_region md_count_v `star` + right_vprop slab_region md_bm_region md_bm_region_q md_region md_count_v `star` (AL.varraylist pred1 pred2 pred3 pred4 pred5 (A.split_l md_region md_count_v) (US.v idx1) (US.v idx2) (US.v idx3) (US.v idx4) (US.v idx5) (US.v idx6) (US.v idx7)) `star` starseq #(pos:US.t{US.v pos < US.v md_count_v}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v md_region_lv) - (f_lemma size_class slab_region md_bm_region md_count_v md_region_lv) + (f size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v md_region_lv) (SeqUtils.init_us_refined (US.v md_count_v)) ) (fun b -> @@ -1744,7 +1813,7 @@ let deallocate_slab' vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun h0 -> let gs0 = AL.v_arraylist pred1 pred2 pred3 pred4 pred5 @@ -1793,31 +1862,31 @@ let deallocate_slab' (US.v idx1) (US.v idx2) (US.v idx3) (US.v idx4) (US.v idx5) (US.v idx6) (US.v idx7) pos in if (U32.eq status1 2ul) then ( let b = deallocate_slab_aux_1 ptr size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos pos2 in pack_right_and_refactor_vrefine_dep - size_class slab_region md_bm_region md_region md_count + size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v; return b ) else if (U32.eq status1 1ul) then ( let b = deallocate_slab_aux_2 ptr size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 pos pos2 in pack_right_and_refactor_vrefine_dep - size_class slab_region md_bm_region md_region md_count + size_class slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v; return b ) else ( deallocate_slab_fail ptr size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 ) ) else ( deallocate_slab_fail ptr size_class - slab_region md_bm_region md_region + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v md_region_lv idx1 idx2 idx3 idx4 idx5 idx6 idx7 ) @@ -1830,6 +1899,7 @@ let deallocate_slab (size_class: sc) (slab_region: array U8.t{A.length slab_region = US.v metadata_max * U32.v page_size}) (md_bm_region: array U64.t{A.length md_bm_region = US.v metadata_max * 4}) + (md_bm_region_q: array U64.t{A.length md_bm_region_q = US.v metadata_max * 4}) (md_region: array AL.cell{A.length md_region = US.v metadata_max}) (md_count: ref US.t) (r_idxs: array US.t{A.length r_idxs = 7}) @@ -1840,14 +1910,14 @@ let deallocate_slab vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (fun b -> (if b then emp else A.varray ptr) `star` vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) ) (requires fun _ -> let diff' = A.offset (A.ptr_of ptr) - A.offset (A.ptr_of slab_region) in @@ -1863,27 +1933,27 @@ let deallocate_slab = elim_vrefinedep (vptr md_count) vrefinedep_prop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs) in + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs) in let md_count_v_ = read md_count in change_equal_slprop - (size_class_vprop_aux size_class slab_region md_bm_region md_region r_idxs (G.reveal md_count_v)) - (left_vprop size_class slab_region md_bm_region md_region + (size_class_vprop_aux size_class slab_region md_bm_region md_bm_region_q md_region r_idxs (G.reveal md_count_v)) + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs md_count_v_ `star` - right_vprop slab_region md_bm_region md_region md_count_v_); + right_vprop slab_region md_bm_region md_bm_region_q md_region md_count_v_); change_equal_slprop - (left_vprop size_class slab_region md_bm_region md_region + (left_vprop size_class slab_region md_bm_region md_bm_region_q md_region r_idxs md_count_v_) (left_vprop1 md_region r_idxs md_count_v_ `vdep` - left_vprop2 size_class slab_region md_bm_region md_region r_idxs md_count_v_); + left_vprop2 size_class slab_region md_bm_region md_bm_region_q md_region r_idxs md_count_v_); let x : G.erased _ = elim_vdep (left_vprop1 md_region r_idxs md_count_v_) - (left_vprop2 size_class slab_region md_bm_region md_region r_idxs md_count_v_) in + (left_vprop2 size_class slab_region md_bm_region md_bm_region_q md_region r_idxs md_count_v_) in let idxs : G.erased _ @@ -1952,18 +2022,18 @@ let deallocate_slab // NOT OK change_equal_slprop - (left_vprop2 size_class slab_region md_bm_region md_region r_idxs md_count_v_ x) - (left_vprop2_aux size_class slab_region md_bm_region md_count_v_ x'); + (left_vprop2 size_class slab_region md_bm_region md_bm_region_q md_region r_idxs md_count_v_ x) + (left_vprop2_aux size_class slab_region md_bm_region md_bm_region_q md_count_v_ x'); change_equal_slprop - (left_vprop2_aux size_class slab_region md_bm_region md_count_v_ x') + (left_vprop2_aux size_class slab_region md_bm_region md_bm_region_q md_count_v_ x') (starseq #(pos:US.t{US.v pos < US.v md_count_v_}) #(t size_class) - (f size_class slab_region md_bm_region md_count_v_ x') - (f_lemma size_class slab_region md_bm_region md_count_v_ x') + (f size_class slab_region md_bm_region md_bm_region_q md_count_v_ x') + (f_lemma size_class slab_region md_bm_region md_bm_region_q md_count_v_ x') (SeqUtils.init_us_refined (US.v md_count_v_))); let b : bool = deallocate_slab' ptr size_class - slab_region md_bm_region md_region md_count r_idxs + slab_region md_bm_region md_bm_region_q md_region md_count r_idxs md_count_v_ x' idx1_ idx2_ idx3_ idx4_ idx5_ idx6_ idx7_ diff_ in return b diff --git a/src/SlotsFree.fsti b/src/SlotsFree.fsti index 4fb4cf5..1bdcbba 100644 --- a/src/SlotsFree.fsti +++ b/src/SlotsFree.fsti @@ -17,8 +17,8 @@ open SlotsCommon val deallocate_slot (size_class: sc) - (md md_q: slab_metadata) (arr: array U8.t{A.length arr = U32.v page_size}) + (md md_q: slab_metadata) (ptr: array U8.t) (diff_: US.t) : Steel bool