diff options
| -rw-r--r-- | README | 44 | ||||
| -rw-r--r-- | libimc/_libimc.h | 94 | ||||
| -rw-r--r-- | libimc/libimc.h | 18 | ||||
| -rw-r--r-- | libimc/master.c | 180 | ||||
| -rw-r--r-- | libimc/worker.c | 286 | ||||
| -rw-r--r-- | libptimc/libptimc.c | 125 | ||||
| -rw-r--r-- | libptimc/libptimc.h | 49 |
7 files changed, 796 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. diff --git a/libimc/_libimc.h b/libimc/_libimc.h new file mode 100644 index 0000000..3cf4dd2 --- /dev/null +++ b/libimc/_libimc.h @@ -0,0 +1,94 @@ +#pragma once + +#define _GNU_SOURCE +#include <fcntl.h> +#include <unistd.h> +#include <errno.h> +#include "libimc.h" + +// #define verbose(...) printf(__VA_ARGS__) +#define verbose(...) + +extern int MASTER2WORKER_RD[N_WORKERS]; +extern int MASTER2WORKER_WR[N_WORKERS]; +extern int WORKER2MASTER_RD[N_WORKERS]; +extern int WORKER2MASTER_WR[N_WORKERS]; + +extern void launch_worker(unsigned int i); +extern void worker_replay(char *path); + +enum message_type { + MSG_NONE, + + // Worker -> Master + MSG_CAN_I_DIE, + MSG_DID_SPLIT, + MSG_NO_SPLIT, + MSG_PROGRESS, + + // Master -> Worker + MSG_PLEASE_SPLIT, + MSG_OK_DIE, + MSG_NO_DIE, +}; + +struct message { + enum message_type message_type; + int new_id; + int pid; + + size_t n_branches; + size_t n_bugs; +}; + +static void tell_pipe(int fd, uint8_t *ptr, size_t n) { + while (n) { + ssize_t n_sent = write(fd, ptr, n); + if (n_sent == -1 && (errno == EAGAIN || errno == EWOULDBLOCK)) + n_sent = 0; + assert(n_sent >= 0); + ptr += n_sent; + n -= n_sent; + } +} + +static void hear_pipe(int fd, uint8_t *ptr, size_t n) { + int any = 0; + while (n) { + ssize_t n_read = read(fd, ptr, n); + if (n_read == -1 && (errno == EAGAIN || errno == EWOULDBLOCK)) + n_read = 0; + assert(n_read >= 0); + ptr += n_read; + n -= n_read; + if (!any && !n_read) return; + any = 1; + } +} + +static void clear_pipe(int fd) { + uint8_t byte; + while (read(fd, &byte, 1) == 1); +} + +static void tell_worker(struct message message, int idx) { + tell_pipe(MASTER2WORKER_WR[idx], (uint8_t*)&message, sizeof(message)); +} + +static void tell_master(struct message message, int idx) { + struct message *msg = calloc(1, sizeof(message)); + *msg = message; + tell_pipe(WORKER2MASTER_WR[idx], (uint8_t*)msg, sizeof(message)); +} + +static struct message hear_worker(int idx) { + struct message message = {0}; + hear_pipe(WORKER2MASTER_RD[idx], (uint8_t*)&message, sizeof(message)); + return message; +} + +static struct message hear_master(int idx) { + struct message message = {0}; + hear_pipe(MASTER2WORKER_RD[idx], (uint8_t*)&message, sizeof(message)); + return message; +} diff --git a/libimc/libimc.h b/libimc/libimc.h new file mode 100644 index 0000000..8777883 --- /dev/null +++ b/libimc/libimc.h @@ -0,0 +1,18 @@ +#pragma once + +#include <stdint.h> +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <stdlib.h> +#include <stddef.h> + +typedef uint64_t choice_t; +typedef uint64_t hash_t; + +choice_t choose(choice_t n, hash_t hash); +void report_error(); +void check_exit_normal(); +extern void check_main(); + +void register_resetter(void (*resetter)(void)); diff --git a/libimc/master.c b/libimc/master.c new file mode 100644 index 0000000..6d48b28 --- /dev/null +++ b/libimc/master.c @@ -0,0 +1,180 @@ +#include "_libimc.h" +#include <stdio.h> +#include <time.h> +#include <assert.h> +#include <string.h> +#include <stdlib.h> +#include <stddef.h> +#include <unistd.h> +#include <signal.h> +#include <sys/wait.h> +#include <sys/prctl.h> + +int MASTER2WORKER_RD[N_WORKERS]; +int MASTER2WORKER_WR[N_WORKERS]; +int WORKER2MASTER_RD[N_WORKERS]; +int WORKER2MASTER_WR[N_WORKERS]; + +static size_t N_BRANCHES[N_WORKERS]; +static size_t N_BUGS[N_WORKERS]; +void handle_progress(struct message message, int worker_id) { + N_BRANCHES[worker_id] += message.n_branches; + N_BUGS[worker_id] += message.n_bugs; +} + +void print_progress(void) { + size_t total_branches = 0, total_bugs = 0; + printf("# branches:"); + for (int i = 0; i < N_WORKERS; i++) { + printf(" %lu", N_BRANCHES[i]); + total_branches += N_BRANCHES[i]; + } + printf("\n"); + printf("# bugs:"); + for (int i = 0; i < N_WORKERS; i++) { + printf(" %lu", N_BUGS[i]); + total_bugs += N_BUGS[i]; + } + printf("\n"); + printf("TOTAL branches: %lu; bugs: %lu\n", total_branches, total_bugs); +} + +void launch_master() { + // make a bugs directory + system("mkdir -p bugs"); + system("rm bugs/*"); + + assert(!prctl(PR_SET_CHILD_SUBREAPER, 1, 0, 0, 0)); + + // set up the control pipes + for (int i = 0; i < N_WORKERS; i++) { + int ends[2]; + pipe2(ends, O_NONBLOCK); + MASTER2WORKER_RD[i] = ends[0]; + MASTER2WORKER_WR[i] = ends[1]; + pipe2(ends, O_NONBLOCK); + WORKER2MASTER_RD[i] = ends[0]; + WORKER2MASTER_WR[i] = ends[1]; + } + + // 0 -> dead, 1 -> alive, -1 -> waiting on it to die + int worker_alive[N_WORKERS] = {0}; + // only guaranteed to be up-to-date for workers with worker_alive[i] == -1 + int worker_pid[N_WORKERS] = {0}; + size_t dead_count = 0; + + // launch an initial worker + if (!fork()) { + launch_worker(0); + exit(0); + } + + worker_alive[0] = 1; + while (1) { + static time_t last_time = 0; + if ((time(0) - last_time) > 1) { + last_time = time(0); + print_progress(); + } + + // First: handle any workers that want to die + for (int i = 0; i < N_WORKERS; i++) { + if (!worker_alive[i]) continue; + if (worker_alive[i] == -1) { + if (waitpid(worker_pid[i], NULL, WNOHANG)) { + worker_alive[i] = 0; + clear_pipe(MASTER2WORKER_RD[i]); + clear_pipe(WORKER2MASTER_RD[i]); + } + continue; + } + + struct message message = hear_worker(i); + switch (message.message_type) { + case MSG_CAN_I_DIE: + worker_alive[i] = -1; + worker_pid[i] = message.pid; + verbose("Telling worker %d (%d) they can die\n", i, message.pid); + tell_worker((struct message){MSG_OK_DIE, 0}, i); + break; + + case MSG_PROGRESS: + handle_progress(message, i); + break; + + case MSG_NONE: + break; + + default: + assert(!"Bad message!"); + break; + } + } + + // Second: if we have empty slots, ask a worker to split. + int n_alive = 0, fill_slot = 0; + for (int i = 0; i < N_WORKERS; i++) { + n_alive += (worker_alive[i] != 0); + if (!worker_alive[i]) fill_slot = i; + } + if (n_alive == 0) break; + if (n_alive == N_WORKERS) continue; + + int which = rand() % n_alive; + for (int i = 0; i < N_WORKERS; i++) { + if (!worker_alive[i]) continue; + if (which--) continue; + if (worker_alive[i] == -1) continue; + + verbose("Requesting a split of %d -> %d\n", i, fill_slot); + tell_worker((struct message){ + .message_type = MSG_PLEASE_SPLIT, + .new_id = fill_slot + }, i); + + while (1) { + struct message reply = hear_worker(i); + switch (reply.message_type) { + case MSG_CAN_I_DIE: + verbose("Telling worker %d not to die, because we want to split\n"); + tell_worker((struct message){MSG_NO_DIE}, i); + break; + + case MSG_DID_SPLIT: + worker_alive[fill_slot] = 1; + waitpid(reply.pid, NULL, 0); + goto finish_split; + + case MSG_NO_SPLIT: + goto finish_split; + + case MSG_PROGRESS: + handle_progress(reply, i); + break; + + case MSG_NONE: + break; + + default: + printf("Unknown message %d!\n", reply.message_type); + break; + } + } + +finish_split: break; + } + } + + printf("Done with exhaustive search.\n"); + print_progress(); +} + +int main(int argc, char **argv) { + if (argc > 1) { + assert(argc == 2); + worker_replay(argv[1]); + } else { + launch_master(); + } + return 0; +} diff --git a/libimc/worker.c b/libimc/worker.c new file mode 100644 index 0000000..d4d57b7 --- /dev/null +++ b/libimc/worker.c @@ -0,0 +1,286 @@ +#include "_libimc.h" +#include <stdio.h> +#include <assert.h> +#include <string.h> +#include <stdlib.h> +#include <stddef.h> +#include <unistd.h> +#include <setjmp.h> +#include <signal.h> +#include <time.h> + +static int IS_REPLAY; +static size_t WORKER_I; +static size_t N_BRANCHES, N_BUGS; +static void send_progress(void) { + tell_master((struct message){ + .message_type = MSG_PROGRESS, + .n_branches = N_BRANCHES, + .n_bugs = N_BUGS + }, WORKER_I); + N_BRANCHES = N_BUGS = 0; +} + +struct resetter { + void (*fn)(void); + struct resetter *next; +}; +static struct resetter *RESETTERS; +void register_resetter(void (*fn)(void)) { + for (struct resetter *r = RESETTERS; r; r = r->next) + if (r->fn == fn) + return; + struct resetter *resetter = malloc(sizeof(struct resetter)); + resetter->fn = fn; + resetter->next = RESETTERS; + RESETTERS = resetter; +} + +// The worker keeps track of a search tree. Each node in the tree contains: +// +// (0) The specific option that was chosen at that node +// (1) An array of the choices we have explored there so far, each one +// associated with a specific child node. +// (2) The choice argument, i.e., how many children it has +// +// The search itself is a simple depth-first search. Once we explore all +// children of a node, we can free it. + +// at each 'choose', we look at the current node's 'pos'. +struct tree_node { + choice_t choice; + // @n_children == 0 means this node hasn't been explored yet. + // note we auto-handle choose(1), so n_children > 2 if it's > 0. + choice_t n_children; + + // if @n_children > 0, @pos should always point to a proper child in + // @children. + choice_t pos; + struct tree_node *children; + struct tree_node *parent; +}; + +struct tree_node *ROOT, *NODE; + +choice_t choose(choice_t n, hash_t hash) { + if (n == 1) return 0; + + if (!NODE) { + // this is the first choice; give it a node + ROOT = NODE = calloc(1, sizeof(struct tree_node)); + } + assert(ROOT); + + if (NODE->n_children) { + NODE = NODE->children + NODE->pos; + return NODE->choice; + } + + // this node is unexplored + NODE->n_children = n; + NODE->children = calloc(n, sizeof(NODE->children[0])); + + choice_t *options = calloc(n, sizeof(options)); + + for (choice_t i = 0; i < n; i++) options[i] = i; + for (choice_t i = 0; i < n; i++) { + size_t swap_with = i + (rand() % (n - i)); + choice_t tmp = options[i]; + options[i] = options[swap_with]; + options[swap_with] = tmp; + } + + for (int i = 0; i < n; i++) { + NODE->children[i].choice = options[i]; + NODE->children[i].parent = NODE; + } + + NODE->pos = 0; + + return choose(n, hash); +} + +static void search_increment(void) { + // finish off this branch + while (1) { + struct tree_node *parent = NODE->parent; + if (!parent) { + send_progress(); + + struct message death_msg = (struct message){ + .message_type = MSG_CAN_I_DIE, + .pid = getpid(), + }; + verbose("%d (%d) trying to die.\n", WORKER_I, getpid()); + tell_master(death_msg, WORKER_I); + while (1) { + struct message message = hear_master(WORKER_I); + switch (message.message_type) { + case MSG_NONE: break; + case MSG_PLEASE_SPLIT: + verbose("%d was asked to split\n", WORKER_I); + tell_master((struct message){MSG_NO_SPLIT}, WORKER_I); + tell_master(death_msg, WORKER_I); + break; + case MSG_OK_DIE: + verbose("%d gets to die.\n", WORKER_I); + exit(0); + break; + case MSG_NO_DIE: + verbose("%d can't die yet.\n", WORKER_I); + break; + default: + printf("While trying to die, %d got unknown message type %d\n", + WORKER_I, message.message_type); + break; + } + } + assert(!"Shouldn't reach here\n"); + } + + parent->pos++; + if (parent->pos < parent->n_children) break; + + free(parent->children); + NODE = parent; + } + NODE = ROOT; +} + +static void try_split(struct message message) { + struct tree_node *node = ROOT; + while (node) { + if (!node->n_children || node->pos == (node->n_children - 1)) { + node = node->children + node->pos; + continue; + } + + send_progress(); + int pid = getpid(); + if (fork()) { // parent + if (fork()) { + // let the parent reap me + exit(0); + } else { + node->n_children--; + tell_master((struct message){ + .message_type = MSG_DID_SPLIT, + .pid = pid, + }, WORKER_I); + } + } else { // child + WORKER_I = message.new_id; + node->pos = node->n_children - 1; + assert(node->pos < node->n_children); + } + return; + } + tell_master((struct message){MSG_NO_SPLIT}, WORKER_I); +} + +static jmp_buf RESET_JMP; + +void report_error() { + if (IS_REPLAY) { + fprintf(stderr, "Done with replay!\n"); + siglongjmp(RESET_JMP, 1); + } + + N_BUGS++; + + char tmpname[128]; + strcpy(tmpname, "bugs/XXXXXX"); + mkstemp(tmpname); + FILE *f = fopen(tmpname, "w"); + + struct tree_node *node = ROOT; + while (node) { + fprintf(f, "%lu\n", node->choice); + node = node->children + node->pos; + } + + fclose(f); + + fprintf(stderr, "Error written to %s\n", tmpname); + + check_exit_normal(); +} + +void check_exit_normal() { + if (IS_REPLAY) { + fprintf(stderr, "Replay finished with normal exit.\n"); + siglongjmp(RESET_JMP, 1); + } + + N_BRANCHES++; + if ((N_BRANCHES + 1) % REPORT_FREQ == 0) + send_progress(); + siglongjmp(RESET_JMP, 1); +} + +static void sighandler(int which) { + printf("Got signal: %d\n", which); + report_error(); +} + +void launch_worker(unsigned int i) { + WORKER_I = i; + srand(i + 24); + + // (0) set up signal handlers + struct sigaction action; + action.sa_handler = sighandler; + sigemptyset(&(action.sa_mask)); + action.sa_flags = 0; + assert(!sigaction(SIGABRT, &action, 0)); + assert(!sigaction(SIGSEGV, &action, 0)); + + // (1) set a setjmp for resetting the search + if (sigsetjmp(RESET_JMP, 1)) search_increment(); + for (struct resetter *r = RESETTERS; r; r = r->next) + r->fn(); + + // (1b) check for commands + struct message message = hear_master(WORKER_I); + switch (message.message_type) { + case MSG_NONE: + break; + + case MSG_PLEASE_SPLIT: + try_split(message); + break; + + default: + printf("!!!!!!!!!!!!!!! In the main loop, %d (%d) got unknown message type %d\n", WORKER_I, getpid(), message.message_type); + break; + } + + // (2) start the program + check_main(); + + // (3) trigger a reset + check_exit_normal(); +} + +void worker_replay(char *path) { + if (sigsetjmp(RESET_JMP, 1)) return; + IS_REPLAY = 1; + + FILE *f = fopen(path, "r"); + assert(f); + NODE = ROOT = calloc(1, sizeof(*ROOT)); + while (1) { + size_t choice = 0; + if (fscanf(f, " %lu", &choice) != 1) break; + + NODE->n_children = 2; + NODE->children = calloc(2, sizeof(NODE->children[0])); + NODE->children[0].choice = choice; + NODE->children[0].parent = NODE; + + NODE = NODE->children; + } + NODE = ROOT->children; + check_main(); + check_exit_normal(); +} diff --git a/libptimc/libptimc.c b/libptimc/libptimc.c new file mode 100644 index 0000000..3cda04b --- /dev/null +++ b/libptimc/libptimc.c @@ -0,0 +1,125 @@ +#include "libptimc.h" + +static struct imcthread **THREADS = 0; +static size_t N_THREADS = 0; +static struct imcthread *CURRENT_THREAD = 0; +static ucontext_t MASTER_CTX; + +static void switch_to_thread(struct imcthread *thread); +static void imcthread_entry_point(int tid); + +static void resetter() { + for (int i = 0; i < N_THREADS; i++) { + free(THREADS[i]->ctx.uc_stack.ss_sp); + free(THREADS[i]); + } + free(THREADS); + THREADS = 0; + N_THREADS = 0; + CURRENT_THREAD = 0; +} + +int imcthread_create(imcthread_t *threadp, + imcthread_attr_t *attr, + void *(*start_routine)(void *), + void *arg) { + assert(!attr); + THREADS = realloc(THREADS, (++N_THREADS) * sizeof(THREADS[0])); + THREADS[N_THREADS - 1] = calloc(1, sizeof(struct imcthread)); + + struct imcthread *thread = THREADS[N_THREADS - 1]; + *threadp = thread; + thread->fn = start_routine; + thread->arg = arg; + thread->state = THREAD_STATE_FETUS; + thread->id = N_THREADS - 1; + + assert(!getcontext(&thread->ctx)); + thread->ctx.uc_stack.ss_size = 4 * 1024 * 1024; + thread->ctx.uc_stack.ss_sp = malloc(thread->ctx.uc_stack.ss_size); + thread->ctx.uc_link = 0; + makecontext(&thread->ctx, imcthread_entry_point, 1, thread->id); + + return 0; +} + +int imcthread_yieldh(hash_t hash) { + // pauses the current thread and returns to the master thread + assert(CURRENT_THREAD); + struct imcthread *thread = CURRENT_THREAD; + + if (thread->state == THREAD_STATE_DEAD) { + for (size_t i = 0; i < N_THREADS; i++) + if (THREADS[i]->waiting_on == thread) + THREADS[i]->waiting_on = 0; + } + + CURRENT_THREAD = 0; + swapcontext(&(thread->ctx), &MASTER_CTX); + + return 0; +} +int imcthread_yield(void) { imcthread_yieldh(0); } + +static void *_imc_check_main(void *_) { imc_check_main(); return 0; } +void check_main() { + register_resetter(resetter); + + imcthread_t _thread; + imcthread_create(&_thread, NULL, _imc_check_main, NULL); + + while (1) { + int n_alive = 0, n_avail = 0; + for (int i = 0; i < N_THREADS; i++) { + if (THREADS[i]->state == THREAD_STATE_DEAD) continue; + n_alive++; + if (THREADS[i]->waiting_on) continue; + n_avail++; + } + // check that we're not in a deadlock + if (!n_avail) { assert(!n_alive); break; } + + int count = choose(n_avail, 0); + for (int i = 0; i < N_THREADS; i++) { + if (THREADS[i]->state == THREAD_STATE_DEAD) continue; + if (THREADS[i]->waiting_on) continue; + if (count--) continue; + switch_to_thread(THREADS[i]); + break; + } + } +} + +int imcthread_joinh(imcthread_t thread, void **retval, hash_t hash) { + if (thread->state != THREAD_STATE_DEAD) { + CURRENT_THREAD->waiting_on = thread; + imcthread_yield(); + } + + if (retval) *retval = thread->retval; + return 0; +} +int imcthread_join(imcthread_t thread, void **retval) { + return imcthread_joinh(thread, retval, 0); +} + +static void switch_to_thread(struct imcthread *thread) { + assert(!CURRENT_THREAD); + assert(thread->state != THREAD_STATE_DEAD); + + CURRENT_THREAD = thread; + swapcontext(&MASTER_CTX, &(thread->ctx)); +} + +static void imcthread_entry_point(int tid) { + struct imcthread *thread = THREADS[tid]; + thread->state = THREAD_STATE_ALIVE; + CURRENT_THREAD = thread; + + void *result = thread->fn(thread->arg); + + thread->retval = result; + thread->state = THREAD_STATE_DEAD; + + imcthread_yield(); +} diff --git a/libptimc/libptimc.h b/libptimc/libptimc.h new file mode 100644 index 0000000..c6314dd --- /dev/null +++ b/libptimc/libptimc.h @@ -0,0 +1,49 @@ +#pragma once + +#ifdef __cplusplus +extern "C" { +#endif + +#include <stdio.h> +#include <assert.h> +#include <stdlib.h> +#include <ucontext.h> +#include "libimc.h" + +enum thread_state { + THREAD_STATE_FETUS, + THREAD_STATE_ALIVE, + THREAD_STATE_DEAD, +}; + +typedef struct imcthread { + void *(*fn)(void *); + void *arg; + enum thread_state state; + int id; + struct imcthread *waiting_on; + void *retval; + + ucontext_t ctx; +} *imcthread_t; + +typedef int imcthread_attr_t; + +int imcthread_create(imcthread_t *thread, + // only support NULL attr for now + imcthread_attr_t *attr, + void *(*start_routine)(void *), + void *arg); +int imcthread_yield(void); +int imcthread_join(imcthread_t thread, void **retval); + +int imcthread_yieldh(hash_t hash); +int imcthread_joinh(imcthread_t thread, void **retval, hash_t hash); + +void check_main(void); + +extern void imc_check_main(void); + +#ifdef __cplusplus +} +#endif |