tweak + refresh dist/

Inria-Prosecco · Jul 21, 2024 · 1c3c3f9 · 1c3c3f9
1 parent 5fbdcf8
commit 1c3c3f9
Show file tree

Hide file tree

Showing 16 changed files with 44 additions and 38 deletions.
diff --git a/Makefile b/Makefile
@@ -93,6 +93,7 @@ FILES = \
   dist/Slots.c \
   dist/Bitmap5.c \
   dist/Utils2.c \
+  dist/Constants.c \
   dist/SizeClass.c \
   dist/SizeClassSelection.c \
   dist/PtrdiffWrapper.c \

diff --git a/dist/Config.c b/dist/Config.c
@@ -19,9 +19,7 @@ bool Config_enable_quarantine_trap = true;
 
 bool Config_enable_quarantine_strict_trap = false;
 
-size_t Config_quarantine_queue_length = (size_t)1024U;
-
-size_t Config_quarantine_queue_threshold = (size_t)256U;
+size_t Config_quarantine_queue_length = (size_t)4096U;
 
 bool Config_enable_zeroing_malloc = true;
 

diff --git a/dist/Config.h b/dist/Config.h
@@ -28,8 +28,6 @@ extern bool Config_enable_quarantine_strict_trap;
 
 extern size_t Config_quarantine_queue_length;
 
-extern size_t Config_quarantine_queue_threshold;
-
 extern bool Config_enable_zeroing_malloc;
 
 extern bool Config_enable_zeroing_free;

diff --git a/dist/Constants.c b/dist/Constants.c
@@ -5,3 +5,8 @@
 
 uint32_t Constants_page_size = 4096U;
 
+uint32_t Constants_nb_slots(uint32_t size_class)
+{
+  return 4096U / size_class;
+}
+
diff --git a/dist/Constants.h b/dist/Constants.h
@@ -8,6 +8,8 @@
 
 extern uint32_t Constants_page_size;
 
+uint32_t Constants_nb_slots(uint32_t size_class);
+
 
 #define __Constants_H_DEFINED
 #endif
