Brian Demsky [Sat, 19 May 2012 01:23:08 +0000 (18:23 -0700)]
remove unused #define
Brian Demsky [Sat, 19 May 2012 01:21:39 +0000 (18:21 -0700)]
my changes
Brian Demsky [Sat, 19 May 2012 01:14:26 +0000 (18:14 -0700)]
let us set the size of the heap in a sane way
Brian Demsky [Sat, 19 May 2012 00:39:47 +0000 (17:39 -0700)]
setup main wrapper and then call into norris code
Brian Demsky [Sat, 19 May 2012 00:22:53 +0000 (17:22 -0700)]
get rid of redundant mallocs
Brian Demsky [Fri, 18 May 2012 23:56:34 +0000 (16:56 -0700)]
transfer stuff
Brian Demsky [Fri, 18 May 2012 23:51:10 +0000 (16:51 -0700)]
makefile
Brian Demsky [Fri, 18 May 2012 23:44:26 +0000 (16:44 -0700)]
At least everything compiles now... Subramanian's changes pushed into main fork... unclear whether it works...
Brian Demsky [Fri, 18 May 2012 23:32:38 +0000 (16:32 -0700)]
merging stuff...made need to clean up some stuff...but need to push it somewhere else for now
Merge branch 'subramanian'
Conflicts:
.gitignore
Makefile
action.h
userprog.c
Brian Demsky [Tue, 15 May 2012 18:21:20 +0000 (11:21 -0700)]
fix this stuff...
Brian Norris [Tue, 15 May 2012 17:19:08 +0000 (10:19 -0700)]
userprog: tweak test program to use simple loads/stores
Brian Norris [Tue, 15 May 2012 17:12:04 +0000 (10:12 -0700)]
libatomic: place the proper read-value in 'atomic_load' ModelActions
Even though I was doing rudimentary loading and storing of atomic values, I
didn't properly record the value in the ModelAction. That will be confusing
soon if I don't fix it. So fix it.
Brian Demsky [Tue, 15 May 2012 17:08:02 +0000 (10:08 -0700)]
don't check in useless files
Brian Norris [Tue, 15 May 2012 17:03:30 +0000 (10:03 -0700)]
librace: actually compute the loads and stores
We need to perform the actual load or store within our race detection library,
since the model checker totally takes over the operation.
Subramanian Ganapathy [Tue, 15 May 2012 01:29:08 +0000 (18:29 -0700)]
Defining the interfaces to add various regions to snapshot
Brian Norris [Mon, 14 May 2012 20:23:24 +0000 (13:23 -0700)]
action: add get_node() accessor
Brian Norris [Mon, 14 May 2012 19:46:14 +0000 (12:46 -0700)]
nodestack: remove unnecessary conditional
I expect that we should never have a totally-empty NodeStack. It is designed
such that there is a stub 'empty' node that represents the choices at the start
of the program, when the first userprogram thread is 'created' (note: there is
no corresponding ModelAction for this first creation).
Brian Norris [Mon, 14 May 2012 19:59:33 +0000 (12:59 -0700)]
model: merge advance_backtracking_state() and get_next_replay_thread()
Brian Norris [Mon, 14 May 2012 19:38:30 +0000 (12:38 -0700)]
model: rename check_current_action() local variables
This function needs some major rewriting when transitioning from our Tree to a
"Stack". Start by properly naming "next" as "curr".
Brian Norris [Mon, 14 May 2012 18:16:44 +0000 (11:16 -0700)]
action: add comparison operator for ModelAction
The operator simply compares the sequence number. Useful for some simple
model-checking tests.
Brian Norris [Mon, 14 May 2012 18:05:02 +0000 (11:05 -0700)]
nodestack: add class NodeStack and class Node
These will replace class TreeNode in the near future, since I don't need to
retain the entire execution tree: just the stack of the current tree, along
with some backtracking information.
Brian Norris [Thu, 10 May 2012 01:43:54 +0000 (18:43 -0700)]
.gitignore: add *~ files
Brian Norris [Wed, 9 May 2012 06:45:00 +0000 (23:45 -0700)]
model: change constructor assignments to initializer list
Apparently this is a nice C++ feature I didn't know of. Not much use here,
but there will be other uses...
Subramanian Ganapathy [Thu, 10 May 2012 21:09:42 +0000 (14:09 -0700)]
Initializing variable which contains global snapshotting regions
Subramanian Ganapathy [Thu, 10 May 2012 21:07:52 +0000 (14:07 -0700)]
Adding support to return global segments of the process using the /proc/maps
Subramanian Ganapathy [Wed, 9 May 2012 22:48:29 +0000 (15:48 -0700)]
Adding STL stuff and operator news of snapshot to model-checker. Need to actuallly find the hooks which do the actual snapshotting
Brian Norris [Wed, 9 May 2012 06:42:32 +0000 (23:42 -0700)]
action: rename 'node' members to 'treenode'
I am transitioning from class TreeNode to another class (perhaps class
Node?), so rename these members to avoid collision.
Brian Norris [Tue, 8 May 2012 18:38:36 +0000 (11:38 -0700)]
model: remove unnecessary "this->"
Brian Norris [Tue, 8 May 2012 17:49:55 +0000 (10:49 -0700)]
main/threads: remove excess headers
Brian Norris [Thu, 3 May 2012 18:33:19 +0000 (11:33 -0700)]
clockvector: add ClockVector class
Brian Norris [Sat, 5 May 2012 07:25:57 +0000 (00:25 -0700)]
action: split ModelAction off into action.cc
Brian Norris [Sat, 5 May 2012 07:19:56 +0000 (00:19 -0700)]
model: free final list
Brian Norris [Sat, 5 May 2012 06:33:42 +0000 (23:33 -0700)]
model: free threads, thread_map at destruction
Brian Norris [Fri, 4 May 2012 07:15:31 +0000 (00:15 -0700)]
tree: include cstddef for NULL
Needed for newer, stricter compilers...
Brian Norris [Fri, 4 May 2012 06:51:26 +0000 (23:51 -0700)]
model: change DEBUG() statement to ASSERT()
Now that I've fixed the model-checking bug that produced this error, turn this
error message into a fail-stop ASSERT() statement. This way, I won't ignore a
bug like this in the future!
Brian Norris [Fri, 4 May 2012 06:46:43 +0000 (23:46 -0700)]
bugfix - set backtrack events according to an *enabled* thread
Previously, I naively set a backtracking point for the thread that performed
the conflicting action, whether or not that thread existed at the point to
which I am backtracking. Utilize the TreeNode::is_enabled() method, plus thread
parent walking, to find the correct thread for the backtracking.
Note that this also requires a model checking event for each THREAD_CREATE
event. So add this feature.
Brian Norris [Fri, 4 May 2012 06:30:28 +0000 (23:30 -0700)]
tree: add is_enabled(Thread *)
Determine "enabled" by: was the thread created at this point. Checking against
num_threads is a naive way to do this...
Brian Norris [Fri, 4 May 2012 06:27:46 +0000 (23:27 -0700)]
tree: revise arguments (use Thread, ModelAction)
Preparation for other changes to the TreeNode.
Brian Norris [Tue, 8 May 2012 17:30:41 +0000 (10:30 -0700)]
main: split main() (and related functions) into main.cc
Brian Norris [Fri, 4 May 2012 05:30:25 +0000 (22:30 -0700)]
schedule: fix printf warning (size_t uses %zu)
Brian Norris [Thu, 3 May 2012 21:04:38 +0000 (14:04 -0700)]
threads: add parent info + get_parent() method
Brian Norris [Thu, 3 May 2012 21:01:58 +0000 (14:01 -0700)]
model: bugfix - rearrange debug message
This debug message depends on 'exploring' still being a valid reference.
However, we immediately explore one step via get_next_replay_thread(), which
could discard this Backtrack object. So print the debug message before doing
any exploration of the next execution stage.
Brian Norris [Thu, 3 May 2012 18:46:27 +0000 (11:46 -0700)]
model: move class Backtrack to model.cc
Backtrack is only used within model.{cc,h}, so make it an "inner class."
Brian Norris [Thu, 3 May 2012 18:39:28 +0000 (11:39 -0700)]
straighten out header includes, comment on Forward declarations
Brian Norris [Thu, 3 May 2012 18:15:47 +0000 (11:15 -0700)]
replace non-fatal error messages with ASSERT()'s
Some errors have been overlooked because they are not 'loud' enough. Use
ASSERT() macro to fail-stop.
Brian Norris [Thu, 3 May 2012 18:09:07 +0000 (11:09 -0700)]
model: print replay/divergence information when starting a new execution
Brian Norris [Thu, 3 May 2012 18:08:36 +0000 (11:08 -0700)]
model: split printing into print_list() function
Brian Norris [Wed, 2 May 2012 23:57:06 +0000 (16:57 -0700)]
threads: don't call the userprogram interface for initial thread, just create it
This will help once I start model-checking thrd_create().
Brian Norris [Wed, 2 May 2012 23:10:51 +0000 (16:10 -0700)]
common: add ASSERT()
Brian Norris [Wed, 2 May 2012 22:54:40 +0000 (15:54 -0700)]
model: number threads from 0, not 1
Brian Norris [Wed, 2 May 2012 22:50:52 +0000 (15:50 -0700)]
userprog: print current thread ID
Brian Norris [Wed, 2 May 2012 07:33:10 +0000 (00:33 -0700)]
model: add sequence numbers to ModelAction
Brian Norris [Wed, 2 May 2012 06:48:01 +0000 (23:48 -0700)]
model: fixup ModelAction print message
Brian Norris [Tue, 1 May 2012 20:25:47 +0000 (13:25 -0700)]
threads: move thread_id_t definition and redefine thrd_t type
Brian Norris [Tue, 1 May 2012 20:24:35 +0000 (13:24 -0700)]
model: index thread_map by int, not thread_id_t
Brian Norris [Tue, 1 May 2012 20:20:31 +0000 (13:20 -0700)]
model: change type for ModelChecker::get_id()
Brian Norris [Tue, 1 May 2012 20:16:09 +0000 (13:16 -0700)]
tree: remove tree_t, map thread ids via int, not thread_id_t
In the underlying structure of the TreeNode, use 'int' as a set and list key,
not 'thread_id_t'.
Brian Norris [Tue, 1 May 2012 20:08:35 +0000 (13:08 -0700)]
threads: add id_to_int() and int_to_id() inline functions
Brian Norris [Mon, 30 Apr 2012 23:35:59 +0000 (16:35 -0700)]
model: remove braces
Brian Norris [Mon, 30 Apr 2012 16:51:17 +0000 (09:51 -0700)]
clean up header #includes
Brian Norris [Mon, 30 Apr 2012 07:36:33 +0000 (00:36 -0700)]
split header out to action.h
Brian Norris [Mon, 30 Apr 2012 07:08:49 +0000 (00:08 -0700)]
tree: fix header for potential multiple inclusions
Brian Norris [Sun, 29 Apr 2012 19:57:05 +0000 (12:57 -0700)]
model: add is_acquire() and is_release() helper functions
Brian Norris [Sun, 29 Apr 2012 06:41:41 +0000 (23:41 -0700)]
model: wrap some ModelAction helper functions
Brian Norris [Fri, 27 Apr 2012 06:50:10 +0000 (23:50 -0700)]
malloc: add exception info to function header
Brian Norris [Fri, 27 Apr 2012 06:42:55 +0000 (23:42 -0700)]
model: backtracking messages are only for debugging
Brian Norris [Fri, 27 Apr 2012 06:42:12 +0000 (23:42 -0700)]
common: add simple DBG_ENABLED() macros
Brian Norris [Fri, 27 Apr 2012 06:36:26 +0000 (23:36 -0700)]
thread: remove dead Thread code
Brian Norris [Fri, 27 Apr 2012 06:35:44 +0000 (23:35 -0700)]
model: fixup thread ID selection
Brian Norris [Thu, 26 Apr 2012 23:52:20 +0000 (16:52 -0700)]
demote 'system_thread' to just 'system_context'
I don't need the extra 'class Thread' metadata for the ModelChecker 'system
thread,' and the dual use of class Thread for both system and user threads was
causing problems. So I separate them: class Thread is used only for user
threads. This changes a few interfaces throughout the code.
Brian Norris [Thu, 26 Apr 2012 23:16:23 +0000 (16:16 -0700)]
libatomic: add atomic_init()
Brian Norris [Thu, 26 Apr 2012 23:15:31 +0000 (16:15 -0700)]
userprog: print atomic load/store values
Brian Norris [Thu, 26 Apr 2012 23:14:27 +0000 (16:14 -0700)]
libatomic: use 'values' for atomic load/store
Brian Norris [Thu, 26 Apr 2012 19:05:08 +0000 (12:05 -0700)]
model: bugfix - detect conflicts properly
Finding a conflict from the same thread does not mean we should quit the search
with no found conflict; we just continue to the next search item.
Brian Norris [Thu, 26 Apr 2012 18:47:22 +0000 (11:47 -0700)]
libatomic: add DBG() calls
Brian Norris [Thu, 26 Apr 2012 18:38:36 +0000 (11:38 -0700)]
model: bugfix - reset the "current_action" after it has been processed
There are executions under which we may call ModelChecker::check_current_action()
twice in a row without an acutal ModelAction (curren_action) being set in
between. This causes the previous action to be queued twice in our trace
listing.
This can be solved 2 ways:
(1) set current_action to NULL after processing it
(2) move all calls to check_current_action() under the THREAD_READY codepath,
so that we guarantee that some Thread pushed an Action back to the
model-checking system
I do both.
Brian Norris [Thu, 26 Apr 2012 17:19:12 +0000 (10:19 -0700)]
librace: format DEBUG() prints properly
Apparently ISO C99 defines macros PRIuXX for proper printing of different-sized
uints.
Brian Norris [Wed, 25 Apr 2012 23:55:46 +0000 (16:55 -0700)]
librace: add load/store interface for checking data races
The compiler portion will need to replace loads/stores with calls to the
store_X() and load_X() functions.
Brian Norris [Tue, 24 Apr 2012 20:44:34 +0000 (13:44 -0700)]
model: remove unused definition
Brian Norris [Tue, 24 Apr 2012 20:38:37 +0000 (13:38 -0700)]
threads: allocate Threads in via userMalloc()
Thread state information should be held in the snapshotting region (when
implemented), so override new and delete.
Brian Norris [Tue, 24 Apr 2012 20:22:38 +0000 (13:22 -0700)]
common: introduce userMalloc() and userFree()
These are stubs for now, but I will need these.
Brian Norris [Tue, 24 Apr 2012 20:07:37 +0000 (13:07 -0700)]
libthreads: remove unnecessary 'extern'
Brian Norris [Tue, 24 Apr 2012 20:03:43 +0000 (13:03 -0700)]
run.sh: add simple 'run' script
Performs the step of setting LD_LIBRARY_PATH for simple runs.
Brian Norris [Tue, 24 Apr 2012 20:03:23 +0000 (13:03 -0700)]
userprog: use typedef'd thrd_start_t
Brian Norris [Tue, 24 Apr 2012 20:01:13 +0000 (13:01 -0700)]
.gitignore: add *.so
Brian Norris [Tue, 24 Apr 2012 20:00:35 +0000 (13:00 -0700)]
Makefile: build model checker as shared library (libmodel.so)
Brian Norris [Tue, 24 Apr 2012 19:06:21 +0000 (12:06 -0700)]
lib*.h: wrap C headers in `extern "C"'
Brian Norris [Tue, 24 Apr 2012 06:31:52 +0000 (23:31 -0700)]
libthreads: don't create ModelAction for thrd_join()
Temporarily? I may need to model-check join operations later.
Brian Norris [Tue, 24 Apr 2012 04:18:06 +0000 (21:18 -0700)]
model: rename print_trace() -> print_summary(), fixup summary printing
Brian Norris [Tue, 24 Apr 2012 03:39:01 +0000 (20:39 -0700)]
schedule: only print when DEBUG is enabled
Brian Norris [Tue, 24 Apr 2012 03:18:44 +0000 (20:18 -0700)]
tmp (model)
Brian Norris [Tue, 24 Apr 2012 03:16:05 +0000 (20:16 -0700)]
threads: cleanup inconsistencies in memory management
Brian Norris [Tue, 24 Apr 2012 03:13:02 +0000 (20:13 -0700)]
threads: set up Thread to be freed properly
To ensure that we can free memory properly, set up a destructor and rename
dispose() to complete().
Brian Norris [Tue, 24 Apr 2012 03:09:45 +0000 (20:09 -0700)]
schedule: reset scheduler when thread is removed
Ensure that the 'current' thread reference is removed properly.
Brian Norris [Tue, 24 Apr 2012 02:46:30 +0000 (19:46 -0700)]
threads: don't make direct call into scheduler
Since I need a ModelChecker::add_thread(Thread *) function anyway, I should
direct add_thread() calls through the model-checker framework rather than the
Scheduler class. This will make things a little cleaner and symmetric when I
add a remove_thread() function.
Brian Norris [Tue, 24 Apr 2012 02:22:52 +0000 (19:22 -0700)]
threads: save id within class Thread
There may be points at which the user's thread ID struct goes out of scope, but
I still need it internally. I think I'll just keep it internally, with a
duplicate in the user's copy.
Brian Norris [Tue, 24 Apr 2012 00:43:42 +0000 (17:43 -0700)]
threads: initialized Thread member variables
Brian Norris [Tue, 24 Apr 2012 00:34:06 +0000 (17:34 -0700)]
unify style for returning pointers
When returning a pointer from a function, always put a space between the type,
the '*', and the function name. E.g.:
type * func(args);
Brian Norris [Tue, 24 Apr 2012 00:14:45 +0000 (17:14 -0700)]
model: print 'number of executions'
In preparation of many executions, I establish a counting variable
'num_executions'.
Brian Norris [Tue, 24 Apr 2012 00:12:01 +0000 (17:12 -0700)]
threads: prepare system to loop over many executions