c11tester.git
9 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)

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

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

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

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

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

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

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

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

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

9 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

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

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

9 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.  :)

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

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

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

9 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

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

9 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

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

9 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

9 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

9 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

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

9 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

9 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

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

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

[Split by Brian Norris]

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

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

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

9 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

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

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

9 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

9 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

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

9 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

9 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

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

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

9 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

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

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

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

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

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

9 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

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

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

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

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

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

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

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

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

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

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

9 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

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

9 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

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

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

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

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

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

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

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

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

9 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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