model: stash actions for lazy release-seq checking

Build up lists of actions to lazily check for new release sequence
developments.

model: report 'updates' when adding mo_graph edges

The rest of the model checker would like to know if any edges were added. Add a
boolean return value to report this.

model: report status of resolved promises

The rest of the model checker needs to know when promises are added, so add a
return status as a boolean.

action, clockvector: add 'has_synchronized_with()' functions

These functions will check whether a ClockVector (or corresponding ModelAction)
is *completely* synchronized with another already. This is different from
simply "happens before," because I may need to update and propagate a clock
vector after initial execution as more information becomes available, and so
this function helps determine whether a particular pair of vectors is worth
merging (and then - expensively - propagating) before actually performing the
synchronization.

[Not documented properly yet...]

action: make synchronize_with() public

action: utilize release sequence(s) for synchronization

Instead of checking only the trivial release sequence (i.e., a read-acquire
reads directly from a write-release) for establishing synchronization, make use
of the ModelChecker's more complete 'get_release_seq_head()' functionality,
then loop through all release heads and synchronize with each. This is
necessary because a read-acquire may synchronize with more than one
store-release.

Note that this step only implements support based on present knowledge. The
incomplete knowledge of the modification order, as given in mo_graph, as well
as "reading from the future" may require lazy checking.

model: add release sequence support

The ModelChecker now can find the head(s) of the release sequence(s) with which
a particular ModelAction (read-acquire) will synchronize.

The ModelChecker::release_seq_head function can locate a release sequence head
for a given ModelAction, based on information at a given moment. That is, it
knows happens-before and modification information for the present, but some
decisions may need to be made in the future as reads-from promises are
fulfilled or modification ordering is observed by future reads and writes.

Lazy checking for the latter cases has yet to be implemented.

model: change pointer spacing style

action: (assertion) disallow out-of-order synchronization

We build our ModelChecker around the assumption that synchronization never
occurs counter to the execution order. This assertion lets us know if that
fails.

model: improve some promise-related comments

action: update 'reads_from' field before synchronization

As the ModelChecker's release/acquire functionality gets more complex,
it makes more sense to assign the ModelAction::reads_from field before
checking synchronization. Currently, this makes no change in behavior.

nodestack: turn magic promise numbers into enum + typedef

Document the enum properly, since it's quite unclear what these flags really
mean.

nodestack, model: use uniform spacing, style

nodestack: don't use uint32_t

uint32_t (and similar) should only be used when an exact field-size is needed
across platforms with different integer sizes. In this case, we only need an
unsigned type, so just use unsigned int.

nodestack: remove unnecessary typedefs

These typedefs are used once or twice and don't add much meaning.

cyclegraph: add public CycleGraph::checkReachable()

The private CycleGraph::checkReachable() function can be useful externally,
when provided with two ModelActions. This implements a small wrapper for public
usage.

model: correct mo_graph comment

My understanding of the mo_graph was incorrect, due to some confusion over the
CycleGraph interfaces. Correct this.

cyclegraph: straighten out header vs. implementation vs. usage

The CycleGraph::addEdge and CycleGraph::addRMWEdge functions were a little
confusing to use, since their implementation and header prototypes had
different parameter naming. This swapped the 'to' and 'from' naming, such that
it appeared as if the addEdge() users were adding edges in the reverse
direction. The functionality was not actually incorrect, but my understanding
was...

This corrects the naming and switches the order of the arguments.

promise: rewrite into a simpler header file

Makefile: rewrite header dependencies

We shouldn't need to add new files in 3 different places. Automatically
generate most of this using GCC's '-MM' option.

model: document ModelChecker::mo_graph

The modification order graph is a complex data structure, and there are a few
pieces of high-level information that should be noted. For example, the edges
are actually directed from most recent to oldest, which is somewhat in reverse
of the usage in the literature, where

  a --mo--> b

means that a comes *before* b in the modification order. This convention can be
changed in the future, but it should be documented here.

model: rename 'cyclegraph' to 'mo_graph'

This is not just an arbitrary graph with cycle-detection; it is specifically a
representation of the modification order of various atomic objects.

model: don't "leak" promises

test/Makefile: remove pointless variable

.gitignore: don't ignore /model anymore

We don't produce an executable named 'model' anymore.

Merge branch 'norris'

schedule: make print() const

Switch to using a "const_iterator" so that the whole function becomes const.

model: privatize check_current_action()

threads: correct 'swap()' documentation

Some of the swap() documentation was duplicated incorrectly. While I'm at it,
make the descriptions more clear and precise.

main, model: don't 'initialize' system_context

I was unnecessarily giving main.cc control of the system_context variable,
since I thought I needed to use getcontext() before entering the model checker.
However, the structure of the runtime scheduling is such that this
"initialization" would be obliterated by the first swapcontext() call
(switching form system-context to user-context).

