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

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

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

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

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

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

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

12 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

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

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

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

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

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

12 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

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

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

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

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

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

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

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

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

12 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

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

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

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

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

12 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

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

12 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

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

12 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

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

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

12 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

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

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

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

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

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

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

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

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

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

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

12 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

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

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

12 years agoaction: add const qualifiers
Brian Norris [Tue, 19 Jun 2012 23:00:57 +0000 (16:00 -0700)]
action: add const qualifiers

12 years agoaction: replace condition check with ASSERT()
Brian Norris [Tue, 19 Jun 2012 22:51:06 +0000 (15:51 -0700)]
action: replace condition check with ASSERT()

Now that the ModelChecker and NodeStack have been refactored a bit, I don't
need to rely on create_cv() to avoid overwriting a previously-existing
clockvector; create_cv() will now be called at most once per ModelAction. So
change this condition to an ASSERT().

12 years agonodestack/model: refactor explore_action(), change return semantics
Brian Norris [Tue, 19 Jun 2012 22:44:13 +0000 (15:44 -0700)]
nodestack/model: refactor explore_action(), change return semantics

ModelChecker would like to know when a new ModelAction is being inserted
into the NodeStack vs. when the new ModelAction should be discarded in
favor of a pre-existing one (due to replay). So I change the semantics of
NodeStack::explore_action() such that it does not always return a
ModelAction; now it returns NULL if the ModelAction was accepted into the
NodeStack, otherwise returning the ModelAction that was already in the
stack.

Now, ModelChecker can choose when to create new clock vectors as well as
other operations (to come) that may be performed only upon *first*
exploration of a new ModelAction.

Additionally, ModelChecker is now responsible for free-ing the ModelAction
if it is not going to be kept in NodeStack.

There should be no change in functionality.

12 years agonodestack: more documentation
Brian Norris [Tue, 19 Jun 2012 17:30:19 +0000 (10:30 -0700)]
nodestack: more documentation

12 years agocyclegraph: make this compile...
Brian Norris [Tue, 19 Jun 2012 17:04:58 +0000 (10:04 -0700)]
cyclegraph: make this compile...

You need 'inttypes' for 'uintptr_t'

