From 041c96ed89a8e1a583b416180977b0ce5b9b8d48 Mon Sep 17 00:00:00 2001 From: Matthew Sotoudeh Date: Tue, 28 May 2024 14:59:23 -0700 Subject: Libimc dump --- README | 44 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 44 insertions(+) create mode 100644 README (limited to 'README') diff --git a/README b/README new file mode 100644 index 0000000..2491d5d --- /dev/null +++ b/README @@ -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. -- cgit v1.2.3