c11tester.git
10 years agoclockvector: add print() method
Brian Norris [Wed, 16 May 2012 19:45:03 +0000 (12:45 -0700)]
clockvector: add print() method

10 years agoaction: add clock vector field, destructor
Brian Norris [Wed, 16 May 2012 18:45:04 +0000 (11:45 -0700)]
action: add clock vector field, destructor

10 years agoaction: use proper location comparison
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.

10 years agoclockvector: add snapshotting new/delete operators
Brian Norris [Sat, 26 May 2012 01:44:23 +0000 (18:44 -0700)]
clockvector: add snapshotting new/delete operators

10 years agorename snapshotStack -> SnapshotStack
Brian Norris [Sat, 26 May 2012 01:28:49 +0000 (18:28 -0700)]
rename snapshotStack -> SnapshotStack

10 years agosnapshot: remove #include, use snapshot_id typedef
Brian Norris [Sat, 26 May 2012 01:23:44 +0000 (18:23 -0700)]
snapshot: remove #include, use snapshot_id typedef

10 years agosnapshot-interface: cleanup interface header
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.

10 years agomodel: remove scheduler comment
Brian Norris [Sat, 26 May 2012 01:00:10 +0000 (18:00 -0700)]
model: remove scheduler comment

It's being snapshotted now.

10 years agomodel: don't clear thread_map (snapshot)
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.

10 years agomodel: don't reset action_trace manually
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

10 years agomain: take/revert snapshots
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()'.

10 years agomodel: make thread_map heap allocated
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.

10 years agoaction: add all action_lists to snapshot...
Brian Norris [Fri, 25 May 2012 23:50:55 +0000 (16:50 -0700)]
action: add all action_lists to snapshot...

10 years agocommon: remove unneeded macros/includes
Brian Norris [Sat, 26 May 2012 00:14:56 +0000 (17:14 -0700)]
common: remove unneeded macros/includes

10 years agothreads: fixup stack allocation (snapshotting...)
Brian Norris [Sat, 26 May 2012 00:14:18 +0000 (17:14 -0700)]
threads: fixup stack allocation (snapshotting...)

10 years agosnapshot: remove time information
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.

10 years agosnapshot: fix indentation
Brian Norris [Fri, 25 May 2012 23:45:37 +0000 (16:45 -0700)]
snapshot: fix indentation

10 years agosnapshot: use %p for printing pointers
Brian Norris [Fri, 25 May 2012 00:14:30 +0000 (17:14 -0700)]
snapshot: use %p for printing pointers

10 years agomore allocation fixes (use snapshotting)
Brian Norris [Fri, 25 May 2012 23:13:02 +0000 (16:13 -0700)]
more allocation fixes (use snapshotting)

10 years agonodestack: bugfix - fixup allocators for vectors
Brian Norris [Fri, 25 May 2012 23:05:23 +0000 (16:05 -0700)]
nodestack: bugfix - fixup allocators for vectors

10 years agoadd more classes to snapshotting region
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.

10 years agomymemory: use the right *&^% allocator!!
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.

10 years agosnapshot: fix EOL spaces
Brian Norris [Thu, 24 May 2012 23:39:08 +0000 (16:39 -0700)]
snapshot: fix EOL spaces

10 years agowow, this is a nasty bug...
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.

10 years agofix one segfault bug...something is still strange, but has to do with 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

10 years agofactor page alignment into function call...place near existing call
Brian Demsky [Thu, 24 May 2012 18:50:19 +0000 (11:50 -0700)]
factor page alignment into function call...place near existing call

10 years agofix page alignment issue...
Brian Demsky [Thu, 24 May 2012 18:40:14 +0000 (11:40 -0700)]
fix page alignment issue...

10 years agosnapshot: use perror() on failed library calls
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.

10 years agomymemory: define the "opposite" of MEMALLOC
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.

10 years agomymemory: include some spacing
Brian Norris [Thu, 24 May 2012 17:31:50 +0000 (10:31 -0700)]
mymemory: include some spacing

10 years agofixup EOL whitespace
Brian Norris [Mon, 21 May 2012 19:33:12 +0000 (12:33 -0700)]
fixup EOL whitespace

10 years agosnapshot: use 'SSDEBUG', not 'DEBUG'
Brian Norris [Mon, 21 May 2012 19:16:30 +0000 (12:16 -0700)]
snapshot: use 'SSDEBUG', not 'DEBUG'

