c11tester.git
11 years agolibrace: format DEBUG() prints properly
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.

11 years agolibrace: add load/store interface for checking data races
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.

11 years agomodel: remove unused definition
Brian Norris [Tue, 24 Apr 2012 20:44:34 +0000 (13:44 -0700)]
model: remove unused definition

11 years agothreads: allocate Threads in via userMalloc()
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.

11 years agocommon: introduce userMalloc() and userFree()
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.

11 years agolibthreads: remove unnecessary 'extern'
Brian Norris [Tue, 24 Apr 2012 20:07:37 +0000 (13:07 -0700)]
libthreads: remove unnecessary 'extern'

11 years agorun.sh: add simple 'run' script
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.

11 years agouserprog: use typedef'd thrd_start_t
Brian Norris [Tue, 24 Apr 2012 20:03:23 +0000 (13:03 -0700)]
userprog: use typedef'd thrd_start_t

11 years ago.gitignore: add *.so
Brian Norris [Tue, 24 Apr 2012 20:01:13 +0000 (13:01 -0700)]
.gitignore: add *.so

11 years agoMakefile: build model checker as shared library (libmodel.so)
Brian Norris [Tue, 24 Apr 2012 20:00:35 +0000 (13:00 -0700)]
Makefile: build model checker as shared library (libmodel.so)

11 years agolib*.h: wrap C headers in `extern "C"'
Brian Norris [Tue, 24 Apr 2012 19:06:21 +0000 (12:06 -0700)]
lib*.h: wrap C headers in `extern "C"'

11 years agolibthreads: don't create ModelAction for thrd_join()
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.

11 years agomodel: rename print_trace() -> print_summary(), fixup summary printing
Brian Norris [Tue, 24 Apr 2012 04:18:06 +0000 (21:18 -0700)]
model: rename print_trace() -> print_summary(), fixup summary printing

11 years agoschedule: only print when DEBUG is enabled
Brian Norris [Tue, 24 Apr 2012 03:39:01 +0000 (20:39 -0700)]
schedule: only print when DEBUG is enabled

11 years agotmp (model)
Brian Norris [Tue, 24 Apr 2012 03:18:44 +0000 (20:18 -0700)]
tmp (model)

11 years agothreads: cleanup inconsistencies in memory management
Brian Norris [Tue, 24 Apr 2012 03:16:05 +0000 (20:16 -0700)]
threads: cleanup inconsistencies in memory management

11 years agothreads: set up Thread to be freed properly
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().

11 years agoschedule: reset scheduler when thread is removed
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.

11 years agothreads: don't make direct call into scheduler
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.

11 years agothreads: save id within class Thread
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.

11 years agothreads: initialized Thread member variables
Brian Norris [Tue, 24 Apr 2012 00:43:42 +0000 (17:43 -0700)]
threads: initialized Thread member variables

11 years agounify style for returning pointers
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);

11 years agomodel: print 'number of executions'
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'.

11 years agothreads: prepare system to loop over many executions
Brian Norris [Tue, 24 Apr 2012 00:12:01 +0000 (17:12 -0700)]
threads: prepare system to loop over many executions

11 years agoimprove scheduler debugging
Brian Norris [Mon, 23 Apr 2012 23:00:06 +0000 (16:00 -0700)]
improve scheduler debugging

11 years agoschedule: bugfix - set 'current' thread in all cases
Brian Norris [Mon, 23 Apr 2012 22:40:42 +0000 (15:40 -0700)]
schedule: bugfix - set 'current' thread in all cases

When the scheduler was following a model-checking replay execution, it did not
set the 'current' thread properly.

11 years agoschedule: refactor next_thread() for better debug printing
Brian Norris [Mon, 23 Apr 2012 22:39:07 +0000 (15:39 -0700)]
schedule: refactor next_thread() for better debug printing

It makes more sense to call print() at the end of the the next_thread()
routine, to see consistent printing for all cases. So I refactor the control
flow to a single return statement.

11 years agoschedule: print debug info
Brian Norris [Mon, 23 Apr 2012 06:14:40 +0000 (23:14 -0700)]
schedule: print debug info

11 years agomodel: add simple comment
Brian Norris [Fri, 20 Apr 2012 17:59:02 +0000 (10:59 -0700)]
model: add simple comment

11 years agomodel: move public functions to private
Brian Norris [Fri, 20 Apr 2012 17:58:40 +0000 (10:58 -0700)]
model: move public functions to private