diff --git a/dist/Slabs.c b/dist/Slabs.c
@@ -58,7 +58,7 @@ update_quarantine2(
   size_t idx7
 )
 {
-  if (idx7 < (size_t)1024U)
+  if (idx7 < (size_t)4096U)
     return ((tuple4){ .x = idx1, .y = idx5, .z = idx6, .w = idx7 });
   else
   {
@@ -78,7 +78,7 @@ static void update_quarantine3_aux(uint8_t *slab_region, tuple4 idxs)
 
 static void update_quarantine3(uint8_t *slab_region, size_t idx7, tuple4 idxs)
 {
-  if (!(idx7 < (size_t)1024U))
+  if (!(idx7 < (size_t)4096U))
     update_quarantine3_aux(slab_region, idxs);
 }
 
@@ -382,7 +382,7 @@ uint8_t
   }
   else
   {
-    bool b = idx7_ >= (size_t)256U;
+    bool b = idx7_ >= (size_t)Constants_nb_slots(size_class) * (size_t)4U;
     if (b)
     {
       bounded_tuple_

diff --git a/dist/Slots.c b/dist/Slots.c
@@ -19,7 +19,7 @@ static uint8_t *get_slot_as_returned_value(uint32_t size_class, uint8_t *arr, ui
 
 static uint32_t get_free_slot(uint32_t size_class, uint64_t *bitmap, uint64_t *bitmap_q)
 {
-  uint32_t nb_slots_v = Utils2_nb_slots(size_class);
+  uint32_t nb_slots_v = Constants_nb_slots(size_class);
   uint32_t bound = nb_slots_v / 64U;
   uint32_t nb_slots_v_rem = nb_slots_v % 64U;
   uint32_t bound2;

diff --git a/dist/Utils2.c b/dist/Utils2.c
@@ -3,14 +3,9 @@
 
 #include "Utils2.h"
 
-uint32_t Utils2_nb_slots(uint32_t size_class)
-{
-  return 4096U / size_class;
-}
-
 size_t Utils2_rounding(uint32_t size_class)
 {
-  return (size_t)(Utils2_nb_slots(size_class) * size_class);
+  return (size_t)(Constants_nb_slots(size_class) * size_class);
 }
 
 uint64_t Utils2_full_n_aux(uint32_t bound)
@@ -32,7 +27,7 @@ uint64_t Utils2_full_n(uint32_t bound)
 
 bool Utils2_is_empty_s(uint32_t size_class, uint64_t *md)
 {
-  uint32_t bound = Utils2_nb_slots(size_class) / 64U;
+  uint32_t bound = Constants_nb_slots(size_class) / 64U;
   uint64_t v0 = md[0U];
   uint64_t v1 = md[1U];
   uint64_t v2 = md[2U];
@@ -47,7 +42,7 @@ bool Utils2_is_empty_s(uint32_t size_class, uint64_t *md)
 
 bool Utils2_is_empty_s2(uint32_t size_class, uint64_t *md, uint64_t *md_q)
 {
-  uint32_t bound = Utils2_nb_slots(size_class) / 64U;
+  uint32_t bound = Constants_nb_slots(size_class) / 64U;
   uint64_t v0 = md[0U];
   uint64_t v1 = md[1U];
   uint64_t v2 = md[2U];
@@ -66,7 +61,7 @@ bool Utils2_is_empty_s2(uint32_t size_class, uint64_t *md, uint64_t *md_q)
 
 bool Utils2_has_free_slot_s(uint32_t size_class, uint64_t *md)
 {
-  uint32_t nb_slots_v = Utils2_nb_slots(size_class);
+  uint32_t nb_slots_v = Constants_nb_slots(size_class);
   uint32_t bound = nb_slots_v / 64U;
   uint32_t nb_slots_v_rem = nb_slots_v % 64U;
   uint32_t bound2;
@@ -88,7 +83,7 @@ bool Utils2_has_free_slot_s(uint32_t size_class, uint64_t *md)
 
 bool Utils2_has_free_slot_s2(uint32_t size_class, uint64_t *md, uint64_t *md_q)
 {
-  uint32_t nb_slots_v = Utils2_nb_slots(size_class);
+  uint32_t nb_slots_v = Constants_nb_slots(size_class);
   uint32_t bound = nb_slots_v / 64U;
   uint32_t nb_slots_v_rem = nb_slots_v % 64U;
   uint32_t bound2;

diff --git a/dist/Utils2.h b/dist/Utils2.h
@@ -6,7 +6,7 @@
 
 #include "krmllib.h"
 
-uint32_t Utils2_nb_slots(uint32_t size_class);
+#include "Constants.h"
 
 size_t Utils2_rounding(uint32_t size_class);
 

diff --git a/dist/internal/Slabs.h b/dist/internal/Slabs.h
@@ -10,6 +10,7 @@
 #include "internal/ArrayList.h"
 #include "Utils2.h"
 #include "MemoryTrap.h"
+#include "Constants.h"
 #include "ArrayList.h"
 
 bool

diff --git a/dist/internal/Slots.h b/dist/internal/Slots.h
@@ -8,6 +8,7 @@
 
 #include "Utils2.h"
 #include "ExternUtils.h"
+#include "Constants.h"
 #include "Bitmap5.h"
 
 uint8_t

diff --git a/src/Config.fst b/src/Config.fst
@@ -153,8 +153,9 @@ let enable_quarantine = true
 let enable_quarantine_slot = true
 let enable_quarantine_trap = true
 let enable_quarantine_strict_trap = false
-let quarantine_queue_length = 1024sz
-let quarantine_queue_threshold = 256sz
+let quarantine_queue_length = 4096sz
+
+let quarantine_queue_threshold sc = US.mul (US.uint32_to_sizet (nb_slots sc)) 4sz
 let enable_quarantine_lemma _ = ()
 
 // zeroing

diff --git a/src/Config.fsti b/src/Config.fsti
@@ -107,8 +107,10 @@ inline_for_extraction
 val enable_quarantine_strict_trap: bool
 inline_for_extraction
 val quarantine_queue_length: v:US.t{0 < US.v v /\ US.v v <= US.v metadata_max}
-inline_for_extraction
-val quarantine_queue_threshold: v:US.t{0 < US.v v /\ US.v v < US.v quarantine_queue_length}
+//: v:US.t{0 < US.v v /\ US.v v < US.v quarantine_queue_length}
+noextract inline_for_extraction
+val quarantine_queue_threshold (size_class: sc) : (v:US.t{0 < US.v v})
+
 // required
 val enable_quarantine_lemma (_:unit)
   : Lemma

diff --git a/src/Constants.fst b/src/Constants.fst
@@ -34,3 +34,16 @@ let sc = x:U32.t{
   // allowing use of SSE instructions
   (U32.v x % 16 == 0)
 }
+
+#push-options "--z3rlimit 30"
+let nb_slots (size_class: sc)
+  : Pure U32.t
+  (requires True)
+  (ensures fun r ->
+    U32.v r >= 1 /\
+    U32.v r <= 256
+  )
+  =
+  //TODO: stabilize
+  U32.div page_size size_class
+#pop-options
diff --git a/src/SlabsAlloc.fst b/src/SlabsAlloc.fst
@@ -3357,8 +3357,10 @@ let allocate_slab'
       (if (A.is_null r) then emp else A.varray r);
     return r
   ) else (
-    let b = US.gte idx7 quarantine_queue_threshold in
+    let b = US.gte idx7 (quarantine_queue_threshold size_class) in
+    //let b = US.gte idx7 (US.mul (US.uint32_to_sizet (nb_slots size_class)) 4sz) in
     if enable_quarantine && b then (
+      assume (idx7 <> 0sz);
       let idxs = allocate_slab_aux_4 size_class
         slab_region md_bm_region md_bm_region_q md_region md_count r_idxs
         md_count_v md_region_lv

diff --git a/src/Utils2.fst b/src/Utils2.fst
@@ -30,19 +30,6 @@ unfold let slab_metadata = r:array U64.t{A.length r = 4}
 let array_u8_alignment = ArrayAlignment.array_u8_alignment
 let array_u8_alignment_lemma = ArrayAlignment.array_u8_alignment_lemma
 
-#push-options "--z3rlimit 30"
-let nb_slots (size_class: sc)
-  : Pure U32.t
-  (requires True)
-  (ensures fun r ->
-    U32.v r >= 1 /\
-    U32.v r <= 256
-  )
-  =
-  //TODO: stabilize
-  U32.div page_size size_class
-#pop-options
-
 open FStar.Mul
 
 open Prelude