c11tester.git
9 years agomodel: bugfix - release sequences - handle Thread completion
Brian Norris [Tue, 25 Sep 2012 23:39:07 +0000 (16:39 -0700)]
model: bugfix - release sequences - handle Thread completion

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

9 years agomodel: fixup spelling (and formatting) in comments
Brian Norris [Tue, 25 Sep 2012 22:33:51 +0000 (15:33 -0700)]
model: fixup spelling (and formatting) in comments

relese -> release

9 years agomodel: split THREAD_* processing into process_thread_action()
Brian Norris [Tue, 25 Sep 2012 22:28:31 +0000 (15:28 -0700)]
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

9 years agoMerge branch 'norris'
Brian Norris [Tue, 25 Sep 2012 19:19:44 +0000 (12:19 -0700)]
Merge branch 'norris'

9 years agomodel: release_seq_head - rewrite RMW recursion as loop
Brian Norris [Tue, 25 Sep 2012 18:38:31 +0000 (11:38 -0700)]
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

9 years agoadd comments
Brian Demsky [Tue, 25 Sep 2012 17:12:38 +0000 (10:12 -0700)]
add comments

9 years agofairness changes...
Brian Demsky [Mon, 24 Sep 2012 22:46:52 +0000 (15:46 -0700)]
fairness changes...
fix bug with putting enabled information in wrong place
reveals norris bug...

9 years agomodel: flatten "pending acquire/release sequence" structure
Brian Norris [Thu, 20 Sep 2012 21:00:13 +0000 (14:00 -0700)]
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'.

9 years agoMerge branch 'norris'
Brian Norris [Fri, 21 Sep 2012 17:27:27 +0000 (10:27 -0700)]
Merge branch 'norris'

1 bugfix

9 years agomodel: bugfix - infinite loop in resolve_release_sequences()
Brian Norris [Fri, 21 Sep 2012 17:23:21 +0000 (10:23 -0700)]
model: bugfix - infinite loop in resolve_release_sequences()

9 years agocomments
Brian Demsky [Fri, 21 Sep 2012 00:57:35 +0000 (17:57 -0700)]
comments

9 years agoMerge branch 'norris'
Brian Norris [Thu, 20 Sep 2012 23:33:37 +0000 (16:33 -0700)]
Merge branch 'norris'

9 years agomodel: fixup style
Brian Norris [Thu, 20 Sep 2012 21:29:08 +0000 (14:29 -0700)]
model: fixup style

