model: remove unnecessary "this->"

main/threads: remove excess headers

clockvector: add ClockVector class

action: split ModelAction off into action.cc

model: free final list

model: free threads, thread_map at destruction

tree: include cstddef for NULL

Needed for newer, stricter compilers...

model: change DEBUG() statement to ASSERT()

Now that I've fixed the model-checking bug that produced this error, turn this
error message into a fail-stop ASSERT() statement. This way, I won't ignore a
bug like this in the future!

bugfix - set backtrack events according to an *enabled* thread

Previously, I naively set a backtracking point for the thread that performed
the conflicting action, whether or not that thread existed at the point to
which I am backtracking. Utilize the TreeNode::is_enabled() method, plus thread
parent walking, to find the correct thread for the backtracking.

Note that this also requires a model checking event for each THREAD_CREATE
event. So add this feature.

tree: add is_enabled(Thread *)

Determine "enabled" by: was the thread created at this point. Checking against
num_threads is a naive way to do this...

tree: revise arguments (use Thread, ModelAction)

Preparation for other changes to the TreeNode.

main: split main() (and related functions) into main.cc

schedule: fix printf warning (size_t uses %zu)

threads: add parent info + get_parent() method

model: bugfix - rearrange debug message

This debug message depends on 'exploring' still being a valid reference.
However, we immediately explore one step via get_next_replay_thread(), which
could discard this Backtrack object. So print the debug message before doing
any exploration of the next execution stage.

model: move class Backtrack to model.cc

Backtrack is only used within model.{cc,h}, so make it an "inner class."

straighten out header includes, comment on Forward declarations

replace non-fatal error messages with ASSERT()'s

Some errors have been overlooked because they are not 'loud' enough. Use
ASSERT() macro to fail-stop.

model: print replay/divergence information when starting a new execution

model: split printing into print_list() function

threads: don't call the userprogram interface for initial thread, just create it

This will help once I start model-checking thrd_create().

common: add ASSERT()

model: number threads from 0, not 1

userprog: print current thread ID

model: add sequence numbers to ModelAction

model: fixup ModelAction print message

threads: move thread_id_t definition and redefine thrd_t type

model: index thread_map by int, not thread_id_t

model: change type for ModelChecker::get_id()

tree: remove tree_t, map thread ids via int, not thread_id_t

In the underlying structure of the TreeNode, use 'int' as a set and list key,
not 'thread_id_t'.

threads: add id_to_int() and int_to_id() inline functions

model: remove braces

clean up header #includes

split header out to action.h

tree: fix header for potential multiple inclusions

model: add is_acquire() and is_release() helper functions

model: wrap some ModelAction helper functions

malloc: add exception info to function header

model: backtracking messages are only for debugging

common: add simple DBG_ENABLED() macros

thread: remove dead Thread code

model: fixup thread ID selection

demote 'system_thread' to just 'system_context'

I don't need the extra 'class Thread' metadata for the ModelChecker 'system
thread,' and the dual use of class Thread for both system and user threads was
causing problems. So I separate them: class Thread is used only for user
threads. This changes a few interfaces throughout the code.

libatomic: add atomic_init()

userprog: print atomic load/store values

libatomic: use 'values' for atomic load/store

model: bugfix - detect conflicts properly

Finding a conflict from the same thread does not mean we should quit the search
with no found conflict; we just continue to the next search item.

libatomic: add DBG() calls

model: bugfix - reset the "current_action" after it has been processed

There are executions under which we may call ModelChecker::check_current_action()
twice in a row without an acutal ModelAction (curren_action) being set in
between. This causes the previous action to be queued twice in our trace
listing.

This can be solved 2 ways:
(1) set current_action to NULL after processing it
(2) move all calls to check_current_action() under the THREAD_READY codepath,
    so that we guarantee that some Thread pushed an Action back to the
    model-checking system

I do both.

librace: format DEBUG() prints properly

Apparently ISO C99 defines macros PRIuXX for proper printing of different-sized
uints.

librace: add load/store interface for checking data races