So, the point is that the model-checker can just declare its own
("uninitialized") context that will be initialized as soon as the model-checker
makes a thread swap. Thus, I remove the external interface for initializing the
context (set_system_context()).

action: don't merge twice in read_from()

synchronize_with() already takes care of the clock vector merging, so don't
merge a second time.

action: rework/rename 'synchronized()' to 'synchronize_with()'

Fix some comments, names, etc.

Privatize synchronized()/synchronize_with(), since it's only intended for
within other wrapper actions performed on ModelAction.

model: remove useless return code from add_thread()

schedule, threads: update comments, const's

model: make scheduler private

To accomplish this, I needed to add one accessor method for
'get_current_thread()'.

main, model: move main execution loop into ModelChecker class

cyclegraph: improve comments, use initializer list

hashtable: document get_safe_ptr()

hashtable: rename ensureptr() to get_safe_ptr()

ensureptr() is kind of vague. This rename -- along with some better description
-- will help clarify what this function does.

hashtable: bugfix - increment size only when new bins are linked

In both put() and ensureptr(), the 'size' counter should not be incremented
until we decide if we're adding a new bin or not. When incremented improperly,
'size' ended up out of sync with the hash table; it reported a size much larger
than the actual table.

hashtable: some refactoring, signed-ness

Since 'capacity' is unsigned, so should the index that compares with it.

The (duplicated) compare/resize code can be a bit shorter and (IMO) easier to
read.

model: reformat/refactor some code

impatomic.h: fixup spacing

Tabs vs. spaces for indentation screws up this indentation, making it even
harder to read than it should be. Switch this all to spaces (for uniformity
across all editor configurations) and align things properly.

threads: trivial change

model: revert unnecessary parameter for print_summary()

CycleGraph::checkForCycles() is a cheap function; it only checks a flag status.
So we don't need to make code more complicated just to avoid calling this
function.

Effectively a revert of:
commit 7cee72d776ddfbf585038f3cad3df799e353cc11

add basic parameter handling

common: add error_msg() function

run.sh: pass command-line arguments through to test program

Once the model-checker begins handling arguments, we should pass through
arguments to the program.

.gitignore: ignore other vim swap file type

model: reformat some code

main, threads: improve comments regarding thread stepping

The comment in thread_system_next was incorrect:
"Returns the 1 if there is another step and 0 otherwise."

Add a few comments throughout to help clarify this behavior.

add a todo flag to a comment so it won't get lost... low priority item though

Makefile: fix config.h dependencies

The snapshotting code needs to be rebuilt when config.h is modified.

Merge branch 'brian'

DEBUGGINGNOTES: include gdb info for Linux

bug fix

run.sh: fixup run script

run.sh will, by default, run ./test/userprog.o now. This can be modified later
to provide several regression tests in-tree, with scripted execution of the
tests.

Makefile: wire up test/ directory for compilation

Makefile: split part into a common makefile (common.mk)

userprog: move to 'test/' directory

Makefile: don't build userprog.c from top level

(Temporarily disables userprog compilation; will restore soon)

blank lines, spacing, etc.

nodestack: remove completed @todo

nodestack: clean up comments

model: do not call isfinalfeasible() too many times

This function call incurs graph exploration, so when performing some
end-of-trace bookkeeping, we should only call it once and cache the result.

hashtable: add some documentation

model: delete Threads on destruction

When switching from STL map to hashtable, the Thread destruction was just
commented out instead of reimplemented. This is a good enough version, I think.

more reformatting/indentation

forgot about events that happen after an unresolved read...  bug fix checked in

fixup whitespace

action: add memory_order printing

change test case to match nice one from spec...  it works.  :)

bugs...

add some comments

standardize names a little

okay...known bugs for my trivial test are out of send future values backwards

finish promise support

more changes towards keeping track of promises resolved by a given write statement

changes

some changes towards reading from future writes

move more configurables and add documentation

more hashtable fixes

clean up memory allocation code a bit

fix some allocation/free bugs when we put non objects into table...

fix my todo comments so they appear in documentation

switch everything over to our own hashtable

give us a calloc to use from our code

hashtable: make more flexible

[Split by Brian Norris]

Add documentation

[Split by Brian Norris]

action: fix ATOMIC_RMW comments

rmw example works

towards making rmw work...

[Split by Brian Norris]

action: add stub ATOMIC_RMWR and ATOMIC_RMWC

trivial - whitespace, debugging cleanup, etc.

remove libatomic

action: switch from "libatomic" to C++-spec "memory_order_*" macros

pull in most of atomic header file

don't forget this file

split these defs out of other stuff

switch rest over to model checker...  might work now

fix missing atomic...

rewrite macros