From c41f015e77eb37f55a99c5af953a246f91ddef94 Mon Sep 17 00:00:00 2001
From: Matthew Sotoudeh <matthew@masot.net>
Date: Thu, 16 May 2024 20:23:16 -0700
Subject: Grow & shrink model checking

---
 imc/checker.c | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'imc')

diff --git a/imc/checker.c b/imc/checker.c
index 2ddf978..a7f62ff 100644
--- a/imc/checker.c
+++ b/imc/checker.c
@@ -20,7 +20,8 @@ struct ll {
 // basically the simulation described by Knuth on pg 445
 void check_main() {
     size_t n_timesteps = 10;
-    size_t pool_size = 1024 * 1024 * 1024;
+    size_t real_pool_size = 1024 * 1024 * 1024;
+    size_t pool_size = real_pool_size;
 
     static void *raw_pool = 0;
     static struct ll **time_to_dielist = 0;
@@ -66,6 +67,18 @@ void check_main() {
             curr_buddy = &buddy2;
         }
 
+        int shrink_grow_nop = choose(3, 0);
+        if (shrink_grow_nop == 0) {
+            if (shrink_buddy(pool_size / 2, curr_buddy))
+                pool_size = pool_size / 2;
+            assert(pool_size);
+        } else if (shrink_grow_nop == 1) {
+            if ((2 * pool_size) <= real_pool_size) {
+                pool_size *= 2;
+                grow_buddy(pool, pool_size, curr_buddy);
+            }
+        }
+
         // free the regions at this timestep, and ensure its contents are good
         for (struct ll *p = time_to_dielist[t]; p;) {
             for (size_t i = 0; i < p->data_size; i++) {
@@ -114,7 +127,7 @@ void check_main() {
 
         assert((void*)ll >= pool);
         assert((uint8_t*)ll + size + sizeof(struct ll)
-                < (uint8_t*)pool + pool_size);
+                <= (uint8_t*)pool + pool_size);
 
         ll->data_size = size;
         for (size_t i = 0; i < ll->data_size; i++) {
-- 
cgit v1.2.3