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

tree: fix invalid free

tree: add class TreeNode

Untested, but ported from Nachos project.

rename threads_internal.h -> threads.h

threads/model: move switch_to_master from class Thread to class ModelChecker

rename binary: libthreads -> model

libthreads: split into libthreads and threads

For user-program vs. internal usage

major rewrite - 'struct thread' replaced with internal 'class Thread'

Rewrite code such that most thread data is kept internally, not within the user
program.

Makefile: add debug compilation flag

scheduler: kill 'replaceable' scheduler

I don't actually need a replaceable scheduler; I need a scheduler that can
switch policies at will. Just remove this level of abstraction for now (it can
be added later if needed).

libthreads: print out trace at end of execution

model: add print_trace() function

Prints out the current program trace.

libthreads: perform 'model checking' when moving to next thread

Simply use the hollow 'check_current_action()' interface to perform model
checking in the thread_system_next() call.

Right now, this just adds the previous (a.k.a. 'current') action to our log.

userprog: use both atomic loads and stores

(Meaningless change to 'user' program; just for testing purposes)

model: add check_current_action() function

This interface provides a wrapper for all our model checking operations on the
current action (at least, ideally this should work...I might need to work on
this a bit).

For now, we just record the program trace of all atomic/thread actions.

libthreads: thread_join: return 'int' as status

threads_internal: pass the current 'action' to the internal thread system

I build a ModelAction object to represent the properties of the current action
that are relevant to the model checker. This action should be passed from the
basic action (atomic_load, atomic_store, thread_yield, etc.) into our thread
library and eventually to the model checker.

I don't use these actions yet, but they will be shortly.

model: add class ModelAction

Represents a single action (sometimes called transition) in our program. This
can be a THREAD_* event (creation, join, etc.) or a relevant read/write
operation (e.g., atomic reads/writes). This object and interface is subject to
change a little...

threads_internal: add 'thread_switch_to_master()' internally

In progress: moving more model-checking/thread actions so that they are
performed only by a system thread, not by the user code.

For now, we replace our uses of thread_yield() (which simply switched to the
next user thread) while thread_switch_to_master() (which will later perform
intermediate actions before choosing the next user thread).

Also, we can begin creating internal and external interfaces in
threads_indernal.h and libthreads.h, respectively.

libthreads: make typedef for 'thread_id_t'

Just in case we need to change it later on, let's use it as a named type.

use my{Malloc,Free} in model-checking code

Also, fixes 'leak' where we forgot to free the main_thread.

malloc: override 'new' and 'delete' globally

Not sure if this is correct...

Q: do we also need to overload new[] and delete[]?

malloc: add myMalloc() and myFree()

common: rename "CONFIG" to "COMMON"

schedule: use STL 'queue' instead of 'list'

remove unnecessary #includes

schedule: make 'current' a private member of the scheduler

schedule: use STL list class instead of custom queue

rename other *.c to *.cc

userprog.c remains for now...

schedule: move schedule.c --> schedule.cc

schedule: create 'class Scheduler' with implementation 'class DefaultScheduler'

libthreads: delete allocated object

model: use 'this' uniformly

model: move model.c --> model.cc

model: change 'struct model_checker' to 'class ModelChecker'

Makefile: switch to C++ builds

stricter typing of function pointers for makecontext()

We need to use functions with no arguments (i.e., 'void (*)()') in order to
retain strict type-checking with makecontext(). Of course, we still circumvent
this type checking with casting, but we should straighten this out sometime...

C++: don't use C++ keywords as names (this, new, etc.)

C++: cast result of malloc