refresh dist/

currently buggy...
Inria-Prosecco · Jul 21, 2024 · bbe47d8 · bbe47d8
1 parent 2f10fa0
commit bbe47d8
Show file tree

Hide file tree

Showing 13 changed files with 414 additions and 124 deletions.
diff --git a/dist/Config.c b/dist/Config.c
@@ -13,7 +13,7 @@ size_t Config_guard_pages_interval = (size_t)2U;
 
 bool Config_enable_quarantine = true;
 
-bool Config_enable_quarantine_slot = false;
+bool Config_enable_quarantine_slot = true;
 
 bool Config_enable_quarantine_trap = true;
 

diff --git a/dist/Slabs.c b/dist/Slabs.c
@@ -97,7 +97,6 @@ SlabsFree_deallocate_slab(
 {
   size_t md_count_v_ = *md_count;
   size_t idx1_ = r_idxs[0U];
-  size_t idx2_ = r_idxs[1U];
   size_t idx3_ = r_idxs[2U];
   size_t idx5_ = r_idxs[4U];
   size_t idx6_ = r_idxs[5U];
@@ -126,16 +125,22 @@ SlabsFree_deallocate_slab(
           pos2);
       if (b)
       {
-        uint64_t *ptr1 = md_bm_region;
-        size_t shift_size_t = pos * (size_t)4U;
-        bool r1 = Utils2_is_empty_s(size_class, ptr1 + shift_size_t);
-        bool cond = r1;
-        if (cond)
+        uint64_t *ptr10 = md_bm_region;
+        size_t shift_size_t0 = pos * (size_t)4U;
+        bool b1 = Utils2_is_empty_s(size_class, ptr10 + shift_size_t0);
+        uint64_t *ptr1 = md_bm_region_q;
+        size_t shift_size_t1 = pos * (size_t)4U;
+        bool b2 = Utils2_is_full_s(size_class, ptr1 + shift_size_t1);
+        bool b_ = b1 && b2;
+        if (b_)
         {
-          uint8_t *ptr1 = slab_region;
+          uint64_t *ptr1 = md_bm_region_q;
+          size_t shift_size_t = pos * (size_t)4U;
+          Utils2_reset_to_empty(size_class, ptr1 + shift_size_t);
+          uint8_t *ptr10 = slab_region;
           size_t page_size_t = (size_t)4096U;
-          size_t shift_size_t = pos * page_size_t;
-          mmap_trap(ptr1 + shift_size_t, (size_t)4096U);
+          size_t shift_size_t0 = pos * page_size_t;
+          mmap_trap(ptr10 + shift_size_t0, (size_t)4096U);
           tuple4 idxs = update_quarantine2(md_region, idx1_, idx5_, idx6_, idx7_);
           size_t v = ArrayList_remove(md_region, idx3_, pos);
           size_t idx3_ = v;
@@ -163,76 +168,30 @@ SlabsFree_deallocate_slab(
           return b;
         }
         else
-        {
-          size_t v = ArrayList_remove(md_region, idx3_, pos);
-          size_t idx3_ = v;
-          ArrayList_insert(md_region, idx2_, pos, 1U);
-          r_idxs[2U] = idx3_;
-          r_idxs[1U] = pos;
-          return b;
-        }
+          return true;
       }
       else
         return b;
     }
     else if (status1 == 1U)
     {
       uint8_t *ptr10 = slab_region;
-      size_t page_size_t0 = (size_t)4096U;
-      size_t shift_size_t0 = pos * page_size_t0;
+      size_t page_size_t = (size_t)4096U;
+      size_t shift_size_t0 = pos * page_size_t;
       uint64_t *ptr11 = md_bm_region;
       size_t shift_size_t1 = pos * (size_t)4U;
-      uint64_t *ptr12 = md_bm_region_q;
-      size_t shift_size_t2 = pos * (size_t)4U;
+      uint64_t *ptr1 = md_bm_region_q;
+      size_t shift_size_t = pos * (size_t)4U;
       bool
       b =
         SlotsFree_deallocate_slot(size_class,
           ptr10 + shift_size_t0,
           ptr11 + shift_size_t1,
-          ptr12 + shift_size_t2,
+          ptr1 + shift_size_t,
           ptr,
           pos2);
       if (b)
-      {
-        uint64_t *ptr1 = md_bm_region;
-        size_t shift_size_t = pos * (size_t)4U;
-        bool r1 = Utils2_is_empty_s(size_class, ptr1 + shift_size_t);
-        bool cond = r1;
-        if (cond)
-        {
-          uint8_t *ptr1 = slab_region;
-          size_t page_size_t = (size_t)4096U;
-          size_t shift_size_t = pos * page_size_t;
-          mmap_trap(ptr1 + shift_size_t, (size_t)4096U);
-          tuple4 idxs = update_quarantine2(md_region, idx1_, idx5_, idx6_, idx7_);
-          size_t v = ArrayList_remove(md_region, idx2_, pos);
-          size_t idx2_ = v;
-          ArrayList_cell cell = { .prev = (size_t)16777217U, .next = idxs.y, .data = 4U };
-          md_region[pos] = cell;
-          if (idxs.y != (size_t)16777217U)
-          {
-            ArrayList_cell cell1 = md_region[idxs.y];
-            ArrayList_cell cell2 = { .prev = pos, .next = cell1.next, .data = cell1.data };
-            md_region[idxs.y] = cell2;
-          }
-          size_t tl_;
-          if (idxs.y == (size_t)16777217U)
-            tl_ = pos;
-          else
-            tl_ = idxs.z;
-          size_t sz_ = idxs.w + (size_t)1U;
-          ArrayListGen_tuple2 idxs_ = { .x1 = tl_, .y1 = sz_ };
-          update_quarantine3(slab_region, idx7_, idxs);
-          r_idxs[0U] = idxs.x;
-          r_idxs[1U] = idx2_;
-          r_idxs[4U] = pos;
-          r_idxs[5U] = idxs_.x1;
-          r_idxs[6U] = idxs_.y1;
-          return b;
-        }
-        else
-          return b;
-      }
+        return true;
       else
         return b;
     }
@@ -366,9 +325,11 @@ uint8_t
         ptr0 + shift_size_t0,
         ptr1 + shift_size_t1,
         ptr2 + shift_size_t2);
-    uint64_t *ptr = md_bm_region;
+    uint64_t *ptr3 = md_bm_region;
+    size_t shift_size_t3 = idx2_ * (size_t)4U;
+    uint64_t *ptr = md_bm_region_q;
     size_t shift_size_t = idx2_ * (size_t)4U;
-    bool r1 = Utils2_is_full_s(size_class, ptr + shift_size_t);
+    bool r1 = Utils2_is_full_s2(size_class, ptr3 + shift_size_t3, ptr + shift_size_t);
     bool cond = r1;
     if (cond)
     {
@@ -396,9 +357,11 @@ uint8_t
         ptr0 + shift_size_t0,
         ptr1 + shift_size_t1,
         ptr2 + shift_size_t2);
-    uint64_t *ptr = md_bm_region;
+    uint64_t *ptr3 = md_bm_region;
+    size_t shift_size_t3 = idx1_ * (size_t)4U;
+    uint64_t *ptr = md_bm_region_q;
     size_t shift_size_t = idx1_ * (size_t)4U;
-    bool r1 = Utils2_is_full_s(size_class, ptr + shift_size_t);
+    bool r1 = Utils2_is_full_s2(size_class, ptr3 + shift_size_t3, ptr + shift_size_t);
     bool cond = r1;
     if (cond)
     {
@@ -437,9 +400,11 @@ uint8_t
           ptr0 + shift_size_t0,
           ptr1 + shift_size_t1,
           ptr2 + shift_size_t2);
-      uint64_t *ptr = md_bm_region;
+      uint64_t *ptr3 = md_bm_region;
+      size_t shift_size_t3 = idxs.x * (size_t)4U;
+      uint64_t *ptr = md_bm_region_q;
       size_t shift_size_t = idxs.x * (size_t)4U;
-      bool r1 = Utils2_is_full_s(size_class, ptr + shift_size_t);
+      bool r1 = Utils2_is_full_s2(size_class, ptr3 + shift_size_t3, ptr + shift_size_t);
       bool cond = r1;
       if (cond)
       {
@@ -495,9 +460,11 @@ uint8_t
             ptr0 + shift_size_t0,
             ptr1 + shift_size_t1,
             ptr2 + shift_size_t2);
-        uint64_t *ptr = md_bm_region;
+        uint64_t *ptr3 = md_bm_region;
+        size_t shift_size_t3 = (md_count_v_ + (size_t)2U - (size_t)2U) * (size_t)4U;
+        uint64_t *ptr = md_bm_region_q;
         size_t shift_size_t = (md_count_v_ + (size_t)2U - (size_t)2U) * (size_t)4U;
-        bool r1 = Utils2_is_full_s(size_class, ptr + shift_size_t);
+        bool r1 = Utils2_is_full_s2(size_class, ptr3 + shift_size_t3, ptr + shift_size_t);
         bool cond = r1;
         if (cond)
         {

diff --git a/dist/Slots.c b/dist/Slots.c
@@ -117,6 +117,7 @@ deallocate_slot_(uint32_t size_class, uint64_t *md, uint64_t *md_q, uint8_t *ptr
     if (b1 && !b2)
     {
       Bitmap5_bm_unset(md, pos);
+      Bitmap5_bm_set(md_q, pos);
       deallocate_zeroing(size_class, ptr);
       return true;
     }

diff --git a/dist/Utils2.c b/dist/Utils2.c
@@ -30,6 +30,40 @@ 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;
+  uint64_t v0 = md[0U];
+  uint64_t v1 = md[1U];
+  uint64_t v2 = md[2U];
+  uint64_t v3 = md[3U];
+  return
+    v0
+    == 0ULL
+    && (bound <= 1U || v1 == 0ULL)
+    && (bound <= 2U || v2 == 0ULL)
+    && (bound <= 3U || v3 == 0ULL);
+}
+
+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;
+  uint64_t v0 = md[0U];
+  uint64_t v1 = md[1U];
+  uint64_t v2 = md[2U];
+  uint64_t v3 = md[3U];
+  uint64_t v0q = md_q[0U];
+  uint64_t v1q = md_q[1U];
+  uint64_t v2q = md_q[2U];
+  uint64_t v3q = md_q[3U];
+  return
+    (v0 | v0q)
+    == 0ULL
+    && (bound <= 1U || (v1 | v1q) == 0ULL)
+    && (bound <= 2U || (v2 | v2q) == 0ULL)
+    && (bound <= 3U || (v3 | v3q) == 0ULL);
+}
+
 bool Utils2_has_free_slot_s(uint32_t size_class, uint64_t *md)
 {
   uint32_t nb_slots_v = Utils2_nb_slots(size_class);
@@ -52,19 +86,30 @@ bool Utils2_has_free_slot_s(uint32_t size_class, uint64_t *md)
     || (bound > 3U && !(v3 == 18446744073709551615ULL));
 }
 
-bool Utils2_is_empty_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 bound = Utils2_nb_slots(size_class) / 64U;
+  uint32_t nb_slots_v = Utils2_nb_slots(size_class);
+  uint32_t bound = nb_slots_v / 64U;
+  uint32_t nb_slots_v_rem = nb_slots_v % 64U;
+  uint32_t bound2;
+  if (nb_slots_v_rem == 0U)
+    bound2 = 64U;
+  else
+    bound2 = nb_slots_v_rem;
+  uint64_t full = Utils2_full_n(bound2);
   uint64_t v0 = md[0U];
   uint64_t v1 = md[1U];
   uint64_t v2 = md[2U];
   uint64_t v3 = md[3U];
+  uint64_t v0q = md_q[0U];
+  uint64_t v1q = md_q[1U];
+  uint64_t v2q = md_q[2U];
+  uint64_t v3q = md_q[3U];
   return
-    v0
-    == 0ULL
-    && (bound <= 1U || v1 == 0ULL)
-    && (bound <= 2U || v2 == 0ULL)
-    && (bound <= 3U || v3 == 0ULL);
+    !((v0 | v0q) == full)
+    || (bound > 1U && !((v1 | v1q) == 18446744073709551615ULL))
+    || (bound > 2U && !((v2 | v2q) == 18446744073709551615ULL))
+    || (bound > 3U && !((v3 | v3q) == 18446744073709551615ULL));
 }
 
 bool Utils2_is_partial_s(uint32_t size_class, uint64_t *md)
