README


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
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.