c11tester.git
12 years agomain, model: move main execution loop into ModelChecker class
Brian Norris [Fri, 10 Aug 2012 21:23:29 +0000 (14:23 -0700)]
main, model: move main execution loop into ModelChecker class

12 years agomodel: reformat/refactor some code
Brian Norris [Fri, 10 Aug 2012 19:21:12 +0000 (12:21 -0700)]
model: reformat/refactor some code

12 years agoimpatomic.h: fixup spacing
Brian Norris [Fri, 10 Aug 2012 18:44:00 +0000 (11:44 -0700)]
impatomic.h: fixup spacing

Tabs vs. spaces for indentation screws up this indentation, making it even
harder to read than it should be. Switch this all to spaces (for uniformity
across all editor configurations) and align things properly.

12 years agothreads: trivial change
Brian Norris [Wed, 8 Aug 2012 23:36:10 +0000 (16:36 -0700)]
threads: trivial change

12 years agomodel: revert unnecessary parameter for print_summary()
Brian Norris [Wed, 8 Aug 2012 23:27:07 +0000 (16:27 -0700)]
model: revert unnecessary parameter for print_summary()

CycleGraph::checkForCycles() is a cheap function; it only checks a flag status.
So we don't need to make code more complicated just to avoid calling this
function.

Effectively a revert of:
commit 7cee72d776ddfbf585038f3cad3df799e353cc11

12 years agoadd basic parameter handling
Brian Norris [Wed, 8 Aug 2012 22:22:25 +0000 (15:22 -0700)]
add basic parameter handling

12 years agocommon: add error_msg() function
Brian Norris [Wed, 8 Aug 2012 22:00:13 +0000 (15:00 -0700)]
common: add error_msg() function

12 years agorun.sh: pass command-line arguments through to test program
Brian Norris [Wed, 8 Aug 2012 19:41:02 +0000 (12:41 -0700)]
run.sh: pass command-line arguments through to test program

Once the model-checker begins handling arguments, we should pass through
arguments to the program.

12 years ago.gitignore: ignore other vim swap file type
Brian Norris [Wed, 8 Aug 2012 23:33:00 +0000 (16:33 -0700)]
.gitignore: ignore other vim swap file type

12 years agomodel: reformat some code
Brian Norris [Wed, 8 Aug 2012 15:59:52 +0000 (08:59 -0700)]
model: reformat some code

12 years agomain, threads: improve comments regarding thread stepping
Brian Norris [Wed, 8 Aug 2012 00:59:44 +0000 (17:59 -0700)]
main, threads: improve comments regarding thread stepping

The comment in thread_system_next was incorrect:
"Returns the 1 if there is another step and 0 otherwise."

Add a few comments throughout to help clarify this behavior.

12 years agoadd a todo flag to a comment so it won't get lost... low priority item though
Brian Demsky [Sat, 4 Aug 2012 07:21:05 +0000 (02:21 -0500)]
add a todo flag to a comment so it won't get lost... low priority item though

12 years agoMakefile: fix config.h dependencies
Brian Norris [Fri, 3 Aug 2012 04:00:22 +0000 (21:00 -0700)]
Makefile: fix config.h dependencies

The snapshotting code needs to be rebuilt when config.h is modified.

12 years agoMerge branch 'brian'
Brian Norris [Thu, 2 Aug 2012 23:55:58 +0000 (16:55 -0700)]
Merge branch 'brian'

12 years agoDEBUGGINGNOTES: include gdb info for Linux
Brian Norris [Thu, 2 Aug 2012 23:51:45 +0000 (16:51 -0700)]
DEBUGGINGNOTES: include gdb info for Linux

12 years agobug fix
Brian Demsky [Thu, 2 Aug 2012 22:40:40 +0000 (15:40 -0700)]
bug fix

12 years agorun.sh: fixup run script
Brian Norris [Thu, 2 Aug 2012 23:37:03 +0000 (16:37 -0700)]
run.sh: fixup run script

run.sh will, by default, run ./test/userprog.o now. This can be modified later
to provide several regression tests in-tree, with scripted execution of the
tests.

12 years agoMakefile: wire up test/ directory for compilation
Brian Norris [Thu, 2 Aug 2012 23:36:29 +0000 (16:36 -0700)]
Makefile: wire up test/ directory for compilation