11 years agomodel: implement get_next_replay() and advance_backtracking_state()
Brian Norris [Fri, 20 Apr 2012 17:55:44 +0000 (10:55 -0700)]
model: implement get_next_replay() and advance_backtracking_state()

11 years agomodel: implement, use schedule_next_thread()
Brian Norris [Fri, 20 Apr 2012 17:50:29 +0000 (10:50 -0700)]
model: implement, use schedule_next_thread()

Relies on the rest of the model checker to set the next thread; simply returns
the chosen thread.

11 years agomodel: add prototypes to header
Brian Norris [Fri, 20 Apr 2012 17:47:10 +0000 (10:47 -0700)]
model: add prototypes to header

I will implement these functions in the next few commits.

11 years agomodel: add iteration routines for class Backtrack
Brian Norris [Fri, 20 Apr 2012 17:35:16 +0000 (10:35 -0700)]
model: add iteration routines for class Backtrack

11 years agomodel: include <cstddef>
Brian Norris [Fri, 20 Apr 2012 17:31:42 +0000 (10:31 -0700)]
model: include <cstddef>

NULL is not a builtin keyword in recent C++ revisions. I have to include
<cstddef>.

11 years agoschedule: replace queue with list
Brian Norris [Fri, 20 Apr 2012 17:30:58 +0000 (10:30 -0700)]
schedule: replace queue with list

I'll need random access to its elements later.

11 years agothreads: introduce THREAD_ID_T_NONE
Brian Norris [Fri, 20 Apr 2012 06:28:41 +0000 (23:28 -0700)]
threads: introduce THREAD_ID_T_NONE

Represents a kind of 'NULL' thread, but for integer IDs.

11 years agothreads: remove leftover class 'prototype'
Brian Norris [Fri, 20 Apr 2012 06:26:33 +0000 (23:26 -0700)]
threads: remove leftover class 'prototype'

11 years agomodel: stash each backtrack event in ModelChecker::backtrack_list
Brian Norris [Thu, 19 Apr 2012 20:21:02 +0000 (13:21 -0700)]
model: stash each backtrack event in ModelChecker::backtrack_list

11 years agomodel: add class Backtrack
Brian Norris [Thu, 19 Apr 2012 20:20:47 +0000 (13:20 -0700)]
model: add class Backtrack

11 years agomodel: create 'action_list_t' typedef
Brian Norris [Thu, 19 Apr 2012 20:00:26 +0000 (13:00 -0700)]
model: create 'action_list_t' typedef

'std::list<class ModelAction *>' is a long name for a repeated type. Replace
it.

11 years agomodel: convert 'action_trace' to pointer
Brian Norris [Thu, 19 Apr 2012 19:56:21 +0000 (12:56 -0700)]
model: convert 'action_trace' to pointer

We need to swap out this list with a new one when we reset, and we want to
retain references to this list easily, so make the ModelChecker::action_trace
member into a pointer to a list.

11 years agomodel: add TreeNode debugging information to print_trace()
Brian Norris [Thu, 19 Apr 2012 18:31:41 +0000 (11:31 -0700)]
model: add TreeNode debugging information to print_trace()

11 years agomodel: implement get_last_conflict()
Brian Norris [Thu, 19 Apr 2012 18:06:30 +0000 (11:06 -0700)]
model: implement get_last_conflict()

This performs a non-optimized check; that is, it uses a simple O(n) linear
search, when it could utilize O(1) lookups instead... but this isn't even the
full memory model yet, so I'm not working for perfection!

11 years agomodel: flesh out set_backtracking()
Brian Norris [Thu, 19 Apr 2012 18:02:48 +0000 (11:02 -0700)]
model: flesh out set_backtracking()

Relies on stub get_last_conflict() function.

Note: so far, implementing based on seq_cst model, not the full memory model...

11 years agomodel: flesh out check_current_action()
Brian Norris [Thu, 19 Apr 2012 18:00:55 +0000 (11:00 -0700)]
model: flesh out check_current_action()

Relies on a stub set_backtracking() function.

11 years agomodel: add accessors for ModelAction variables
Brian Norris [Thu, 19 Apr 2012 17:58:31 +0000 (10:58 -0700)]
model: add accessors for ModelAction variables

(+ add 'node' member, pointing to the state-space tree just before the action)

