diff options
author | Matthew Sotoudeh <matthew@masot.net> | 2024-05-16 15:15:40 -0700 |
---|---|---|
committer | Matthew Sotoudeh <matthew@masot.net> | 2024-05-16 15:15:40 -0700 |
commit | 92996a3671732b6c883b325414a1e313786d48d6 (patch) | |
tree | 94b29907c5e167ca44ebd8e232ba9e3f44a7e58a /README | |
parent | 54c09d54c0c170f1369751f8bf5a8a0b771a167c (diff) |
checker
Diffstat (limited to 'README')
-rw-r--r-- | README | 18 |
1 files changed, 18 insertions, 0 deletions
@@ -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. |