diff options
Diffstat (limited to 'README')
-rw-r--r-- | README | 44 |
1 files changed, 44 insertions, 0 deletions
@@ -0,0 +1,44 @@ +# libimc + +libimc is an optimized IMC (implementation model checking) library for Linux. + +It is based on the eXplode paper: +https://www.cs.columbia.edu/~junfeng/papers/yang-explode-osdi.talk.pdf + +To use libimc, you write your test harness in a function called + + void check_main() { ... } + +Your program is allowed to make a call to the function + + choice_t choose(choice_t n, hash_t hash); + +Upon doing so, the program conceptually forks, where each fork has "choose" +return a different value in the range 0, 1, ..., n-1. + +If the program receives a SIGABRT or SIGSEGV, it will write the sequence of +choices that led to that error condition to a bugs/ directory. + +If your program requires a resetter, you may call: + + void register_resetter(void (*resetter)(void)); + +# libptimc + +libptimc is a pthreads-like library that uses libimc to try all possible thread +interleavings. + +#### Under the hood +Forking for every call to "choose" is far too slow and far too memory-hungry. + +libimc instead keeps track of multiple worker threads, each one exploring an +entire subtree of possible choices in a depth-first fashion. + +If a worker finds itself with no more work to do, it exits. The master process +then picks another worker at random and asks it to fork its current search tree +in half to fill the space of the previous worker. This ensures rather good +consistent utilization. + +Within a worker, the choices are visited in a random order. This ensures the +search is not biased away from bugs by taking zero choices too frequently early +on. |