10 years agomodel: remove incorrect #undef
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.

10 years agouserprog: use modulo
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.

10 years agolibthreads: fix thrd_create() to use typedef'd start_routine
Brian Norris [Mon, 21 May 2012 18:58:26 +0000 (11:58 -0700)]
libthreads: fix thrd_create() to use typedef'd start_routine

10 years agofix indentation + spacing, esp. for MEMALLOC macro
Brian Norris [Mon, 21 May 2012 18:51:07 +0000 (11:51 -0700)]
fix indentation + spacing, esp. for MEMALLOC macro

10 years agomymemory: fix indentation, spacing
Brian Norris [Mon, 21 May 2012 18:32:56 +0000 (11:32 -0700)]
mymemory: fix indentation, spacing

10 years agonodestack: allocate from "mymemory" region
Brian Norris [Mon, 21 May 2012 18:24:43 +0000 (11:24 -0700)]
nodestack: allocate from "mymemory" region

10 years agoMerge commit: branch 'work'
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

10 years agosnapshot: remove references to libmymemory.so
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.

10 years agosnapshot: move local defines after #includes
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.

10 years agomain: clear out redundant comments
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 :)

10 years agocommon: disable debugging
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.

10 years agorun.sh: provide gdb option
Brian Norris [Mon, 21 May 2012 17:32:05 +0000 (10:32 -0700)]
run.sh: provide gdb option

10 years agoMakefile: only build a single shared library
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.

10 years agoMakefile: clean up Makefile
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

10 years agoMakfile: remove MEMCPPFLAGS, more uniform command format
Brian Norris [Mon, 21 May 2012 16:38:50 +0000 (09:38 -0700)]
Makfile: remove MEMCPPFLAGS, more uniform command format

10 years agoremove lines from other files
Brian Demsky [Mon, 21 May 2012 07:40:46 +0000 (00:40 -0700)]
remove lines from other files

10 years agoFound new way to fix emacs issue.. There are directory level preferences.
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.

10 years agofix various problems with my 64-bit clean hack
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

10 years agofix code to be 64 bit clean
Brian Demsky [Mon, 21 May 2012 06:20:43 +0000 (23:20 -0700)]
fix code to be 64 bit clean

10 years agoswitch back to norris style spacing in changed files
Brian Demsky [Mon, 21 May 2012 05:54:13 +0000 (22:54 -0700)]
switch back to norris style spacing in changed files

10 years agomain: what are these variables for? (subramanian...)
Brian Norris [Mon, 21 May 2012 04:31:11 +0000 (21:31 -0700)]
main: what are these variables for? (subramanian...)

10 years agorun.sh: don't touch my run script subramanian
Brian Norris [Mon, 21 May 2012 04:27:38 +0000 (21:27 -0700)]
run.sh: don't touch my run script subramanian

10 years agoMakfile: fix linking error + remove EOL whitespace
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.

10 years ago.gitignore: fixup bad merge step
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)

10 years agoremove unused #define
Brian Demsky [Sat, 19 May 2012 01:23:08 +0000 (18:23 -0700)]
remove unused #define

10 years agomy changes
Brian Demsky [Sat, 19 May 2012 01:21:39 +0000 (18:21 -0700)]
my changes

10 years agolet us set the size of the heap in a sane way
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

10 years agosetup main wrapper and then call into norris code
Brian Demsky [Sat, 19 May 2012 00:39:47 +0000 (17:39 -0700)]
setup main wrapper and then call into norris code

10 years agoget rid of redundant mallocs
Brian Demsky [Sat, 19 May 2012 00:22:53 +0000 (17:22 -0700)]
get rid of redundant mallocs

10 years agotransfer stuff
Brian Demsky [Fri, 18 May 2012 23:56:34 +0000 (16:56 -0700)]
transfer stuff

10 years agomakefile
Brian Demsky [Fri, 18 May 2012 23:51:10 +0000 (16:51 -0700)]
makefile

10 years agoAt least everything compiles now... Subramanian's changes pushed into main fork...
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...

10 years agomerging stuff...made need to clean up some stuff...but need to push it somewhere...
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

10 years agofix this stuff...
Brian Demsky [Tue, 15 May 2012 18:21:20 +0000 (11:21 -0700)]
fix this stuff...

10 years agoaction: neuter the "same_var" function for now...
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...

