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

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.

model: fixup happens_before/reflexivity, add 'curr' to lists earlier

Some code under 'check_current_action' assumes that the current action is not
added to the ModelChecker trace/list data structures yet. However, some
features I need to add will require the current action to be in these
data structures already. So there are a few spots I need to fixup so that the
code can handle "happens_before" reflexivity properly.

This commit moves the "add_action_to_lists()" call as well as fixes up
reflexivity.

Merge branch 'norris'

model: release_seq synchronization generates mo_graph edge "work entries"

Now, when the synchronization for a ModelAction is updated while resolving
release sequences, the affected ModelAction(s) can be queued to the work_queue
for later processing (i.e., checking for mo_graph edge additions).

Note that the MOEdgeWorkEntry is not yet handled in the work_queue loop.

.gitignore: ignore .dot graph files

model: record the number of feasible executions

The 'num_executions' statistic isn't quite as useful now. We want to compare
total executions to the number of feasible executions.

config: don't enable graph dumping in master repo

model: add work queue loop

This commit does not change the actual computations performed yet. It only
prepares a loop structure in which we could perform many different Work items,
queueing them up as they are generated.

workqueue: add work queue structures

tabbing

(1) add actions for the fence
(2) a little more support for cyclegraph -- show rmw edges
(3) add extra documentation for norris

add support for dumping cyclegraphs as dot files...  also eliminate redundant edges to make them easier to view

model: more restructuring of read/write processing

Make a ModelChecker::process_write function, for symmetry and to shorten the
code portions where the main control flow happens.

model: remove unnecessary parameter to ModelChecker::process_read

The current Thread can be generated later.

Makefile: add PHONY targets

Just in case there ever are files named clean, mrclean, etc.

bugfix: straighten out STL vector allocation (snapshotted vs. persistent)

When using a STL data structure allocated on the stack, we must make sure its
elements are allocated with the same allocator as the structure. For instance,
in a model-checking context, the stack is persistent (non-snapshotting), so any
stack-allocated std::vector should use the non-snapshotting allocator (i.e.,
MyAlloc).

At the same time, clarify CycleGraph and CycleNode classes by labelling them as
SNAPSHOTALLOC.

model: bugfix - don't clobber 'updated'

The 'updated' variable should stay 'true' even if modification orders and
promises aren't updated by the "write" checks. This could be a RMW which made
updates via the "read" checks.

Revert "Makefile: don't always rebuild make.deps"

The Makefile wasn't using its dependency generation correctly. Revert this for
now.

This reverts commit 870ba814eceb1afee4eefb17dab3980549ca73e2.

snapshot: print stack trace on segfault

common: add print_trace() for backtracing

model: trivial fixups

Makefile: don't always rebuild make.deps

The dependencies don't need to be regenerated for "make tags", "make docs",
etc.

model: simple ASSERT() bug

Don't ASSERT(rf->is_write()) until we're sure that rf is non-NULL.

main: wrap help message

model: kill unneeded local variable

The "Thread *th" variable is used only on a few control paths, and it is never
reused. Might as well just calculate it on the fly. Also, it's recalculated and
masked by another local variable at a deeper level of nesting.

spacing

Merge remote-tracking branch 'origin/makefile'

lots of debugging here... finally working with my rmw example...

Makefile: fixup Mac dependencies

Now, Mac OSX builds can just use "make", not "make mac". (This also allows
"make debug" for Mac OSX)

cleanup style

commit new test case

fix for horrible bug...  turns out that we could generate an infinite set of bad executions due to future values...
fix--don't send future values backwards until all of your promises are resolved...

missing changes

right fix for avoid rmw cycles...  bad assumption in the cyclegraph

another bug fix...

separate out rmw actions
make sure we don't insert promises twice for a node

(1) structure code a little better
(2) add startChanges to cyclegraph...  This is just to check some assertions that rollback is being used correctly and doesn't rollback unintended changes

deal with looping due to bogus future value via promise expiration
fix promise bug

fun issues...
(1) need to compute promises for rmw nodes...they could satisfy them
(2) don't call rmwedge if you don't know where you are reading from yet
(3) miscopied commit from big merge (already_added -> !already_added)
(4) avoid adding rmw edges back to itself
(5) probably worth adding a check that the execution isfeasible before sending future values
(6) resolve promises should add rmwedges when appropriate
(7) fix seq_cst to mask earlier writes..

threads, model, schedule: refactor thread joining

