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

9 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

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

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

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

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

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

9 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

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

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

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

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

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

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

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

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

9 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

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

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

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

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

9 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

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