model-checker.git
11 years agorewrite macros
Brian Demsky [Thu, 19 Jul 2012 23:55:52 +0000 (16:55 -0700)]
rewrite macros

11 years agoimport header file from specification
Brian Demsky [Thu, 19 Jul 2012 23:18:11 +0000 (16:18 -0700)]
import header file from specification

taken from n2427.html

11 years agoupdate TODO's
Brian Norris [Wed, 1 Aug 2012 00:13:30 +0000 (17:13 -0700)]
update TODO's

11 years agoAdd RMW support to core.
Brian Demsky [Thu, 19 Jul 2012 21:15:27 +0000 (14:15 -0700)]
Add RMW support to core.

Eliminate annoying warning.

11 years agomodel: add documentation
Brian Norris [Tue, 31 Jul 2012 23:58:00 +0000 (16:58 -0700)]
model: add documentation

[Split from Brian Demsky's work]

11 years agosmall changes (things still work) towards support RMW
Brian Demsky [Thu, 19 Jul 2012 19:18:25 +0000 (12:18 -0700)]
small changes (things still work) towards support RMW

Reserve value field only for writes. Using it for reads will only make thinks
weird for RMW operations.

[Amended by Brian Norris]

11 years agotrying to get fork based snapshotting to work
Brian Demsky [Wed, 18 Jul 2012 22:55:22 +0000 (15:55 -0700)]
trying to get fork based snapshotting to work

[Amended by Brian Norris,
 includes some later clean up]

11 years agotoss a place for useful information
Brian Demsky [Wed, 18 Jul 2012 18:08:10 +0000 (11:08 -0700)]
toss a place for useful information

11 years agomodel: refactor "infeasible" printing
Brian Norris [Tue, 31 Jul 2012 23:32:59 +0000 (16:32 -0700)]
model: refactor "infeasible" printing

11 years agoprint less stuff
Brian Demsky [Wed, 18 Jul 2012 05:28:20 +0000 (22:28 -0700)]
print less stuff

11 years agomodel: add support for modification orders
Brian Demsky [Wed, 18 Jul 2012 05:03:01 +0000 (22:03 -0700)]
model: add support for modification orders

This update adds support for modification orders and kills the bogus executions
seen before...

[Updated, split by Brian Norris]

11 years agocyclegraph: bugfix - graph reachability was reversed
Brian Norris [Tue, 31 Jul 2012 22:59:56 +0000 (15:59 -0700)]
cyclegraph: bugfix - graph reachability was reversed

[Split from Brian Demsky's commit]

11 years agocyclegraph: add destructor, use 'const' appropriately
Brian Norris [Tue, 31 Jul 2012 22:50:07 +0000 (15:50 -0700)]
cyclegraph: add destructor, use 'const' appropriately

[Split from Brian Demsky's larger commit]

11 years agonodestack: document pop_restofstack()
Brian Norris [Tue, 31 Jul 2012 22:41:35 +0000 (15:41 -0700)]
nodestack: document pop_restofstack()

11 years agoAdd basic reads from support
Brian Demsky [Wed, 18 Jul 2012 03:36:07 +0000 (20:36 -0700)]
Add basic reads from support

Now we need to use the cyclegraph to eliminate bad executions...

11 years agoMake stack popping explicit.
Brian Demsky [Tue, 17 Jul 2012 23:02:27 +0000 (16:02 -0700)]
Make stack popping explicit.

The current check will break in subtle ways as soon as we start to
add reads_from support as the thread selection is no longer the
only backtracking choice.

11 years agonodestack: re-insert falsely-declared "dead code"
Brian Norris [Tue, 17 Jul 2012 05:44:40 +0000 (22:44 -0700)]
nodestack: re-insert falsely-declared "dead code"

"remove dead code...  loop entrance condition is i<backtrack.size().  Therefore,
this branch can never be taken."

False.

While the entrance condition prevents 'i == backtrack.size()', the loop may
exit with 'i == backtrack.size()', since i++ is executed after the last
iteration. Since we do not expect or want this condition to occur, though, I
transform this to a documented ASSERT().

11 years agoconfig: automatically determine BIT48
Brian Norris [Tue, 17 Jul 2012 05:26:25 +0000 (22:26 -0700)]
config: automatically determine BIT48

GCC says we can use _LP64, and LLVM (clang) imitates, so this can be
automatically redefined for 32-bit/64-bit architectures.

Also, add config.h to Makefile so it triggers a rebuild. This is still a blunt
mechanism, but it's fine for now.

11 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Brian Demsky [Tue, 17 Jul 2012 05:28:01 +0000 (22:28 -0700)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

11 years agoremove dead code... loop entrance condition is i<backtrack.size(). Therefore,
Brian Demsky [Tue, 17 Jul 2012 05:26:54 +0000 (22:26 -0700)]
remove dead code...  loop entrance condition is i<backtrack.size().  Therefore,
this branch can never be taken.  remove it as it is confusing.

11 years agoaction: fix uint64_t printf warning
Brian Norris [Tue, 17 Jul 2012 05:07:26 +0000 (22:07 -0700)]
action: fix uint64_t printf warning

11 years agono need to store into the object field... this will probably just lead to weird...
Brian Demsky [Mon, 16 Jul 2012 23:24:53 +0000 (16:24 -0700)]
no need to store into the object field...  this will probably just lead to weird bugs in the future where
people wrongly assume reasonable values in the field...

11 years agoreally should be using a type that is big enough for all commonly used data types...
Brian Demsky [Mon, 16 Jul 2012 23:14:27 +0000 (16:14 -0700)]
really should be using a type that is big enough for all commonly used data types...

added some notes on unused_value flag to specify that this value does not guarantee an unused value...

11 years agothe initialized logic appears to be wrong... release/acquire pairs only
Brian Demsky [Fri, 13 Jul 2012 17:21:58 +0000 (10:21 -0700)]
the initialized logic appears to be wrong...  release/acquire pairs only
establish synchronization if the load reads the release store...  just because
all possible reads would synchronize doesn't mean that load can't fail to see them all...

11 years agodatarace: fixup, properly document BIT48
Brian Norris [Fri, 13 Jul 2012 06:15:58 +0000 (23:15 -0700)]
datarace: fixup, properly document BIT48

The "48-bit virtual address" macro should be checked with #if, not #ifdef,
since it's defined to 1 or 0. You would use #ifdef if it's either "define" or
"not defined." Make this clear in the comment as well.

11 years agomodel: remove unused #include
Brian Norris [Fri, 13 Jul 2012 06:12:29 +0000 (23:12 -0700)]
model: remove unused #include

11 years agolibthreads: thrd_join() always return 0
Brian Norris [Fri, 13 Jul 2012 05:18:25 +0000 (22:18 -0700)]
libthreads: thrd_join() always return 0

According to the spec, thrd_join() should return the return code from the
joining thread function. But for now, I implement the function type
(thrd_start_t, from C11) as returning void, not int. So just return 0 always.

11 years agomodel: add documentation
Brian Norris [Fri, 13 Jul 2012 05:17:48 +0000 (22:17 -0700)]
model: add documentation

11 years agomodel: fixup "initialized" check in build_reads_from_past()
Brian Norris [Fri, 13 Jul 2012 01:58:18 +0000 (18:58 -0700)]
model: fixup "initialized" check in build_reads_from_past()

Some... (TODO: finish message here)

11 years agomodel: only include the most recent seq_cst write in may_read_from
Brian Norris [Fri, 13 Jul 2012 00:50:14 +0000 (17:50 -0700)]
model: only include the most recent seq_cst write in may_read_from

11 years agomodel: add ModelChecker::get_last_seq_cst()
Brian Norris [Fri, 13 Jul 2012 00:43:47 +0000 (17:43 -0700)]
model: add ModelChecker::get_last_seq_cst()

Add a function to get the last memory_order_seq_cst action (in the total global
sequence) performed on a particular object (i.e., memory location). Will be
used for build_reads_from_past().

11 years agomodel: improve ModelChecker::get_last_conflict() search
Brian Norris [Thu, 12 Jul 2012 22:38:10 +0000 (15:38 -0700)]
model: improve ModelChecker::get_last_conflict() search

Use the recently-added 'obj_map' to isolate a list of actions on only the
current object (memory location). That way, we don't have to iterate through as
much noise in our lists.

11 years agomodel: add per-object action lists (obj_map)
Brian Norris [Thu, 12 Jul 2012 22:33:14 +0000 (15:33 -0700)]
model: add per-object action lists (obj_map)

This object list will map objects (i.e., memory locations) to traces of all
actions performed on the respective objects. This will be used for some seq_cst
and backtracking-conflict computations to reduce the space we have to search.

11 years agoreformat some doxygen comments, remove newlines
Brian Norris [Thu, 12 Jul 2012 20:56:15 +0000 (13:56 -0700)]
reformat some doxygen comments, remove newlines

Avoiding newlines between a comment and its function header makes it more
obvious which function the comment belongs to.

11 years agomodel: rearrange switch block, handle RMW
Brian Norris [Thu, 12 Jul 2012 19:29:34 +0000 (12:29 -0700)]
model: rearrange switch block, handle RMW

This switch block shouldn't have to be updated for every new action_type_t.
Rewrite so that we only have to worry about significant actions, like
ATOMIC_{READ,WRITE,RMW}.

11 years agoMerge branch 'master' into brian
Brian Norris [Thu, 12 Jul 2012 18:18:00 +0000 (11:18 -0700)]
Merge branch 'master' into brian

11 years agomodel: bugfix - resize thrd_last_action when adding objects
Brian Norris [Thu, 12 Jul 2012 18:05:20 +0000 (11:05 -0700)]
model: bugfix - resize thrd_last_action when adding objects

Apparently, STL vectors don't resize automatically, nor do they warn or print
errors when you access them out-of-bounds...

11 years agomodel: factor out 'tid' calculation
Brian Norris [Thu, 12 Jul 2012 18:04:58 +0000 (11:04 -0700)]
model: factor out 'tid' calculation

11 years agomain: make function static
Brian Norris [Wed, 11 Jul 2012 21:57:16 +0000 (14:57 -0700)]
main: make function static

11 years agoaction / threads: add THREAD_START action at start of each thread
Brian Norris [Wed, 11 Jul 2012 21:52:56 +0000 (14:52 -0700)]
action / threads: add THREAD_START action at start of each thread

The datarace code needs every thread to have at least one action in it, so that
the action has a valid non-zero clock.

11 years agothreads: use constructor initializer list
Brian Norris [Wed, 11 Jul 2012 21:37:53 +0000 (14:37 -0700)]
threads: use constructor initializer list

11 years agoaction: add 'reads_from' member variable
Brian Norris [Wed, 11 Jul 2012 21:10:40 +0000 (14:10 -0700)]
action: add 'reads_from' member variable

Just printed out for now, but the 'reads_from' parameter might be used more
later.

11 years agoaction: remove unused ModelAction::set_value()
Brian Norris [Wed, 11 Jul 2012 19:15:06 +0000 (12:15 -0700)]
action: remove unused ModelAction::set_value()

11 years agomodel: release/acquire synchronization
Brian Norris [Wed, 11 Jul 2012 18:53:07 +0000 (11:53 -0700)]
model: release/acquire synchronization

I forgot that I had already written the ModelAction::reads_from() code, and it
was just waiting to be hooked up :)

Anyway, I haven't really tested all the synchronization yet...

11 years agoclockvector: add 'const', fix comments in ClockVector::merge()
Brian Norris [Wed, 11 Jul 2012 18:50:35 +0000 (11:50 -0700)]
clockvector: add 'const', fix comments in ClockVector::merge()

11 years agoremove EOL spaces, fix indentation
Brian Norris [Wed, 11 Jul 2012 04:31:24 +0000 (21:31 -0700)]
remove EOL spaces, fix indentation

11 years agobug
Brian Demsky [Wed, 11 Jul 2012 04:12:42 +0000 (21:12 -0700)]
bug

11 years agodocumentation
Brian Demsky [Wed, 11 Jul 2012 03:39:58 +0000 (20:39 -0700)]
documentation

11 years agofix bug
Brian Demsky [Tue, 10 Jul 2012 22:01:44 +0000 (15:01 -0700)]
fix bug
get rid of annoying compiler warning

11 years agohook up the race detector...
Brian Demsky [Tue, 10 Jul 2012 21:44:48 +0000 (14:44 -0700)]
hook up the race detector...

11 years agoMerge branch 'datarace'
Brian Norris [Sat, 7 Jul 2012 07:06:09 +0000 (00:06 -0700)]
Merge branch 'datarace'

11 years agodatarace: fix build error
Brian Norris [Sat, 7 Jul 2012 07:05:34 +0000 (00:05 -0700)]
datarace: fix build error

11 years agochanges
Brian Demsky [Sat, 7 Jul 2012 06:56:24 +0000 (23:56 -0700)]
changes

11 years agolibatomic: atomic_load() - use proper reads_from value
Brian Norris [Thu, 5 Jul 2012 20:57:50 +0000 (13:57 -0700)]
libatomic: atomic_load() - use proper reads_from value

Finally utilize a return value from the model-checker, instead of
storing/retrieving a sequentially-consistent value in obj->value.

11 years agomodel: set reads_from "return value" in model-checker
Brian Norris [Sat, 7 Jul 2012 01:37:11 +0000 (18:37 -0700)]
model: set reads_from "return value" in model-checker

Previously, values (let alone the reads-from relationship) were not actually
returned from the model-checker to the user. This step sets up the return value
so that the user context can retrieve it rather than using a value stuck in the
snapshotting memory.

There are still several TODOs along with the reads-from relationship, but this
code is stable enough for providing a basis for further work.

11 years agonodestack: add stub 'get_next_read_from()' function
Brian Norris [Sat, 7 Jul 2012 01:12:59 +0000 (18:12 -0700)]
nodestack: add stub 'get_next_read_from()' function

This is the start of providing functional model-checking reads-from
relationships. It is a stub because it doesn't properly handle "backtracking"
and replay for reads-from assignments. It will simply return the first element
in may_read_from.

11 years agodocument some enumerated types
Brian Norris [Sat, 7 Jul 2012 01:58:21 +0000 (18:58 -0700)]
document some enumerated types

11 years agomodel: detect uninitialized atomic reads
Brian Norris [Sat, 7 Jul 2012 00:54:54 +0000 (17:54 -0700)]
model: detect uninitialized atomic reads

11 years agonodestack: add print_may_read_from()
Brian Norris [Sat, 7 Jul 2012 00:52:40 +0000 (17:52 -0700)]
nodestack: add print_may_read_from()

11 years agomodel: improve build_reads_from_past() comment
Brian Norris [Sat, 7 Jul 2012 00:39:42 +0000 (17:39 -0700)]
model: improve build_reads_from_past() comment

11 years agoaction: use constructor initializer list
Brian Norris [Sat, 7 Jul 2012 00:21:33 +0000 (17:21 -0700)]
action: use constructor initializer list

11 years agoaction: support ATOMIC_INIT
Brian Norris [Sat, 7 Jul 2012 00:09:17 +0000 (17:09 -0700)]
action: support ATOMIC_INIT

For now, atomic_init() will be supported as simply a relaxed write. This
doesn't quite match the spec exactly [1, 2], but it is expedient for supporting
the common case of checking proper initialization.

[1] From C++ N3242, Section 29.6.5, Statement 8:

       Non-atomically initializes *object with value desired.

       Note: Concurrent access from another thread, even via an atomic
       operation, constitutes a data race.

[2] Note that for now, my implementation will not flag concurrent atomic_init()
    and atomic_store() as data races.

11 years agothreads: add per-thread "return" values for 'model-checking/user context' switch
Brian Norris [Tue, 3 Jul 2012 23:31:45 +0000 (16:31 -0700)]
threads: add per-thread "return" values for 'model-checking/user context' switch

The model-checker needs to return a value to the user context when performing
atomic loads, for instance. I will be implementing this by caching the return
value on a per-thread basis. This is because an atomic_load() might result in a
context switch before actually returning the value.

These functions are not yet used.

11 years agonodestack: build 'may_read_from' out of constant ModelActions
Brian Norris [Thu, 5 Jul 2012 23:41:49 +0000 (16:41 -0700)]
nodestack: build 'may_read_from' out of constant ModelActions

Make the 'may_read_from' set include only constant pointers.

11 years agonodestack: action_set_t: replace STL 'set' with 'list'
Brian Norris [Tue, 3 Jul 2012 23:47:20 +0000 (16:47 -0700)]
nodestack: action_set_t: replace STL 'set' with 'list'

11 years agotrivial changes
Brian Norris [Fri, 6 Jul 2012 00:33:08 +0000 (17:33 -0700)]
trivial changes

* remove unnecessary 'class' keyword
* add ASSERT() in the 'thread_current()' function
* move #include into .cc file
* remove more end-of-line spaces

11 years agoadd more const qualifiers
Brian Norris [Fri, 6 Jul 2012 23:08:34 +0000 (16:08 -0700)]
add more const qualifiers

11 years agomodel: make set_current_action() private
Brian Norris [Tue, 3 Jul 2012 21:57:40 +0000 (14:57 -0700)]
model: make set_current_action() private

It's only used within ModelChecker...

11 years agodatarace: factor subtle clock-vector logic into a reusable function
Brian Norris [Fri, 6 Jul 2012 18:44:46 +0000 (11:44 -0700)]
datarace: factor subtle clock-vector logic into a reusable function

These comparisons are performed many times throughout datarace.cc, featuring a
lot of code duplication without strong documentation. This factors the
duplicated code into a single function and documents that single function more
clearly.

Brian Demsky: please review this fix (it should make no actual logical change)
and take a look at the TODO I have inserted; I'm not sure if the TODO is
warranted.

11 years agodatarace: remove EOL spaces
Brian Norris [Fri, 6 Jul 2012 18:27:20 +0000 (11:27 -0700)]
datarace: remove EOL spaces

11 years agodatarace/clockvector: switch 'clocks' to use 'unsigned int' (modelclock_t)
Brian Norris [Fri, 6 Jul 2012 18:00:27 +0000 (11:00 -0700)]
datarace/clockvector: switch 'clocks' to use 'unsigned int' (modelclock_t)

11 years agoclock: add modelclock_t typedef, use 'unsigned int'
Brian Norris [Fri, 6 Jul 2012 00:31:30 +0000 (17:31 -0700)]
clock: add modelclock_t typedef, use 'unsigned int'

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

11 years agoadd forgetten file
Brian Demsky [Fri, 6 Jul 2012 07:39:00 +0000 (00:39 -0700)]
add forgetten file

11 years agoadd support for datarace detection...
Brian Demsky [Fri, 6 Jul 2012 07:38:38 +0000 (00:38 -0700)]
add support for datarace detection...

11 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Brian Demsky [Tue, 3 Jul 2012 23:41:31 +0000 (16:41 -0700)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

11 years agoMerge branch 'brian'
Brian Norris [Tue, 3 Jul 2012 21:16:02 +0000 (14:16 -0700)]
Merge branch 'brian'

11 years agoAdding relevant comments for fork based implementation.
Subramanian Ganapathy [Thu, 21 Jun 2012 19:21:37 +0000 (12:21 -0700)]
Adding relevant comments for fork based implementation.

11 years agoMakefile: compile *.cc separately
Brian Norris [Tue, 3 Jul 2012 19:54:03 +0000 (12:54 -0700)]
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.

11 years agonodestack: revert may_read_from to a normal member variable, not pointer
Brian Norris [Tue, 3 Jul 2012 18:03:51 +0000 (11:03 -0700)]
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.

11 years agoaction: add {get,set}_value(), assign default value
Brian Norris [Tue, 3 Jul 2012 16:23:11 +0000 (09:23 -0700)]
action: add {get,set}_value(), assign default value

11 years agoadd documentation
Brian Norris [Mon, 25 Jun 2012 20:24:50 +0000 (13:24 -0700)]
add documentation

11 years agonodestack: only create may_read_from sets for read operations
Brian Norris [Mon, 25 Jun 2012 19:22:31 +0000 (12:22 -0700)]
nodestack: only create may_read_from sets for read operations

11 years agonodestack: re-associate ModelAction/Node relationship
Brian Norris [Mon, 25 Jun 2012 19:07:39 +0000 (12:07 -0700)]
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.

11 years agonodestack: add Node::get_parent() function
Brian Norris [Mon, 25 Jun 2012 18:47:24 +0000 (11:47 -0700)]
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

11 years agomodel: make print_list() into a static C function
Brian Norris [Thu, 21 Jun 2012 22:13:56 +0000 (15:13 -0700)]
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.

11 years agoAdding relevant comments for fork based implementation.
Subramanian Ganapathy [Thu, 21 Jun 2012 19:21:37 +0000 (12:21 -0700)]
Adding relevant comments for fork based implementation.

11 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Subramanian Ganapathy [Thu, 21 Jun 2012 18:45:14 +0000 (11:45 -0700)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

11 years agomodel: make comment more accurate
Brian Norris [Thu, 21 Jun 2012 18:17:40 +0000 (11:17 -0700)]
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.

11 years agoaction: add const qualifier
Brian Norris [Thu, 21 Jun 2012 18:16:38 +0000 (11:16 -0700)]
action: add const qualifier

11 years agoclockvector: add const qualifiers
Brian Norris [Thu, 21 Jun 2012 09:38:31 +0000 (02:38 -0700)]
clockvector: add const qualifiers

11 years agoclockvector: add documentation
Brian Norris [Thu, 21 Jun 2012 09:37:47 +0000 (02:37 -0700)]
clockvector: add documentation

11 years agoMerge branch 'sandbox' (remove finalize())
Brian Norris [Thu, 21 Jun 2012 09:11:15 +0000 (02:11 -0700)]
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...

11 years agosnapshot: switch back to mprotect-based snapshotting
Brian Norris [Thu, 21 Jun 2012 09:10:12 +0000 (02:10 -0700)]
snapshot: switch back to mprotect-based snapshotting

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

11 years agomodel: build up 'may_read_from' set
Brian Norris [Thu, 21 Jun 2012 09:04:11 +0000 (02:04 -0700)]
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().

11 years agomodel: add build_reads_from_past() function
Brian Norris [Thu, 21 Jun 2012 08:59:01 +0000 (01:59 -0700)]
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.

11 years agoaction: add happens_before() function
Brian Norris [Thu, 21 Jun 2012 08:56:50 +0000 (01:56 -0700)]
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...

11 years agoclockvector: fix 'happens_before', change name to 'synchronized_since'
Brian Norris [Thu, 21 Jun 2012 08:48:03 +0000 (01:48 -0700)]
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.

11 years agoaction: add 'get_cv()' accessor function
Brian Norris [Thu, 21 Jun 2012 08:05:15 +0000 (01:05 -0700)]
action: add 'get_cv()' accessor function

11 years agonodestack: add 'may_read_from' set
Brian Norris [Thu, 21 Jun 2012 07:54:01 +0000 (00:54 -0700)]
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.

11 years agonodestack: don't perform linear search to check if backtrack is empty
Brian Norris [Tue, 19 Jun 2012 23:33:52 +0000 (16:33 -0700)]
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.