Adding fixes for the fork based implementation, also removed some redundant code pointed to by Prof. Demsky

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

check in message

snapshot-interface: replace Subramanian's /proc/*/maps checking

Subramanian's code needed rewriting. It didn't actual snapshot any globals, and
it was also written so that it would never snapshot libmodel.so. I rewrite this
code and fix these problems, after Brian Demsky has fixed the problem with
dynamic linking of the HandlePF() code.

fix bug...this is another evil one...

node: do not use static member variable

Static member variables of a class are going to be snapshotted. Move them so
they aren't static in order to prevent this.

(This can create interesting behavior, where the "total number of nodes
created" is decreasing at times!)

snapshot: move declarations to the right interface header

We should have a minimal set of code/declarations in the snapshot-interface.h
header. And it should not include other headers unless necessary. With this
change, the model checker code only needs to use snapshot-interface.h.

snapshot: rename MyFuncPtr to VoidFuncPtr

Better descriptive name.

snapshot: rename USE_CHECKPOINTING to USE_MPROTECT_SNAPSHOT

"Checkpointing" is a generic name for either method. USE_MPROTECT_SNAPSHOT is a
more descriptive name.

snapshot-interface: don't redefine PAGESIZE

snapshot-interface: bugfix - fixup array indeces

When removing code, I missed a few magic numbers in the code.

nodestack: push 'create_cv' functionality responsibility back to ModelChecker

It doesn't really make sense to have NodeStack call the 'create_cv' function
for a ModelAction. This commit separates the functionality of 'explore_action'
from 'create_cv', calling each separately from the higher-level
'check_current_action' model-checking function.

model: thread creation establishes synchronization

First, I add a get_parent_action() wrapper which finds either the last action
in the current thread (get_last_action()) or if NULL, finds the parent
thread-creation action.

Then, using this functionality, I provide the correct 'parent' to the
explore_action() function, which performs the clock-vector creation.

threads: add 'creation' information

The 'creation' field will hold the ModelAction that created the thread. For the
main user-thread, this is NULL.

libthreads: pass 'class Thread' object as ModelAction 'location'

Currently, the 'location' parameter is unused for THREAD_CREATE. I need to
provide a reference from a Thread object to the ModelAction which created it,
so I will use this parameter as an entry point into the ModelChecker, which can
build the necessary reference later.

model: move bookkeeping to add_action_to_lists()

I keep a lot of bookkeeping info for efficiently locating ModelActions (e.g.,
in lists, maps, vectors). Let's just perform the dirty calculations in a single
function to help separate logical functions a little better.

model: set 'last action in thread' as an action's parent

This is a step toward synchronizing clock vectors properly: on exploration of
an action, we use only the last action in the current thread as the 'parent'
(or NULL).

Note that this still does not include the parent thread in determining each
ModelAction's parent.

model: log the last action in each thread

The last action in each thread is needed for some model-checking computations.
This could be expanded to a full-fledged per-thread list if needed...

nodestack: compute parent ModelAction externally

For a particular ModelAction, the 'parent' may be the last action in the
current thread, or otherwise, the action in the parent thread that created the
current thread. This calculation is not suitable for within the NodeStack (and
the current implementation is wrong, taking the last action performed by *any*
thread as the parent). Thus, I set up the method calls to pass the 'parent' to
explore_action() and leave the details to further work.

clockvector: fixup initialization

Two related fixes:

Even if parent is NULL, pass the current ModelAction to ClockVector
constructor.

When no parent is present, do not make special case for initializing
clock[0] = 1. This is only correct for a single case (the root Action)
and is already handled in other ways.

nodestack: construct Node with 'number of threads', not 'parent node'

I don't really want to base the number of threads off of a 'parent'; I can
just record the global 'number of threads' as a Node parameter.

model: add obj_thrd_map

Provides a mapping of ModelActions so that we can efficiently sort through the
actions on a particular object (memory location) in a particular thread.

Makefile: add 'make debug'

This is sort of hacky, but it works! Now (after cleaning), you can recompile
with 'make debug' to enable my debugging features (not Subramanian's).

action: enhance print() message

Include clock vector, realign

nodestack: create ModelAction clock vectors

Only create the clock vector if the ModelAction will be retained in our
nodestack, and hence will be used for synchronization, etc.

action: add create_cv() and read_from()

These functions provide basic wrapper functionality for creating and updating
the clock vector for a particular ModelAction.

clockvector: bugfix - fixup vector initialization, size

This fixes a few bugs in ClockVector:

- The parent-less vector is the initial-thread creation, so set its vector
  clock[0] = 1
- The clock vector's data should be initialized to 0
- A clock vector cannot determine its size simply by the size of its parent (+1
  if 'act' is THREAD_CREATE); other threads could have been created, giving an
  inconsistent result here. Instead of trying to be smart about calculating
  num_threads from the parent, then, I just ask for it globally.

model: add get_num_threads()

clockvector: fixup print message

clockvector: add print() method

action: add clock vector field, destructor

action: use proper location comparison

Now that snapshotting is in place for the initial state, stack allocation is
deterministic across executions, so we can compare stack-allocated addresses
again.

clockvector: add snapshotting new/delete operators

rename snapshotStack -> SnapshotStack

snapshot: remove #include, use snapshot_id typedef

snapshot-interface: cleanup interface header

The MyString type does not belong in an interface header. It's only used in one
file, so move its typedef locally.

Remove/move a bunch of misplaced #includes.

There's an unnecessary forward declaration of class snapshotStack.

model: remove scheduler comment

It's being snapshotted now.

model: don't clear thread_map (snapshot)

The thread_map structure is being snapshotted, so no need to clear it.

model: don't reset action_trace manually

Snapshotting takes care of this one

main: take/revert snapshots

Use basic snapshotting for 'reset_to_initial_state()'.

model: make thread_map heap allocated

I want to snapshot this structure, so make it heap-allocated.

action: add all action_lists to snapshot...

common: remove unneeded macros/includes

threads: fixup stack allocation (snapshotting...)

snapshot: remove time information

Why do we need timestamps? This is unneeded extra code and might cause
problems.

snapshot: fix indentation

snapshot: use %p for printing pointers

more allocation fixes (use snapshotting)

nodestack: bugfix - fixup allocators for vectors

add more classes to snapshotting region

Classes that don't use MyAlloc or MEMALLOC are snapshotted by default.

mymemory: use the right *&^% allocator!!

We're using MYMALLOC in the global new/delete instead of defaulting to
snapshottable malloc, as planned. What a stupid bug.

Also extend new/delete operators to be sure.

snapshot: fix EOL spaces

wow, this is a nasty bug...

the last part of the snapshot bug is the following:
we snapshot the user threads stack...  when we get a seg fault,
the signal handler is using the same write protected stack...
obviously this is going to cause problems.  luckily there is support
for a special stack for the signal handler.  this checkin switches
the signal handler to run on a different stack than the program stack.

Revert "fixing the segfault"

This reverts commit 7f305f5e6af465a60ec930832fbc6ec35bd8c693.

fixing the segfault

fix one segfault bug...something is still strange, but has to do with stack

factor page alignment into function call...place near existing call

fix page alignment issue...

snapshot: use perror() on failed library calls

This will print more informative messages when we fail.

mymemory: define the "opposite" of MEMALLOC

We may want an identifier to show that a particular class is intended to be
snapshotted.

mymemory: include some spacing

fixup EOL whitespace

snapshot: use 'SSDEBUG', not 'DEBUG'

model: remove incorrect #undef

Don't 'undef' something; rename it. Anyway, this is unnecessary now, since
someone renamed the new DEBUG.

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