12 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Brian Demsky [Mon, 18 Jun 2012 18:44:13 +0000 (11:44 -0700)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

12 years agobuilds
Brian Demsky [Mon, 18 Jun 2012 18:43:32 +0000 (11:43 -0700)]
builds

12 years agoadd hashtable
Brian Demsky [Sun, 17 Jun 2012 13:10:35 +0000 (06:10 -0700)]
add hashtable

12 years agoDoxyfile: exclude malloc.c
Brian Norris [Fri, 15 Jun 2012 06:55:25 +0000 (23:55 -0700)]
Doxyfile: exclude malloc.c

I don't think we really want documentation for the dlmalloc code. It provides
several Doxygen warnings/complaints, and it muddies up some of the output HTML.
Maybe we can fix this up somehow later, but it's not really worth doing right
now.

12 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Brian Demsky [Fri, 15 Jun 2012 06:29:55 +0000 (14:29 +0800)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

12 years agofixup some doc wording
Brian Norris [Fri, 15 Jun 2012 06:20:20 +0000 (23:20 -0700)]
fixup some doc wording

12 years agoadd more documentation
Brian Norris [Fri, 15 Jun 2012 06:09:05 +0000 (23:09 -0700)]
add more documentation

I'm trying to add doxygen comments next to the definitions (not the
declaration) as much as possible, to keep the documentation as close to the
actual code as much as possible, helping to prevent errors as functionality
changes.

12 years agosubramanian lied when he said he fixed these...
Brian Demsky [Fri, 15 Jun 2012 05:59:42 +0000 (13:59 +0800)]
subramanian lied when he said he fixed these...

12 years agoMakefile: force `make docs' to depend on all source files
Brian Norris [Fri, 15 Jun 2012 05:51:30 +0000 (22:51 -0700)]
Makefile: force `make docs' to depend on all source files

That way, if I change a file that might have documentation comments in it,
`make docs' will rerun doxygen.

12 years ago(snapshot) removing mbFinalize and usage of finalize
Subramanian Ganapathy [Thu, 14 Jun 2012 23:13:59 +0000 (16:13 -0700)]
(snapshot) removing mbFinalize and usage of finalize

Now there is no need for finalize mechanism at all.
All that was required was resetting the rollback id

12 years agosnapshot: refactor the fork-based stack initialization
Brian Norris [Thu, 14 Jun 2012 22:31:44 +0000 (15:31 -0700)]
snapshot: refactor the fork-based stack initialization

This complicated code block uses a getcontext()/setcontext() pair with an
'alreadySwapped' boolean (int) to perform basically the same functionality as
'swapcontext()'. Refactor this code to make it simpler.

12 years agosnapshot: remove unused 'uc_link' context
Brian Norris [Thu, 14 Jun 2012 22:30:25 +0000 (15:30 -0700)]
snapshot: remove unused 'uc_link' context

The 'currentContext' variable was never initialized, and so doesn't perform any
useful functionality as a 'uc_link' address. Remove it.

12 years agosnapshotimp: reindent file
Brian Norris [Thu, 14 Jun 2012 16:29:42 +0000 (09:29 -0700)]
snapshotimp: reindent file

12 years agosnapshot: don't put entire if (...) on one line
Brian Norris [Thu, 14 Jun 2012 16:28:15 +0000 (09:28 -0700)]
snapshot: don't put entire if (...) on one line

It's harder to read the failure conditions if you put if (...) and the
following statement all on one line.

12 years agosnapshot: define macros with type size_t
Brian Norris [Thu, 14 Jun 2012 16:22:31 +0000 (09:22 -0700)]
snapshot: define macros with type size_t

The SHARED_MEMORY_DEFAULT and STACK_SIZE_DEFAULT macros need to be of type
size_t, so cast them when they're defined, not when they're used.

12 years agosnapshot: use (void *) instead of (char *)
Brian Norris [Thu, 14 Jun 2012 16:19:41 +0000 (09:19 -0700)]
snapshot: use (void *) instead of (char *)

12 years agosnapshot: rearrange #if a little
Brian Norris [Thu, 14 Jun 2012 16:16:47 +0000 (09:16 -0700)]
snapshot: rearrange #if a little

HandlePF() is only used in mprotect-based snapshotting, so keep it entirely
within the #if block.

12 years agosnapshot: remove extra blank lines
Brian Norris [Thu, 14 Jun 2012 06:57:01 +0000 (23:57 -0700)]
snapshot: remove extra blank lines

12 years agosnapshot: make other file-scope functions static
Brian Norris [Thu, 14 Jun 2012 06:55:45 +0000 (23:55 -0700)]
snapshot: make other file-scope functions static

12 years agosnapshot: don't export page-aligning functions
Brian Norris [Thu, 14 Jun 2012 06:53:44 +0000 (23:53 -0700)]
snapshot: don't export page-aligning functions

Declare these functions static and move them upward in the file.

12 years agorename struct Snapshot_t => struct Snapshot
Brian Norris [Thu, 14 Jun 2012 06:51:07 +0000 (23:51 -0700)]
rename struct Snapshot_t => struct Snapshot

12 years agosnapshot: don't declare sTheRecord in both #if and #else
Brian Norris [Thu, 14 Jun 2012 06:39:59 +0000 (23:39 -0700)]
snapshot: don't declare sTheRecord in both #if and #else

12 years agosnapshot: remove 'extern "C"' block
Brian Norris [Thu, 14 Jun 2012 06:28:10 +0000 (23:28 -0700)]
snapshot: remove 'extern "C"' block

We do not need to wrap this function in 'extern "C"' for two reasons:

1) It's not actually exported and used in C code
2) You only need this sort of declaration in the header file that may be
   included in both C++ and C compilation. But snapshot.cc should only be
   compiled by the C++ compiler, and snapshot.h is not included in any C
   compilation.

12 years agosnapshot-interface: don't export SnapshotGlobalSegments()
Brian Norris [Thu, 14 Jun 2012 06:20:43 +0000 (23:20 -0700)]
snapshot-interface: don't export SnapshotGlobalSegments()

SnapshotGlobalSegments() is only used within snapshot-interface.cc, so declare
it static and remove it from the header.

12 years agosnapshot: replace DumpIntoLog() with lighter-weight debugging
Brian Norris [Thu, 14 Jun 2012 06:13:29 +0000 (23:13 -0700)]
snapshot: replace DumpIntoLog() with lighter-weight debugging

This file I/O "debug" messaging gets in the way. Make the debugging code simple
and succinct, or don't put it in at all. Now, you can enabled SnapShot
debugging by adding this near the top of snapshot.cc:

 #define CONFIG_DEBUG

12 years agosnapshot: move comments to the right place
Brian Norris [Thu, 14 Jun 2012 05:08:57 +0000 (22:08 -0700)]
snapshot: move comments to the right place

12 years agoRemoving comment asking to fix fork(), has been fixed now
Subramanian Ganapathy [Wed, 13 Jun 2012 20:07:22 +0000 (13:07 -0700)]
Removing comment asking to fix fork(), has been fixed now

12 years agofixing calloc(), fix Makefile
Subramanian Ganapathy [Wed, 13 Jun 2012 19:58:54 +0000 (12:58 -0700)]
fixing calloc(), fix Makefile

Adding sbrk() calls and hooked into free also to avoid freeing sbrked memory...
checked both fork and paged implementation. seems to work Also everytime we
switch between fork and paged impl, we need to rebuild so adding snapshot.h as
dependency to mymemory.cc in makefile

12 years agolibatomic: perform write before context switch
Brian Norris [Thu, 7 Jun 2012 00:34:47 +0000 (17:34 -0700)]
libatomic: perform write before context switch

Atomic actions block a thread at the "switch_to_master" function call, so under
the current structure (which isn't quite fit for relaxed modeling yet...) we
should perform the memory write before calling "switch_to_master".

If not, we can observe sequences like the following, where x is an atomic
variable. All actions are seq_cst:

 Initially, x = 0

 Thread    Action
 ------    ------
 1         r1 = x;       // r1 = 0
 1          x = r1 + 1;  //  x = 1, not stored yet?
 2         r2 = x;       // r2 = 0
 2          x = r2       //  x = 1, not stored yet?

Then, depending on scheduling, Thread 1 or Thread 2 might complete first, with
its write being performed *after* it receives control again.

12 years ago.gitignore: ignore docs directory
Brian Norris [Wed, 6 Jun 2012 19:22:07 +0000 (12:22 -0700)]
.gitignore: ignore docs directory

12 years agoaction: fix some comments
Brian Norris [Wed, 6 Jun 2012 16:48:54 +0000 (09:48 -0700)]
action: fix some comments

12 years agoMakefile: have `mrclean' depend on `clean'
Brian Norris [Wed, 6 Jun 2012 16:46:44 +0000 (09:46 -0700)]
Makefile: have `mrclean' depend on `clean'

12 years agomore comments
Brian Demsky [Wed, 6 Jun 2012 09:16:04 +0000 (02:16 -0700)]
more comments

12 years agomore doc changes
Brian Demsky [Wed, 6 Jun 2012 09:01:38 +0000 (02:01 -0700)]
more doc changes

12 years agomore documentation
Brian Demsky [Wed, 6 Jun 2012 08:53:30 +0000 (01:53 -0700)]
more documentation

12 years ago1) Add more comments.
Brian Demsky [Wed, 6 Jun 2012 08:46:49 +0000 (01:46 -0700)]
1) Add more comments.
2) Change is_dependent to is_synchronizing and make it capture actual synchronizing behavior...
3) Add more support for RMW operations.