@@ -74,9 +119,31 @@ bool Utils2_is_partial_s(uint32_t size_class, uint64_t *md)
   return b1 && !b2;
 }
 
+bool Utils2_is_partial_s2(uint32_t size_class, uint64_t *md, uint64_t *md_q)
+{
+  bool b1 = Utils2_has_free_slot_s2(size_class, md, md_q);
+  bool b2 = Utils2_is_empty_s2(size_class, md, md_q);
+  return b1 && !b2;
+}
+
 bool Utils2_is_full_s(uint32_t size_class, uint64_t *md)
 {
   bool b = Utils2_has_free_slot_s(size_class, md);
   return !b;
 }
 
+bool Utils2_is_full_s2(uint32_t size_class, uint64_t *md, uint64_t *md_q)
+{
+  bool b = Utils2_has_free_slot_s2(size_class, md, md_q);
+  return !b;
+}
+
+void Utils2_reset_to_empty(uint32_t size_class, uint64_t *md)
+{
+  KRML_MAYBE_UNUSED_VAR(size_class);
+  md[0U] = 0ULL;
+  md[1U] = 0ULL;
+  md[2U] = 0ULL;
+  md[3U] = 0ULL;
+}
+
diff --git a/dist/Utils2.h b/dist/Utils2.h
@@ -14,14 +14,24 @@ uint64_t Utils2_full_n_aux(uint32_t bound);
 
 uint64_t Utils2_full_n(uint32_t bound);
 
