userprog: use modulo

Increasing the number of loops is useless unless we have modulo here... I
don't know why this was changed by Subramanian.

libthreads: fix thrd_create() to use typedef'd start_routine

fix indentation + spacing, esp. for MEMALLOC macro

mymemory: fix indentation, spacing

nodestack: allocate from "mymemory" region

Merge commit: branch 'work'

tree.{cc,h} were replaced with NodeStack. (Will need to update them)

Other trivial conflicts in Makefile and model.h

Conflicts:
Makefile
model.h
tree.cc
tree.h

snapshot: remove references to libmymemory.so

This library doesn't exist any more.

snapshot: move local defines after #includes

Prevents accidental dependencies, where a header *might* use PAGESIZE, e.g.

main: clear out redundant comments

We don't really need these. I can read the source :)

common: disable debugging

Note to others: do not enable debugging in the checked-in code. It is for
testint purposes only.

run.sh: provide gdb option

Makefile: only build a single shared library

Now that everything is uniform, we can easily just build a single library.

Makefile: clean up Makefile

There are a number of inconsistencies and superfluous arguments:

- For libmymemory, we don't need (or want) to hardcode a shared library
  relative path
- For libmodel, we don't really need the 'soname' parameter
- Linking C++ probably should be done with the C++ compiler, not the C compiler
- We don't need CPPFLAGS for linking-only stages
- We want to use LDFLAGS for an early-stage linking rather than the late-stage
  linking of the user program

Overall, simpler is better

Makfile: remove MEMCPPFLAGS, more uniform command format

remove lines from other files

Found new way to fix emacs issue..  There are directory level preferences.

Remove file-level emacs comment and replace with directory level overrides.

fix various problems with my 64-bit clean hack
found missing initializer bug in scheduler

fix code to be 64 bit clean

switch back to norris style spacing in changed files

main: what are these variables for? (subramanian...)

run.sh: don't touch my run script subramanian

Makfile: fix linking error + remove EOL whitespace

If you're using libdl for dynamic loading, you need to include the library flag
at the top-level linking.

.gitignore: fixup bad merge step

(You don't need both the *~ and *.*~ rules)

remove unused #define

my changes

let us set the size of the heap in a sane way

setup main wrapper and then call into norris code

get rid of redundant mallocs

transfer stuff

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

action: neuter the "same_var" function for now...

Due to some incorrect functionality for 'reset_to_initial_state()' we may not
always have the right stack locations for every execution. I'll ignore the
problem temporarily...

model: remove free_action_list() function

model: remove class Backtrack

tree: kill class TreeNode

Superceded by NodeStack

model: replace TreeNode with NodeStack

Big structural change to the model-checker internal data structure. It's now
tested to work, and hopefully it's still easy enough to understand.

Note that also, we remove the backtrack_list, since this type of structure
depended on keeping around "action lists" of each trace. Instead, I can free up
those lists at the end of each execution, preventing leaks and limiting memory
usage.

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