1 files changed, 44 insertions, 0 deletions
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.