.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

import header file from specification

taken from n2427.html

update TODO's

Add RMW support to core.

Eliminate annoying warning.

model: add documentation

[Split from Brian Demsky's work]

small changes (things still work) towards support RMW

Reserve value field only for writes. Using it for reads will only make thinks
weird for RMW operations.

[Amended by Brian Norris]

trying to get fork based snapshotting to work

[Amended by Brian Norris,
 includes some later clean up]

toss a place for useful information

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.