9 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Brian Demsky [Thu, 20 Sep 2012 22:49:20 +0000 (15:49 -0700)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

9 years agomore documentation
Brian Demsky [Thu, 20 Sep 2012 22:49:02 +0000 (15:49 -0700)]
more documentation

9 years agomodel: release_seq_head: improve ordering of tests
Brian Norris [Thu, 20 Sep 2012 17:59:14 +0000 (10:59 -0700)]
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.

9 years agomodel: release sequences: check last action in each thread
Brian Norris [Thu, 20 Sep 2012 17:47:31 +0000 (10:47 -0700)]
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.

9 years agomodel: pad the digits in exec#.dot filenames
Brian Norris [Thu, 20 Sep 2012 17:45:39 +0000 (10:45 -0700)]
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.

9 years agomodel: add const qualifiers, fixup comments
Brian Norris [Thu, 20 Sep 2012 17:33:58 +0000 (10:33 -0700)]
model: add const qualifiers, fixup comments

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

Also, some of the comments were missing/incorrect.

9 years agodocumentation
Brian Demsky [Thu, 20 Sep 2012 20:59:05 +0000 (13:59 -0700)]
documentation

9 years agomodel: get_last_conflict - replace if/else-if block with switch
Brian Norris [Thu, 20 Sep 2012 17:08:03 +0000 (10:08 -0700)]
model: get_last_conflict - replace if/else-if block with switch

9 years agoMakefile: move common Mac flags to common.mk
Brian Norris [Thu, 20 Sep 2012 16:44:31 +0000 (09:44 -0700)]
Makefile: move common Mac flags to common.mk

9 years agofix compilation (includes)
Brian Norris [Thu, 20 Sep 2012 16:42:14 +0000 (09:42 -0700)]
fix compilation (includes)

9 years agobug fixes for lock support...think it works now...
Brian Demsky [Thu, 20 Sep 2012 08:20:34 +0000 (01:20 -0700)]
bug fixes for lock support...think it works now...

9 years agofix merge
Brian Demsky [Thu, 20 Sep 2012 00:42:13 +0000 (17:42 -0700)]
fix merge

9 years agochanges
Brian Demsky [Thu, 20 Sep 2012 00:38:39 +0000 (17:38 -0700)]
changes

9 years agopush changes
Brian Demsky [Thu, 20 Sep 2012 00:38:24 +0000 (17:38 -0700)]
push changes

9 years agomerge stuff
Brian Demsky [Wed, 19 Sep 2012 23:55:10 +0000 (16:55 -0700)]
merge stuff
Merge branch 'master' into mutex

Conflicts:
model.cc
model.h

9 years agomore mutex changes
Brian Demsky [Wed, 19 Sep 2012 23:38:33 +0000 (16:38 -0700)]
more mutex changes

9 years agosupport for locks... untested, but doesn't break quick run of a sample of test cases
Brian Demsky [Wed, 19 Sep 2012 23:09:19 +0000 (16:09 -0700)]
support for locks...  untested, but doesn't break quick run of a sample of test cases

9 years agomore bugs
Brian Demsky [Wed, 19 Sep 2012 08:19:39 +0000 (01:19 -0700)]
more bugs

9 years agofix merge bug
Brian Demsky [Wed, 19 Sep 2012 07:38:14 +0000 (00:38 -0700)]
fix merge bug

9 years agofix
Brian Demsky [Wed, 19 Sep 2012 07:35:54 +0000 (00:35 -0700)]
fix
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

Conflicts:
model.cc

9 years agomy schedule changes
Brian Demsky [Wed, 19 Sep 2012 07:34:37 +0000 (00:34 -0700)]
my schedule changes

9 years agomerge in master
Brian Demsky [Wed, 19 Sep 2012 07:34:02 +0000 (00:34 -0700)]
merge in master

9 years agofix bug
Brian Demsky [Wed, 19 Sep 2012 07:25:45 +0000 (00:25 -0700)]
fix bug

9 years agomodel: replace list type with action_list_t
Brian Norris [Wed, 19 Sep 2012 02:29:05 +0000 (19:29 -0700)]
model: replace list type with action_list_t

9 years agomodel: add typedef for list of release sequence heads
Brian Norris [Wed, 19 Sep 2012 01:54:40 +0000 (18:54 -0700)]
model: add typedef for list of release sequence heads

9 years agomodel: THREAD_JOIN synchronizes with THREAD_FINISH
Brian Norris [Wed, 19 Sep 2012 01:45:17 +0000 (18:45 -0700)]
model: THREAD_JOIN synchronizes with THREAD_FINISH

9 years agoaction: THREAD_JOIN can synchronize against execution order
Brian Norris [Wed, 19 Sep 2012 01:37:22 +0000 (18:37 -0700)]
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.

9 years agoichange
Brian Demsky [Wed, 19 Sep 2012 00:15:01 +0000 (17:15 -0700)]
ichange

9 years agomodel: add curr to action lists early
Brian Norris [Tue, 18 Sep 2012 23:42:09 +0000 (16:42 -0700)]
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.

9 years agomodel: document behavior of ModelChecker::initialize_curr_action
Brian Norris [Tue, 18 Sep 2012 23:35:46 +0000 (16:35 -0700)]
model: document behavior of ModelChecker::initialize_curr_action

9 years agomodel: pull "may_read_from set" calculation out of initialization
Brian Norris [Tue, 18 Sep 2012 23:26:52 +0000 (16:26 -0700)]
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.

9 years agomodel: refactor ModelChecker::initialize_curr_action
Brian Norris [Tue, 18 Sep 2012 23:16:38 +0000 (16:16 -0700)]
model: refactor ModelChecker::initialize_curr_action

Rewrite some logic for simplification. Just refactorization.

9 years agomodel: move init code to ModelChecker::initialize_curr_action
Brian Norris [Tue, 18 Sep 2012 22:51:37 +0000 (15:51 -0700)]
model: move init code to ModelChecker::initialize_curr_action

Refactoring

9 years agochanges
Brian Demsky [Tue, 18 Sep 2012 22:46:29 +0000 (15:46 -0700)]
changes

9 years agomodel: pull computation out of conditional
Brian Norris [Tue, 18 Sep 2012 22:39:35 +0000 (15:39 -0700)]
model: pull computation out of conditional

9 years agotests: add releaseseq test
Brian Norris [Fri, 14 Sep 2012 20:12:42 +0000 (13:12 -0700)]
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.

9 years agomodel: add some mo_graph fixup code to work_queue
Brian Norris [Fri, 14 Sep 2012 20:11:08 +0000 (13:11 -0700)]
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.

9 years agoMerge branch 'norris'
Brian Norris [Tue, 18 Sep 2012 20:26:55 +0000 (13:26 -0700)]
Merge branch 'norris'

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

9 years agocyclegraph: add ASSERT() for reflexive edges
Brian Norris [Tue, 18 Sep 2012 20:24:47 +0000 (13:24 -0700)]
cyclegraph: add ASSERT() for reflexive edges

9 years agomodel: add infeasibility debugging
Brian Norris [Tue, 18 Sep 2012 19:00:30 +0000 (12:00 -0700)]
model: add infeasibility debugging

9 years agocommon: print tracing info for ASSERT() failures
Brian Norris [Fri, 14 Sep 2012 19:58:05 +0000 (12:58 -0700)]
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.

9 years agomodel: bugfix - w_modification_order handling current action
Brian Norris [Tue, 18 Sep 2012 17:40:33 +0000 (10:40 -0700)]
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.

9 years agomodel: fixup r_modification_order
Brian Norris [Tue, 18 Sep 2012 17:39:44 +0000 (10:39 -0700)]
model: fixup r_modification_order

Bugfix thanks to Brian D.

9 years agomodel: check_recency - "already_added" always true
Brian Norris [Tue, 18 Sep 2012 17:36:06 +0000 (10:36 -0700)]
model: check_recency - "already_added" always true

The current action is always part of the lists now.

Bugfix thanks to Brian D.

9 years agomodel: bugfix get_last_seq_action()
Brian Norris [Tue, 18 Sep 2012 17:29:04 +0000 (10:29 -0700)]
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.

9 years agomore changes towards locks
Brian Demsky [Tue, 18 Sep 2012 08:15:06 +0000 (01:15 -0700)]
more changes towards locks

9 years agoMerge branch 'master' into mutex
Brian Demsky [Tue, 18 Sep 2012 05:18:56 +0000 (22:18 -0700)]
Merge branch 'master' into mutex

9 years agoadd mutex files
Brian Demsky [Tue, 18 Sep 2012 05:15:55 +0000 (22:15 -0700)]
add mutex files

9 years agoadd mutex files
Brian Demsky [Tue, 18 Sep 2012 05:15:55 +0000 (22:15 -0700)]
add mutex files

9 years agostart towards adding support for mutexes
Brian Demsky [Tue, 18 Sep 2012 05:15:35 +0000 (22:15 -0700)]
start towards adding support for mutexes

9 years agomodel: fixup happens_before/reflexivity, add 'curr' to lists earlier
Brian Norris [Fri, 14 Sep 2012 19:43:25 +0000 (12:43 -0700)]
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.

9 years agoMerge branch 'norris'
Brian Norris [Fri, 14 Sep 2012 18:25:59 +0000 (11:25 -0700)]
Merge branch 'norris'

9 years agomodel: release_seq synchronization generates mo_graph edge "work entries"
Brian Norris [Fri, 14 Sep 2012 18:07:22 +0000 (11:07 -0700)]
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.

9 years ago.gitignore: ignore .dot graph files
Brian Norris [Fri, 14 Sep 2012 17:33:53 +0000 (10:33 -0700)]
.gitignore: ignore .dot graph files

9 years agomodel: record the number of feasible executions
Brian Norris [Fri, 14 Sep 2012 17:24:24 +0000 (10:24 -0700)]
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.

9 years agoconfig: don't enable graph dumping in master repo
Brian Norris [Fri, 14 Sep 2012 17:29:35 +0000 (10:29 -0700)]
config: don't enable graph dumping in master repo

9 years agomodel: add work queue loop
Brian Norris [Fri, 14 Sep 2012 16:52:49 +0000 (09:52 -0700)]
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.

9 years agoworkqueue: add work queue structures
Brian Norris [Fri, 14 Sep 2012 16:46:56 +0000 (09:46 -0700)]
workqueue: add work queue structures

9 years agotabbing
Brian Demsky [Fri, 14 Sep 2012 08:33:48 +0000 (01:33 -0700)]
tabbing

9 years ago(1) add actions for the fence
Brian Demsky [Fri, 14 Sep 2012 08:31:09 +0000 (01:31 -0700)]
(1) add actions for the fence
(2) a little more support for cyclegraph -- show rmw edges
(3) add extra documentation for norris

9 years agoadd support for dumping cyclegraphs as dot files... also eliminate redundant edges...
Brian Demsky [Fri, 14 Sep 2012 05:04:45 +0000 (22:04 -0700)]
add support for dumping cyclegraphs as dot files...  also eliminate redundant edges to make them easier to view

9 years agomodel: more restructuring of read/write processing
Brian Norris [Thu, 13 Sep 2012 23:16:30 +0000 (16:16 -0700)]
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.

9 years agomodel: remove unnecessary parameter to ModelChecker::process_read
Brian Norris [Thu, 13 Sep 2012 23:08:04 +0000 (16:08 -0700)]
model: remove unnecessary parameter to ModelChecker::process_read

The current Thread can be generated later.

9 years agoMakefile: add PHONY targets
Brian Norris [Thu, 13 Sep 2012 23:03:23 +0000 (16:03 -0700)]
Makefile: add PHONY targets

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

9 years agobugfix: straighten out STL vector allocation (snapshotted vs. persistent)
Brian Norris [Thu, 13 Sep 2012 22:42:21 +0000 (15:42 -0700)]
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.

9 years agomodel: bugfix - don't clobber 'updated'
Brian Norris [Thu, 13 Sep 2012 21:58:36 +0000 (14:58 -0700)]
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.

9 years agoRevert "Makefile: don't always rebuild make.deps"
Brian Norris [Thu, 13 Sep 2012 21:56:16 +0000 (14:56 -0700)]
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.

9 years agosnapshot: print stack trace on segfault
Brian Norris [Thu, 13 Sep 2012 21:47:44 +0000 (14:47 -0700)]
snapshot: print stack trace on segfault

9 years agocommon: add print_trace() for backtracing
Brian Norris [Thu, 13 Sep 2012 21:47:23 +0000 (14:47 -0700)]
common: add print_trace() for backtracing

9 years agomodel: trivial fixups
Brian Norris [Thu, 13 Sep 2012 18:45:42 +0000 (11:45 -0700)]
model: trivial fixups

9 years agoMakefile: don't always rebuild make.deps
Brian Norris [Thu, 13 Sep 2012 18:35:48 +0000 (11:35 -0700)]
Makefile: don't always rebuild make.deps

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

9 years agomodel: simple ASSERT() bug
Brian Norris [Thu, 13 Sep 2012 17:16:37 +0000 (10:16 -0700)]
model: simple ASSERT() bug

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

9 years agomain: wrap help message
Brian Norris [Thu, 13 Sep 2012 17:04:28 +0000 (10:04 -0700)]
main: wrap help message

9 years agomodel: kill unneeded local variable
Brian Norris [Thu, 13 Sep 2012 16:53:59 +0000 (09:53 -0700)]
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.

9 years agospacing
Brian Norris [Thu, 13 Sep 2012 16:42:54 +0000 (09:42 -0700)]
spacing

9 years agoMerge remote-tracking branch 'origin/makefile'
Brian Norris [Thu, 13 Sep 2012 16:21:08 +0000 (09:21 -0700)]
Merge remote-tracking branch 'origin/makefile'

9 years agolots of debugging here... finally working with my rmw example...
Brian Demsky [Thu, 13 Sep 2012 08:33:24 +0000 (01:33 -0700)]
lots of debugging here... finally working with my rmw example...

9 years agoMakefile: fixup Mac dependencies
Brian Norris [Thu, 13 Sep 2012 07:22:55 +0000 (00:22 -0700)]
Makefile: fixup Mac dependencies

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

9 years agocleanup style
Brian Norris [Thu, 13 Sep 2012 07:01:01 +0000 (00:01 -0700)]
cleanup style

9 years agocommit new test case
Brian Demsky [Thu, 13 Sep 2012 05:59:03 +0000 (22:59 -0700)]
commit new test case

9 years agofix for horrible bug... turns out that we could generate an infinite set of bad...
Brian Demsky [Thu, 13 Sep 2012 05:57:00 +0000 (22:57 -0700)]
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...

9 years agomissing changes
Brian Demsky [Thu, 13 Sep 2012 05:08:22 +0000 (22:08 -0700)]
missing changes

9 years agoright fix for avoid rmw cycles... bad assumption in the cyclegraph
Brian Demsky [Thu, 13 Sep 2012 05:06:51 +0000 (22:06 -0700)]
right fix for avoid rmw cycles...  bad assumption in the cyclegraph

9 years agoanother bug fix...
Brian Demsky [Thu, 13 Sep 2012 04:03:37 +0000 (21:03 -0700)]
another bug fix...

9 years agoseparate out rmw actions
Brian Demsky [Thu, 13 Sep 2012 03:35:47 +0000 (20:35 -0700)]
separate out rmw actions
make sure we don't insert promises twice for a node

9 years ago(1) structure code a little better
Brian Demsky [Wed, 12 Sep 2012 23:24:07 +0000 (16:24 -0700)]
(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

9 years agodeal with looping due to bogus future value via promise expiration
Brian Demsky [Wed, 12 Sep 2012 22:12:31 +0000 (15:12 -0700)]
deal with looping due to bogus future value via promise expiration
fix promise bug