The Thread can hold a list of ModelAction (instead of Threads) that are waiting
for its completion. This will give the exiting Thread a better ability to
handle the event.

This also deletes Scheduler::wait, since it is no superceded by Scheduler::sleep.

model: add ModelChecker::get_thread(ModelAction *act)

Many times, I need to convert ModelAction to a Thread. Overload get_thread() to
make it easier to use.

schedule: add sleep() function

The wait() and wake() functions are not very complementary. I will be removing
wait() in favor of a simpler sleep() function, which is introduced here.

cyclegraph: add non-NULL assertions

Merge branch 'demsky'

Branch cleaned up by Brian Norris

model: cleaning up some code

model: handle RMW, unresolved reads in w_modification_order checks

model: fix the maxreads support

model: some bug fixes to the model checker

linuxrwlocks: two bug fixes; guess the model checker helps find bugs

model: bug fixes to new code

cyclegraph: support rolling back changes

model: replace action conditions with switch block

model: add check_recency()

Note the weaknesses of the code, as documented in @todo.

model: refactor "get next thread" code

get_next_replay_thread() might as well handle all the Thread decisions for the
model-checker. Refactor, and rename to get_next_thread().

model: add too_many_reads flag

nodestack: add get_read_from_size()

main: add "maxreads" parameter

main: add parameter parsing

Only has a help message for now.

model: fix release sequence with RMW, acq vs. acq/rel

Check in a bugfix from Brian D

model: maintain a count of the pending lazy synchronizations

lazy_sync_size should be the sum of the size of all the lists in
lazy_sync_with_release.

model: group snapshottable ModelChecker members in struct

These items shouldn't be reset individually, but rather should be grouped
together and allocated on the snapshotting heap. This puts us a step closer to
utilizing partial rollback within executions.

model: force THREAD_START to immediately follow THREAD_CREATE

Note that on the current userprog.c test case, this change causes more
infeasible executions to appear. This is somewhat unexpected but probably just
a result of sub-optimal scheduling.

model: fix release_seq for open-ended synchronization

This fix handles the case where a thread may not yet have synchronized in a way
that ensures no future writes may break a release sequence. If we encounter
such a thread, we can return false (uncertain) and re-check this potential
release sequence later in the execution.

model: use std::find for release sequence search

model: don't use global 'model' unnecessarily

changes

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

check in my stuff...

Conflicts:
model.cc
threads.h

changes

Merge branch 'norris'

Fixes up some THREAD_JOIN behavior, cleaning up a little bit of general model-checker structure.

model: complete the Thread teardown during THREAD_FINISH

model: enforce rule: current_action != NULL

Now that I've fixed THREAD_JOIN, modify the comments and safety checks.

libthreads: don't spin on THREAD_JOIN

THREAD_JOIN can now be implemented properly here. We shouldn't have to spin,
waiting for another thread to complete. This may help improve the ModelChecker
architecture, since we will never have NULL actions passed to the ModelChecker.

model: hook up THREAD_JOIN and THREAD_FINISH actions

schedule: add wait and wake functions

These functions will be used to prevent execution of threads that should be
waiting for another event (e.g., a THREAD_JOIN should cause a thread to wait
for another thread's exit).

threads: fixup THREAD_READY comment

This state will be used for more than just a context switch, so reword the
comment.

threads: add THREAD_BLOCKED state

To signal that a Thread cannot yet be added back to the Scheduler's ready list.

threads: add a wait_list

This list will contain all Threads that are waiting on the current Thread. Will
be used for Thread joins, in particular.

threads: add is_complete() helper function

action: add THREAD_FINISH action

For cleanly finalizing a thread.

snapshot-interface: debug prints: lengthen the "regionname" field

working towards making datarace detection work

bug in race detector

another example

model: document ModelChecker::check_current_action

model: check_current_action returns its 'nextThread'

To begin some code structure rearrangements, I make check_current_action()
return the 'nextThread' value as a true return value. Eventually, the
nextThread field might not be needed, and the model-checker behavior might make
more sense...

model/schedule: revise 'nextThread' data flow

The ModelChecker::nextThread field was being abused a little in my aging
design. It really should be either a private field (not accessed even via
accessors) or else just a return value / function parameter.

This commit makes a change so that nextThread is a Thread pointer and is
directly supplied to the Scheduler. If it is NULL, then the Scheduler is
allowed to pick its own Thread to run.