11 years agotree: bugfix - fix backtrack status
Brian Norris [Thu, 19 Apr 2012 17:47:11 +0000 (10:47 -0700)]
tree: bugfix - fix backtrack status

11 years agotree: don't use 'NULL' for a thread ID
Brian Norris [Thu, 19 Apr 2012 07:10:17 +0000 (00:10 -0700)]
tree: don't use 'NULL' for a thread ID

12 years agolibthreads: only record 'final' even for thrd_join
Brian Norris [Wed, 18 Apr 2012 19:36:58 +0000 (12:36 -0700)]
libthreads: only record 'final' even for thrd_join

12 years agomodel: use TreeNode()
Brian Norris [Wed, 18 Apr 2012 01:23:25 +0000 (18:23 -0700)]
model: use TreeNode()

Very basic initialization...

12 years agotree: fix invalid free
Brian Norris [Wed, 18 Apr 2012 01:23:09 +0000 (18:23 -0700)]
tree: fix invalid free

12 years agotree: add class TreeNode
Brian Norris [Wed, 18 Apr 2012 00:50:29 +0000 (17:50 -0700)]
tree: add class TreeNode

Untested, but ported from Nachos project.

12 years agorename threads_internal.h -> threads.h
Brian Norris [Tue, 17 Apr 2012 23:40:23 +0000 (16:40 -0700)]
rename threads_internal.h -> threads.h

12 years agothreads/model: move switch_to_master from class Thread to class ModelChecker
Brian Norris [Tue, 17 Apr 2012 22:46:11 +0000 (15:46 -0700)]
threads/model: move switch_to_master from class Thread to class ModelChecker

12 years agorename binary: libthreads -> model
Brian Norris [Mon, 16 Apr 2012 06:20:44 +0000 (23:20 -0700)]
rename binary: libthreads -> model

12 years agolibthreads: split into libthreads and threads
Brian Norris [Mon, 16 Apr 2012 06:15:24 +0000 (23:15 -0700)]
libthreads: split into libthreads and threads

For user-program vs. internal usage

12 years agomajor rewrite - 'struct thread' replaced with internal 'class Thread'
Brian Norris [Mon, 16 Apr 2012 06:01:24 +0000 (23:01 -0700)]
major rewrite - 'struct thread' replaced with internal 'class Thread'

Rewrite code such that most thread data is kept internally, not within the user
program.

12 years agoMakefile: add debug compilation flag
Brian Norris [Mon, 16 Apr 2012 05:32:55 +0000 (22:32 -0700)]
Makefile: add debug compilation flag

12 years agoscheduler: kill 'replaceable' scheduler
Brian Norris [Tue, 10 Apr 2012 23:26:26 +0000 (16:26 -0700)]
scheduler: kill 'replaceable' scheduler

I don't actually need a replaceable scheduler; I need a scheduler that can
switch policies at will. Just remove this level of abstraction for now (it can
be added later if needed).

12 years agolibthreads: print out trace at end of execution
Brian Norris [Tue, 10 Apr 2012 22:51:33 +0000 (15:51 -0700)]
libthreads: print out trace at end of execution

12 years agomodel: add print_trace() function
Brian Norris [Tue, 10 Apr 2012 22:51:05 +0000 (15:51 -0700)]
model: add print_trace() function

Prints out the current program trace.

12 years agolibthreads: perform 'model checking' when moving to next thread
Brian Norris [Tue, 10 Apr 2012 22:25:34 +0000 (15:25 -0700)]
libthreads: perform 'model checking' when moving to next thread

Simply use the hollow 'check_current_action()' interface to perform model
checking in the thread_system_next() call.

Right now, this just adds the previous (a.k.a. 'current') action to our log.

12 years agouserprog: use both atomic loads and stores
Brian Norris [Tue, 10 Apr 2012 22:19:29 +0000 (15:19 -0700)]
userprog: use both atomic loads and stores

(Meaningless change to 'user' program; just for testing purposes)

12 years agomodel: add check_current_action() function
Brian Norris [Tue, 10 Apr 2012 22:14:45 +0000 (15:14 -0700)]
model: add check_current_action() function

This interface provides a wrapper for all our model checking operations on the
current action (at least, ideally this should work...I might need to work on
this a bit).

For now, we just record the program trace of all atomic/thread actions.

