makefile

At least everything compiles now...  Subramanian's changes pushed into main fork...  unclear whether it works...

merging stuff...made need to clean up some stuff...but need to push it somewhere else for now
Merge branch 'subramanian'

Conflicts:
.gitignore
Makefile
action.h
userprog.c

fix this stuff...

userprog: tweak test program to use simple loads/stores

libatomic: place the proper read-value in 'atomic_load' ModelActions

Even though I was doing rudimentary loading and storing of atomic values, I
didn't properly record the value in the ModelAction. That will be confusing
soon if I don't fix it. So fix it.

don't check in useless files

librace: actually compute the loads and stores

We need to perform the actual load or store within our race detection library,
since the model checker totally takes over the operation.

Defining the interfaces to add various regions to snapshot

action: add get_node() accessor

nodestack: remove unnecessary conditional

I expect that we should never have a totally-empty NodeStack. It is designed
such that there is a stub 'empty' node that represents the choices at the start
of the program, when the first userprogram thread is 'created' (note: there is
no corresponding ModelAction for this first creation).

model: merge advance_backtracking_state() and get_next_replay_thread()

model: rename check_current_action() local variables

This function needs some major rewriting when transitioning from our Tree to a
"Stack". Start by properly naming "next" as "curr".

action: add comparison operator for ModelAction

The operator simply compares the sequence number. Useful for some simple
model-checking tests.

nodestack: add class NodeStack and class Node

These will replace class TreeNode in the near future, since I don't need to
retain the entire execution tree: just the stack of the current tree, along
with some backtracking information.

.gitignore: add *~ files

model: change constructor assignments to initializer list

Apparently this is a nice C++ feature I didn't know of. Not much use here,
but there will be other uses...

Initializing variable which contains global snapshotting regions

Adding support to return global segments of the process using the /proc/maps

Adding STL stuff and operator news of snapshot to model-checker. Need to actuallly find the hooks which do the actual snapshotting

action: rename 'node' members to 'treenode'

I am transitioning from class TreeNode to another class (perhaps class
Node?), so rename these members to avoid collision.

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