diff options
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. |