datarace/clockvector: switch 'clocks' to use 'unsigned int' (modelclock_t)

clock: add modelclock_t typedef, use 'unsigned int'

Clocks should be unsigned and documented as their own 'modelclock_t' type.

add forgetten file

add support for datarace detection...

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

Merge branch 'brian'

Adding relevant comments for fork based implementation.

Makefile: compile *.cc separately

This Makefile rule doesn't have to include all *.cc files at once. They can be
compiled separately.

Note that this slows down compilation slightly, but it also allows better
parallel (jobserver) compilation; for example, you can use `make -j4' to
perform separate compilations using 4 different threads, utilizing a multi-core
system more effectively.

nodestack: revert may_read_from to a normal member variable, not pointer

Because we don't control the 'new' operator for STL sets, I can't properly
ensure that it is allocated in non-snapshotting memory. So just make
may_read_from a normal member variable within class Node, so that its
initial 'allocation' is performed as part of the instantiation of its
subsuming Node object.

action: add {get,set}_value(), assign default value

add documentation

nodestack: only create may_read_from sets for read operations

nodestack: re-associate ModelAction/Node relationship

Currently, the Node that is returned by ModelAction::get_node() actually
represents the Node that is parent to the ModelAction. This works well for
some of the backtracking computations (since the backtracking set is held
in the parent Node), but it creates confusion when performing computations
such as the following:

 Node *node;
 ...
 ModelAction *act = node->get_action();
 Node *node2 = act->get_parent();

 ASSERT(node == node2); // Fails
 ASSERT(node->get_parent() == node2); // Succeeds

So this patch changes this behavior so that the first assertion (above)
succeeds and the second one fails. This is probably more desirable in the
long run.

nodestack: add Node::get_parent() function

As I add more complicated backtracking and may-read-from relationships,
each Node might need some structural information to be able to reach its
parent Node.

To support this:
* the NodeStack should provide the parent information via Node constructor
* the Node should provide a get_parent() method

model: make print_list() into a static C function

This function does not need to be a class member function. It only performs
a standard 'printing' option on a STL list of ModelAction objects.

Adding relevant comments for fork based implementation.

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

model: make comment more accurate

add_action_to_lists() does not only work on the per-object, per-thread action
list. It performs several pieces of bookkeeping.

action: add const qualifier

clockvector: add const qualifiers

clockvector: add documentation

Merge branch 'sandbox' (remove finalize())

Merge in the fix from Subramanian and me that eliminates the need for a
finalize() call. It was a kind of bug, in a way, that hopefully is fixed now...

snapshot: switch back to mprotect-based snapshotting

Subramanian accidentally switched this configuration macro in his last
commit...

model: build up 'may_read_from' set

Finally wire up the model-checker so that it builds the may_read_from set
for every 'read' action. I think this is working OK, although I don't have
much to really test it on yet.

Also, improve comments to describe the process in check_current_action().

model: add build_reads_from_past() function

Add function that will build up the initial set of all past writes that a
'read' action may read from.

action: add happens_before() function

Now I can easily compare two ModelActions with the happens_before()
relationship. Of course, the clock vectors are not fully complete yet, but
this sets the stage...

clockvector: fix 'happens_before', change name to 'synchronized_since'

First, the 'happens_before' function needed to use an inclusive 'less-than'
(i.e., <=) instead of 'strictly less-than' (i.e., <) in order to fit with
most of the algorithm.

Second, the association of 'happens_before' directly with the ClockVector is
not very intuitive to use. I will write an additional happens_before()
function that can easily compare two ModelAction objects. So change this
happens_before() (with it awkward usage) to be called synchronized_since(),
representing whether the ClockVector's thread has previously synchronized
with the ModelAction's thread.

action: add 'get_cv()' accessor function

nodestack: add 'may_read_from' set

Each Node (at least, each Node that is a 'read') will be associated with a
may_read_from set - the set of all possible ModelActions to read from. For now,
this interface handles only actions that exist in the past. It won't properly
retain information from future actions.

nodestack: don't perform linear search to check if backtrack is empty

Add a simple add/remove counter to record when threads are 'added' and
'removed' from the backtracking set.

action: add const qualifiers

action: replace condition check with ASSERT()

Now that the ModelChecker and NodeStack have been refactored a bit, I don't
need to rely on create_cv() to avoid overwriting a previously-existing
clockvector; create_cv() will now be called at most once per ModelAction. So
change this condition to an ASSERT().

nodestack/model: refactor explore_action(), change return semantics

ModelChecker would like to know when a new ModelAction is being inserted
into the NodeStack vs. when the new ModelAction should be discarded in
favor of a pre-existing one (due to replay). So I change the semantics of
NodeStack::explore_action() such that it does not always return a
ModelAction; now it returns NULL if the ModelAction was accepted into the
NodeStack, otherwise returning the ModelAction that was already in the
stack.

Now, ModelChecker can choose when to create new clock vectors as well as
other operations (to come) that may be performed only upon *first*
exploration of a new ModelAction.

Additionally, ModelChecker is now responsible for free-ing the ModelAction
if it is not going to be kept in NodeStack.

There should be no change in functionality.

nodestack: more documentation

cyclegraph: make this compile...

You need 'inttypes' for 'uintptr_t'

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

builds

add hashtable

Doxyfile: exclude malloc.c

I don't think we really want documentation for the dlmalloc code. It provides
several Doxygen warnings/complaints, and it muddies up some of the output HTML.
Maybe we can fix this up somehow later, but it's not really worth doing right
now.

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

fixup some doc wording

add more documentation

I'm trying to add doxygen comments next to the definitions (not the
declaration) as much as possible, to keep the documentation as close to the
actual code as much as possible, helping to prevent errors as functionality
changes.

subramanian lied when he said he fixed these...

Makefile: force `make docs' to depend on all source files