+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);
+
 bool Utils2_has_free_slot_s(uint32_t size_class, uint64_t *md);
 
-bool Utils2_is_empty_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);
 
 bool Utils2_is_partial_s(uint32_t size_class, uint64_t *md);
 
+bool Utils2_is_partial_s2(uint32_t size_class, uint64_t *md, uint64_t *md_q);
+
 bool Utils2_is_full_s(uint32_t size_class, uint64_t *md);
 
+bool Utils2_is_full_s2(uint32_t size_class, uint64_t *md, uint64_t *md_q);
+
+void Utils2_reset_to_empty(uint32_t size_class, uint64_t *md);
+
 
 #define __Utils2_H_DEFINED
 #endif
diff --git a/src/Config.fst b/src/Config.fst
@@ -150,7 +150,7 @@ let guard_pages_interval = 2sz
 
 // quarantine
 let enable_quarantine = true
-let enable_quarantine_slot = false
+let enable_quarantine_slot = true
 let enable_quarantine_trap = true
 let enable_quarantine_strict_trap = false
 let quarantine_queue_length = 1024sz

diff --git a/src/SlabsAlloc.fst b/src/SlabsAlloc.fst
@@ -59,12 +59,12 @@ let allocate_slab_aux_cond
     r == is_full size_class (seq_u64_or (fst mds) (snd mds))
   )
   =