12 years agolibthreads: thread_join: return 'int' as status
Brian Norris [Tue, 10 Apr 2012 22:08:23 +0000 (15:08 -0700)]
libthreads: thread_join: return 'int' as status

12 years agothreads_internal: pass the current 'action' to the internal thread system
Brian Norris [Tue, 10 Apr 2012 22:00:13 +0000 (15:00 -0700)]
threads_internal: pass the current 'action' to the internal thread system

I build a ModelAction object to represent the properties of the current action
that are relevant to the model checker. This action should be passed from the
basic action (atomic_load, atomic_store, thread_yield, etc.) into our thread
library and eventually to the model checker.

I don't use these actions yet, but they will be shortly.

12 years agomodel: add class ModelAction
Brian Norris [Tue, 10 Apr 2012 21:51:30 +0000 (14:51 -0700)]
model: add class ModelAction

Represents a single action (sometimes called transition) in our program. This
can be a THREAD_* event (creation, join, etc.) or a relevant read/write
operation (e.g., atomic reads/writes). This object and interface is subject to
change a little...

12 years agothreads_internal: add 'thread_switch_to_master()' internally
Brian Norris [Tue, 10 Apr 2012 21:09:42 +0000 (14:09 -0700)]
threads_internal: add 'thread_switch_to_master()' internally

In progress: moving more model-checking/thread actions so that they are
performed only by a system thread, not by the user code.

For now, we replace our uses of thread_yield() (which simply switched to the
next user thread) while thread_switch_to_master() (which will later perform
intermediate actions before choosing the next user thread).

Also, we can begin creating internal and external interfaces in
threads_indernal.h and libthreads.h, respectively.

12 years agolibthreads: make typedef for 'thread_id_t'
Brian Norris [Thu, 15 Mar 2012 22:42:36 +0000 (15:42 -0700)]
libthreads: make typedef for 'thread_id_t'

Just in case we need to change it later on, let's use it as a named type.

12 years agouse my{Malloc,Free} in model-checking code
Brian Norris [Thu, 5 Apr 2012 03:14:27 +0000 (20:14 -0700)]
use my{Malloc,Free} in model-checking code

Also, fixes 'leak' where we forgot to free the main_thread.

12 years agomalloc: override 'new' and 'delete' globally
Brian Norris [Thu, 5 Apr 2012 02:41:46 +0000 (19:41 -0700)]
malloc: override 'new' and 'delete' globally

Not sure if this is correct...

Q: do we also need to overload new[] and delete[]?

12 years agomalloc: add myMalloc() and myFree()
Brian Norris [Thu, 5 Apr 2012 02:35:41 +0000 (19:35 -0700)]
malloc: add myMalloc() and myFree()

12 years agocommon: rename "CONFIG" to "COMMON"
Brian Norris [Thu, 5 Apr 2012 02:12:19 +0000 (19:12 -0700)]
common: rename "CONFIG" to "COMMON"

12 years agoschedule: use STL 'queue' instead of 'list'
Brian Norris [Thu, 15 Mar 2012 18:12:44 +0000 (11:12 -0700)]
schedule: use STL 'queue' instead of 'list'

12 years agoremove unnecessary #includes
Brian Norris [Thu, 15 Mar 2012 06:01:27 +0000 (23:01 -0700)]
remove unnecessary #includes

12 years agoschedule: make 'current' a private member of the scheduler
Brian Norris [Thu, 15 Mar 2012 05:56:30 +0000 (22:56 -0700)]
schedule: make 'current' a private member of the scheduler

12 years agoschedule: use STL list class instead of custom queue
Brian Norris [Thu, 15 Mar 2012 05:52:42 +0000 (22:52 -0700)]
schedule: use STL list class instead of custom queue

12 years agorename other *.c to *.cc
Brian Norris [Wed, 14 Mar 2012 22:59:49 +0000 (15:59 -0700)]
rename other *.c to *.cc

userprog.c remains for now...

12 years agoschedule: move schedule.c --> schedule.cc
Brian Norris [Wed, 14 Mar 2012 22:56:56 +0000 (15:56 -0700)]
schedule: move schedule.c --> schedule.cc

12 years agoschedule: create 'class Scheduler' with implementation 'class DefaultScheduler'
Brian Norris [Wed, 14 Mar 2012 22:54:36 +0000 (15:54 -0700)]
schedule: create 'class Scheduler' with implementation 'class DefaultScheduler'

