cdsspec-compiler.git
12 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.

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

12 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

12 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

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

12 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...

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

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

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

12 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

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

12 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

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

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

12 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

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

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

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

12 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

12 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

12 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

12 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.

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

12 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.

12 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

12 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.

12 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.

12 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

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

12 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

12 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.

12 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.

12 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()'

12 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

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

12 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.

12 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.

12 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.

12 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.

12 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.

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

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

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

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

12 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

12 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.

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

12 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.

12 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

12 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.

12 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

12 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.

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

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

12 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

12 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

12 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.

12 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.

12 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.

12 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.

12 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.

12 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.

12 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

12 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

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

12 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.

12 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.

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

12 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.

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

12 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'

12 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...

12 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)

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

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

12 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...

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

12 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

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

12 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

12 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

12 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

12 years agofun issues...
Brian Demsky [Wed, 12 Sep 2012 09:52:34 +0000 (02:52 -0700)]
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..

12 years agothreads, model, schedule: refactor thread joining
Brian Norris [Wed, 12 Sep 2012 02:48:38 +0000 (19:48 -0700)]
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.

12 years agomodel: add ModelChecker::get_thread(ModelAction *act)
Brian Norris [Wed, 12 Sep 2012 02:45:57 +0000 (19:45 -0700)]
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.

12 years agoschedule: add sleep() function
Brian Norris [Wed, 12 Sep 2012 02:38:50 +0000 (19:38 -0700)]
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.

12 years agocyclegraph: add non-NULL assertions
Brian Norris [Wed, 12 Sep 2012 00:54:29 +0000 (17:54 -0700)]
cyclegraph: add non-NULL assertions

12 years agoMerge branch 'demsky'
Brian Norris [Wed, 12 Sep 2012 00:52:02 +0000 (17:52 -0700)]
Merge branch 'demsky'

Branch cleaned up by Brian Norris

12 years agomodel: cleaning up some code
Brian Demsky [Tue, 11 Sep 2012 03:17:10 +0000 (20:17 -0700)]
model: cleaning up some code

12 years agomodel: handle RMW, unresolved reads in w_modification_order checks
Brian Norris [Tue, 11 Sep 2012 18:43:18 +0000 (11:43 -0700)]
model: handle RMW, unresolved reads in w_modification_order checks

12 years agomodel: fix the maxreads support
Brian Demsky [Mon, 10 Sep 2012 00:43:20 +0000 (17:43 -0700)]
model: fix the maxreads support

12 years agomodel: some bug fixes to the model checker
Brian Demsky [Sun, 9 Sep 2012 09:25:47 +0000 (02:25 -0700)]
model: some bug fixes to the model checker

12 years agolinuxrwlocks: two bug fixes; guess the model checker helps find bugs
Brian Demsky [Sun, 9 Sep 2012 09:25:47 +0000 (02:25 -0700)]
linuxrwlocks: two bug fixes; guess the model checker helps find bugs

12 years agomodel: bug fixes to new code
Brian Demsky [Sun, 9 Sep 2012 02:37:11 +0000 (19:37 -0700)]
model: bug fixes to new code

12 years agocyclegraph: support rolling back changes
Brian Demsky [Sun, 9 Sep 2012 02:37:11 +0000 (19:37 -0700)]
cyclegraph: support rolling back changes

12 years agomodel: replace action conditions with switch block
Brian Norris [Tue, 11 Sep 2012 19:24:15 +0000 (12:24 -0700)]
model: replace action conditions with switch block

12 years agomodel: add check_recency()
Brian Norris [Tue, 11 Sep 2012 17:20:06 +0000 (10:20 -0700)]
model: add check_recency()

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

12 years agomodel: refactor "get next thread" code
Brian Norris [Tue, 11 Sep 2012 18:19:50 +0000 (11:19 -0700)]
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().

12 years agomodel: add too_many_reads flag
Brian Norris [Tue, 11 Sep 2012 17:19:46 +0000 (10:19 -0700)]
model: add too_many_reads flag

12 years agonodestack: add get_read_from_size()
Brian Norris [Tue, 11 Sep 2012 17:19:10 +0000 (10:19 -0700)]
nodestack: add get_read_from_size()