12 years agomore documentation
Brian Demsky [Wed, 6 Jun 2012 07:45:15 +0000 (00:45 -0700)]
more documentation

12 years agomore docs
Brian Demsky [Wed, 6 Jun 2012 07:13:23 +0000 (00:13 -0700)]
more docs

12 years agoadd support for docs
Brian Demsky [Wed, 6 Jun 2012 06:51:02 +0000 (23:51 -0700)]
add support for docs

12 years agosnapshot: zero out entire siginfo_t
Brian Norris [Tue, 5 Jun 2012 19:54:52 +0000 (12:54 -0700)]
snapshot: zero out entire siginfo_t

We should initialize this variable to all zeros, just to be safe.

12 years agoChanges needed to run on OS X... Example runs on my laptop now. No need to push...
Brian Demsky [Mon, 4 Jun 2012 05:35:41 +0000 (22:35 -0700)]
Changes needed to run on OS X...  Example runs on my laptop now.  No need to push code back and forth to test...

Out of time for fun hack, have to get back to real work now.  :(

12 years agohack some stuff towards running on mac... unrelated bugs still..
Brian Demsky [Mon, 4 Jun 2012 01:05:39 +0000 (18:05 -0700)]
hack some stuff towards running on mac...  unrelated bugs still..

12 years agosnapshot: remove duplicate definition of finalize()
Brian Norris [Thu, 31 May 2012 18:40:25 +0000 (11:40 -0700)]
snapshot: remove duplicate definition of finalize()

finalize() was moved to snapshot-interface.h but wasn't removed from snapshot.h

12 years agouse EXIT_SUCCESS and EXIT_FAILURE
Brian Norris [Thu, 31 May 2012 02:49:03 +0000 (19:49 -0700)]
use EXIT_SUCCESS and EXIT_FAILURE

We were wildly inconsistent with our exit status. We might as well follow the
C standard.

12 years agouserprog: use atomics allocated on "heap"
Brian Norris [Thu, 31 May 2012 02:42:07 +0000 (19:42 -0700)]
userprog: use atomics allocated on "heap"

Just for kicks, since snapshotting is working properly. We might as well test
this.

12 years agoAdding fixes for the fork based implementation, also removed some redundant code...
Subramanian Ganapathy [Wed, 30 May 2012 23:52:38 +0000 (16:52 -0700)]
Adding fixes for the fork based implementation, also removed some redundant code pointed to by Prof. Demsky

12 years agoMerge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
Subramanian Ganapathy [Wed, 30 May 2012 21:25:42 +0000 (14:25 -0700)]
Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker