model: unify JOIN- and LOCK-related sleep/wake code

We might as well use similar code paths for JOIN and LOCK operations
that must wait on another thread to re-enable it. The side benefit here
is that the JOIN action is now placed at the correct sequence point in
the execution trace.

model: refactor mutex thread-blocking code

There are a few functions that are used in suboptimal ways.

* use the ModelChecker::get_thread(ModelAction *) version of overloaded
  'get_thread()' function

* the add/remove interfaces were used inconsistently previously; for
  "waking" we directly utilized Scheduler::add_thread, whereas the
  "sleeping" case used ModelChecker::remove_thread

* use the Scheduler::sleep and Scheduler::wake functions for sleep/wake
  instead of explicitly adding/removing

action: don't print clock vector when it is invalid

Due to clock vector snapshotting, a ModelAction may hold a pointer to
an inavlid ClockVector. This fix allows callers of ModelAction::print()
to prevent it from printing a corrupted ClockVector.

small hack to optimize our common case for snapshotting and set config option to turn this back on.

hack assumes that same pages will be dirty across different executions so just copies them and doesn't reprotect them

fix bug....  not quite perfect for linux locks, but runs to completion...

Revert "model: revert broken bugfix"

This reverts commit ae7fcd2e5e499f72d9d1530bdc293f4fbc5f0644.

clockvector: snapshot the whole object

model: revert broken bugfix

This reverts parts of the following commit:

 commit 7ba211ec7d1cacbaa3ef2027f1a0f534888f1708

The bugfix broke our basic test case (userprog)

model: fix "earliest diverge" NULL pointer exception

start support for drawing execution diagrams

fix some signed/unsigned warnings

Fixed bug breaking our consolidation of future values...

Two change:
(1) Bug fix...  Check that rf is non-null before calling
r_modification

(2) Add a hook into assert mechanism for the debugger

rename MYFREE -> model_free

rename MYCALLOC -> model_calloc

rename MYMALLOC -> model_malloc

model: refactor/reword initialize_curr_action()

clockvector: snapshot our clock vectors

Clock vectors need to be snapshotted

mymemory: add placeholder "snapshot_{calloc,malloc,free}" functions

Eventually, we may want a separate heap for the model-checker's
snapshotted data (vs. user's snapshotted data), so create allocator
stubs for this. This allows us to begin annotating our malloc()'s
properly.

model: always re-calculate clock vectors

Clock vectors are mutable, via synchronization. We will need to both
snapshot and recompute clock vectors as they are generated. Right now,
we have some incorrect assumptions in place. This bugfix prevents stale
clock vectors (from previous executions) from polluting subsequent
executions.

another bug fix

bug fix...recompute promises of RMW actions at divergence points

model: utilize bad_synchronization flag

model: add "bad synchronization" flag

Can be used for aborting a trace when an incorrectly-ordered
synchronization occurs.

action: synchronize_with - return status for out-of-order synchronization

"synchronize_with()" now can return a boolean status, rather than just
using an ASSERT(). This allows synchronize_with() to be called with
actions that are against the program trace order, then return a status
to signify success/failure. This will allow, for instance, release
sequence calculations to simply abort this single execution, not the
whole model-checker.

model: remove debug print

missing commit of mo_graph changes

fix bug from moving read_from check_recency...check_recency had the assumption that the read_from field was set...

nodestack: add debug prints

model: push mo_graph cycle check into release_seq code

Release sequences traveral should only be undertaken if the mo_graph has
no cycles. Instead of just making this check a hack within
resolve_promises(), make it part of every release sequence exploration.

model: add RMW violation debug print

doc: add release sequence notes

docs: move to subdirectory

model: avoid infinite loop in release_seq_head()

To understand the problem I'm solving here, note that resolve_promises()
calls ModelAction::read_from() which calls ModelChecker::release_seq_head().

Now, release_seq_head() has the basic assumption that the mo_graph
doesn't have cycles (or specifically, in this case it's important that
sequences of RMW's don't form loops in the reads-from relation).
Unfortunately, resolve_promises() can create such a cycle (by assigning
the "reads-from" value) before checking if that would create a cycle.
This will trigger a check to release_seq_head, which gets stuck in an
infinite loop...

The solution, at least for this targeted portion of code, is to:
(1) First add the relevant RMW edge, if possible
(2) If (1) didn't create mo_graph cycles:
       Then assign reads-from, check release sequences, update
       synchronization
(3) Calculate other normal mo_graph edges

This way, (2) will simply be skipped if we have cycles, avoiding the
problem.

model: bugfix - iterator naming conflict

There's already another iterator named 'it' in resolve_release_sequences().
Although this iterator probably will mask the earlier iterator (giving correct
behavior), it's probably safer to rename the later one for clarity.

model: re-check release sequences after THREAD_JOIN

If a THREAD-specific operation (from process_thread_action()) added any
synchronization, we should re-check all release sequences.

model: add current action work_queue comment

model: mutex synchronization -> re-check release sequences

All synchronization updates should generate a re-check of release sequences.
This commit corrects this for mutexes.

model: trivial - rename 'updated' -> 'update'

model: bugfix - release sequences - handle Thread completion