12 years agoMakefile: split part into a common makefile (common.mk)
Brian Norris [Thu, 2 Aug 2012 23:33:16 +0000 (16:33 -0700)]
Makefile: split part into a common makefile (common.mk)

12 years agouserprog: move to 'test/' directory
Brian Norris [Thu, 2 Aug 2012 23:27:02 +0000 (16:27 -0700)]
userprog: move to 'test/' directory

12 years agoMakefile: don't build userprog.c from top level
Brian Norris [Thu, 2 Aug 2012 23:25:44 +0000 (16:25 -0700)]
Makefile: don't build userprog.c from top level

(Temporarily disables userprog compilation; will restore soon)

12 years agoblank lines, spacing, etc.
Brian Norris [Thu, 2 Aug 2012 19:55:04 +0000 (12:55 -0700)]
blank lines, spacing, etc.

12 years agonodestack: remove completed @todo
Brian Norris [Thu, 2 Aug 2012 19:35:21 +0000 (12:35 -0700)]
nodestack: remove completed @todo

12 years agonodestack: clean up comments
Brian Norris [Thu, 2 Aug 2012 19:33:43 +0000 (12:33 -0700)]
nodestack: clean up comments

12 years agomodel: do not call isfinalfeasible() too many times
Brian Norris [Thu, 2 Aug 2012 18:13:46 +0000 (11:13 -0700)]
model: do not call isfinalfeasible() too many times

This function call incurs graph exploration, so when performing some
end-of-trace bookkeeping, we should only call it once and cache the result.

12 years agohashtable: add some documentation
Brian Norris [Thu, 2 Aug 2012 17:59:16 +0000 (10:59 -0700)]
hashtable: add some documentation

12 years agomodel: delete Threads on destruction
Brian Norris [Thu, 2 Aug 2012 17:25:31 +0000 (10:25 -0700)]
model: delete Threads on destruction

When switching from STL map to hashtable, the Thread destruction was just
commented out instead of reimplemented. This is a good enough version, I think.

12 years agomore reformatting/indentation
Brian Norris [Thu, 2 Aug 2012 17:25:17 +0000 (10:25 -0700)]
more reformatting/indentation

12 years agoforgot about events that happen after an unresolved read... bug fix checked in
Brian Demsky [Sat, 28 Jul 2012 17:45:48 +0000 (10:45 -0700)]
forgot about events that happen after an unresolved read...  bug fix checked in

12 years agofixup whitespace
Brian Norris [Wed, 1 Aug 2012 03:13:17 +0000 (20:13 -0700)]
fixup whitespace

12 years agoaction: add memory_order printing
Brian Norris [Fri, 27 Jul 2012 21:50:15 +0000 (14:50 -0700)]
action: add memory_order printing

12 years agochange test case to match nice one from spec... it works. :)
Brian Demsky [Fri, 27 Jul 2012 09:06:29 +0000 (02:06 -0700)]
change test case to match nice one from spec...  it works.  :)

12 years agobugs...
Brian Demsky [Fri, 27 Jul 2012 08:59:52 +0000 (01:59 -0700)]
bugs...

12 years agoadd some comments
Brian Demsky [Fri, 27 Jul 2012 08:24:24 +0000 (01:24 -0700)]
add some comments

12 years agostandardize names a little
Brian Demsky [Fri, 27 Jul 2012 08:19:07 +0000 (01:19 -0700)]
standardize names a little

12 years agookay...known bugs for my trivial test are out of send future values backwards
Brian Demsky [Fri, 27 Jul 2012 07:25:19 +0000 (00:25 -0700)]
okay...known bugs for my trivial test are out of send future values backwards

12 years agofinish promise support
Brian Demsky [Fri, 27 Jul 2012 05:20:54 +0000 (22:20 -0700)]
finish promise support

12 years agomore changes towards keeping track of promises resolved by a given write statement
Brian Demsky [Thu, 26 Jul 2012 23:20:02 +0000 (16:20 -0700)]
more changes towards keeping track of promises resolved by a given write statement

12 years agochanges
Brian Demsky [Thu, 26 Jul 2012 05:59:41 +0000 (22:59 -0700)]
changes

