model: refactor "infeasible" printing

print less stuff

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]

cyclegraph: bugfix - graph reachability was reversed

[Split from Brian Demsky's commit]

cyclegraph: add destructor, use 'const' appropriately

[Split from Brian Demsky's larger commit]

nodestack: document pop_restofstack()

Add basic reads from support

Now we need to use the cyclegraph to eliminate bad executions...

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.

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().

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.

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

remove dead code...  loop entrance condition is i<backtrack.size().  Therefore,
this branch can never be taken.  remove it as it is confusing.

action: fix uint64_t printf warning

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

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

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

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.

model: remove unused #include

libthreads: thrd_join() always return 0

According to the spec, thrd_join() should return the return code from the
joining thread function. But for now, I implement the function type
(thrd_start_t, from C11) as returning void, not int. So just return 0 always.

model: add documentation

model: fixup "initialized" check in build_reads_from_past()

Some... (TODO: finish message here)

model: only include the most recent seq_cst write in may_read_from

model: add ModelChecker::get_last_seq_cst()

Add a function to get the last memory_order_seq_cst action (in the total global
sequence) performed on a particular object (i.e., memory location). Will be
used for build_reads_from_past().

model: improve ModelChecker::get_last_conflict() search

Use the recently-added 'obj_map' to isolate a list of actions on only the
current object (memory location). That way, we don't have to iterate through as
much noise in our lists.

model: add per-object action lists (obj_map)

This object list will map objects (i.e., memory locations) to traces of all
actions performed on the respective objects. This will be used for some seq_cst
and backtracking-conflict computations to reduce the space we have to search.

reformat some doxygen comments, remove newlines

Avoiding newlines between a comment and its function header makes it more
obvious which function the comment belongs to.

model: rearrange switch block, handle RMW

This switch block shouldn't have to be updated for every new action_type_t.
Rewrite so that we only have to worry about significant actions, like
ATOMIC_{READ,WRITE,RMW}.

Merge branch 'master' into brian

model: bugfix - resize thrd_last_action when adding objects

Apparently, STL vectors don't resize automatically, nor do they warn or print
errors when you access them out-of-bounds...

model: factor out 'tid' calculation

main: make function static

action / threads: add THREAD_START action at start of each thread

The datarace code needs every thread to have at least one action in it, so that
the action has a valid non-zero clock.

threads: use constructor initializer list

action: add 'reads_from' member variable

Just printed out for now, but the 'reads_from' parameter might be used more
later.

action: remove unused ModelAction::set_value()

model: release/acquire synchronization

I forgot that I had already written the ModelAction::reads_from() code, and it
was just waiting to be hooked up :)

Anyway, I haven't really tested all the synchronization yet...

clockvector: add 'const', fix comments in ClockVector::merge()

remove EOL spaces, fix indentation

bug

documentation

fix bug
get rid of annoying compiler warning

hook up the race detector...

Merge branch 'datarace'

datarace: fix build error

changes

libatomic: atomic_load() - use proper reads_from value

Finally utilize a return value from the model-checker, instead of
storing/retrieving a sequentially-consistent value in obj->value.

model: set reads_from "return value" in model-checker

Previously, values (let alone the reads-from relationship) were not actually
returned from the model-checker to the user. This step sets up the return value
so that the user context can retrieve it rather than using a value stuck in the
snapshotting memory.

There are still several TODOs along with the reads-from relationship, but this
code is stable enough for providing a basis for further work.

nodestack: add stub 'get_next_read_from()' function

This is the start of providing functional model-checking reads-from
relationships. It is a stub because it doesn't properly handle "backtracking"
and replay for reads-from assignments. It will simply return the first element
in may_read_from.

document some enumerated types

model: detect uninitialized atomic reads

nodestack: add print_may_read_from()

model: improve build_reads_from_past() comment

action: use constructor initializer list

action: support ATOMIC_INIT

For now, atomic_init() will be supported as simply a relaxed write. This
doesn't quite match the spec exactly [1, 2], but it is expedient for supporting
the common case of checking proper initialization.

[1] From C++ N3242, Section 29.6.5, Statement 8:

       Non-atomically initializes *object with value desired.

       Note: Concurrent access from another thread, even via an atomic
       operation, constitutes a data race.

[2] Note that for now, my implementation will not flag concurrent atomic_init()
    and atomic_store() as data races.

threads: add per-thread "return" values for 'model-checking/user context' switch

The model-checker needs to return a value to the user context when performing
atomic loads, for instance. I will be implementing this by caching the return
value on a per-thread basis. This is because an atomic_load() might result in a
context switch before actually returning the value.

These functions are not yet used.

nodestack: build 'may_read_from' out of constant ModelActions

Make the 'may_read_from' set include only constant pointers.

nodestack: action_set_t: replace STL 'set' with 'list'

trivial changes

* remove unnecessary 'class' keyword
* add ASSERT() in the 'thread_current()' function
* move #include into .cc file
* remove more end-of-line spaces

add more const qualifiers

model: make set_current_action() private

It's only used within ModelChecker...

datarace: factor subtle clock-vector logic into a reusable function

These comparisons are performed many times throughout datarace.cc, featuring a
lot of code duplication without strong documentation. This factors the
duplicated code into a single function and documents that single function more
clearly.

Brian Demsky: please review this fix (it should make no actual logical change)
and take a look at the TODO I have inserted; I'm not sure if the TODO is
warranted.

datarace: remove EOL spaces

datarace/clockvector: switch 'clocks' to use 'unsigned int' (modelclock_t)

clock: add modelclock_t typedef, use 'unsigned int'

Clocks should be unsigned and documented as their own 'modelclock_t' type.

add forgetten file

add support for datarace detection...

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

Merge branch 'brian'

Adding relevant comments for fork based implementation.

Makefile: compile *.cc separately

This Makefile rule doesn't have to include all *.cc files at once. They can be
compiled separately.

Note that this slows down compilation slightly, but it also allows better
parallel (jobserver) compilation; for example, you can use `make -j4' to
perform separate compilations using 4 different threads, utilizing a multi-core
system more effectively.

nodestack: revert may_read_from to a normal member variable, not pointer

Because we don't control the 'new' operator for STL sets, I can't properly
ensure that it is allocated in non-snapshotting memory. So just make
may_read_from a normal member variable within class Node, so that its
initial 'allocation' is performed as part of the instantiation of its
subsuming Node object.

action: add {get,set}_value(), assign default value

add documentation

nodestack: only create may_read_from sets for read operations

nodestack: re-associate ModelAction/Node relationship

Currently, the Node that is returned by ModelAction::get_node() actually
represents the Node that is parent to the ModelAction. This works well for
some of the backtracking computations (since the backtracking set is held
in the parent Node), but it creates confusion when performing computations
such as the following:

 Node *node;
 ...
 ModelAction *act = node->get_action();
 Node *node2 = act->get_parent();

 ASSERT(node == node2); // Fails
 ASSERT(node->get_parent() == node2); // Succeeds

So this patch changes this behavior so that the first assertion (above)
succeeds and the second one fails. This is probably more desirable in the
long run.

nodestack: add Node::get_parent() function

As I add more complicated backtracking and may-read-from relationships,
each Node might need some structural information to be able to reach its
parent Node.

To support this:
* the NodeStack should provide the parent information via Node constructor
* the Node should provide a get_parent() method

model: make print_list() into a static C function

This function does not need to be a class member function. It only performs
a standard 'printing' option on a STL list of ModelAction objects.

Adding relevant comments for fork based implementation.

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

model: make comment more accurate

add_action_to_lists() does not only work on the per-object, per-thread action
list. It performs several pieces of bookkeeping.

action: add const qualifier

clockvector: add const qualifiers

clockvector: add documentation

Merge branch 'sandbox' (remove finalize())

Merge in the fix from Subramanian and me that eliminates the need for a
finalize() call. It was a kind of bug, in a way, that hopefully is fixed now...

snapshot: switch back to mprotect-based snapshotting

Subramanian accidentally switched this configuration macro in his last
commit...

model: build up 'may_read_from' set

Finally wire up the model-checker so that it builds the may_read_from set
for every 'read' action. I think this is working OK, although I don't have
much to really test it on yet.

Also, improve comments to describe the process in check_current_action().

model: add build_reads_from_past() function

Add function that will build up the initial set of all past writes that a
'read' action may read from.

action: add happens_before() function

Now I can easily compare two ModelActions with the happens_before()
relationship. Of course, the clock vectors are not fully complete yet, but
this sets the stage...

clockvector: fix 'happens_before', change name to 'synchronized_since'

First, the 'happens_before' function needed to use an inclusive 'less-than'
(i.e., <=) instead of 'strictly less-than' (i.e., <) in order to fit with
most of the algorithm.

Second, the association of 'happens_before' directly with the ClockVector is
not very intuitive to use. I will write an additional happens_before()
function that can easily compare two ModelAction objects. So change this
happens_before() (with it awkward usage) to be called synchronized_since(),
representing whether the ClockVector's thread has previously synchronized
with the ModelAction's thread.

action: add 'get_cv()' accessor function

nodestack: add 'may_read_from' set

Each Node (at least, each Node that is a 'read') will be associated with a
may_read_from set - the set of all possible ModelActions to read from. For now,
this interface handles only actions that exist in the past. It won't properly
retain information from future actions.

nodestack: don't perform linear search to check if backtrack is empty

Add a simple add/remove counter to record when threads are 'added' and
'removed' from the backtracking set.

action: add const qualifiers

action: replace condition check with ASSERT()

Now that the ModelChecker and NodeStack have been refactored a bit, I don't
need to rely on create_cv() to avoid overwriting a previously-existing
clockvector; create_cv() will now be called at most once per ModelAction. So
change this condition to an ASSERT().

nodestack/model: refactor explore_action(), change return semantics

ModelChecker would like to know when a new ModelAction is being inserted
into the NodeStack vs. when the new ModelAction should be discarded in
favor of a pre-existing one (due to replay). So I change the semantics of
NodeStack::explore_action() such that it does not always return a
ModelAction; now it returns NULL if the ModelAction was accepted into the
NodeStack, otherwise returning the ModelAction that was already in the
stack.

Now, ModelChecker can choose when to create new clock vectors as well as
other operations (to come) that may be performed only upon *first*
exploration of a new ModelAction.

Additionally, ModelChecker is now responsible for free-ing the ModelAction
if it is not going to be kept in NodeStack.

There should be no change in functionality.

nodestack: more documentation

cyclegraph: make this compile...

You need 'inttypes' for 'uintptr_t'

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker

builds

add hashtable