+  //TODO: should be benign
   admit ();
   assert (t_of (A.varray md) == Seq.lseq U64.t 4);
   let mds : G.erased (Seq.lseq U64.t 4 & Seq.lseq U64.t 4)
     = elim_slab_vprop size_class arr md md_q in
-  //TODO
-  let r = is_full_s size_class md in
+  let r = is_full_s2 size_class md md_q in
   intro_slab_vprop size_class arr md md_q (fst mds);
   return r
 #pop-options
@@ -2037,10 +2037,12 @@ let allocate_slab_aux_3_3_2_1_aux2 (#opened:_)
     (A.varray (md_bm_array md_bm_region_q (US.add md_count_v (US.sub i 1sz))));
 
   let md_as_seq = gget (A.varray (md_bm_array md_bm_region (US.add md_count_v (US.sub i 1sz)))) in
+  let md_as_seq' = gget (A.varray (md_bm_array md_bm_region (US.add md_count_v (US.sub i 1sz)))) in
   assert (G.reveal md_as_seq == Seq.create 4 0UL);
+  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
+  //TODO: FIXME, should be benign
   admit ();
   intro_slab_vprop size_class
     (slab_array slab_region (US.add md_count_v (US.sub i 1sz)))
@@ -3103,7 +3105,7 @@ let allocate_slab_aux_4_aux2
   Helpers.slab_to_slots size_class (slab_array slab_region idxs.x);
   let md = gget (A.varray (md_bm_array md_bm_region idxs.x)) in
   empty_md_is_properly_zeroed size_class;
-  //TODO: QUARANTINEv4
+  //TODO: FIXME, should be benign
   admit ();
   intro_slab_vprop size_class
     (slab_array slab_region idxs.x)