Brian Norris [Mon, 28 May 2012 19:42:54 +0000 (12:42 -0700)]
model: log the last action in each thread
The last action in each thread is needed for some model-checking computations.
This could be expanded to a full-fledged per-thread list if needed...
Brian Norris [Mon, 28 May 2012 19:20:01 +0000 (12:20 -0700)]
nodestack: compute parent ModelAction externally
For a particular ModelAction, the 'parent' may be the last action in the
current thread, or otherwise, the action in the parent thread that created the
current thread. This calculation is not suitable for within the NodeStack (and
the current implementation is wrong, taking the last action performed by *any*
thread as the parent). Thus, I set up the method calls to pass the 'parent' to
explore_action() and leave the details to further work.
Brian Norris [Mon, 28 May 2012 19:12:04 +0000 (12:12 -0700)]
clockvector: fixup initialization
Two related fixes:
Even if parent is NULL, pass the current ModelAction to ClockVector
constructor.
When no parent is present, do not make special case for initializing
clock[0] = 1. This is only correct for a single case (the root Action)
and is already handled in other ways.
Brian Norris [Mon, 28 May 2012 17:16:34 +0000 (10:16 -0700)]
nodestack: construct Node with 'number of threads', not 'parent node'
I don't really want to base the number of threads off of a 'parent'; I can
just record the global 'number of threads' as a Node parameter.
Brian Norris [Sat, 26 May 2012 02:17:51 +0000 (19:17 -0700)]
model: add obj_thrd_map
Provides a mapping of ModelActions so that we can efficiently sort through the
actions on a particular object (memory location) in a particular thread.
Brian Norris [Sat, 26 May 2012 01:35:27 +0000 (18:35 -0700)]
Makefile: add 'make debug'
This is sort of hacky, but it works! Now (after cleaning), you can recompile
with 'make debug' to enable my debugging features (not Subramanian's).
Brian Norris [Sat, 26 May 2012 02:19:15 +0000 (19:19 -0700)]
action: enhance print() message
Include clock vector, realign
Brian Norris [Sat, 26 May 2012 02:16:06 +0000 (19:16 -0700)]
nodestack: create ModelAction clock vectors
Only create the clock vector if the ModelAction will be retained in our
nodestack, and hence will be used for synchronization, etc.
Brian Norris [Sat, 26 May 2012 02:13:36 +0000 (19:13 -0700)]
action: add create_cv() and read_from()
These functions provide basic wrapper functionality for creating and updating
the clock vector for a particular ModelAction.
Brian Norris [Sat, 26 May 2012 03:28:58 +0000 (20:28 -0700)]
clockvector: bugfix - fixup vector initialization, size
This fixes a few bugs in ClockVector:
- The parent-less vector is the initial-thread creation, so set its vector
clock[0] = 1
- The clock vector's data should be initialized to 0
- A clock vector cannot determine its size simply by the size of its parent (+1
if 'act' is THREAD_CREATE); other threads could have been created, giving an
inconsistent result here. Instead of trying to be smart about calculating
num_threads from the parent, then, I just ask for it globally.
Brian Norris [Sat, 26 May 2012 03:28:30 +0000 (20:28 -0700)]
model: add get_num_threads()
Brian Norris [Sat, 26 May 2012 02:36:06 +0000 (19:36 -0700)]
clockvector: fixup print message
Brian Norris [Wed, 16 May 2012 19:45:03 +0000 (12:45 -0700)]
clockvector: add print() method
Brian Norris [Wed, 16 May 2012 18:45:04 +0000 (11:45 -0700)]
action: add clock vector field, destructor
Brian Norris [Sat, 26 May 2012 02:00:37 +0000 (19:00 -0700)]
action: use proper location comparison
Now that snapshotting is in place for the initial state, stack allocation is
deterministic across executions, so we can compare stack-allocated addresses
again.
Brian Norris [Sat, 26 May 2012 01:44:23 +0000 (18:44 -0700)]
clockvector: add snapshotting new/delete operators
Brian Norris [Sat, 26 May 2012 01:28:49 +0000 (18:28 -0700)]
rename snapshotStack -> SnapshotStack
Brian Norris [Sat, 26 May 2012 01:23:44 +0000 (18:23 -0700)]
snapshot: remove #include, use snapshot_id typedef
Brian Norris [Sat, 26 May 2012 01:10:58 +0000 (18:10 -0700)]
snapshot-interface: cleanup interface header
The MyString type does not belong in an interface header. It's only used in one
file, so move its typedef locally.
Remove/move a bunch of misplaced #includes.
There's an unnecessary forward declaration of class snapshotStack.
Brian Norris [Sat, 26 May 2012 01:00:10 +0000 (18:00 -0700)]
model: remove scheduler comment
It's being snapshotted now.
Brian Norris [Sat, 26 May 2012 00:59:13 +0000 (17:59 -0700)]
model: don't clear thread_map (snapshot)
The thread_map structure is being snapshotted, so no need to clear it.
Brian Norris [Sat, 26 May 2012 00:11:09 +0000 (17:11 -0700)]
model: don't reset action_trace manually
Snapshotting takes care of this one
Brian Norris [Thu, 24 May 2012 18:33:36 +0000 (11:33 -0700)]
main: take/revert snapshots
Use basic snapshotting for 'reset_to_initial_state()'.
Brian Norris [Sat, 26 May 2012 00:53:56 +0000 (17:53 -0700)]
model: make thread_map heap allocated
I want to snapshot this structure, so make it heap-allocated.
Brian Norris [Fri, 25 May 2012 23:50:55 +0000 (16:50 -0700)]
action: add all action_lists to snapshot...
Brian Norris [Sat, 26 May 2012 00:14:56 +0000 (17:14 -0700)]
common: remove unneeded macros/includes
Brian Norris [Sat, 26 May 2012 00:14:18 +0000 (17:14 -0700)]
threads: fixup stack allocation (snapshotting...)
Brian Norris [Thu, 24 May 2012 18:31:39 +0000 (11:31 -0700)]
snapshot: remove time information
Why do we need timestamps? This is unneeded extra code and might cause
problems.
Brian Norris [Fri, 25 May 2012 23:45:37 +0000 (16:45 -0700)]
snapshot: fix indentation
Brian Norris [Fri, 25 May 2012 00:14:30 +0000 (17:14 -0700)]
snapshot: use %p for printing pointers
Brian Norris [Fri, 25 May 2012 23:13:02 +0000 (16:13 -0700)]
more allocation fixes (use snapshotting)
Brian Norris [Fri, 25 May 2012 23:05:23 +0000 (16:05 -0700)]
nodestack: bugfix - fixup allocators for vectors
Brian Norris [Thu, 24 May 2012 18:32:55 +0000 (11:32 -0700)]
add more classes to snapshotting region
Classes that don't use MyAlloc or MEMALLOC are snapshotted by default.
Brian Norris [Fri, 25 May 2012 00:23:38 +0000 (17:23 -0700)]
mymemory: use the right *&^% allocator!!
We're using MYMALLOC in the global new/delete instead of defaulting to
snapshottable malloc, as planned. What a stupid bug.
Also extend new/delete operators to be sure.
Brian Norris [Thu, 24 May 2012 23:39:08 +0000 (16:39 -0700)]
snapshot: fix EOL spaces
Brian Demsky [Thu, 24 May 2012 20:32:55 +0000 (13:32 -0700)]
wow, this is a nasty bug...
the last part of the snapshot bug is the following:
we snapshot the user threads stack... when we get a seg fault,
the signal handler is using the same write protected stack...
obviously this is going to cause problems. luckily there is support
for a special stack for the signal handler. this checkin switches
the signal handler to run on a different stack than the program stack.
Brian Demsky [Thu, 24 May 2012 19:09:39 +0000 (12:09 -0700)]
fix one segfault bug...something is still strange, but has to do with stack
Brian Demsky [Thu, 24 May 2012 18:50:19 +0000 (11:50 -0700)]
factor page alignment into function call...place near existing call
Brian Demsky [Thu, 24 May 2012 18:40:14 +0000 (11:40 -0700)]
fix page alignment issue...
Brian Norris [Thu, 24 May 2012 17:57:20 +0000 (10:57 -0700)]
snapshot: use perror() on failed library calls
This will print more informative messages when we fail.
Brian Norris [Thu, 24 May 2012 17:32:19 +0000 (10:32 -0700)]
mymemory: define the "opposite" of MEMALLOC
We may want an identifier to show that a particular class is intended to be
snapshotted.
Brian Norris [Thu, 24 May 2012 17:31:50 +0000 (10:31 -0700)]
mymemory: include some spacing
Brian Norris [Mon, 21 May 2012 19:33:12 +0000 (12:33 -0700)]
fixup EOL whitespace
Brian Norris [Mon, 21 May 2012 19:16:30 +0000 (12:16 -0700)]
snapshot: use 'SSDEBUG', not 'DEBUG'
Brian Norris [Mon, 21 May 2012 19:13:33 +0000 (12:13 -0700)]
model: remove incorrect #undef
Don't 'undef' something; rename it. Anyway, this is unnecessary now, since
someone renamed the new DEBUG.
Brian Norris [Mon, 21 May 2012 18:59:02 +0000 (11:59 -0700)]
userprog: use modulo
Increasing the number of loops is useless unless we have modulo here... I
don't know why this was changed by Subramanian.
Brian Norris [Mon, 21 May 2012 18:58:26 +0000 (11:58 -0700)]
libthreads: fix thrd_create() to use typedef'd start_routine
Brian Norris [Mon, 21 May 2012 18:51:07 +0000 (11:51 -0700)]
fix indentation + spacing, esp. for MEMALLOC macro
Brian Norris [Mon, 21 May 2012 18:32:56 +0000 (11:32 -0700)]
mymemory: fix indentation, spacing
Brian Norris [Mon, 21 May 2012 18:24:43 +0000 (11:24 -0700)]
nodestack: allocate from "mymemory" region
Brian Norris [Mon, 21 May 2012 18:07:44 +0000 (11:07 -0700)]
Merge commit: branch 'work'
tree.{cc,h} were replaced with NodeStack. (Will need to update them)
Other trivial conflicts in Makefile and model.h
Conflicts:
Makefile
model.h
tree.cc
tree.h
Brian Norris [Mon, 21 May 2012 17:57:16 +0000 (10:57 -0700)]
snapshot: remove references to libmymemory.so
This library doesn't exist any more.
Brian Norris [Mon, 21 May 2012 17:55:28 +0000 (10:55 -0700)]
snapshot: move local defines after #includes
Prevents accidental dependencies, where a header *might* use PAGESIZE, e.g.
Brian Norris [Mon, 21 May 2012 17:52:46 +0000 (10:52 -0700)]
main: clear out redundant comments
We don't really need these. I can read the source :)
Brian Norris [Mon, 21 May 2012 17:32:34 +0000 (10:32 -0700)]
common: disable debugging
Note to others: do not enable debugging in the checked-in code. It is for
testint purposes only.
Brian Norris [Mon, 21 May 2012 17:32:05 +0000 (10:32 -0700)]
run.sh: provide gdb option
Brian Norris [Mon, 21 May 2012 17:05:47 +0000 (10:05 -0700)]
Makefile: only build a single shared library
Now that everything is uniform, we can easily just build a single library.
Brian Norris [Mon, 21 May 2012 16:47:05 +0000 (09:47 -0700)]
Makefile: clean up Makefile
There are a number of inconsistencies and superfluous arguments:
- For libmymemory, we don't need (or want) to hardcode a shared library
relative path
- For libmodel, we don't really need the 'soname' parameter
- Linking C++ probably should be done with the C++ compiler, not the C compiler
- We don't need CPPFLAGS for linking-only stages
- We want to use LDFLAGS for an early-stage linking rather than the late-stage
linking of the user program
Overall, simpler is better
Brian Norris [Mon, 21 May 2012 16:38:50 +0000 (09:38 -0700)]
Makfile: remove MEMCPPFLAGS, more uniform command format
Brian Demsky [Mon, 21 May 2012 07:40:46 +0000 (00:40 -0700)]
remove lines from other files
Brian Demsky [Mon, 21 May 2012 07:25:37 +0000 (00:25 -0700)]
Found new way to fix emacs issue.. There are directory level preferences.
Remove file-level emacs comment and replace with directory level overrides.
Brian Demsky [Mon, 21 May 2012 06:50:34 +0000 (23:50 -0700)]
fix various problems with my 64-bit clean hack
found missing initializer bug in scheduler
Brian Demsky [Mon, 21 May 2012 06:20:43 +0000 (23:20 -0700)]
fix code to be 64 bit clean
Brian Demsky [Mon, 21 May 2012 05:54:13 +0000 (22:54 -0700)]
switch back to norris style spacing in changed files
Brian Norris [Mon, 21 May 2012 04:31:11 +0000 (21:31 -0700)]
main: what are these variables for? (subramanian...)
Brian Norris [Mon, 21 May 2012 04:27:38 +0000 (21:27 -0700)]
run.sh: don't touch my run script subramanian
Brian Norris [Mon, 21 May 2012 04:26:07 +0000 (21:26 -0700)]
Makfile: fix linking error + remove EOL whitespace
If you're using libdl for dynamic loading, you need to include the library flag
at the top-level linking.
Brian Norris [Mon, 21 May 2012 04:20:17 +0000 (21:20 -0700)]
.gitignore: fixup bad merge step
(You don't need both the *~ and *.*~ rules)
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 [Mon, 14 May 2012 18:39:24 +0000 (11:39 -0700)]
action: neuter the "same_var" function for now...
Due to some incorrect functionality for 'reset_to_initial_state()' we may not
always have the right stack locations for every execution. I'll ignore the
problem temporarily...
Brian Norris [Mon, 14 May 2012 19:08:13 +0000 (12:08 -0700)]
model: remove free_action_list() function
Brian Norris [Mon, 14 May 2012 20:22:18 +0000 (13:22 -0700)]
model: remove class Backtrack
Brian Norris [Mon, 14 May 2012 19:14:53 +0000 (12:14 -0700)]
tree: kill class TreeNode
Superceded by NodeStack
Brian Norris [Mon, 14 May 2012 20:26:03 +0000 (13:26 -0700)]
model: replace TreeNode with NodeStack
Big structural change to the model-checker internal data structure. It's now
tested to work, and hopefully it's still easy enough to understand.
Note that also, we remove the backtrack_list, since this type of structure
depended on keeping around "action lists" of each trace. Instead, I can free up
those lists at the end of each execution, preventing leaks and limiting memory
usage.
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.