That way, if I change a file that might have documentation comments in it,
`make docs' will rerun doxygen.

(snapshot) removing mbFinalize and usage of finalize

Now there is no need for finalize mechanism at all.
All that was required was resetting the rollback id

snapshot: refactor the fork-based stack initialization

This complicated code block uses a getcontext()/setcontext() pair with an
'alreadySwapped' boolean (int) to perform basically the same functionality as
'swapcontext()'. Refactor this code to make it simpler.

snapshot: remove unused 'uc_link' context

The 'currentContext' variable was never initialized, and so doesn't perform any
useful functionality as a 'uc_link' address. Remove it.

snapshotimp: reindent file

snapshot: don't put entire if (...) on one line

It's harder to read the failure conditions if you put if (...) and the
following statement all on one line.

snapshot: define macros with type size_t

The SHARED_MEMORY_DEFAULT and STACK_SIZE_DEFAULT macros need to be of type
size_t, so cast them when they're defined, not when they're used.

snapshot: use (void *) instead of (char *)

snapshot: rearrange #if a little

HandlePF() is only used in mprotect-based snapshotting, so keep it entirely
within the #if block.

snapshot: remove extra blank lines

snapshot: make other file-scope functions static

snapshot: don't export page-aligning functions

Declare these functions static and move them upward in the file.

rename struct Snapshot_t => struct Snapshot

snapshot: don't declare sTheRecord in both #if and #else

snapshot: remove 'extern "C"' block

We do not need to wrap this function in 'extern "C"' for two reasons:

1) It's not actually exported and used in C code
2) You only need this sort of declaration in the header file that may be
   included in both C++ and C compilation. But snapshot.cc should only be
   compiled by the C++ compiler, and snapshot.h is not included in any C
   compilation.

snapshot-interface: don't export SnapshotGlobalSegments()

SnapshotGlobalSegments() is only used within snapshot-interface.cc, so declare
it static and remove it from the header.

snapshot: replace DumpIntoLog() with lighter-weight debugging

This file I/O "debug" messaging gets in the way. Make the debugging code simple
and succinct, or don't put it in at all. Now, you can enabled SnapShot
debugging by adding this near the top of snapshot.cc:

 #define CONFIG_DEBUG

snapshot: move comments to the right place

Removing comment asking to fix fork(), has been fixed now

fixing calloc(), fix Makefile

Adding sbrk() calls and hooked into free also to avoid freeing sbrked memory...
checked both fork and paged implementation. seems to work Also everytime we
switch between fork and paged impl, we need to rebuild so adding snapshot.h as
dependency to mymemory.cc in makefile

libatomic: perform write before context switch

Atomic actions block a thread at the "switch_to_master" function call, so under
the current structure (which isn't quite fit for relaxed modeling yet...) we
should perform the memory write before calling "switch_to_master".

If not, we can observe sequences like the following, where x is an atomic
variable. All actions are seq_cst:

 Initially, x = 0

 Thread    Action
 ------    ------
 1         r1 = x;       // r1 = 0
 1          x = r1 + 1;  //  x = 1, not stored yet?
 2         r2 = x;       // r2 = 0
 2          x = r2       //  x = 1, not stored yet?

Then, depending on scheduling, Thread 1 or Thread 2 might complete first, with
its write being performed *after* it receives control again.

.gitignore: ignore docs directory

action: fix some comments

Makefile: have `mrclean' depend on `clean'

more comments

more doc changes

more documentation

1) Add more comments.
2) Change is_dependent to is_synchronizing and make it capture actual synchronizing behavior...
3) Add more support for RMW operations.

more documentation

more docs

add support for docs

snapshot: zero out entire siginfo_t

We should initialize this variable to all zeros, just to be safe.

Changes needed to run on OS X...  Example runs on my laptop now.  No need to push code back and forth to test...

Out of time for fun hack, have to get back to real work now.  :(

hack some stuff towards running on mac...  unrelated bugs still..

snapshot: remove duplicate definition of finalize()

finalize() was moved to snapshot-interface.h but wasn't removed from snapshot.h

use EXIT_SUCCESS and EXIT_FAILURE

We were wildly inconsistent with our exit status. We might as well follow the
C standard.

userprog: use atomics allocated on "heap"

Just for kicks, since snapshotting is working properly. We might as well test
this.

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.