Skip to content

Files

Latest commit

May 16, 2024
69252d9 · May 16, 2024

History

History

exhaust-libptimc

##### Replaying bugs

Bugs will be placed in the bugs/ subdirectory.

To replay a bug, use

    $ ./build/examples/whatever bugs/BugID

##### 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