12 years agosome changes towards reading from future writes
Brian Demsky [Wed, 25 Jul 2012 23:11:51 +0000 (16:11 -0700)]
some changes towards reading from future writes

12 years agomove more configurables and add documentation
Brian Demsky [Sat, 21 Jul 2012 02:12:20 +0000 (19:12 -0700)]
move more configurables and add documentation

12 years agomore hashtable fixes
Brian Demsky [Sat, 21 Jul 2012 01:52:55 +0000 (18:52 -0700)]
more hashtable fixes

clean up memory allocation code a bit

12 years agofix some allocation/free bugs when we put non objects into table...
Brian Demsky [Fri, 20 Jul 2012 21:48:01 +0000 (14:48 -0700)]
fix some allocation/free bugs when we put non objects into table...

12 years agofix my todo comments so they appear in documentation
Brian Demsky [Fri, 20 Jul 2012 21:45:03 +0000 (14:45 -0700)]
fix my todo comments so they appear in documentation

12 years agoswitch everything over to our own hashtable
Brian Demsky [Fri, 20 Jul 2012 21:39:23 +0000 (14:39 -0700)]
switch everything over to our own hashtable

give us a calloc to use from our code

12 years agohashtable: make more flexible
Brian Demsky [Fri, 20 Jul 2012 21:01:03 +0000 (14:01 -0700)]
hashtable: make more flexible

[Split by Brian Norris]

12 years agoAdd documentation
Brian Demsky [Fri, 20 Jul 2012 21:01:03 +0000 (14:01 -0700)]
Add documentation

[Split by Brian Norris]

12 years agoaction: fix ATOMIC_RMW comments
Brian Norris [Wed, 1 Aug 2012 02:45:49 +0000 (19:45 -0700)]
action: fix ATOMIC_RMW comments

12 years agormw example works
Brian Demsky [Fri, 20 Jul 2012 19:42:42 +0000 (12:42 -0700)]
rmw example works

12 years agotowards making rmw work...
Brian Demsky [Fri, 20 Jul 2012 19:32:42 +0000 (12:32 -0700)]
towards making rmw work...

[Split by Brian Norris]

12 years agoaction: add stub ATOMIC_RMWR and ATOMIC_RMWC
Brian Norris [Wed, 1 Aug 2012 02:25:52 +0000 (19:25 -0700)]
action: add stub ATOMIC_RMWR and ATOMIC_RMWC

12 years agotrivial - whitespace, debugging cleanup, etc.
Brian Norris [Wed, 1 Aug 2012 02:20:16 +0000 (19:20 -0700)]
trivial - whitespace, debugging cleanup, etc.

12 years agoremove libatomic
Brian Demsky [Fri, 20 Jul 2012 05:42:46 +0000 (22:42 -0700)]
remove libatomic

12 years agoaction: switch from "libatomic" to C++-spec "memory_order_*" macros
Brian Norris [Wed, 1 Aug 2012 02:14:16 +0000 (19:14 -0700)]
action: switch from "libatomic" to C++-spec "memory_order_*" macros

12 years agopull in most of atomic header file
Brian Norris [Wed, 1 Aug 2012 00:25:38 +0000 (17:25 -0700)]
pull in most of atomic header file

12 years agodon't forget this file
Brian Demsky [Fri, 20 Jul 2012 05:43:07 +0000 (22:43 -0700)]
don't forget this file

12 years agosplit these defs out of other stuff
Brian Demsky [Fri, 20 Jul 2012 00:53:45 +0000 (17:53 -0700)]
split these defs out of other stuff

12 years agoswitch rest over to model checker... might work now
Brian Demsky [Fri, 20 Jul 2012 00:15:12 +0000 (17:15 -0700)]
switch rest over to model checker...  might work now

12 years agofix missing atomic...
Brian Demsky [Fri, 20 Jul 2012 00:06:11 +0000 (17:06 -0700)]
fix missing atomic...

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

12 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

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

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

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

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

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

12 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

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

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

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

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

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

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

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

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

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

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

12 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

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

12 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

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

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

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

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

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

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

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

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

12 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

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

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

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

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

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

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

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

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

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

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

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