10 years agomodel: remove free_action_list() function
Brian Norris [Mon, 14 May 2012 19:08:13 +0000 (12:08 -0700)]
model: remove free_action_list() function

10 years agomodel: remove class Backtrack
Brian Norris [Mon, 14 May 2012 20:22:18 +0000 (13:22 -0700)]
model: remove class Backtrack

10 years agotree: kill class TreeNode
Brian Norris [Mon, 14 May 2012 19:14:53 +0000 (12:14 -0700)]
tree: kill class TreeNode

Superceded by NodeStack

10 years agomodel: replace TreeNode with 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.

10 years agouserprog: tweak test program to use simple loads/stores
Brian Norris [Tue, 15 May 2012 17:19:08 +0000 (10:19 -0700)]
userprog: tweak test program to use simple loads/stores

10 years agolibatomic: place the proper read-value in 'atomic_load' ModelActions
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.

10 years agodon't check in useless files
Brian Demsky [Tue, 15 May 2012 17:08:02 +0000 (10:08 -0700)]
don't check in useless files

10 years agolibrace: actually compute the loads and stores
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.

10 years agoDefining the interfaces to add various regions to snapshot
Subramanian Ganapathy [Tue, 15 May 2012 01:29:08 +0000 (18:29 -0700)]
Defining the interfaces to add various regions to snapshot

10 years agoaction: add get_node() accessor
Brian Norris [Mon, 14 May 2012 20:23:24 +0000 (13:23 -0700)]
action: add get_node() accessor

10 years agonodestack: remove unnecessary conditional
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).

10 years agomodel: merge advance_backtracking_state() and get_next_replay_thread()
Brian Norris [Mon, 14 May 2012 19:59:33 +0000 (12:59 -0700)]
model: merge advance_backtracking_state() and get_next_replay_thread()

10 years agomodel: rename check_current_action() local variables
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".

10 years agoaction: add comparison operator for ModelAction
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.

10 years agonodestack: add class NodeStack and class Node
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.

10 years ago.gitignore: add *~ files
Brian Norris [Thu, 10 May 2012 01:43:54 +0000 (18:43 -0700)]
.gitignore: add *~ files

10 years agomodel: change constructor assignments to initializer list
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...

10 years agoInitializing variable which contains global snapshotting regions
Subramanian Ganapathy [Thu, 10 May 2012 21:09:42 +0000 (14:09 -0700)]
Initializing variable which contains global snapshotting regions

10 years agoAdding support to return global segments of the process using the /proc/maps
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

10 years agoAdding STL stuff and operator news of snapshot to model-checker. Need to actuallly...
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

10 years agoaction: rename 'node' members to 'treenode'
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.

10 years agomodel: remove unnecessary "this->"
Brian Norris [Tue, 8 May 2012 18:38:36 +0000 (11:38 -0700)]
model: remove unnecessary "this->"

10 years agomain/threads: remove excess headers
Brian Norris [Tue, 8 May 2012 17:49:55 +0000 (10:49 -0700)]
main/threads: remove excess headers

10 years agoclockvector: add ClockVector class
Brian Norris [Thu, 3 May 2012 18:33:19 +0000 (11:33 -0700)]
clockvector: add ClockVector class

10 years agoaction: split ModelAction off into action.cc
Brian Norris [Sat, 5 May 2012 07:25:57 +0000 (00:25 -0700)]
action: split ModelAction off into action.cc

10 years agomodel: free final list
Brian Norris [Sat, 5 May 2012 07:19:56 +0000 (00:19 -0700)]
model: free final list

10 years agomodel: free threads, thread_map at destruction
Brian Norris [Sat, 5 May 2012 06:33:42 +0000 (23:33 -0700)]
model: free threads, thread_map at destruction

10 years agotree: include cstddef for NULL
Brian Norris [Fri, 4 May 2012 07:15:31 +0000 (00:15 -0700)]
tree: include cstddef for NULL

Needed for newer, stricter compilers...

10 years agomodel: change DEBUG() statement to ASSERT()
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!

10 years agobugfix - set backtrack events according to an *enabled* thread
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.

10 years agotree: add is_enabled(Thread *)
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...

10 years agotree: revise arguments (use Thread, ModelAction)
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.

10 years agomain: split main() (and related functions) into main.cc
Brian Norris [Tue, 8 May 2012 17:30:41 +0000 (10:30 -0700)]
main: split main() (and related functions) into main.cc