A completed Thread cannot generate any new writes that would break release
sequences.

model: fixup spelling (and formatting) in comments

relese -> release

model: split THREAD_* processing into process_thread_action()

The THREAD_* specific functionality can easily be in its own function.

Additionally, this patch:

* performs the trivial rearrangement of moving this code inside the
  work_queue loop, for consistency

* returns a "synchronized" status, so that THREAD_FINISH/THREAD_JOIN can be
  hooked into the work_queue update loop later

Merge branch 'norris'

model: release_seq_head - rewrite RMW recursion as loop

A bug in release sequences coce (independent of this patch) causes a huge
blowup of the recursion, yielding strange stack errors. So I address "@todo
Might it be better to make this into a loop", causing a loop of memory usage
instead. This can be triggered, for example, with:

  ./run.sh ./test/linuxrwlocks.o -e 1 -f 4 -m 1

add comments

fairness changes...
fix bug with putting enabled information in wrong place
reveals norris bug...

model: flatten "pending acquire/release sequence" structure

This structure should just be a simple flat array, so that we can simply
iterate through all acquire operations with pending release sequences. There
probably wasn't much to be saved by organizing this structure as a hash table
of lists; if so, I can add the complexity back in later.

This eliminates the need for a separate 'lazy_sync_size' count and renames
'lazy_sync_with_release' to 'pending_acq_rel_seq'.

Merge branch 'norris'

1 bugfix

model: bugfix - infinite loop in resolve_release_sequences()

comments

Merge branch 'norris'

model: fixup style

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

more documentation

model: release_seq_head: improve ordering of tests

We can get useful information from a non-write action, as long as we aren't
checking it for modification order or breaking of the release sequence.

model: release sequences: check last action in each thread

Previously, release_seq_head would only examine actions on a particular, given
object to determine a release sequence. However, we can get information
regarding the possibility of future disruptive writes by checking the clock
vector of the last action of each thread, regardless of object.

model: pad the digits in exec#.dot filenames

The generated .dot files can't be sorted alphabetically once we have double
digit executions. Make the filename use a 4-digit number, padded with zeros.

model: add const qualifiers, fixup comments

The "get_last_*" series of functions should be labeled const.

Also, some of the comments were missing/incorrect.

documentation

model: get_last_conflict - replace if/else-if block with switch

Makefile: move common Mac flags to common.mk

fix compilation (includes)

bug fixes for lock support...think it works now...

fix merge

changes

push changes

merge stuff
Merge branch 'master' into mutex

Conflicts:
model.cc
model.h

more mutex changes

support for locks...  untested, but doesn't break quick run of a sample of test cases

more bugs

fix merge bug

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

Conflicts:
model.cc

my schedule changes

merge in master

fix bug

model: replace list type with action_list_t

model: add typedef for list of release sequence heads

model: THREAD_JOIN synchronizes with THREAD_FINISH

action: THREAD_JOIN can synchronize against execution order

synchronize_with() had an assertion to ensure that synchronization never
occurred opposite the execution trace ordering. But THREAD_JOIN is a special
case, where this ordering won't break the rest of the model-checker.

ichange

model: add curr to action lists early

The current action should be added to the ModelChecker lists early within
check_current_action, so that we can have consistency throughout the function.
We only allow an isolated piece of initialization (initialize_curr_action) to
occur before this step.

model: document behavior of ModelChecker::initialize_curr_action

model: pull "may_read_from set" calculation out of initialization

The build_reads_from_past calculation shouldn't be part of the action
initialization. It requires more information from the ModelChecker.

In the future, we will assume that all check_curren_action code (after
initialization) may include the current action in the model-checker lists. So
this also fixes up the build_reads_from_past code so that it skips the current
action.

model: refactor ModelChecker::initialize_curr_action

Rewrite some logic for simplification. Just refactorization.

model: move init code to ModelChecker::initialize_curr_action

Refactoring

changes

model: pull computation out of conditional

tests: add releaseseq test

Very simple release/acquire test, with some relaxed writes thrown in. The test
is semi-useful and can certainly be tweaked a bit.

model: add some mo_graph fixup code to work_queue

The work queue has all its work items implemented now. But I haven't fully
verified that this is complete yet.

Merge branch 'norris'

Primary change: push 'add_action_to_lists()' before main work in
'check_current_action()'

cyclegraph: add ASSERT() for reflexive edges

model: add infeasibility debugging

common: print tracing info for ASSERT() failures

This adds a global model_print_summary() function, so we can view the current
ModelChecker summary info when we hit an assertion.

model: bugfix - w_modification_order handling current action

The current action should be skipped when iterating lists in
w_modification_order.

Bugfix thanks to Brian D.

model: fixup r_modification_order

Bugfix thanks to Brian D.

model: check_recency - "already_added" always true

The current action is always part of the lists now.

Bugfix thanks to Brian D.

model: bugfix get_last_seq_action()

The action lists may include the current action, which we don't want to
consider for 'get_last_seq_action()'.

Also, rewrite some of the comments for this function.

Bugfix thanks to Brian D.

more changes towards locks

Merge branch 'master' into mutex

add mutex files

add mutex files

start towards adding support for mutexes