12 years agolibthreads: delete allocated object
Brian Norris [Wed, 14 Mar 2012 22:10:31 +0000 (15:10 -0700)]
libthreads: delete allocated object

12 years agomodel: use 'this' uniformly
Brian Norris [Wed, 14 Mar 2012 22:08:25 +0000 (15:08 -0700)]
model: use 'this' uniformly

12 years agomodel: move model.c --> model.cc
Brian Norris [Wed, 14 Mar 2012 22:07:04 +0000 (15:07 -0700)]
model: move model.c --> model.cc

12 years agomodel: change 'struct model_checker' to 'class ModelChecker'
Brian Norris [Wed, 14 Mar 2012 22:05:54 +0000 (15:05 -0700)]
model: change 'struct model_checker' to 'class ModelChecker'

12 years agoMakefile: switch to C++ builds
Brian Norris [Wed, 14 Mar 2012 22:00:46 +0000 (15:00 -0700)]
Makefile: switch to C++ builds

12 years agostricter typing of function pointers for makecontext()
Brian Norris [Tue, 13 Mar 2012 18:37:45 +0000 (11:37 -0700)]
stricter typing of function pointers for makecontext()

We need to use functions with no arguments (i.e., 'void (*)()') in order to
retain strict type-checking with makecontext(). Of course, we still circumvent
this type checking with casting, but we should straighten this out sometime...

12 years agoC++: don't use C++ keywords as names (this, new, etc.)
Brian Norris [Tue, 13 Mar 2012 18:35:55 +0000 (11:35 -0700)]
C++: don't use C++ keywords as names (this, new, etc.)

12 years agoC++: cast result of malloc
Brian Norris [Tue, 13 Mar 2012 18:35:09 +0000 (11:35 -0700)]
C++: cast result of malloc

12 years agoterminology - use 'thread id' instead of 'thread index'
Brian Norris [Tue, 13 Mar 2012 06:10:26 +0000 (23:10 -0700)]
terminology - use 'thread id' instead of 'thread index'

12 years agolibthreads: use model-checker's thread ID assignment
Brian Norris [Tue, 13 Mar 2012 06:08:12 +0000 (23:08 -0700)]
libthreads: use model-checker's thread ID assignment

12 years agomodel: add thread ID assignment function
Brian Norris [Tue, 13 Mar 2012 06:07:47 +0000 (23:07 -0700)]
model: add thread ID assignment function

12 years agolibthreads: separate private functions from user interface
Brian Norris [Tue, 13 Mar 2012 05:28:14 +0000 (22:28 -0700)]
libthreads: separate private functions from user interface

12 years agolibthreads: perform all scheduling/model-checking from master thread
Brian Norris [Tue, 13 Mar 2012 03:51:25 +0000 (20:51 -0700)]
libthreads: perform all scheduling/model-checking from master thread

To keep all user-space actions under control, we should perform all scheduling
and model-checking from the main system thread. This pushes some of the
thread_yield() logic to a system function (as desired).

12 years agolibthreads: add THREAD_* states
Brian Norris [Tue, 13 Mar 2012 03:38:18 +0000 (20:38 -0700)]
libthreads: add THREAD_* states

12 years agoschedule: exit if we run out of linked-list nodes
Brian Norris [Mon, 12 Mar 2012 23:52:04 +0000 (16:52 -0700)]
schedule: exit if we run out of linked-list nodes

12 years agomodel: move 'main_thread' to model_checker struct
Brian Norris [Mon, 12 Mar 2012 23:14:11 +0000 (16:14 -0700)]
model: move 'main_thread' to model_checker struct

12 years agomove 'current thread' details
Brian Norris [Mon, 12 Mar 2012 23:06:14 +0000 (16:06 -0700)]
move 'current thread' details

The low level details regarding the 'current thread' should be encapsulated in
the scheduler (i.e., 'get_current_thread()'). So we move the 'current' variable
to scheduler.c.

12 years agolibthreads: utilize new model_checker framework
Brian Norris [Mon, 12 Mar 2012 22:52:44 +0000 (15:52 -0700)]
libthreads: utilize new model_checker framework

Just a simple drop-in of the current FCFS scheduler (with the ability to
generically switch out schedulers).

12 years agomodel: add global model_checker initialization
Brian Norris [Mon, 12 Mar 2012 22:51:56 +0000 (15:51 -0700)]
model: add global model_checker initialization