The compiler portion will need to replace loads/stores with calls to the
store_X() and load_X() functions.

model: remove unused definition

threads: allocate Threads in via userMalloc()

Thread state information should be held in the snapshotting region (when
implemented), so override new and delete.

common: introduce userMalloc() and userFree()

These are stubs for now, but I will need these.

libthreads: remove unnecessary 'extern'

run.sh: add simple 'run' script

Performs the step of setting LD_LIBRARY_PATH for simple runs.

userprog: use typedef'd thrd_start_t

.gitignore: add *.so

Makefile: build model checker as shared library (libmodel.so)

lib*.h: wrap C headers in `extern "C"'

libthreads: don't create ModelAction for thrd_join()

Temporarily? I may need to model-check join operations later.

model: rename print_trace() -> print_summary(), fixup summary printing

schedule: only print when DEBUG is enabled

tmp (model)

threads: cleanup inconsistencies in memory management

threads: set up Thread to be freed properly

To ensure that we can free memory properly, set up a destructor and rename
dispose() to complete().

schedule: reset scheduler when thread is removed

Ensure that the 'current' thread reference is removed properly.

threads: don't make direct call into scheduler

Since I need a ModelChecker::add_thread(Thread *) function anyway, I should
direct add_thread() calls through the model-checker framework rather than the
Scheduler class. This will make things a little cleaner and symmetric when I
add a remove_thread() function.

threads: save id within class Thread

There may be points at which the user's thread ID struct goes out of scope, but
I still need it internally. I think I'll just keep it internally, with a
duplicate in the user's copy.

threads: initialized Thread member variables

unify style for returning pointers

When returning a pointer from a function, always put a space between the type,
the '*', and the function name. E.g.:

  type * func(args);

model: print 'number of executions'

In preparation of many executions, I establish a counting variable
'num_executions'.

threads: prepare system to loop over many executions

improve scheduler debugging

schedule: bugfix - set 'current' thread in all cases

When the scheduler was following a model-checking replay execution, it did not
set the 'current' thread properly.

schedule: refactor next_thread() for better debug printing

It makes more sense to call print() at the end of the the next_thread()
routine, to see consistent printing for all cases. So I refactor the control
flow to a single return statement.

schedule: print debug info

model: add simple comment

model: move public functions to private

model: implement get_next_replay() and advance_backtracking_state()

model: implement, use schedule_next_thread()

Relies on the rest of the model checker to set the next thread; simply returns
the chosen thread.

model: add prototypes to header

I will implement these functions in the next few commits.

model: add iteration routines for class Backtrack

model: include <cstddef>

NULL is not a builtin keyword in recent C++ revisions. I have to include
<cstddef>.

schedule: replace queue with list

I'll need random access to its elements later.

threads: introduce THREAD_ID_T_NONE

Represents a kind of 'NULL' thread, but for integer IDs.

threads: remove leftover class 'prototype'

model: stash each backtrack event in ModelChecker::backtrack_list

model: add class Backtrack

model: create 'action_list_t' typedef

'std::list<class ModelAction *>' is a long name for a repeated type. Replace
it.

model: convert 'action_trace' to pointer

We need to swap out this list with a new one when we reset, and we want to
retain references to this list easily, so make the ModelChecker::action_trace
member into a pointer to a list.

model: add TreeNode debugging information to print_trace()

model: implement get_last_conflict()

This performs a non-optimized check; that is, it uses a simple O(n) linear
search, when it could utilize O(1) lookups instead... but this isn't even the
full memory model yet, so I'm not working for perfection!

model: flesh out set_backtracking()

Relies on stub get_last_conflict() function.

Note: so far, implementing based on seq_cst model, not the full memory model...

model: flesh out check_current_action()

Relies on a stub set_backtracking() function.

model: add accessors for ModelAction variables

(+ add 'node' member, pointing to the state-space tree just before the action)

tree: bugfix - fix backtrack status

tree: don't use 'NULL' for a thread ID

libthreads: only record 'final' even for thrd_join

model: use TreeNode()

Very basic initialization...