From 92996a3671732b6c883b325414a1e313786d48d6 Mon Sep 17 00:00:00 2001
From: Matthew Sotoudeh <matthew@masot.net>
Date: Thu, 16 May 2024 15:15:40 -0700
Subject: checker

---
 README | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'README')

diff --git a/README b/README
index d85de3f..3a7c8b1 100644
--- a/README
+++ b/README
@@ -15,6 +15,9 @@ Benefits are:
     4. Support for realloc and reserving subregions (e.g., device MMIO
        addresses).
 
+    5. Core functionality is reasonably well-tested with an exhaustive
+       implementation model checker.
+
 Caveats are:
 
     1. The minimum allocation size is nontrivial, approximately 64 bytes
@@ -52,6 +55,21 @@ The only sources of memory overhead are:
 But it retains the nice property of buddy allocators that liberation is linear
 in the computer's address size.
 
+### Model Checking
+The imc/ directory includes code to "exhaustively fuzz" the allocator. The
+basic approach is based on the EXPLODE paper by Yang, Sar, and Engler.
+
+Current status of the test harness(es):
+
+    - [X] init_buddy
+    - [X] allocate
+    - [X] liberate
+    - [ ] reallocate
+    - [ ] reserve
+    - [ ] grow_buddy
+    - [ ] shrink_buddy
+    - [ ] move_buddy
+
 ### Usage
 
 Usage example in main.c.
-- 
cgit v1.2.3