exhaustive-libptimc seems to be the best

Author: matthewsot

Diff for: exhaust-libptimc/README

@@ -0,0 +1,58 @@
+##### Exhaustive-parallel implementation
+
+Basically:
+
+    - The master sets itself up as a subreaper
+
+    - @N control pipes are opened
+
+    - The master forks off an initial worker, with id 0
+
+    - On every iteration, the master reads from each control pipe. Processes
+      must ask for permission before dying; the master will give them
+      permission after recording the death.
+
+    - After allowing process deaths, if there are empty slots, it picks a
+      random living child. It sends that child a control message telling it to
+      fork, and which id to use.
+
+    - The child *must* respond to this control message, with either success or
+      failure.
+
+#####
+
+# libpthreadsimc
+
+Wrapper for the POSIX Threads API. It should have identical behavior, except
+that it tries running the code _with every possible interleaving_.
+
+Basically, need to do green threading. Keep a list of all threads. At each
+iteration, pick one of the threads to run for some period of time. Fork on the
+choice of which thread to run.
+
+Currently, we require the user to insert yield() calls, and we only switch
+threads at those yield calls.
+
+Eventually, we would like to support automatic single-stepping so these
+explicit yield annotations aren't needed. That should be relatively easy to do;
+fork off a manager thread that single-steps the underlying process when
+requested. But for now we can assume we have yields.
+
+#### Architecture
+
+libimc handles basic branching/choice; it knows nothing about the greenthreads.
+this is mostly copied over from the libraft stuff.
+
+libptimc is a greenthreads implementation using libimc to determine thread
+ordering.
+
+#### Usage
+
+Write your code inside a function called
+
+    void imc_check_main(void)
+
+Use imcthread_create and imcthread_yield
+
+#### Random Notes
+- imcthread_create does *not* act as a yield

Diff for: exhaust-libptimc/examples/5threads.c

@@ -0,0 +1,22 @@
+#include "libptimc.h"
+#include <assert.h>
+
+void *worker(void *_) {
+    // printf("Running worker %llu\n", (size_t)_);
+    return 0;
+}
+
+void imc_check_main(void) {
+    imcthread_t ts[10];
+    int n = (sizeof ts) / (sizeof ts[0]);
+    for (size_t i = 0; i < n; i++)
+        imcthread_create(&ts[i], NULL, worker, (void *)i);
+
+    for (size_t i = 0; i < n; i++) {
+        // printf("Starting the join on %llu\n", i);
+        imcthread_join(ts[i], NULL);
+        // printf("Finished the join on %llu\n", i);
+    }
+    // printf("Done!\n");
+    // printf("---------------------\n");
+}

Diff for: exhaust-libptimc/examples/global_state.c

@@ -0,0 +1,40 @@
+#include "libptimc.h"
+#include <stdint.h>
+
+static uint64_t counter;
+
+static void resetter(void) {
+    counter = 0;
+}
+
+void *worker(void *_) {
+    uint64_t cval = counter;
+    // imcthread_yield();
+    cval += UINT32_MAX;
+    // imcthread_yield();
+    counter = cval;
+    return NULL;
+}
+
+void *sub_worker(void *_) {
+    counter += UINT32_MAX;
+    counter -= UINT32_MAX;
+    return NULL;
+}
+
+void imc_check_main(void) {
+    register_resetter(resetter);
+
+    printf("Starting main; counter value is %llu\n", counter);
+
+    imcthread_t t1, t2, t3;
+    imcthread_create(&t1, NULL, worker, 0);
+    imcthread_create(&t2, NULL, worker, 0);
+    imcthread_create(&t3, NULL, sub_worker, 0);
+
+    imcthread_join(t1, NULL);
+    imcthread_join(t2, NULL);
+    imcthread_join(t3, NULL);
+
+    assert(counter == ((uint64_t)UINT32_MAX) + ((uint64_t)UINT32_MAX));
+}

Diff for: exhaust-libptimc/examples/hashing.c

@@ -0,0 +1,10 @@
+#include "libptimc.h"
+#include <assert.h>
+
+void imc_check_main(void) {
+    int counter = 0;
+    for (int i = 0; i < 5; i++) {
+        counter += choose(2, (counter << 8) | i);
+        assert(counter < 6);
+    }
+}

Diff for: exhaust-libptimc/examples/simple_race.c

@@ -0,0 +1,31 @@
+#include "libptimc.h"
+#include <assert.h>
+
+static int COUNTER = 0;
+
+static void resetter(void) {
+    COUNTER = 0;
+}
+
+void *worker(void *_) {
+    int local_counter = COUNTER;
+    local_counter++;
+    imcthread_yield();
+    COUNTER = local_counter;
+}
+
+void imc_check_main(void) {
+    register_resetter(resetter);
+
+    imcthread_t t1;
+    imcthread_t t2;
+    // printf("About to create two threads!\n");
+    imcthread_create(&t1, NULL, worker, 0);
+    imcthread_create(&t2, NULL, worker, 0);
+    // printf("Threads created!\n");
+
+    imcthread_join(t1, NULL);
+    imcthread_join(t2, NULL);
+
+    assert(COUNTER == 2);
+}

Diff for: exhaust-libptimc/libimc/README

@@ -0,0 +1,40 @@
+###### Using the Core IMC Library ######
+The IMC library header is `libimc.h`. It looks like:
+
+    int choose(int n, size_t hash);
+    void report_error();
+    void check_exit_normal();
+    extern void check_main();
+
+Basic usage:
+
+    1. You write your test harness in a function called "check_main."
+    2. Whenever you want to make a nondeterministic choice, call `choose(n,h)`
+       where `n` is the number of possible choices (must be greater than 0) and
+       `h` is a hash of the current state (or 0 to disable state hashing)
+    3. When you encounter an error, call report_error()
+
+A small example is shown in `imc_wrapper/test.c`:
+
+    #include <stdio.h>
+    #include "../libimc/libimc.h"
+
+    void check_main() {
+        int sum = 1;
+        for (int i = 0; i < 6; i++) {
+            sum += choose(7, ((size_t)sum << 3) + i);
+            if (sum == 37) report_error();
+        }
+        return;
+    }
+
+It should report an error:
+
+    $ ./build/test
+    Found an error with path: 6 6 6 6 6 6
+
+You can trigger a replay of that error like so:
+
+    $ ./build/test 6 6 6 6 6 6
+    $ echo $?
+    1

Diff for: exhaust-libptimc/libimc/_libimc.h

@@ -0,0 +1,77 @@
+#pragma once
+
+#define _GNU_SOURCE
+#include <fcntl.h>
+#include <unistd.h>
+#include <errno.h>
+#include "libimc.h"
+
+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);
+
+enum message_type {
+    MSG_NONE,
+
+    // Worker -> Master
+    MSG_CAN_I_DIE,
+    MSG_DID_SPLIT,
+    MSG_NO_SPLIT,
+
+    // 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 count;
+};
+
+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 == EAGAIN || n_sent == EWOULDBLOCK) 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;
+        ptr += n_read;
+        n -= n_read;
+        if (!any && !n_read) return;
+        any = 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) {
+    tell_pipe(WORKER2MASTER_WR[idx], (uint8_t*)&message, 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 for: exhaust-libptimc/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 uint8_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 for: exhaust-libptimc/libimc/libimc_linux.c

@@ -0,0 +1,9 @@
+#include "_libimc.h"
+#include <signal.h>
+#include <unistd.h>
+#include <fcntl.h>
+#include <stdlib.h>
+#include <sys/wait.h>
+#include <time.h>
+
+extern void launch_replay(choice_t *path);