c11tester.git
9 years agoMerge branch 'norris'
Brian Norris [Thu, 16 Aug 2012 17:40:59 +0000 (10:40 -0700)]
Merge branch 'norris'

9 years agoschedule: make print() const
Brian Norris [Fri, 10 Aug 2012 23:20:15 +0000 (16:20 -0700)]
schedule: make print() const

Switch to using a "const_iterator" so that the whole function becomes const.

9 years agomodel: privatize check_current_action()
Brian Norris [Fri, 10 Aug 2012 22:27:38 +0000 (15:27 -0700)]
model: privatize check_current_action()

9 years agothreads: correct 'swap()' documentation
Brian Norris [Fri, 10 Aug 2012 22:22:33 +0000 (15:22 -0700)]
threads: correct 'swap()' documentation

Some of the swap() documentation was duplicated incorrectly. While I'm at it,
make the descriptions more clear and precise.

9 years agomain, model: don't 'initialize' system_context
Brian Norris [Fri, 10 Aug 2012 22:15:24 +0000 (15:15 -0700)]
main, model: don't 'initialize' system_context

I was unnecessarily giving main.cc control of the system_context variable,
since I thought I needed to use getcontext() before entering the model checker.
However, the structure of the runtime scheduling is such that this
"initialization" would be obliterated by the first swapcontext() call
(switching form system-context to user-context).

So, the point is that the model-checker can just declare its own
("uninitialized") context that will be initialized as soon as the model-checker
makes a thread swap. Thus, I remove the external interface for initializing the
context (set_system_context()).

9 years agoaction: don't merge twice in read_from()
Brian Norris [Fri, 10 Aug 2012 21:59:20 +0000 (14:59 -0700)]
action: don't merge twice in read_from()

synchronize_with() already takes care of the clock vector merging, so don't
merge a second time.

9 years agoaction: rework/rename 'synchronized()' to 'synchronize_with()'
Brian Norris [Fri, 10 Aug 2012 21:57:20 +0000 (14:57 -0700)]
action: rework/rename 'synchronized()' to 'synchronize_with()'

Fix some comments, names, etc.

Privatize synchronized()/synchronize_with(), since it's only intended for
within other wrapper actions performed on ModelAction.

9 years agomodel: remove useless return code from add_thread()
Brian Norris [Fri, 10 Aug 2012 21:51:27 +0000 (14:51 -0700)]
model: remove useless return code from add_thread()

9 years agoschedule, threads: update comments, const's
Brian Norris [Fri, 10 Aug 2012 21:43:19 +0000 (14:43 -0700)]
schedule, threads: update comments, const's

9 years agomodel: make scheduler private
Brian Norris [Fri, 10 Aug 2012 21:29:06 +0000 (14:29 -0700)]
model: make scheduler private

To accomplish this, I needed to add one accessor method for
'get_current_thread()'.

9 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

9 years agocyclegraph: improve comments, use initializer list
Brian Norris [Tue, 14 Aug 2012 22:25:11 +0000 (15:25 -0700)]
cyclegraph: improve comments, use initializer list

9 years agohashtable: document get_safe_ptr()
Brian Norris [Sat, 11 Aug 2012 01:11:12 +0000 (18:11 -0700)]
hashtable: document get_safe_ptr()

9 years agohashtable: rename ensureptr() to get_safe_ptr()
Brian Norris [Sat, 11 Aug 2012 01:10:20 +0000 (18:10 -0700)]
hashtable: rename ensureptr() to get_safe_ptr()

ensureptr() is kind of vague. This rename -- along with some better description
-- will help clarify what this function does.

9 years agohashtable: bugfix - increment size only when new bins are linked
Brian Norris [Sat, 11 Aug 2012 00:44:36 +0000 (17:44 -0700)]
hashtable: bugfix - increment size only when new bins are linked

In both put() and ensureptr(), the 'size' counter should not be incremented
until we decide if we're adding a new bin or not. When incremented improperly,
'size' ended up out of sync with the hash table; it reported a size much larger
than the actual table.

9 years agohashtable: some refactoring, signed-ness
Brian Norris [Sat, 11 Aug 2012 00:42:40 +0000 (17:42 -0700)]
hashtable: some refactoring, signed-ness

Since 'capacity' is unsigned, so should the index that compares with it.

The (duplicated) compare/resize code can be a bit shorter and (IMO) easier to
read.

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

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

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

9 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

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

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

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

9 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

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

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

9 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

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

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

9 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

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

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

9 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

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