Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-priv
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 8 Oct 2013 17:11:19 +0000 (10:11 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 8 Oct 2013 17:11:19 +0000 (10:11 -0700)
112 files changed:
.dir-locals.el [new file with mode: 0644]
.gitignore [new file with mode: 0644]
DEBUGGINGNOTES.txt [new file with mode: 0644]
Doxyfile [new file with mode: 0644]
LICENSE [new file with mode: 0644]
Makefile [new file with mode: 0644]
README.md [new file with mode: 0644]
action.cc [new file with mode: 0644]
action.h [new file with mode: 0644]
bugmessage.h [new file with mode: 0644]
clockvector.cc [new file with mode: 0644]
clockvector.h [new file with mode: 0644]
cmodelint.cc [new file with mode: 0644]
common.cc [new file with mode: 0644]
common.h [new file with mode: 0644]
common.mk [new file with mode: 0644]
conditionvariable.cc [new file with mode: 0644]
config.h [new file with mode: 0644]
context.cc [new file with mode: 0644]
context.h [new file with mode: 0644]
cyclegraph.cc [new file with mode: 0644]
cyclegraph.h [new file with mode: 0644]
datarace.cc [new file with mode: 0644]
datarace.h [new file with mode: 0644]
doc/Markdown/License.text [new file with mode: 0644]
doc/Markdown/Markdown Readme.text [new file with mode: 0644]
doc/Markdown/Markdown.pl [new file with mode: 0755]
doc/notes/fence.txt [new file with mode: 0644]
doc/notes/release-sequence.txt [new file with mode: 0644]
execution.cc [new file with mode: 0644]
execution.h [new file with mode: 0644]
hashtable.h [new file with mode: 0644]
impatomic.cc [new file with mode: 0644]
include/atomic [new file with mode: 0644]
include/cdsannotate.h [new file with mode: 0644]
include/cmodelint.h [new file with mode: 0644]
include/condition_variable [new file with mode: 0644]
include/cstdatomic [new file with mode: 0644]
include/impatomic.h [new file with mode: 0644]
include/librace.h [new file with mode: 0644]
include/memoryorder.h [new file with mode: 0644]
include/model-assert.h [new file with mode: 0644]
include/modeltypes.h [new file with mode: 0644]
include/mutex [new file with mode: 0644]
include/stdatomic.h [new file with mode: 0644]
include/threads.h [new file with mode: 0644]
libannotate.cc [new file with mode: 0644]
librace.cc [new file with mode: 0644]
libthreads.cc [new file with mode: 0644]
main.cc [new file with mode: 0644]
mainpage.dox [new file with mode: 0644]
malloc.c [new file with mode: 0644]
model.cc [new file with mode: 0644]
model.h [new file with mode: 0644]
mutex.cc [new file with mode: 0644]
mymemory.cc [new file with mode: 0644]
mymemory.h [new file with mode: 0644]
nodestack.cc [new file with mode: 0644]
nodestack.h [new file with mode: 0644]
output.h [new file with mode: 0644]
params.h [new file with mode: 0644]
plugins.cc [new file with mode: 0644]
plugins.h [new file with mode: 0644]
promise.cc [new file with mode: 0644]
promise.h [new file with mode: 0644]
run.sh [new file with mode: 0755]
scanalysis.cc [new file with mode: 0644]
scanalysis.h [new file with mode: 0644]
schedule.cc [new file with mode: 0644]
schedule.h [new file with mode: 0644]
snapshot-interface.cc [new file with mode: 0644]
snapshot-interface.h [new file with mode: 0644]
snapshot.cc [new file with mode: 0644]
snapshot.h [new file with mode: 0644]
stacktrace.h [new file with mode: 0644]
stl-model.h [new file with mode: 0644]
test/Makefile [new file with mode: 0644]
test/addr-satcycle.cc [new file with mode: 0644]
test/condvar.cc [new file with mode: 0644]
test/csetest.c [new file with mode: 0644]
test/deadlock.cc [new file with mode: 0644]
test/double-read-fv.c [new file with mode: 0755]
test/double-relseq.c [new file with mode: 0644]
test/fences.c [new file with mode: 0644]
test/fences2.c [new file with mode: 0644]
test/insanesync.cc [new file with mode: 0644]
test/linuxrwlocks.c [new file with mode: 0644]
test/linuxrwlocksyield.c [new file with mode: 0644]
test/litmus/Makefile [new file with mode: 0644]
test/litmus/iriw.cc [new file with mode: 0644]
test/litmus/load-buffer.cc [new file with mode: 0644]
test/litmus/message-passing.cc [new file with mode: 0644]
test/litmus/seq-lock.cc [new file with mode: 0644]
test/litmus/store-buffer.cc [new file with mode: 0644]
test/litmus/wrc.cc [new file with mode: 0644]
test/mo-satcycle.cc [new file with mode: 0644]
test/mutextest.cc [new file with mode: 0644]
test/nestedpromise.c [new file with mode: 0644]
test/pending-release.c [new file with mode: 0644]
test/releaseseq.c [new file with mode: 0644]
test/rmw2prog.c [new file with mode: 0644]
test/rmwprog.c [new file with mode: 0644]
test/sctest.c [new file with mode: 0644]
test/thinair.c [new file with mode: 0644]
test/uninit.cc [new file with mode: 0644]
test/userprog.c [new file with mode: 0644]
test/wrc.c [new file with mode: 0644]
test/wrcs.c [new file with mode: 0644]
threads-model.h [new file with mode: 0644]
threads.cc [new file with mode: 0644]
traceanalysis.h [new file with mode: 0644]
workqueue.h [new file with mode: 0644]

diff --git a/.dir-locals.el b/.dir-locals.el
new file mode 100644 (file)
index 0000000..ce85e5f
--- /dev/null
@@ -0,0 +1 @@
+((nil . ((indent-tabs-mode . t))))
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
new file mode 100644 (file)
index 0000000..8df9862
--- /dev/null
@@ -0,0 +1,15 @@
+# generic types
+*.o
+*.swp
+*.swo
+*.so
+*~
+*.dot
+.*.d
+*.pdf
+
+# files in this directory
+/tags
+/doc/docs
+/benchmarks
+/README.html
diff --git a/DEBUGGINGNOTES.txt b/DEBUGGINGNOTES.txt
new file mode 100644 (file)
index 0000000..70cbba6
--- /dev/null
@@ -0,0 +1,6 @@
+To run inside MacOS under gdb you need:
+set dont-handle-bad-access 1
+handle SIGBUS nostop noprint
+
+To run in Linux under gdb, use:
+handle SIGSEGV nostop noprint
diff --git a/Doxyfile b/Doxyfile
new file mode 100644 (file)
index 0000000..ed9f000
--- /dev/null
+++ b/Doxyfile
@@ -0,0 +1,1801 @@
+# Doxyfile 1.8.0
+
+# This file describes the settings to be used by the documentation system
+# doxygen (www.doxygen.org) for a project.
+#
+# All text after a hash (#) is considered a comment and will be ignored.
+# The format is:
+#       TAG = value [value, ...]
+# For lists items can also be appended using:
+#       TAG += value [value, ...]
+# Values that contain spaces should be placed between quotes (" ").
+
+#---------------------------------------------------------------------------
+# Project related configuration options
+#---------------------------------------------------------------------------
+
+# This tag specifies the encoding used for all characters in the config file
+# that follow. The default is UTF-8 which is also the encoding used for all
+# text before the first occurrence of this tag. Doxygen uses libiconv (or the
+# iconv built into libc) for the transcoding. See
+# http://www.gnu.org/software/libiconv for the list of possible encodings.
+
+DOXYFILE_ENCODING      = UTF-8
+
+# The PROJECT_NAME tag is a single word (or sequence of words) that should
+# identify the project. Note that if you do not use Doxywizard you need
+# to put quotes around the project name if it contains spaces.
+
+PROJECT_NAME           = "CDSChecker: A Model Checker for C11/C++11 Atomics"
+
+# The PROJECT_NUMBER tag can be used to enter a project or revision number.
+# This could be handy for archiving the generated documentation or
+# if some version control system is used.
+
+PROJECT_NUMBER         =
+
+# Using the PROJECT_BRIEF tag one can provide an optional one line description
+# for a project that appears at the top of each page and should give viewer
+# a quick idea about the purpose of the project. Keep the description short.
+
+PROJECT_BRIEF          =
+
+# With the PROJECT_LOGO tag one can specify an logo or icon that is
+# included in the documentation. The maximum height of the logo should not
+# exceed 55 pixels and the maximum width should not exceed 200 pixels.
+# Doxygen will copy the logo to the output directory.
+
+PROJECT_LOGO           =
+
+# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute)
+# base path where the generated documentation will be put.
+# If a relative path is entered, it will be relative to the location
+# where doxygen was started. If left blank the current directory will be used.
+
+OUTPUT_DIRECTORY       = doc
+
+# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create
+# 4096 sub-directories (in 2 levels) under the output directory of each output
+# format and will distribute the generated files over these directories.
+# Enabling this option can be useful when feeding doxygen a huge amount of
+# source files, where putting all generated files in the same directory would
+# otherwise cause performance problems for the file system.
+
+CREATE_SUBDIRS         = NO
+
+# The OUTPUT_LANGUAGE tag is used to specify the language in which all
+# documentation generated by doxygen is written. Doxygen will use this
+# information to generate all constant output in the proper language.
+# The default language is English, other supported languages are:
+# Afrikaans, Arabic, Brazilian, Catalan, Chinese, Chinese-Traditional,
+# Croatian, Czech, Danish, Dutch, Esperanto, Farsi, Finnish, French, German,
+# Greek, Hungarian, Italian, Japanese, Japanese-en (Japanese with English
+# messages), Korean, Korean-en, Lithuanian, Norwegian, Macedonian, Persian,
+# Polish, Portuguese, Romanian, Russian, Serbian, Serbian-Cyrillic, Slovak,
+# Slovene, Spanish, Swedish, Ukrainian, and Vietnamese.
+
+OUTPUT_LANGUAGE        = English
+
+# If the BRIEF_MEMBER_DESC tag is set to YES (the default) Doxygen will
+# include brief member descriptions after the members that are listed in
+# the file and class documentation (similar to JavaDoc).
+# Set to NO to disable this.
+
+BRIEF_MEMBER_DESC      = YES
+
+# If the REPEAT_BRIEF tag is set to YES (the default) Doxygen will prepend
+# the brief description of a member or function before the detailed description.
+# Note: if both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the
+# brief descriptions will be completely suppressed.
+
+REPEAT_BRIEF           = YES
+
+# This tag implements a quasi-intelligent brief description abbreviator
+# that is used to form the text in various listings. Each string
+# in this list, if found as the leading text of the brief description, will be
+# stripped from the text and the result after processing the whole list, is
+# used as the annotated text. Otherwise, the brief description is used as-is.
+# If left blank, the following values are used ("$name" is automatically
+# replaced with the name of the entity): "The $name class" "The $name widget"
+# "The $name file" "is" "provides" "specifies" "contains"
+# "represents" "a" "an" "the"
+
+ABBREVIATE_BRIEF       =
+
+# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then
+# Doxygen will generate a detailed section even if there is only a brief
+# description.
+
+ALWAYS_DETAILED_SEC    = NO
+
+# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all
+# inherited members of a class in the documentation of that class as if those
+# members were ordinary class members. Constructors, destructors and assignment
+# operators of the base classes will not be shown.
+
+INLINE_INHERITED_MEMB  = NO
+
+# If the FULL_PATH_NAMES tag is set to YES then Doxygen will prepend the full
+# path before files name in the file list and in the header files. If set
+# to NO the shortest path that makes the file name unique will be used.
+
+FULL_PATH_NAMES        = YES
+
+# If the FULL_PATH_NAMES tag is set to YES then the STRIP_FROM_PATH tag
+# can be used to strip a user-defined part of the path. Stripping is
+# only done if one of the specified strings matches the left-hand part of
+# the path. The tag can be used to show relative paths in the file list.
+# If left blank the directory from which doxygen is run is used as the
+# path to strip.
+
+STRIP_FROM_PATH        =
+
+# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of
+# the path mentioned in the documentation of a class, which tells
+# the reader which header file to include in order to use a class.
+# If left blank only the name of the header file containing the class
+# definition is used. Otherwise one should specify the include paths that
+# are normally passed to the compiler using the -I flag.
+
+STRIP_FROM_INC_PATH    =
+
+# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter
+# (but less readable) file names. This can be useful if your file system
+# doesn't support long names like on DOS, Mac, or CD-ROM.
+
+SHORT_NAMES            = NO
+
+# If the JAVADOC_AUTOBRIEF tag is set to YES then Doxygen
+# will interpret the first line (until the first dot) of a JavaDoc-style
+# comment as the brief description. If set to NO, the JavaDoc
+# comments will behave just like regular Qt-style comments
+# (thus requiring an explicit @brief command for a brief description.)
+
+JAVADOC_AUTOBRIEF      = NO
+
+# If the QT_AUTOBRIEF tag is set to YES then Doxygen will
+# interpret the first line (until the first dot) of a Qt-style
+# comment as the brief description. If set to NO, the comments
+# will behave just like regular Qt-style comments (thus requiring
+# an explicit \brief command for a brief description.)
+
+QT_AUTOBRIEF           = NO
+
+# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make Doxygen
+# treat a multi-line C++ special comment block (i.e. a block of //! or ///
+# comments) as a brief description. This used to be the default behaviour.
+# The new default is to treat a multi-line C++ comment block as a detailed
+# description. Set this tag to YES if you prefer the old behaviour instead.
+
+MULTILINE_CPP_IS_BRIEF = NO
+
+# If the INHERIT_DOCS tag is set to YES (the default) then an undocumented
+# member inherits the documentation from any documented member that it
+# re-implements.
+
+INHERIT_DOCS           = YES
+
+# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce
+# a new page for each member. If set to NO, the documentation of a member will
+# be part of the file/class/namespace that contains it.
+
+SEPARATE_MEMBER_PAGES  = NO
+
+# The TAB_SIZE tag can be used to set the number of spaces in a tab.
+# Doxygen uses this value to replace tabs by spaces in code fragments.
+
+TAB_SIZE               = 5
+
+# This tag can be used to specify a number of aliases that acts
+# as commands in the documentation. An alias has the form "name=value".
+# For example adding "sideeffect=\par Side Effects:\n" will allow you to
+# put the command \sideeffect (or @sideeffect) in the documentation, which
+# will result in a user-defined paragraph with heading "Side Effects:".
+# You can put \n's in the value part of an alias to insert newlines.
+
+ALIASES                =
+
+# This tag can be used to specify a number of word-keyword mappings (TCL only).
+# A mapping has the form "name=value". For example adding
+# "class=itcl::class" will allow you to use the command class in the
+# itcl::class meaning.
+
+TCL_SUBST              =
+
+# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C
+# sources only. Doxygen will then generate output that is more tailored for C.
+# For instance, some of the names that are used will be different. The list
+# of all members will be omitted, etc.
+
+OPTIMIZE_OUTPUT_FOR_C  = NO
+
+# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java
+# sources only. Doxygen will then generate output that is more tailored for
+# Java. For instance, namespaces will be presented as packages, qualified
+# scopes will look different, etc.
+
+OPTIMIZE_OUTPUT_JAVA   = NO
+
+# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran
+# sources only. Doxygen will then generate output that is more tailored for
+# Fortran.
+
+OPTIMIZE_FOR_FORTRAN   = NO
+
+# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL
+# sources. Doxygen will then generate output that is tailored for
+# VHDL.
+
+OPTIMIZE_OUTPUT_VHDL   = NO
+
+# Doxygen selects the parser to use depending on the extension of the files it
+# parses. With this tag you can assign which parser to use for a given extension.
+# Doxygen has a built-in mapping, but you can override or extend it using this
+# tag. The format is ext=language, where ext is a file extension, and language
+# is one of the parsers supported by doxygen: IDL, Java, Javascript, CSharp, C,
+# C++, D, PHP, Objective-C, Python, Fortran, VHDL, C, C++. For instance to make
+# doxygen treat .inc files as Fortran files (default is PHP), and .f files as C
+# (default is Fortran), use: inc=Fortran f=C. Note that for custom extensions
+# you also need to set FILE_PATTERNS otherwise the files are not read by doxygen.
+
+EXTENSION_MAPPING      =
+
+# If MARKDOWN_SUPPORT is enabled (the default) then doxygen pre-processes all
+# comments according to the Markdown format, which allows for more readable
+# documentation. See http://daringfireball.net/projects/markdown/ for details.
+# The output of markdown processing is further processed by doxygen, so you
+# can mix doxygen, HTML, and XML commands with Markdown formatting.
+# Disable only in case of backward compatibilities issues.
+
+MARKDOWN_SUPPORT       = YES
+
+# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want
+# to include (a tag file for) the STL sources as input, then you should
+# set this tag to YES in order to let doxygen match functions declarations and
+# definitions whose arguments contain STL classes (e.g. func(std::string); v.s.
+# func(std::string) {}). This also makes the inheritance and collaboration
+# diagrams that involve STL classes more complete and accurate.
+
+BUILTIN_STL_SUPPORT    = NO
+
+# If you use Microsoft's C++/CLI language, you should set this option to YES to
+# enable parsing support.
+
+CPP_CLI_SUPPORT        = NO
+
+# Set the SIP_SUPPORT tag to YES if your project consists of sip sources only.
+# Doxygen will parse them like normal C++ but will assume all classes use public
+# instead of private inheritance when no explicit protection keyword is present.
+
+SIP_SUPPORT            = NO
+
+# For Microsoft's IDL there are propget and propput attributes to indicate getter
+# and setter methods for a property. Setting this option to YES (the default)
+# will make doxygen replace the get and set methods by a property in the
+# documentation. This will only work if the methods are indeed getting or
+# setting a simple type. If this is not the case, or you want to show the
+# methods anyway, you should set this option to NO.
+
+IDL_PROPERTY_SUPPORT   = YES
+
+# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC
+# tag is set to YES, then doxygen will reuse the documentation of the first
+# member in the group (if any) for the other members of the group. By default
+# all members of a group must be documented explicitly.
+
+DISTRIBUTE_GROUP_DOC   = NO
+
+# Set the SUBGROUPING tag to YES (the default) to allow class member groups of
+# the same type (for instance a group of public functions) to be put as a
+# subgroup of that type (e.g. under the Public Functions section). Set it to
+# NO to prevent subgrouping. Alternatively, this can be done per class using
+# the \nosubgrouping command.
+
+SUBGROUPING            = YES
+
+# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and
+# unions are shown inside the group in which they are included (e.g. using
+# @ingroup) instead of on a separate page (for HTML and Man pages) or
+# section (for LaTeX and RTF).
+
+INLINE_GROUPED_CLASSES = NO
+
+# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and
+# unions with only public data fields will be shown inline in the documentation
+# of the scope in which they are defined (i.e. file, namespace, or group
+# documentation), provided this scope is documented. If set to NO (the default),
+# structs, classes, and unions are shown on a separate page (for HTML and Man
+# pages) or section (for LaTeX and RTF).
+
+INLINE_SIMPLE_STRUCTS  = NO
+
+# When TYPEDEF_HIDES_STRUCT is enabled, a typedef of a struct, union, or enum
+# is documented as struct, union, or enum with the name of the typedef. So
+# typedef struct TypeS {} TypeT, will appear in the documentation as a struct
+# with name TypeT. When disabled the typedef will appear as a member of a file,
+# namespace, or class. And the struct will be named TypeS. This can typically
+# be useful for C code in case the coding convention dictates that all compound
+# types are typedef'ed and only the typedef is referenced, never the tag name.
+
+TYPEDEF_HIDES_STRUCT   = NO
+
+# The SYMBOL_CACHE_SIZE determines the size of the internal cache use to
+# determine which symbols to keep in memory and which to flush to disk.
+# When the cache is full, less often used symbols will be written to disk.
+# For small to medium size projects (<1000 input files) the default value is
+# probably good enough. For larger projects a too small cache size can cause
+# doxygen to be busy swapping symbols to and from disk most of the time
+# causing a significant performance penalty.
+# If the system has enough physical memory increasing the cache will improve the
+# performance by keeping more symbols in memory. Note that the value works on
+# a logarithmic scale so increasing the size by one will roughly double the
+# memory usage. The cache size is given by this formula:
+# 2^(16+SYMBOL_CACHE_SIZE). The valid range is 0..9, the default is 0,
+# corresponding to a cache size of 2^16 = 65536 symbols.
+
+SYMBOL_CACHE_SIZE      = 0
+
+# Similar to the SYMBOL_CACHE_SIZE the size of the symbol lookup cache can be
+# set using LOOKUP_CACHE_SIZE. This cache is used to resolve symbols given
+# their name and scope. Since this can be an expensive process and often the
+# same symbol appear multiple times in the code, doxygen keeps a cache of
+# pre-resolved symbols. If the cache is too small doxygen will become slower.
+# If the cache is too large, memory is wasted. The cache size is given by this
+# formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range is 0..9, the default is 0,
+# corresponding to a cache size of 2^16 = 65536 symbols.
+
+LOOKUP_CACHE_SIZE      = 0
+
+#---------------------------------------------------------------------------
+# Build related configuration options
+#---------------------------------------------------------------------------
+
+# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in
+# documentation are documented, even if no documentation was available.
+# Private class members and static file members will be hidden unless
+# the EXTRACT_PRIVATE and EXTRACT_STATIC tags are set to YES
+
+EXTRACT_ALL            = NO
+
+# If the EXTRACT_PRIVATE tag is set to YES all private members of a class
+# will be included in the documentation.
+
+EXTRACT_PRIVATE        = YES
+
+# If the EXTRACT_PACKAGE tag is set to YES all members with package or internal scope will be included in the documentation.
+
+EXTRACT_PACKAGE        = NO
+
+# If the EXTRACT_STATIC tag is set to YES all static members of a file
+# will be included in the documentation.
+
+EXTRACT_STATIC         = NO
+
+# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs)
+# defined locally in source files will be included in the documentation.
+# If set to NO only classes defined in header files are included.
+
+EXTRACT_LOCAL_CLASSES  = YES
+
+# This flag is only useful for Objective-C code. When set to YES local
+# methods, which are defined in the implementation section but not in
+# the interface are included in the documentation.
+# If set to NO (the default) only methods in the interface are included.
+
+EXTRACT_LOCAL_METHODS  = NO
+
+# If this flag is set to YES, the members of anonymous namespaces will be
+# extracted and appear in the documentation as a namespace called
+# 'anonymous_namespace{file}', where file will be replaced with the base
+# name of the file that contains the anonymous namespace. By default
+# anonymous namespaces are hidden.
+
+EXTRACT_ANON_NSPACES   = NO
+
+# If the HIDE_UNDOC_MEMBERS tag is set to YES, Doxygen will hide all
+# undocumented members of documented classes, files or namespaces.
+# If set to NO (the default) these members will be included in the
+# various overviews, but no documentation section is generated.
+# This option has no effect if EXTRACT_ALL is enabled.
+
+HIDE_UNDOC_MEMBERS     = NO
+
+# If the HIDE_UNDOC_CLASSES tag is set to YES, Doxygen will hide all
+# undocumented classes that are normally visible in the class hierarchy.
+# If set to NO (the default) these classes will be included in the various
+# overviews. This option has no effect if EXTRACT_ALL is enabled.
+
+HIDE_UNDOC_CLASSES     = NO
+
+# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, Doxygen will hide all
+# friend (class|struct|union) declarations.
+# If set to NO (the default) these declarations will be included in the
+# documentation.
+
+HIDE_FRIEND_COMPOUNDS  = NO
+
+# If the HIDE_IN_BODY_DOCS tag is set to YES, Doxygen will hide any
+# documentation blocks found inside the body of a function.
+# If set to NO (the default) these blocks will be appended to the
+# function's detailed documentation block.
+
+HIDE_IN_BODY_DOCS      = NO
+
+# The INTERNAL_DOCS tag determines if documentation
+# that is typed after a \internal command is included. If the tag is set
+# to NO (the default) then the documentation will be excluded.
+# Set it to YES to include the internal documentation.
+
+INTERNAL_DOCS          = NO
+
+# If the CASE_SENSE_NAMES tag is set to NO then Doxygen will only generate
+# file names in lower-case letters. If set to YES upper-case letters are also
+# allowed. This is useful if you have classes or files whose names only differ
+# in case and if your file system supports case sensitive file names. Windows
+# and Mac users are advised to set this option to NO.
+
+CASE_SENSE_NAMES       = NO
+
+# If the HIDE_SCOPE_NAMES tag is set to NO (the default) then Doxygen
+# will show members with their full class and namespace scopes in the
+# documentation. If set to YES the scope will be hidden.
+
+HIDE_SCOPE_NAMES       = NO
+
+# If the SHOW_INCLUDE_FILES tag is set to YES (the default) then Doxygen
+# will put a list of the files that are included by a file in the documentation
+# of that file.
+
+SHOW_INCLUDE_FILES     = YES
+
+# If the FORCE_LOCAL_INCLUDES tag is set to YES then Doxygen
+# will list include files with double quotes in the documentation
+# rather than with sharp brackets.
+
+FORCE_LOCAL_INCLUDES   = NO
+
+# If the INLINE_INFO tag is set to YES (the default) then a tag [inline]
+# is inserted in the documentation for inline members.
+
+INLINE_INFO            = YES
+
+# If the SORT_MEMBER_DOCS tag is set to YES (the default) then doxygen
+# will sort the (detailed) documentation of file and class members
+# alphabetically by member name. If set to NO the members will appear in
+# declaration order.
+
+SORT_MEMBER_DOCS       = YES
+
+# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the
+# brief documentation of file, namespace and class members alphabetically
+# by member name. If set to NO (the default) the members will appear in
+# declaration order.
+
+SORT_BRIEF_DOCS        = NO
+
+# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen
+# will sort the (brief and detailed) documentation of class members so that
+# constructors and destructors are listed first. If set to NO (the default)
+# the constructors will appear in the respective orders defined by
+# SORT_MEMBER_DOCS and SORT_BRIEF_DOCS.
+# This tag will be ignored for brief docs if SORT_BRIEF_DOCS is set to NO
+# and ignored for detailed docs if SORT_MEMBER_DOCS is set to NO.
+
+SORT_MEMBERS_CTORS_1ST = NO
+
+# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the
+# hierarchy of group names into alphabetical order. If set to NO (the default)
+# the group names will appear in their defined order.
+
+SORT_GROUP_NAMES       = NO
+
+# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be
+# sorted by fully-qualified names, including namespaces. If set to
+# NO (the default), the class list will be sorted only by class name,
+# not including the namespace part.
+# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES.
+# Note: This option applies only to the class list, not to the
+# alphabetical list.
+
+SORT_BY_SCOPE_NAME     = NO
+
+# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to
+# do proper type resolution of all parameters of a function it will reject a
+# match between the prototype and the implementation of a member function even
+# if there is only one candidate or it is obvious which candidate to choose
+# by doing a simple string match. By disabling STRICT_PROTO_MATCHING doxygen
+# will still accept a match between prototype and implementation in such cases.
+
+STRICT_PROTO_MATCHING  = NO
+
+# The GENERATE_TODOLIST tag can be used to enable (YES) or
+# disable (NO) the todo list. This list is created by putting \todo
+# commands in the documentation.
+
+GENERATE_TODOLIST      = YES
+
+# The GENERATE_TESTLIST tag can be used to enable (YES) or
+# disable (NO) the test list. This list is created by putting \test
+# commands in the documentation.
+
+GENERATE_TESTLIST      = YES
+
+# The GENERATE_BUGLIST tag can be used to enable (YES) or
+# disable (NO) the bug list. This list is created by putting \bug
+# commands in the documentation.
+
+GENERATE_BUGLIST       = YES
+
+# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or
+# disable (NO) the deprecated list. This list is created by putting
+# \deprecated commands in the documentation.
+
+GENERATE_DEPRECATEDLIST= YES
+
+# The ENABLED_SECTIONS tag can be used to enable conditional
+# documentation sections, marked by \if sectionname ... \endif.
+
+ENABLED_SECTIONS       =
+
+# The MAX_INITIALIZER_LINES tag determines the maximum number of lines
+# the initial value of a variable or macro consists of for it to appear in
+# the documentation. If the initializer consists of more lines than specified
+# here it will be hidden. Use a value of 0 to hide initializers completely.
+# The appearance of the initializer of individual variables and macros in the
+# documentation can be controlled using \showinitializer or \hideinitializer
+# command in the documentation regardless of this setting.
+
+MAX_INITIALIZER_LINES  = 30
+
+# Set the SHOW_USED_FILES tag to NO to disable the list of files generated
+# at the bottom of the documentation of classes and structs. If set to YES the
+# list will mention the files that were used to generate the documentation.
+
+SHOW_USED_FILES        = YES
+
+# If the sources in your project are distributed over multiple directories
+# then setting the SHOW_DIRECTORIES tag to YES will show the directory hierarchy
+# in the documentation. The default is NO.
+
+SHOW_DIRECTORIES       = NO
+
+# Set the SHOW_FILES tag to NO to disable the generation of the Files page.
+# This will remove the Files entry from the Quick Index and from the
+# Folder Tree View (if specified). The default is YES.
+
+SHOW_FILES             = YES
+
+# Set the SHOW_NAMESPACES tag to NO to disable the generation of the
+# Namespaces page.
+# This will remove the Namespaces entry from the Quick Index
+# and from the Folder Tree View (if specified). The default is YES.
+
+SHOW_NAMESPACES        = YES
+
+# The FILE_VERSION_FILTER tag can be used to specify a program or script that
+# doxygen should invoke to get the current version for each file (typically from
+# the version control system). Doxygen will invoke the program by executing (via
+# popen()) the command <command> <input-file>, where <command> is the value of
+# the FILE_VERSION_FILTER tag, and <input-file> is the name of an input file
+# provided by doxygen. Whatever the program writes to standard output
+# is used as the file version. See the manual for examples.
+
+FILE_VERSION_FILTER    =
+
+# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed
+# by doxygen. The layout file controls the global structure of the generated
+# output files in an output format independent way. The create the layout file
+# that represents doxygen's defaults, run doxygen with the -l option.
+# You can optionally specify a file name after the option, if omitted
+# DoxygenLayout.xml will be used as the name of the layout file.
+
+LAYOUT_FILE            =
+
+# The CITE_BIB_FILES tag can be used to specify one or more bib files
+# containing the references data. This must be a list of .bib files. The
+# .bib extension is automatically appended if omitted. Using this command
+# requires the bibtex tool to be installed. See also
+# http://en.wikipedia.org/wiki/BibTeX for more info. For LaTeX the style
+# of the bibliography can be controlled using LATEX_BIB_STYLE. To use this
+# feature you need bibtex and perl available in the search path.
+
+CITE_BIB_FILES         =
+
+#---------------------------------------------------------------------------
+# configuration options related to warning and progress messages
+#---------------------------------------------------------------------------
+
+# The QUIET tag can be used to turn on/off the messages that are generated
+# by doxygen. Possible values are YES and NO. If left blank NO is used.
+
+QUIET                  = NO
+
+# The WARNINGS tag can be used to turn on/off the warning messages that are
+# generated by doxygen. Possible values are YES and NO. If left blank
+# NO is used.
+
+WARNINGS               = YES
+
+# If WARN_IF_UNDOCUMENTED is set to YES, then doxygen will generate warnings
+# for undocumented members. If EXTRACT_ALL is set to YES then this flag will
+# automatically be disabled.
+
+WARN_IF_UNDOCUMENTED   = YES
+
+# If WARN_IF_DOC_ERROR is set to YES, doxygen will generate warnings for
+# potential errors in the documentation, such as not documenting some
+# parameters in a documented function, or documenting parameters that
+# don't exist or using markup commands wrongly.
+
+WARN_IF_DOC_ERROR      = YES
+
+# The WARN_NO_PARAMDOC option can be enabled to get warnings for
+# functions that are documented, but have no documentation for their parameters
+# or return value. If set to NO (the default) doxygen will only warn about
+# wrong or incomplete parameter documentation, but not about the absence of
+# documentation.
+
+WARN_NO_PARAMDOC       = NO
+
+# The WARN_FORMAT tag determines the format of the warning messages that
+# doxygen can produce. The string should contain the $file, $line, and $text
+# tags, which will be replaced by the file and line number from which the
+# warning originated and the warning text. Optionally the format may contain
+# $version, which will be replaced by the version of the file (if it could
+# be obtained via FILE_VERSION_FILTER)
+
+WARN_FORMAT            = "$file:$line: $text"
+
+# The WARN_LOGFILE tag can be used to specify a file to which warning
+# and error messages should be written. If left blank the output is written
+# to stderr.
+
+WARN_LOGFILE           =
+
+#---------------------------------------------------------------------------
+# configuration options related to the input files
+#---------------------------------------------------------------------------
+
+# The INPUT tag can be used to specify the files and/or directories that contain
+# documented source files. You may enter file names like "myfile.cpp" or
+# directories like "/usr/src/myproject". Separate the files or directories
+# with spaces.
+
+INPUT                  = . include/ include/atomic include/condition_variable include/cstdatomic include/mutex
+
+
+# This tag can be used to specify the character encoding of the source files
+# that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
+# also the default input encoding. Doxygen uses libiconv (or the iconv built
+# into libc) for the transcoding. See http://www.gnu.org/software/libiconv for
+# the list of possible encodings.
+
+INPUT_ENCODING         = UTF-8
+
+# If the value of the INPUT tag contains directories, you can use the
+# FILE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp
+# and *.h) to filter out the source-files in the directories. If left
+# blank the following patterns are tested:
+# *.c *.cc *.cxx *.cpp *.c++ *.d *.java *.ii *.ixx *.ipp *.i++ *.inl *.h *.hh
+# *.hxx *.hpp *.h++ *.idl *.odl *.cs *.php *.php3 *.inc *.m *.mm *.dox *.py
+# *.f90 *.f *.for *.vhd *.vhdl
+
+FILE_PATTERNS          =
+
+# The RECURSIVE tag can be used to turn specify whether or not subdirectories
+# should be searched for input files as well. Possible values are YES and NO.
+# If left blank NO is used.
+
+RECURSIVE              = NO
+
+# The EXCLUDE tag can be used to specify files and/or directories that should be
+# excluded from the INPUT source files. This way you can easily exclude a
+# subdirectory from a directory tree whose root is specified with the INPUT tag.
+# Note that relative paths are relative to the directory from which doxygen is
+# run.
+
+EXCLUDE                = malloc.c
+
+# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or
+# directories that are symbolic links (a Unix file system feature) are excluded
+# from the input.
+
+EXCLUDE_SYMLINKS       = NO
+
+# If the value of the INPUT tag contains directories, you can use the
+# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude
+# certain files from those directories. Note that the wildcards are matched
+# against the file with absolute path, so to exclude all test directories
+# for example use the pattern */test/*
+
+EXCLUDE_PATTERNS       =
+
+# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names
+# (namespaces, classes, functions, etc.) that should be excluded from the
+# output. The symbol name can be a fully qualified name, a word, or if the
+# wildcard * is used, a substring. Examples: ANamespace, AClass,
+# AClass::ANamespace, ANamespace::*Test
+
+EXCLUDE_SYMBOLS        =
+
+# The EXAMPLE_PATH tag can be used to specify one or more files or
+# directories that contain example code fragments that are included (see
+# the \include command).
+
+EXAMPLE_PATH           = .
+
+# If the value of the EXAMPLE_PATH tag contains directories, you can use the
+# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp
+# and *.h) to filter out the source-files in the directories. If left
+# blank all files are included.
+
+EXAMPLE_PATTERNS       =
+
+# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be
+# searched for input files to be used with the \include or \dontinclude
+# commands irrespective of the value of the RECURSIVE tag.
+# Possible values are YES and NO. If left blank NO is used.
+
+EXAMPLE_RECURSIVE      = NO
+
+# The IMAGE_PATH tag can be used to specify one or more files or
+# directories that contain image that are included in the documentation (see
+# the \image command).
+
+IMAGE_PATH             =
+
+# The INPUT_FILTER tag can be used to specify a program that doxygen should
+# invoke to filter for each input file. Doxygen will invoke the filter program
+# by executing (via popen()) the command <filter> <input-file>, where <filter>
+# is the value of the INPUT_FILTER tag, and <input-file> is the name of an
+# input file. Doxygen will then use the output that the filter program writes
+# to standard output.
+# If FILTER_PATTERNS is specified, this tag will be
+# ignored.
+
+INPUT_FILTER           =
+
+# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern
+# basis.
+# Doxygen will compare the file name with each pattern and apply the
+# filter if there is a match.
+# The filters are a list of the form:
+# pattern=filter (like *.cpp=my_cpp_filter). See INPUT_FILTER for further
+# info on how filters are used. If FILTER_PATTERNS is empty or if
+# non of the patterns match the file name, INPUT_FILTER is applied.
+
+FILTER_PATTERNS        =
+
+# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using
+# INPUT_FILTER) will be used to filter the input files when producing source
+# files to browse (i.e. when SOURCE_BROWSER is set to YES).
+
+FILTER_SOURCE_FILES    = NO
+
+# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file
+# pattern. A pattern will override the setting for FILTER_PATTERN (if any)
+# and it is also possible to disable source filtering for a specific pattern
+# using *.ext= (so without naming a filter). This option only has effect when
+# FILTER_SOURCE_FILES is enabled.
+
+FILTER_SOURCE_PATTERNS =
+
+#---------------------------------------------------------------------------
+# configuration options related to source browsing
+#---------------------------------------------------------------------------
+
+# If the SOURCE_BROWSER tag is set to YES then a list of source files will
+# be generated. Documented entities will be cross-referenced with these sources.
+# Note: To get rid of all source code in the generated output, make sure also
+# VERBATIM_HEADERS is set to NO.
+
+SOURCE_BROWSER         = NO
+
+# Setting the INLINE_SOURCES tag to YES will include the body
+# of functions and classes directly in the documentation.
+
+INLINE_SOURCES         = NO
+
+# Setting the STRIP_CODE_COMMENTS tag to YES (the default) will instruct
+# doxygen to hide any special comment blocks from generated source code
+# fragments. Normal C and C++ comments will always remain visible.
+
+STRIP_CODE_COMMENTS    = YES
+
+# If the REFERENCED_BY_RELATION tag is set to YES
+# then for each documented function all documented
+# functions referencing it will be listed.
+
+REFERENCED_BY_RELATION = NO
+
+# If the REFERENCES_RELATION tag is set to YES
+# then for each documented function all documented entities
+# called/used by that function will be listed.
+
+REFERENCES_RELATION    = NO
+
+# If the REFERENCES_LINK_SOURCE tag is set to YES (the default)
+# and SOURCE_BROWSER tag is set to YES, then the hyperlinks from
+# functions in REFERENCES_RELATION and REFERENCED_BY_RELATION lists will
+# link to the source code.
+# Otherwise they will link to the documentation.
+
+REFERENCES_LINK_SOURCE = YES
+
+# If the USE_HTAGS tag is set to YES then the references to source code
+# will point to the HTML generated by the htags(1) tool instead of doxygen
+# built-in source browser. The htags tool is part of GNU's global source
+# tagging system (see http://www.gnu.org/software/global/global.html). You
+# will need version 4.8.6 or higher.
+
+USE_HTAGS              = NO
+
+# If the VERBATIM_HEADERS tag is set to YES (the default) then Doxygen
+# will generate a verbatim copy of the header file for each class for
+# which an include is specified. Set to NO to disable this.
+
+VERBATIM_HEADERS       = YES
+
+#---------------------------------------------------------------------------
+# configuration options related to the alphabetical class index
+#---------------------------------------------------------------------------
+
+# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index
+# of all compounds will be generated. Enable this if the project
+# contains a lot of classes, structs, unions or interfaces.
+
+ALPHABETICAL_INDEX     = YES
+
+# If the alphabetical index is enabled (see ALPHABETICAL_INDEX) then
+# the COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns
+# in which this list will be split (can be a number in the range [1..20])
+
+COLS_IN_ALPHA_INDEX    = 5
+
+# In case all classes in a project start with a common prefix, all
+# classes will be put under the same header in the alphabetical index.
+# The IGNORE_PREFIX tag can be used to specify one or more prefixes that
+# should be ignored while generating the index headers.
+
+IGNORE_PREFIX          =
+
+#---------------------------------------------------------------------------
+# configuration options related to the HTML output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_HTML tag is set to YES (the default) Doxygen will
+# generate HTML output.
+
+GENERATE_HTML          = YES
+
+# The HTML_OUTPUT tag is used to specify where the HTML docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `html' will be used as the default path.
+
+HTML_OUTPUT            = docs
+
+# The HTML_FILE_EXTENSION tag can be used to specify the file extension for
+# each generated HTML page (for example: .htm,.php,.asp). If it is left blank
+# doxygen will generate files with .html extension.
+
+HTML_FILE_EXTENSION    = .html
+
+# The HTML_HEADER tag can be used to specify a personal HTML header for
+# each generated HTML page. If it is left blank doxygen will generate a
+# standard header. Note that when using a custom header you are responsible
+#  for the proper inclusion of any scripts and style sheets that doxygen
+# needs, which is dependent on the configuration options used.
+# It is advised to generate a default header using "doxygen -w html
+# header.html footer.html stylesheet.css YourConfigFile" and then modify
+# that header. Note that the header is subject to change so you typically
+# have to redo this when upgrading to a newer version of doxygen or when
+# changing the value of configuration settings such as GENERATE_TREEVIEW!
+
+HTML_HEADER            =
+
+# The HTML_FOOTER tag can be used to specify a personal HTML footer for
+# each generated HTML page. If it is left blank doxygen will generate a
+# standard footer.
+
+HTML_FOOTER            =
+
+# The HTML_STYLESHEET tag can be used to specify a user-defined cascading
+# style sheet that is used by each HTML page. It can be used to
+# fine-tune the look of the HTML output. If the tag is left blank doxygen
+# will generate a default style sheet. Note that doxygen will try to copy
+# the style sheet file to the HTML output directory, so don't put your own
+# style sheet in the HTML output directory as well, or it will be erased!
+
+HTML_STYLESHEET        =
+
+# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or
+# other source files which should be copied to the HTML output directory. Note
+# that these files will be copied to the base HTML output directory. Use the
+# $relpath$ marker in the HTML_HEADER and/or HTML_FOOTER files to load these
+# files. In the HTML_STYLESHEET file, use the file name only. Also note that
+# the files will be copied as-is; there are no commands or markers available.
+
+HTML_EXTRA_FILES       =
+
+# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output.
+# Doxygen will adjust the colors in the style sheet and background images
+# according to this color. Hue is specified as an angle on a colorwheel,
+# see http://en.wikipedia.org/wiki/Hue for more information.
+# For instance the value 0 represents red, 60 is yellow, 120 is green,
+# 180 is cyan, 240 is blue, 300 purple, and 360 is red again.
+# The allowed range is 0 to 359.
+
+HTML_COLORSTYLE_HUE    = 220
+
+# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of
+# the colors in the HTML output. For a value of 0 the output will use
+# grayscales only. A value of 255 will produce the most vivid colors.
+
+HTML_COLORSTYLE_SAT    = 100
+
+# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to
+# the luminance component of the colors in the HTML output. Values below
+# 100 gradually make the output lighter, whereas values above 100 make
+# the output darker. The value divided by 100 is the actual gamma applied,
+# so 80 represents a gamma of 0.8, The value 220 represents a gamma of 2.2,
+# and 100 does not change the gamma.
+
+HTML_COLORSTYLE_GAMMA  = 80
+
+# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML
+# page will contain the date and time when the page was generated. Setting
+# this to NO can help when comparing the output of multiple runs.
+
+HTML_TIMESTAMP         = YES
+
+# If the HTML_ALIGN_MEMBERS tag is set to YES, the members of classes,
+# files or namespaces will be aligned in HTML using tables. If set to
+# NO a bullet list will be used.
+
+HTML_ALIGN_MEMBERS     = YES
+
+# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML
+# documentation will contain sections that can be hidden and shown after the
+# page has loaded. For this to work a browser that supports
+# JavaScript and DHTML is required (for instance Mozilla 1.0+, Firefox
+# Netscape 6.0+, Internet explorer 5.0+, Konqueror, or Safari).
+
+HTML_DYNAMIC_SECTIONS  = NO
+
+# If the GENERATE_DOCSET tag is set to YES, additional index files
+# will be generated that can be used as input for Apple's Xcode 3
+# integrated development environment, introduced with OSX 10.5 (Leopard).
+# To create a documentation set, doxygen will generate a Makefile in the
+# HTML output directory. Running make will produce the docset in that
+# directory and running "make install" will install the docset in
+# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find
+# it at startup.
+# See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html
+# for more information.
+
+GENERATE_DOCSET        = NO
+
+# When GENERATE_DOCSET tag is set to YES, this tag determines the name of the
+# feed. A documentation feed provides an umbrella under which multiple
+# documentation sets from a single provider (such as a company or product suite)
+# can be grouped.
+
+DOCSET_FEEDNAME        = "Doxygen generated docs"
+
+# When GENERATE_DOCSET tag is set to YES, this tag specifies a string that
+# should uniquely identify the documentation set bundle. This should be a
+# reverse domain-name style string, e.g. com.mycompany.MyDocSet. Doxygen
+# will append .docset to the name.
+
+DOCSET_BUNDLE_ID       = org.doxygen.Project
+
+# When GENERATE_PUBLISHER_ID tag specifies a string that should uniquely identify
+# the documentation publisher. This should be a reverse domain-name style
+# string, e.g. com.mycompany.MyDocSet.documentation.
+
+DOCSET_PUBLISHER_ID    = org.doxygen.Publisher
+
+# The GENERATE_PUBLISHER_NAME tag identifies the documentation publisher.
+
+DOCSET_PUBLISHER_NAME  = Publisher
+
+# If the GENERATE_HTMLHELP tag is set to YES, additional index files
+# will be generated that can be used as input for tools like the
+# Microsoft HTML help workshop to generate a compiled HTML help file (.chm)
+# of the generated HTML documentation.
+
+GENERATE_HTMLHELP      = NO
+
+# If the GENERATE_HTMLHELP tag is set to YES, the CHM_FILE tag can
+# be used to specify the file name of the resulting .chm file. You
+# can add a path in front of the file if the result should not be
+# written to the html output directory.
+
+CHM_FILE               =
+
+# If the GENERATE_HTMLHELP tag is set to YES, the HHC_LOCATION tag can
+# be used to specify the location (absolute path including file name) of
+# the HTML help compiler (hhc.exe). If non-empty doxygen will try to run
+# the HTML help compiler on the generated index.hhp.
+
+HHC_LOCATION           =
+
+# If the GENERATE_HTMLHELP tag is set to YES, the GENERATE_CHI flag
+# controls if a separate .chi index file is generated (YES) or that
+# it should be included in the master .chm file (NO).
+
+GENERATE_CHI           = NO
+
+# If the GENERATE_HTMLHELP tag is set to YES, the CHM_INDEX_ENCODING
+# is used to encode HtmlHelp index (hhk), content (hhc) and project file
+# content.
+
+CHM_INDEX_ENCODING     =
+
+# If the GENERATE_HTMLHELP tag is set to YES, the BINARY_TOC flag
+# controls whether a binary table of contents is generated (YES) or a
+# normal table of contents (NO) in the .chm file.
+
+BINARY_TOC             = NO
+
+# The TOC_EXPAND flag can be set to YES to add extra items for group members
+# to the contents of the HTML help documentation and to the tree view.
+
+TOC_EXPAND             = NO
+
+# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and
+# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated
+# that can be used as input for Qt's qhelpgenerator to generate a
+# Qt Compressed Help (.qch) of the generated HTML documentation.
+
+GENERATE_QHP           = NO
+
+# If the QHG_LOCATION tag is specified, the QCH_FILE tag can
+# be used to specify the file name of the resulting .qch file.
+# The path specified is relative to the HTML output folder.
+
+QCH_FILE               =
+
+# The QHP_NAMESPACE tag specifies the namespace to use when generating
+# Qt Help Project output. For more information please see
+# http://doc.trolltech.com/qthelpproject.html#namespace
+
+QHP_NAMESPACE          = org.doxygen.Project
+
+# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating
+# Qt Help Project output. For more information please see
+# http://doc.trolltech.com/qthelpproject.html#virtual-folders
+
+QHP_VIRTUAL_FOLDER     = doc
+
+# If QHP_CUST_FILTER_NAME is set, it specifies the name of a custom filter to
+# add. For more information please see
+# http://doc.trolltech.com/qthelpproject.html#custom-filters
+
+QHP_CUST_FILTER_NAME   =
+
+# The QHP_CUST_FILT_ATTRS tag specifies the list of the attributes of the
+# custom filter to add. For more information please see
+# <a href="http://doc.trolltech.com/qthelpproject.html#custom-filters">
+# Qt Help Project / Custom Filters</a>.
+
+QHP_CUST_FILTER_ATTRS  =
+
+# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this
+# project's
+# filter section matches.
+# <a href="http://doc.trolltech.com/qthelpproject.html#filter-attributes">
+# Qt Help Project / Filter Attributes</a>.
+
+QHP_SECT_FILTER_ATTRS  =
+
+# If the GENERATE_QHP tag is set to YES, the QHG_LOCATION tag can
+# be used to specify the location of Qt's qhelpgenerator.
+# If non-empty doxygen will try to run qhelpgenerator on the generated
+# .qhp file.
+
+QHG_LOCATION           =
+
+# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files
+#  will be generated, which together with the HTML files, form an Eclipse help
+# plugin. To install this plugin and make it available under the help contents
+# menu in Eclipse, the contents of the directory containing the HTML and XML
+# files needs to be copied into the plugins directory of eclipse. The name of
+# the directory within the plugins directory should be the same as
+# the ECLIPSE_DOC_ID value. After copying Eclipse needs to be restarted before
+# the help appears.
+
+GENERATE_ECLIPSEHELP   = NO
+
+# A unique identifier for the eclipse help plugin. When installing the plugin
+# the directory name containing the HTML and XML files should also have
+# this name.
+
+ECLIPSE_DOC_ID         = org.doxygen.Project
+
+# The DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs)
+# at top of each HTML page. The value NO (the default) enables the index and
+# the value YES disables it. Since the tabs have the same information as the
+# navigation tree you can set this option to NO if you already set
+# GENERATE_TREEVIEW to YES.
+
+DISABLE_INDEX          = NO
+
+# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index
+# structure should be generated to display hierarchical information.
+# If the tag value is set to YES, a side panel will be generated
+# containing a tree-like index structure (just like the one that
+# is generated for HTML Help). For this to work a browser that supports
+# JavaScript, DHTML, CSS and frames is required (i.e. any modern browser).
+# Windows users are probably better off using the HTML help feature.
+# Since the tree basically has the same information as the tab index you
+# could consider to set DISABLE_INDEX to NO when enabling this option.
+
+GENERATE_TREEVIEW      = NO
+
+# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values
+# (range [0,1..20]) that doxygen will group on one line in the generated HTML
+# documentation. Note that a value of 0 will completely suppress the enum
+# values from appearing in the overview section.
+
+ENUM_VALUES_PER_LINE   = 4
+
+# By enabling USE_INLINE_TREES, doxygen will generate the Groups, Directories,
+# and Class Hierarchy pages using a tree view instead of an ordered list.
+
+USE_INLINE_TREES       = NO
+
+# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be
+# used to set the initial width (in pixels) of the frame in which the tree
+# is shown.
+
+TREEVIEW_WIDTH         = 250
+
+# When the EXT_LINKS_IN_WINDOW option is set to YES doxygen will open
+# links to external symbols imported via tag files in a separate window.
+
+EXT_LINKS_IN_WINDOW    = NO
+
+# Use this tag to change the font size of Latex formulas included
+# as images in the HTML documentation. The default is 10. Note that
+# when you change the font size after a successful doxygen run you need
+# to manually remove any form_*.png images from the HTML output directory
+# to force them to be regenerated.
+
+FORMULA_FONTSIZE       = 10
+
+# Use the FORMULA_TRANPARENT tag to determine whether or not the images
+# generated for formulas are transparent PNGs. Transparent PNGs are
+# not supported properly for IE 6.0, but are supported on all modern browsers.
+# Note that when changing this option you need to delete any form_*.png files
+# in the HTML output before the changes have effect.
+
+FORMULA_TRANSPARENT    = YES
+
+# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax
+# (see http://www.mathjax.org) which uses client side Javascript for the
+# rendering instead of using prerendered bitmaps. Use this if you do not
+# have LaTeX installed or if you want to formulas look prettier in the HTML
+# output. When enabled you may also need to install MathJax separately and
+# configure the path to it using the MATHJAX_RELPATH option.
+
+USE_MATHJAX            = NO
+
+# When MathJax is enabled you need to specify the location relative to the
+# HTML output directory using the MATHJAX_RELPATH option. The destination
+# directory should contain the MathJax.js script. For instance, if the mathjax
+# directory is located at the same level as the HTML output directory, then
+# MATHJAX_RELPATH should be ../mathjax. The default value points to
+# the MathJax Content Delivery Network so you can quickly see the result without
+# installing MathJax.
+# However, it is strongly recommended to install a local
+# copy of MathJax from http://www.mathjax.org before deployment.
+
+MATHJAX_RELPATH        = http://cdn.mathjax.org/mathjax/latest
+
+# The MATHJAX_EXTENSIONS tag can be used to specify one or MathJax extension
+# names that should be enabled during MathJax rendering.
+
+MATHJAX_EXTENSIONS     =
+
+# When the SEARCHENGINE tag is enabled doxygen will generate a search box
+# for the HTML output. The underlying search engine uses javascript
+# and DHTML and should work on any modern browser. Note that when using
+# HTML help (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets
+# (GENERATE_DOCSET) there is already a search function so this one should
+# typically be disabled. For large projects the javascript based search engine
+# can be slow, then enabling SERVER_BASED_SEARCH may provide a better solution.
+
+SEARCHENGINE           = YES
+
+# When the SERVER_BASED_SEARCH tag is enabled the search engine will be
+# implemented using a PHP enabled web server instead of at the web client
+# using Javascript. Doxygen will generate the search PHP script and index
+# file to put on the web server. The advantage of the server
+# based approach is that it scales better to large projects and allows
+# full text search. The disadvantages are that it is more difficult to setup
+# and does not have live searching capabilities.
+
+SERVER_BASED_SEARCH    = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the LaTeX output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_LATEX tag is set to YES (the default) Doxygen will
+# generate Latex output.
+
+GENERATE_LATEX         = NO
+
+# The LATEX_OUTPUT tag is used to specify where the LaTeX docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `latex' will be used as the default path.
+
+LATEX_OUTPUT           = latex
+
+# The LATEX_CMD_NAME tag can be used to specify the LaTeX command name to be
+# invoked. If left blank `latex' will be used as the default command name.
+# Note that when enabling USE_PDFLATEX this option is only used for
+# generating bitmaps for formulas in the HTML output, but not in the
+# Makefile that is written to the output directory.
+
+LATEX_CMD_NAME         = latex
+
+# The MAKEINDEX_CMD_NAME tag can be used to specify the command name to
+# generate index for LaTeX. If left blank `makeindex' will be used as the
+# default command name.
+
+MAKEINDEX_CMD_NAME     = makeindex
+
+# If the COMPACT_LATEX tag is set to YES Doxygen generates more compact
+# LaTeX documents. This may be useful for small projects and may help to
+# save some trees in general.
+
+COMPACT_LATEX          = NO
+
+# The PAPER_TYPE tag can be used to set the paper type that is used
+# by the printer. Possible values are: a4, letter, legal and
+# executive. If left blank a4wide will be used.
+
+PAPER_TYPE             = a4
+
+# The EXTRA_PACKAGES tag can be to specify one or more names of LaTeX
+# packages that should be included in the LaTeX output.
+
+EXTRA_PACKAGES         =
+
+# The LATEX_HEADER tag can be used to specify a personal LaTeX header for
+# the generated latex document. The header should contain everything until
+# the first chapter. If it is left blank doxygen will generate a
+# standard header. Notice: only use this tag if you know what you are doing!
+
+LATEX_HEADER           =
+
+# The LATEX_FOOTER tag can be used to specify a personal LaTeX footer for
+# the generated latex document. The footer should contain everything after
+# the last chapter. If it is left blank doxygen will generate a
+# standard footer. Notice: only use this tag if you know what you are doing!
+
+LATEX_FOOTER           =
+
+# If the PDF_HYPERLINKS tag is set to YES, the LaTeX that is generated
+# is prepared for conversion to pdf (using ps2pdf). The pdf file will
+# contain links (just like the HTML output) instead of page references
+# This makes the output suitable for online browsing using a pdf viewer.
+
+PDF_HYPERLINKS         = YES
+
+# If the USE_PDFLATEX tag is set to YES, pdflatex will be used instead of
+# plain latex in the generated Makefile. Set this option to YES to get a
+# higher quality PDF documentation.
+
+USE_PDFLATEX           = YES
+
+# If the LATEX_BATCHMODE tag is set to YES, doxygen will add the \\batchmode.
+# command to the generated LaTeX files. This will instruct LaTeX to keep
+# running if errors occur, instead of asking the user for help.
+# This option is also used when generating formulas in HTML.
+
+LATEX_BATCHMODE        = NO
+
+# If LATEX_HIDE_INDICES is set to YES then doxygen will not
+# include the index chapters (such as File Index, Compound Index, etc.)
+# in the output.
+
+LATEX_HIDE_INDICES     = NO
+
+# If LATEX_SOURCE_CODE is set to YES then doxygen will include
+# source code with syntax highlighting in the LaTeX output.
+# Note that which sources are shown also depends on other settings
+# such as SOURCE_BROWSER.
+
+LATEX_SOURCE_CODE      = NO
+
+# The LATEX_BIB_STYLE tag can be used to specify the style to use for the
+# bibliography, e.g. plainnat, or ieeetr. The default style is "plain". See
+# http://en.wikipedia.org/wiki/BibTeX for more info.
+
+LATEX_BIB_STYLE        = plain
+
+#---------------------------------------------------------------------------
+# configuration options related to the RTF output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_RTF tag is set to YES Doxygen will generate RTF output
+# The RTF output is optimized for Word 97 and may not look very pretty with
+# other RTF readers or editors.
+
+GENERATE_RTF           = NO
+
+# The RTF_OUTPUT tag is used to specify where the RTF docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `rtf' will be used as the default path.
+
+RTF_OUTPUT             = rtf
+
+# If the COMPACT_RTF tag is set to YES Doxygen generates more compact
+# RTF documents. This may be useful for small projects and may help to
+# save some trees in general.
+
+COMPACT_RTF            = NO
+
+# If the RTF_HYPERLINKS tag is set to YES, the RTF that is generated
+# will contain hyperlink fields. The RTF file will
+# contain links (just like the HTML output) instead of page references.
+# This makes the output suitable for online browsing using WORD or other
+# programs which support those fields.
+# Note: wordpad (write) and others do not support links.
+
+RTF_HYPERLINKS         = NO
+
+# Load style sheet definitions from file. Syntax is similar to doxygen's
+# config file, i.e. a series of assignments. You only have to provide
+# replacements, missing definitions are set to their default value.
+
+RTF_STYLESHEET_FILE    =
+
+# Set optional variables used in the generation of an rtf document.
+# Syntax is similar to doxygen's config file.
+
+RTF_EXTENSIONS_FILE    =
+
+#---------------------------------------------------------------------------
+# configuration options related to the man page output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_MAN tag is set to YES (the default) Doxygen will
+# generate man pages
+
+GENERATE_MAN           = NO
+
+# The MAN_OUTPUT tag is used to specify where the man pages will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `man' will be used as the default path.
+
+MAN_OUTPUT             = man
+
+# The MAN_EXTENSION tag determines the extension that is added to
+# the generated man pages (default is the subroutine's section .3)
+
+MAN_EXTENSION          = .3
+
+# If the MAN_LINKS tag is set to YES and Doxygen generates man output,
+# then it will generate one additional man file for each entity
+# documented in the real man page(s). These additional files
+# only source the real man page, but without them the man command
+# would be unable to find the correct page. The default is NO.
+
+MAN_LINKS              = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the XML output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_XML tag is set to YES Doxygen will
+# generate an XML file that captures the structure of
+# the code including all documentation.
+
+GENERATE_XML           = NO
+
+# The XML_OUTPUT tag is used to specify where the XML pages will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `xml' will be used as the default path.
+
+XML_OUTPUT             = xml
+
+# The XML_SCHEMA tag can be used to specify an XML schema,
+# which can be used by a validating XML parser to check the
+# syntax of the XML files.
+
+XML_SCHEMA             =
+
+# The XML_DTD tag can be used to specify an XML DTD,
+# which can be used by a validating XML parser to check the
+# syntax of the XML files.
+
+XML_DTD                =
+
+# If the XML_PROGRAMLISTING tag is set to YES Doxygen will
+# dump the program listings (including syntax highlighting
+# and cross-referencing information) to the XML output. Note that
+# enabling this will significantly increase the size of the XML output.
+
+XML_PROGRAMLISTING     = YES
+
+#---------------------------------------------------------------------------
+# configuration options for the AutoGen Definitions output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_AUTOGEN_DEF tag is set to YES Doxygen will
+# generate an AutoGen Definitions (see autogen.sf.net) file
+# that captures the structure of the code including all
+# documentation. Note that this feature is still experimental
+# and incomplete at the moment.
+
+GENERATE_AUTOGEN_DEF   = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the Perl module output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_PERLMOD tag is set to YES Doxygen will
+# generate a Perl module file that captures the structure of
+# the code including all documentation. Note that this
+# feature is still experimental and incomplete at the
+# moment.
+
+GENERATE_PERLMOD       = NO
+
+# If the PERLMOD_LATEX tag is set to YES Doxygen will generate
+# the necessary Makefile rules, Perl scripts and LaTeX code to be able
+# to generate PDF and DVI output from the Perl module output.
+
+PERLMOD_LATEX          = NO
+
+# If the PERLMOD_PRETTY tag is set to YES the Perl module output will be
+# nicely formatted so it can be parsed by a human reader.
+# This is useful
+# if you want to understand what is going on.
+# On the other hand, if this
+# tag is set to NO the size of the Perl module output will be much smaller
+# and Perl will parse it just the same.
+
+PERLMOD_PRETTY         = YES
+
+# The names of the make variables in the generated doxyrules.make file
+# are prefixed with the string contained in PERLMOD_MAKEVAR_PREFIX.
+# This is useful so different doxyrules.make files included by the same
+# Makefile don't overwrite each other's variables.
+
+PERLMOD_MAKEVAR_PREFIX =
+
+#---------------------------------------------------------------------------
+# Configuration options related to the preprocessor
+#---------------------------------------------------------------------------
+
+# If the ENABLE_PREPROCESSING tag is set to YES (the default) Doxygen will
+# evaluate all C-preprocessor directives found in the sources and include
+# files.
+
+ENABLE_PREPROCESSING   = YES
+
+# If the MACRO_EXPANSION tag is set to YES Doxygen will expand all macro
+# names in the source code. If set to NO (the default) only conditional
+# compilation will be performed. Macro expansion can be done in a controlled
+# way by setting EXPAND_ONLY_PREDEF to YES.
+
+MACRO_EXPANSION        = NO
+
+# If the EXPAND_ONLY_PREDEF and MACRO_EXPANSION tags are both set to YES
+# then the macro expansion is limited to the macros specified with the
+# PREDEFINED and EXPAND_AS_DEFINED tags.
+
+EXPAND_ONLY_PREDEF     = NO
+
+# If the SEARCH_INCLUDES tag is set to YES (the default) the includes files
+# pointed to by INCLUDE_PATH will be searched when a #include is found.
+
+SEARCH_INCLUDES        = YES
+
+# The INCLUDE_PATH tag can be used to specify one or more directories that
+# contain include files that are not input files but should be processed by
+# the preprocessor.
+
+INCLUDE_PATH           =
+
+# You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard
+# patterns (like *.h and *.hpp) to filter out the header-files in the
+# directories. If left blank, the patterns specified with FILE_PATTERNS will
+# be used.
+
+INCLUDE_FILE_PATTERNS  =
+
+# The PREDEFINED tag can be used to specify one or more macro names that
+# are defined before the preprocessor is started (similar to the -D option of
+# gcc). The argument of the tag is a list of macros of the form: name
+# or name=definition (no spaces). If the definition and the = are
+# omitted =1 is assumed. To prevent a macro definition from being
+# undefined via #undef or recursively expanded use the := operator
+# instead of the = operator.
+
+PREDEFINED             =
+
+# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then
+# this tag can be used to specify a list of macro names that should be expanded.
+# The macro definition that is found in the sources will be used.
+# Use the PREDEFINED tag if you want to use a different macro definition that
+# overrules the definition found in the source code.
+
+EXPAND_AS_DEFINED      =
+
+# If the SKIP_FUNCTION_MACROS tag is set to YES (the default) then
+# doxygen's preprocessor will remove all references to function-like macros
+# that are alone on a line, have an all uppercase name, and do not end with a
+# semicolon, because these will confuse the parser if not removed.
+
+SKIP_FUNCTION_MACROS   = YES
+
+#---------------------------------------------------------------------------
+# Configuration::additions related to external references
+#---------------------------------------------------------------------------
+
+# The TAGFILES option can be used to specify one or more tagfiles. For each
+# tag file the location of the external documentation should be added. The
+# format of a tag file without this location is as follows:
+#
+# TAGFILES = file1 file2 ...
+# Adding location for the tag files is done as follows:
+#
+# TAGFILES = file1=loc1 "file2 = loc2" ...
+# where "loc1" and "loc2" can be relative or absolute paths
+# or URLs. Note that each tag file must have a unique name (where the name does
+# NOT include the path). If a tag file is not located in the directory in which
+# doxygen is run, you must also specify the path to the tagfile here.
+
+TAGFILES               =
+
+# When a file name is specified after GENERATE_TAGFILE, doxygen will create
+# a tag file that is based on the input files it reads.
+
+GENERATE_TAGFILE       =
+
+# If the ALLEXTERNALS tag is set to YES all external classes will be listed
+# in the class index. If set to NO only the inherited external classes
+# will be listed.
+
+ALLEXTERNALS           = NO
+
+# If the EXTERNAL_GROUPS tag is set to YES all external groups will be listed
+# in the modules index. If set to NO, only the current project's groups will
+# be listed.
+
+EXTERNAL_GROUPS        = YES
+
+# The PERL_PATH should be the absolute path and name of the perl script
+# interpreter (i.e. the result of `which perl').
+
+PERL_PATH              = /usr/bin/perl
+
+#---------------------------------------------------------------------------
+# Configuration options related to the dot tool
+#---------------------------------------------------------------------------
+
+# If the CLASS_DIAGRAMS tag is set to YES (the default) Doxygen will
+# generate a inheritance diagram (in HTML, RTF and LaTeX) for classes with base
+# or super classes. Setting the tag to NO turns the diagrams off. Note that
+# this option also works with HAVE_DOT disabled, but it is recommended to
+# install and use dot, since it yields more powerful graphs.
+
+CLASS_DIAGRAMS         = YES
+
+# You can define message sequence charts within doxygen comments using the \msc
+# command. Doxygen will then run the mscgen tool (see
+# http://www.mcternan.me.uk/mscgen/) to produce the chart and insert it in the
+# documentation. The MSCGEN_PATH tag allows you to specify the directory where
+# the mscgen tool resides. If left empty the tool is assumed to be found in the
+# default search path.
+
+MSCGEN_PATH            =
+
+# If set to YES, the inheritance and collaboration graphs will hide
+# inheritance and usage relations if the target is undocumented
+# or is not a class.
+
+HIDE_UNDOC_RELATIONS   = YES
+
+# If you set the HAVE_DOT tag to YES then doxygen will assume the dot tool is
+# available from the path. This tool is part of Graphviz, a graph visualization
+# toolkit from AT&T and Lucent Bell Labs. The other options in this section
+# have no effect if this option is set to NO (the default)
+
+HAVE_DOT               = NO
+
+# The DOT_NUM_THREADS specifies the number of dot invocations doxygen is
+# allowed to run in parallel. When set to 0 (the default) doxygen will
+# base this on the number of processors available in the system. You can set it
+# explicitly to a value larger than 0 to get control over the balance
+# between CPU load and processing speed.
+
+DOT_NUM_THREADS        = 0
+
+# By default doxygen will use the Helvetica font for all dot files that
+# doxygen generates. When you want a differently looking font you can specify
+# the font name using DOT_FONTNAME. You need to make sure dot is able to find
+# the font, which can be done by putting it in a standard location or by setting
+# the DOTFONTPATH environment variable or by setting DOT_FONTPATH to the
+# directory containing the font.
+
+DOT_FONTNAME           = Helvetica
+
+# The DOT_FONTSIZE tag can be used to set the size of the font of dot graphs.
+# The default size is 10pt.
+
+DOT_FONTSIZE           = 10
+
+# By default doxygen will tell dot to use the Helvetica font.
+# If you specify a different font using DOT_FONTNAME you can use DOT_FONTPATH to
+# set the path where dot can find it.
+
+DOT_FONTPATH           =
+
+# If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for each documented class showing the direct and
+# indirect inheritance relations. Setting this tag to YES will force the
+# CLASS_DIAGRAMS tag to NO.
+
+CLASS_GRAPH            = YES
+
+# If the COLLABORATION_GRAPH and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for each documented class showing the direct and
+# indirect implementation dependencies (inheritance, containment, and
+# class references variables) of the class with other documented classes.
+
+COLLABORATION_GRAPH    = YES
+
+# If the GROUP_GRAPHS and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for groups, showing the direct groups dependencies
+
+GROUP_GRAPHS           = YES
+
+# If the UML_LOOK tag is set to YES doxygen will generate inheritance and
+# collaboration diagrams in a style similar to the OMG's Unified Modeling
+# Language.
+
+UML_LOOK               = NO
+
+# If the UML_LOOK tag is enabled, the fields and methods are shown inside
+# the class node. If there are many fields or methods and many nodes the
+# graph may become too big to be useful. The UML_LIMIT_NUM_FIELDS
+# threshold limits the number of items for each type to make the size more
+# managable. Set this to 0 for no limit. Note that the threshold may be
+# exceeded by 50% before the limit is enforced.
+
+UML_LIMIT_NUM_FIELDS   = 10
+
+# If set to YES, the inheritance and collaboration graphs will show the
+# relations between templates and their instances.
+
+TEMPLATE_RELATIONS     = NO
+
+# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDE_GRAPH, and HAVE_DOT
+# tags are set to YES then doxygen will generate a graph for each documented
+# file showing the direct and indirect include dependencies of the file with
+# other documented files.
+
+INCLUDE_GRAPH          = YES
+
+# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDED_BY_GRAPH, and
+# HAVE_DOT tags are set to YES then doxygen will generate a graph for each
+# documented header file showing the documented files that directly or
+# indirectly include this file.
+
+INCLUDED_BY_GRAPH      = YES
+
+# If the CALL_GRAPH and HAVE_DOT options are set to YES then
+# doxygen will generate a call dependency graph for every global function
+# or class method. Note that enabling this option will significantly increase
+# the time of a run. So in most cases it will be better to enable call graphs
+# for selected functions only using the \callgraph command.
+
+CALL_GRAPH             = NO
+
+# If the CALLER_GRAPH and HAVE_DOT tags are set to YES then
+# doxygen will generate a caller dependency graph for every global function
+# or class method. Note that enabling this option will significantly increase
+# the time of a run. So in most cases it will be better to enable caller
+# graphs for selected functions only using the \callergraph command.
+
+CALLER_GRAPH           = NO
+
+# If the GRAPHICAL_HIERARCHY and HAVE_DOT tags are set to YES then doxygen
+# will generate a graphical hierarchy of all classes instead of a textual one.
+
+GRAPHICAL_HIERARCHY    = YES
+
+# If the DIRECTORY_GRAPH, SHOW_DIRECTORIES and HAVE_DOT tags are set to YES
+# then doxygen will show the dependencies a directory has on other directories
+# in a graphical way. The dependency relations are determined by the #include
+# relations between the files in the directories.
+
+DIRECTORY_GRAPH        = YES
+
+# The DOT_IMAGE_FORMAT tag can be used to set the image format of the images
+# generated by dot. Possible values are svg, png, jpg, or gif.
+# If left blank png will be used. If you choose svg you need to set
+# HTML_FILE_EXTENSION to xhtml in order to make the SVG files
+# visible in IE 9+ (other browsers do not have this requirement).
+
+DOT_IMAGE_FORMAT       = png
+
+# If DOT_IMAGE_FORMAT is set to svg, then this option can be set to YES to
+# enable generation of interactive SVG images that allow zooming and panning.
+# Note that this requires a modern browser other than Internet Explorer.
+# Tested and working are Firefox, Chrome, Safari, and Opera. For IE 9+ you
+# need to set HTML_FILE_EXTENSION to xhtml in order to make the SVG files
+# visible. Older versions of IE do not have SVG support.
+
+INTERACTIVE_SVG        = NO
+
+# The tag DOT_PATH can be used to specify the path where the dot tool can be
+# found. If left blank, it is assumed the dot tool can be found in the path.
+
+DOT_PATH               =
+
+# The DOTFILE_DIRS tag can be used to specify one or more directories that
+# contain dot files that are included in the documentation (see the
+# \dotfile command).
+
+DOTFILE_DIRS           =
+
+# The MSCFILE_DIRS tag can be used to specify one or more directories that
+# contain msc files that are included in the documentation (see the
+# \mscfile command).
+
+MSCFILE_DIRS           =
+
+# The DOT_GRAPH_MAX_NODES tag can be used to set the maximum number of
+# nodes that will be shown in the graph. If the number of nodes in a graph
+# becomes larger than this value, doxygen will truncate the graph, which is
+# visualized by representing a node as a red box. Note that doxygen if the
+# number of direct children of the root node in a graph is already larger than
+# DOT_GRAPH_MAX_NODES then the graph will not be shown at all. Also note
+# that the size of a graph can be further restricted by MAX_DOT_GRAPH_DEPTH.
+
+DOT_GRAPH_MAX_NODES    = 50
+
+# The MAX_DOT_GRAPH_DEPTH tag can be used to set the maximum depth of the
+# graphs generated by dot. A depth value of 3 means that only nodes reachable
+# from the root by following a path via at most 3 edges will be shown. Nodes
+# that lay further from the root node will be omitted. Note that setting this
+# option to 1 or 2 may greatly reduce the computation time needed for large
+# code bases. Also note that the size of a graph can be further restricted by
+# DOT_GRAPH_MAX_NODES. Using a depth of 0 means no depth restriction.
+
+MAX_DOT_GRAPH_DEPTH    = 0
+
+# Set the DOT_TRANSPARENT tag to YES to generate images with a transparent
+# background. This is disabled by default, because dot on Windows does not
+# seem to support this out of the box. Warning: Depending on the platform used,
+# enabling this option may lead to badly anti-aliased labels on the edges of
+# a graph (i.e. they become hard to read).
+
+DOT_TRANSPARENT        = NO
+
+# Set the DOT_MULTI_TARGETS tag to YES allow dot to generate multiple output
+# files in one run (i.e. multiple -o and -T options on the command line). This
+# makes dot run faster, but since only newer versions of dot (>1.8.10)
+# support this, this feature is disabled by default.
+
+DOT_MULTI_TARGETS      = NO
+
+# If the GENERATE_LEGEND tag is set to YES (the default) Doxygen will
+# generate a legend page explaining the meaning of the various boxes and
+# arrows in the dot generated graphs.
+
+GENERATE_LEGEND        = YES
+
+# If the DOT_CLEANUP tag is set to YES (the default) Doxygen will
+# remove the intermediate dot files that are used to generate
+# the various graphs.
+
+DOT_CLEANUP            = YES
diff --git a/LICENSE b/LICENSE
new file mode 100644 (file)
index 0000000..d159169
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,339 @@
+                    GNU GENERAL PUBLIC LICENSE
+                       Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The licenses for most software are designed to take away your
+freedom to share and change it.  By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users.  This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it.  (Some other Free Software Foundation software is covered by
+the GNU Lesser General Public License instead.)  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+  To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have.  You must make sure that they, too, receive or can get the
+source code.  And you must show them these terms so they know their
+rights.
+
+  We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+  Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software.  If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+  Finally, any free program is threatened constantly by software
+patents.  We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary.  To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                    GNU GENERAL PUBLIC LICENSE
+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+  0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License.  The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language.  (Hereinafter, translation is included without limitation in
+the term "modification".)  Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope.  The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+  1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+  2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+    a) You must cause the modified files to carry prominent notices
+    stating that you changed the files and the date of any change.
+
+    b) You must cause any work that you distribute or publish, that in
+    whole or in part contains or is derived from the Program or any
+    part thereof, to be licensed as a whole at no charge to all third
+    parties under the terms of this License.
+
+    c) If the modified program normally reads commands interactively
+    when run, you must cause it, when started running for such
+    interactive use in the most ordinary way, to print or display an
+    announcement including an appropriate copyright notice and a
+    notice that there is no warranty (or else, saying that you provide
+    a warranty) and that users may redistribute the program under
+    these conditions, and telling the user how to view a copy of this
+    License.  (Exception: if the Program itself is interactive but
+    does not normally print such an announcement, your work based on
+    the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole.  If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works.  But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+  3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+    a) Accompany it with the complete corresponding machine-readable
+    source code, which must be distributed under the terms of Sections
+    1 and 2 above on a medium customarily used for software interchange; or,
+
+    b) Accompany it with a written offer, valid for at least three
+    years, to give any third party, for a charge no more than your
+    cost of physically performing source distribution, a complete
+    machine-readable copy of the corresponding source code, to be
+    distributed under the terms of Sections 1 and 2 above on a medium
+    customarily used for software interchange; or,
+
+    c) Accompany it with the information you received as to the offer
+    to distribute corresponding source code.  (This alternative is
+    allowed only for noncommercial distribution and only if you
+    received the program in object code or executable form with such
+    an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it.  For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable.  However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+  4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License.  Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+  5. You are not required to accept this License, since you have not
+signed it.  However, nothing else grants you permission to modify or
+distribute the Program or its derivative works.  These actions are
+prohibited by law if you do not accept this License.  Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+  6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions.  You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+  7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all.  For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices.  Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+  8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded.  In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+  9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number.  If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation.  If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+  10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission.  For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this.  Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+                            NO WARRANTY
+
+  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+                     END OF TERMS AND CONDITIONS
+
+            How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+    Gnomovision version 69, Copyright (C) year name of author
+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary.  Here is a sample; alter the names:
+
+  Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+  `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+  <signature of Ty Coon>, 1 April 1989
+  Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs.  If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.
diff --git a/Makefile b/Makefile
new file mode 100644 (file)
index 0000000..f44a895
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,85 @@
+include common.mk
+
+OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
+          nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
+          datarace.o impatomic.o cmodelint.o \
+          snapshot.o malloc.o mymemory.o common.o mutex.o promise.o conditionvariable.o \
+          context.o scanalysis.o execution.o plugins.o libannotate.o
+
+CPPFLAGS += -Iinclude -I.
+LDFLAGS := -ldl -lrt -rdynamic
+SHARED := -shared
+
+# Mac OSX options
+ifeq ($(UNAME), Darwin)
+LDFLAGS := -ldl
+SHARED := -Wl,-undefined,dynamic_lookup -dynamiclib
+endif
+
+TESTS_DIR := test
+
+MARKDOWN := doc/Markdown/Markdown.pl
+
+all: $(LIB_SO) tests README.html
+
+debug: CPPFLAGS += -DCONFIG_DEBUG
+debug: all
+
+PHONY += docs
+docs: *.c *.cc *.h README.html
+       doxygen
+
+README.html: README.md
+       $(MARKDOWN) $< > $@
+
+$(LIB_SO): $(OBJECTS)
+       $(CXX) $(SHARED) -o $(LIB_SO) $+ $(LDFLAGS)
+
+malloc.o: malloc.c
+       $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable
+
+%.o: %.cc
+       $(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS)
+
+%.pdf: %.dot
+       dot -Tpdf $< -o $@
+
+-include $(OBJECTS:%=.%.d)
+
+PHONY += clean
+clean:
+       rm -f *.o *.so .*.d *.pdf *.dot
+       $(MAKE) -C $(TESTS_DIR) clean
+
+PHONY += mrclean
+mrclean: clean
+       rm -rf docs
+
+PHONY += tags
+tags:
+       ctags -R
+
+PHONY += tests
+tests: $(LIB_SO)
+       $(MAKE) -C $(TESTS_DIR)
+
+BENCH_DIR := benchmarks
+
+PHONY += benchmarks
+benchmarks: $(LIB_SO)
+       @if ! test -d $(BENCH_DIR); then \
+               echo "Directory $(BENCH_DIR) does not exist" && \
+               echo "Please clone the benchmarks repository" && \
+               echo && \
+               exit 1; \
+       fi
+       $(MAKE) -C $(BENCH_DIR)
+
+PHONY += pdfs
+pdfs: $(patsubst %.dot,%.pdf,$(wildcard *.dot))
+
+.PHONY: $(PHONY)
+
+# A 1-inch margin PDF generated by 'pandoc'
+%.pdf: %.md
+       pandoc -o $@ $< -V header-includes='\usepackage[margin=1in]{geometry}'
diff --git a/README.md b/README.md
new file mode 100644 (file)
index 0000000..ba64e18
--- /dev/null
+++ b/README.md
@@ -0,0 +1,410 @@
+CDSChecker: A Model Checker for C11 and C++11 Atomics
+=====================================================
+
+CDSChecker is a model checker for C11/C++11 which exhaustively explores the
+behaviors of code under the C/C++ memory model. It uses partial order reduction
+as well as a few other novel techniques to eliminate time spent on redundant
+execution behaviors and to significantly shrink the state space. The model
+checking algorithm is described in more detail in this paper (published in
+OOPSLA '13):
+
+>   <http://demsky.eecs.uci.edu/publications/c11modelcheck.pdf>
+
+It is designed to support unit tests on concurrent data structure written using
+C/C++ atomics.
+
+CDSChecker is constructed as a dynamically-linked shared library which
+implements the C and C++ atomic types and portions of the other thread-support
+libraries of C/C++ (e.g., std::atomic, std::mutex, etc.). Notably, we only
+support the C version of threads (i.e., `thrd_t` and similar, from `<threads.h>`),
+because C++ threads require features which are only available to a C++11
+compiler (and we want to support others, at least for now).
+
+CDSChecker should compile on Linux and Mac OSX with no dependencies and has been
+tested with LLVM (clang/clang++) and GCC. It likely can be ported to other \*NIX
+flavors. We have not attempted to port to Windows.
+
+
+Getting Started
+---------------
+
+If you haven't done so already, you may download CDSChecker using
+[git](http://git-scm.com/):
+
+      git clone git://demsky.eecs.uci.edu/model-checker.git
+
+Source code can also be downloaded via the snapshot links on Gitweb (found in
+the __See Also__ section).
+
+Get the benchmarks (not required; distributed separately), placing them as a
+subdirectory under the `model-checker` directory:
+
+      cd model-checker
+      git clone git://demsky.eecs.uci.edu/model-checker-benchmarks.git benchmarks
+
+Compile the model checker:
+
+      make
+
+Compile the benchmarks:
+
+      make benchmarks
+
+Run a simple example (the `run.sh` script does some very minimal processing for
+you):
+
+      ./run.sh test/userprog.o
+
+To see the help message on how to run CDSChecker, execute:
+
+      ./run.sh -h
+
+
+Useful Options
+--------------
+
+`-m num`
+
+  > Controls the liveness of the memory system. Note that multithreaded programs
+  > often rely on memory liveness for termination, so this parameter is
+  > necessary for such programs.
+  >
+  > Liveness is controlled by `num`: the number of times a load is allowed to
+  > see the same store when a newer store exists---one that is ordered later in
+  > the modification order.
+
+`-y`
+
+  > Turns on CHESS-like yield-based fairness support (requires `thrd_yield()`
+  > instrumentation in test program).
+
+`-f num`
+
+  > Turns on alternative fairness support (less desirable than `-y`). A
+  > necessary alternative for some programs that do not support yield-based
+  > fairness properly.
+
+`-v`
+
+  > Verbose: show all executions and not just buggy ones.
+
+`-s num`
+
+  > Constrain how long we will run to wait for a future value past when it is
+  > expected
+
+`-u num`
+
+  > Value to provide to atomics loads from uninitialized memory locations. The
+  > default is 0, but this may cause some programs to throw exceptions
+  > (segfault) before the model checker prints a trace.
+
+Suggested options:
+
+>     -m 2 -y
+
+or
+
+>     -m 2 -f 10
+
+
+Benchmarks
+-------------------
+
+Many simple tests are located in the `tests/` directory. You may also want to
+try the larger benchmarks (distributed separately), which can be placed under
+the `benchmarks/` directory. After building CDSChecker, you can build and run
+the benchmarks as follows:
+
+>     make benchmarks
+>     cd benchmarks
+>
+>     # run barrier test with fairness/memory liveness
+>     ./run.sh barrier/barrier -y -m 2
+>
+>     # Linux reader/write lock test with fairness/memory liveness
+>     ./run.sh linuxrwlocks/linuxrwlocks -y -m 2
+>
+>     # run all benchmarks and provide timing results
+>     ./bench.sh
+
+
+Running your own code
+---------------------
+
+You likely want to test your own code, not just our simple tests. To do so, you
+need to perform a few steps.
+
+First, because CDSChecker executes your program dozens (if not hundreds or
+thousands) of times, you will have the most success if your code is written as a
+unit test and not as a full-blown program.
+
+Second, because CDSChecker must be able to manage your program for you, your
+program should declare its main entry point as `user_main(int, char**)` rather
+than `main(int, char**)`.
+
+Third, test programs must use the standard C11/C++11 library headers (see below
+for supported APIs) and must compile against the versions provided in
+CDSChecker's `include/` directory. Notably, we only support C11 thread syntax
+(`thrd_t`, etc. from `<thread.h>`).
+
+Test programs may also use our included happens-before race detector by
+including <librace.h> and utilizing the appropriate functions
+(`store_{8,16,32,64}()` and `load_{8,16,32,64}()`) for storing/loading data
+to/from non-atomic shared memory.
+
+CDSChecker can also check boolean assertions in your test programs. Just
+include `<model-assert.h>` and use the `MODEL_ASSERT()` macro in your test program.
+CDSChecker will report a bug in any possible execution in which the argument to
+`MODEL_ASSERT()` evaluates to false (that is, 0).
+
+Test programs should be compiled against our shared library (libmodel.so) using
+the headers in the `include/` directory. Then the shared library must be made
+available to the dynamic linker, using the `LD_LIBRARY_PATH` environment
+variable, for instance.
+
+
+### Supported C11/C++11 APIs ###
+
+To model-check multithreaded code properly, CDSChecker needs to instrument any
+concurrency-related API calls made in your code. Currently, we support parts of
+the following thread-support libraries. The C versions can be used in either C
+or C++.
+
+* `<atomic>`, `<cstdatomic>`, `<stdatomic.h>`
+* `<condition_variable>`
+* `<mutex>`
+* `<threads.h>`
+
+Because we want to extend support to legacy (i.e., non-C++11) compilers, we do
+not support some new C++11 features that can't be implemented in C++03 (e.g.,
+C++ `<thread>`).
+
+Reading an execution trace
+--------------------------
+
+When CDSChecker detects a bug in your program (or when run with the `--verbose`
+flag), it prints the output of the program run (STDOUT) along with some summary
+trace information for the execution in question. The trace is given as a
+sequence of lines, where each line represents an operation in the execution
+trace. These lines are ordered by the order in which they were run by CDSChecker
+(i.e., the "execution order"), which does not necessarily align with the "order"
+of the values observed (i.e., the modification order or the reads-from
+relation).
+
+The following list describes each of the columns in the execution trace output:
+
+ * \#: The sequence number within the execution. That is, sequence number "9"
+   means the operation was the 9th operation executed by CDSChecker. Note that
+   this represents the execution order, not necessarily any other order (e.g.,
+   modification order or reads-from).
+
+ * t: The thread number
+
+ * Action type: The type of operation performed
+
+ * MO: The memory-order for this operation (i.e., `memory_order_XXX`, where `XXX` is
+   `relaxed`, `release`, `acquire`, `rel_acq`, or `seq_cst`)
+
+ * Location: The memory location on which this operation is operating. This is
+   well-defined for atomic write/read/RMW, but other operations are subject to
+   CDSChecker implementation details.
+
+ * Value: For reads/writes/RMW, the value returned by the operation. Note that
+   for RMW, this is the value that is *read*, not the value that was *written*.
+   For other operations, 'value' may have some CDSChecker-internal meaning, or
+   it may simply be a don't-care (such as `0xdeadbeef`).
+
+ * Rf: For reads, the sequence number of the operation from which it reads.
+   [Note: If the execution is a partial, infeasible trace (labeled INFEASIBLE),
+   as printed during `--verbose` execution, reads may not be resolved and so may
+   have Rf=? or Rf=Px, where x is a promised future value.]
+
+ * CV: The clock vector, encapsulating the happens-before relation (see our
+   paper, or the C/C++ memory model itself). We use a Lamport-style clock vector
+   similar to [1]. The "clock" is just the sequence number (#). The clock vector
+   can be read as follows:
+
+   Each entry is indexed as CV[i], where
+
+            i = 0, 1, 2, ..., <number of threads>
+
+   So for any thread i, we say CV[i] is the sequence number of the most recent
+   operation in thread i such that operation i happens-before this operation.
+   Notably, thread 0 is reserved as a dummy thread for certain CDSChecker
+   operations.
+
+See the following example trace:
+
+    ------------------------------------------------------------------------------------
+    #    t    Action type     MO       Location         Value               Rf  CV
+    ------------------------------------------------------------------------------------
+    1    1    thread start    seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0,  1)
+    2    1    init atomic     relaxed        0x601068   0                       ( 0,  2)
+    3    1    init atomic     relaxed        0x60106c   0                       ( 0,  3)
+    4    1    thread create   seq_cst  0x7f68fe51c710   0x7f68fe51c6e0          ( 0,  4)
+    5    2    thread start    seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4,  5)
+    6    2    atomic read     relaxed        0x60106c   0                   3   ( 0,  4,  6)
+    7    1    thread create   seq_cst  0x7f68fe51c720   0x7f68fe51c6e0          ( 0,  7)
+    8    3    thread start    seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0,  8)
+    9    2    atomic write    relaxed        0x601068   0                       ( 0,  4,  9)
+    10   3    atomic read     relaxed        0x601068   0                   2   ( 0,  7,  0, 10)
+    11   2    thread finish   seq_cst  0x7f68ff11ebc0   0xdeadbeef              ( 0,  4, 11)
+    12   3    atomic write    relaxed        0x60106c   0x2a                    ( 0,  7,  0, 12)
+    13   1    thread join     seq_cst  0x7f68ff11ebc0   0x2                     ( 0, 13, 11)
+    14   3    thread finish   seq_cst  0x7f68ff11efc0   0xdeadbeef              ( 0,  7,  0, 14)
+    15   1    thread join     seq_cst  0x7f68ff11efc0   0x3                     ( 0, 15, 11, 14)
+    16   1    thread finish   seq_cst  0x7f68ff11e7c0   0xdeadbeef              ( 0, 16, 11, 14)
+    HASH 4073708854
+    ------------------------------------------------------------------------------------
+
+Now consider, for example, operation 10:
+
+This is the 10th operation in the execution order. It is an atomic read-relaxed
+operation performed by thread 3 at memory address `0x601068`. It reads the value
+"0", which was written by the 2nd operation in the execution order. Its clock
+vector consists of the following values:
+
+        CV[0] = 0, CV[1] = 7, CV[2] = 0, CV[3] = 10
+
+End of Execution Summary
+------------------------
+
+CDSChecker prints summary statistics at the end of each execution. These
+summaries are based off of a few different properties of an execution, which we
+will break down here:
+
+* An _infeasible_ execution is an execution which is not consistent with the
+  memory model. Such an execution can be considered overhead for the
+  model-checker, since it should never appear in practice.
+
+* A _buggy_ execution is an execution in which CDSChecker has found a real
+  bug: a data race, a deadlock, failure of a user-provided assertion, or an
+  uninitialized load, for instance. CDSChecker will only report bugs in feasible
+  executions.
+
+* A _redundant_ execution is a feasible execution that is exploring the same
+  state space explored by a previous feasible execution. Such exploration is
+  another instance of overhead, so CDSChecker terminates these executions as
+  soon as they are detected. CDSChecker is mostly able to avoid such executions
+  but may encounter them if a fairness option is enabled.
+
+Now, we can examine the end-of-execution summary of one test program:
+
+    $ ./run.sh test/rmwprog.o
+    + test/rmwprog.o
+    ******* Model-checking complete: *******
+    Number of complete, bug-free executions: 6
+    Number of redundant executions: 0
+    Number of buggy executions: 0
+    Number of infeasible executions: 29
+    Total executions: 35
+
+* _Number of complete, bug-free executions:_ these are feasible, non-buggy, and
+  non-redundant executions. They each represent different, legal behaviors you
+  can expect to see in practice.
+
+* _Number of redundant executions:_ these are feasible but redundant executions
+  that were terminated as soon as CDSChecker noticed the redundancy.
+
+* _Number of buggy executions:_ these are feasible, buggy executions. These are
+  the trouble spots where your program is triggering a bug or assertion.
+  Ideally, this number should be 0.
+
+* _Number of infeasible executions:_ these are infeasible executions,
+  representing some of the overhead of model-checking.
+
+* _Total executions:_ the total number of executions explored by CDSChecker.
+  Should be the sum of the above categories, since they are mutually exclusive.
+
+
+Other Notes and Pitfalls
+------------------------
+
+* Many programs require some form of fairness in order to terminate in a finite
+  amount of time. CDSChecker supports the `-y num` and `-f num` flags for these
+  cases. The `-y` option (yield-based fairness) is preferable, but it requires
+  careful usage of yields (i.e., `thrd_yield()`) in the test program. For
+  programs without proper `thrd_yield()`, you may consider using `-f` instead.
+
+* Deadlock detection: CDSChecker can detect deadlocks. For instance, try the
+  following test program.
+
+  >     ./run.sh test/deadlock.o
+
+  Deadlock detection currently detects when a thread is about to step into a
+  deadlock, without actually including the final step in the trace. But you can
+  examine the program to see the next step.
+
+* CDSChecker has to speculatively explore many execution behaviors due to the
+  relaxed memory model, and many of these turn out to be infeasible (that is,
+  they cannot be legally produced by the memory model). CDSChecker discards
+  these executions as soon as it identifies them (see the "Number of infeasible
+  executions" statistic); however, the speculation can occasionally cause
+  CDSChecker to hit unexpected parts of the unit test program (causing a
+  division by 0, for instance). In such programs, you might consider running
+  CDSChecker with the `-u num` option.
+
+* Related to the previous point, CDSChecker may report more than one bug for a
+  particular candidate execution. This is because some bugs may not be
+  reportable until CDSChecker has explored more of the program, and in the
+  time between initial discovery and final assessment of the bug, CDSChecker may
+  discover another bug.
+
+* Data races may be reported as multiple bugs, one for each byte-address of the
+  data race in question. See, for example, this run:
+
+        $ ./run.sh test/releaseseq.o
+        ...
+        Bug report: 4 bugs detected
+          [BUG] Data race detected @ address 0x601078:
+            Access 1: write in thread  2 @ clock   4
+            Access 2:  read in thread  3 @ clock   9
+          [BUG] Data race detected @ address 0x601079:
+            Access 1: write in thread  2 @ clock   4
+            Access 2:  read in thread  3 @ clock   9
+          [BUG] Data race detected @ address 0x60107a:
+            Access 1: write in thread  2 @ clock   4
+            Access 2:  read in thread  3 @ clock   9
+          [BUG] Data race detected @ address 0x60107b:
+            Access 1: write in thread  2 @ clock   4
+            Access 2:  read in thread  3 @ clock   9
+
+
+See Also
+--------
+
+The CDSChecker project page:
+
+>   <http://demsky.eecs.uci.edu/c11modelchecker.html>
+
+The CDSChecker source and accompanying benchmarks on Gitweb:
+
+>   <http://demsky.eecs.uci.edu/git/?p=model-checker.git>
+>
+>   <http://demsky.eecs.uci.edu/git/?p=model-checker-benchmarks.git>
+
+
+Contact
+-------
+
+Please feel free to contact us for more information. Bug reports are welcome,
+and we are happy to hear from our users. We are also very interested to know if
+CDSChecker catches bugs in your programs.
+
+Contact Brian Norris at <banorris@uci.edu> or Brian Demsky at <bdemsky@uci.edu>.
+
+
+Copyright
+---------
+
+Copyright &copy; 2013 Regents of the University of California. All rights reserved.
+
+CDSChecker is distributed under the GPL v2. See the LICENSE file for details.
+
+
+References
+----------
+
+[1] L. Lamport. Time, clocks, and the ordering of events in a distributed
+    system. CACM, 21(7):558-565, July 1978.
diff --git a/action.cc b/action.cc
new file mode 100644 (file)
index 0000000..2010a0b
--- /dev/null
+++ b/action.cc
@@ -0,0 +1,658 @@
+#include <stdio.h>
+#define __STDC_FORMAT_MACROS
+#include <inttypes.h>
+#include <stdlib.h>
+
+#include "model.h"
+#include "action.h"
+#include "clockvector.h"
+#include "common.h"
+#include "threads-model.h"
+#include "nodestack.h"
+
+#define ACTION_INITIAL_CLOCK 0
+
+/** @brief A special value to represent a successful trylock */
+#define VALUE_TRYSUCCESS 1
+
+/** @brief A special value to represent a failed trylock */
+#define VALUE_TRYFAILED 0
+
+/**
+ * @brief Construct a new ModelAction
+ *
+ * @param type The type of action
+ * @param order The memory order of this action. A "don't care" for non-ATOMIC
+ * actions (e.g., THREAD_* or MODEL_* actions).
+ * @param loc The location that this action acts upon
+ * @param value (optional) A value associated with the action (e.g., the value
+ * read or written). Defaults to a given macro constant, for debugging purposes.
+ * @param thread (optional) The Thread in which this action occurred. If NULL
+ * (default), then a Thread is assigned according to the scheduler.
+ */
+ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
+               uint64_t value, Thread *thread) :
+       type(type),
+       order(order),
+       location(loc),
+       value(value),
+       reads_from(NULL),
+       reads_from_promise(NULL),
+       last_fence_release(NULL),
+       node(NULL),
+       seq_number(ACTION_INITIAL_CLOCK),
+       cv(NULL),
+       sleep_flag(false)
+{
+       /* References to NULL atomic variables can end up here */
+       ASSERT(loc || type == ATOMIC_FENCE || type == MODEL_FIXUP_RELSEQ);
+
+       Thread *t = thread ? thread : thread_current();
+       this->tid = t->get_id();
+}
+
+/** @brief ModelAction destructor */
+ModelAction::~ModelAction()
+{
+       /**
+        * We can't free the clock vector:
+        * Clock vectors are snapshotting state. When we delete model actions,
+        * they are at the end of the node list and have invalid old clock
+        * vectors which have already been rolled back to an unallocated state.
+        */
+
+       /*
+        if (cv)
+               delete cv; */
+}
+
+void ModelAction::copy_from_new(ModelAction *newaction)
+{
+       seq_number = newaction->seq_number;
+}
+
+void ModelAction::set_seq_number(modelclock_t num)
+{
+       /* ATOMIC_UNINIT actions should never have non-zero clock */
+       ASSERT(!is_uninitialized());
+       ASSERT(seq_number == ACTION_INITIAL_CLOCK);
+       seq_number = num;
+}
+
+bool ModelAction::is_thread_start() const
+{
+       return type == THREAD_START;
+}
+
+bool ModelAction::is_thread_join() const
+{
+       return type == THREAD_JOIN;
+}
+
+bool ModelAction::is_relseq_fixup() const
+{
+       return type == MODEL_FIXUP_RELSEQ;
+}
+
+bool ModelAction::is_mutex_op() const
+{
+       return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
+}
+
+bool ModelAction::is_lock() const
+{
+       return type == ATOMIC_LOCK;
+}
+
+bool ModelAction::is_wait() const {
+       return type == ATOMIC_WAIT;
+}
+
+bool ModelAction::is_notify() const {
+       return type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
+}
+
+bool ModelAction::is_notify_one() const {
+       return type == ATOMIC_NOTIFY_ONE;
+}
+
+bool ModelAction::is_unlock() const
+{
+       return type == ATOMIC_UNLOCK;
+}
+
+bool ModelAction::is_trylock() const
+{
+       return type == ATOMIC_TRYLOCK;
+}
+
+bool ModelAction::is_success_lock() const
+{
+       return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
+}
+
+bool ModelAction::is_failed_trylock() const
+{
+       return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
+}
+
+/** @return True if this operation is performed on a C/C++ atomic variable */
+bool ModelAction::is_atomic_var() const
+{
+       return is_read() || could_be_write();
+}
+
+bool ModelAction::is_uninitialized() const
+{
+       return type == ATOMIC_UNINIT;
+}
+
+bool ModelAction::is_read() const
+{
+       return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;
+}
+
+bool ModelAction::is_write() const
+{
+       return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT;
+}
+
+bool ModelAction::could_be_write() const
+{
+       return is_write() || is_rmwr();
+}
+
+bool ModelAction::is_yield() const
+{
+       return type == THREAD_YIELD;
+}
+
+bool ModelAction::is_rmwr() const
+{
+       return type == ATOMIC_RMWR;
+}
+
+bool ModelAction::is_rmw() const
+{
+       return type == ATOMIC_RMW;
+}
+
+bool ModelAction::is_rmwc() const
+{
+       return type == ATOMIC_RMWC;
+}
+
+bool ModelAction::is_fence() const
+{
+       return type == ATOMIC_FENCE;
+}
+
+bool ModelAction::is_initialization() const
+{
+       return type == ATOMIC_INIT;
+}
+
+bool ModelAction::is_annotation() const
+{
+       return type == ATOMIC_ANNOTATION;
+}
+
+bool ModelAction::is_relaxed() const
+{
+       return order == std::memory_order_relaxed;
+}
+
+bool ModelAction::is_acquire() const
+{
+       switch (order) {
+       case std::memory_order_acquire:
+       case std::memory_order_acq_rel:
+       case std::memory_order_seq_cst:
+               return true;
+       default:
+               return false;
+       }
+}
+
+bool ModelAction::is_release() const
+{
+       switch (order) {
+       case std::memory_order_release:
+       case std::memory_order_acq_rel:
+       case std::memory_order_seq_cst:
+               return true;
+       default:
+               return false;
+       }
+}
+
+bool ModelAction::is_seqcst() const
+{
+       return order == std::memory_order_seq_cst;
+}
+
+bool ModelAction::same_var(const ModelAction *act) const
+{
+       if (act->is_wait() || is_wait()) {
+               if (act->is_wait() && is_wait()) {
+                       if (((void *)value) == ((void *)act->value))
+                               return true;
+               } else if (is_wait()) {
+                       if (((void *)value) == act->location)
+                               return true;
+               } else if (act->is_wait()) {
+                       if (location == ((void *)act->value))
+                               return true;
+               }
+       }
+
+       return location == act->location;
+}
+
+bool ModelAction::same_thread(const ModelAction *act) const
+{
+       return tid == act->tid;
+}
+
+void ModelAction::copy_typeandorder(ModelAction * act)
+{
+       this->type = act->type;
+       this->order = act->order;
+}
+
+/**
+ * Get the Thread which is the operand of this action. This is only valid for
+ * THREAD_* operations (currently only for THREAD_CREATE and THREAD_JOIN). Note
+ * that this provides a central place for determining the conventions of Thread
+ * storage in ModelAction, where we generally aren't very type-safe (e.g., we
+ * store object references in a (void *) address.
+ *
+ * For THREAD_CREATE, this yields the Thread which is created.
+ * For THREAD_JOIN, this yields the Thread we are joining with.
+ *
+ * @return The Thread which this action acts on, if exists; otherwise NULL
+ */
+Thread * ModelAction::get_thread_operand() const
+{
+       if (type == THREAD_CREATE) {
+               /* THREAD_CREATE stores its (Thread *) in a thrd_t::priv */
+               thrd_t *thrd = (thrd_t *)get_location();
+               return thrd->priv;
+       } else if (type == THREAD_JOIN)
+               /* THREAD_JOIN uses (Thread *) for location */
+               return (Thread *)get_location();
+       else
+               return NULL;
+}
+
+/**
+ * @brief Convert the read portion of an RMW
+ *
+ * Changes an existing read part of an RMW action into either:
+ *  -# a full RMW action in case of the completed write or
+ *  -# a READ action in case a failed action.
+ *
+ * @todo  If the memory_order changes, we may potentially need to update our
+ * clock vector.
+ *
+ * @param act The second half of the RMW (either RMWC or RMW)
+ */
+void ModelAction::process_rmw(ModelAction *act)
+{
+       this->order = act->order;
+       if (act->is_rmwc())
+               this->type = ATOMIC_READ;
+       else if (act->is_rmw()) {
+               this->type = ATOMIC_RMW;
+               this->value = act->value;
+       }
+}
+
+/**
+ * @brief Check if this action should be backtracked with another, due to
+ * potential synchronization
+ *
+ * The is_synchronizing method should only explore interleavings if:
+ *  -# the operations are seq_cst and don't commute or
+ *  -# the reordering may establish or break a synchronization relation.
+ *
+ * Other memory operations will be dealt with by using the reads_from relation.
+ *
+ * @param act The action to consider exploring a reordering
+ * @return True, if we have to explore a reordering; otherwise false
+ */
+bool ModelAction::could_synchronize_with(const ModelAction *act) const
+{
+       // Same thread can't be reordered
+       if (same_thread(act))
+               return false;
+
+       // Different locations commute
+       if (!same_var(act))
+               return false;
+
+       // Explore interleavings of seqcst writes/fences to guarantee total
+       // order of seq_cst operations that don't commute
+       if ((could_be_write() || act->could_be_write() || is_fence() || act->is_fence()) && is_seqcst() && act->is_seqcst())
+               return true;
+
+       // Explore synchronizing read/write pairs
+       if (is_acquire() && act->is_release() && is_read() && act->could_be_write())
+               return true;
+
+       // lock just released...we can grab lock
+       if ((is_lock() || is_trylock()) && (act->is_unlock() || act->is_wait()))
+               return true;
+
+       // lock just acquired...we can fail to grab lock
+       if (is_trylock() && act->is_success_lock())
+               return true;
+
+       // other thread stalling on lock...we can release lock
+       if (is_unlock() && (act->is_trylock() || act->is_lock()))
+               return true;
+
+       if (is_trylock() && (act->is_unlock() || act->is_wait()))
+               return true;
+
+       if (is_notify() && act->is_wait())
+               return true;
+
+       if (is_wait() && act->is_notify())
+               return true;
+
+       // Otherwise handle by reads_from relation
+       return false;
+}
+
+bool ModelAction::is_conflicting_lock(const ModelAction *act) const
+{
+       // Must be different threads to reorder
+       if (same_thread(act))
+               return false;
+
+       // Try to reorder a lock past a successful lock
+       if (act->is_success_lock())
+               return true;
+
+       // Try to push a successful trylock past an unlock
+       if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
+               return true;
+
+       // Try to push a successful trylock past a wait
+       if (act->is_wait() && is_trylock() && value == VALUE_TRYSUCCESS)
+               return true;
+
+       return false;
+}
+
+/**
+ * Create a new clock vector for this action. Note that this function allows a
+ * user to clobber (and leak) a ModelAction's existing clock vector. A user
+ * should ensure that the vector has already either been rolled back
+ * (effectively "freed") or freed.
+ *
+ * @param parent A ModelAction from which to inherit a ClockVector
+ */
+void ModelAction::create_cv(const ModelAction *parent)
+{
+       if (parent)
+               cv = new ClockVector(parent->cv, this);
+       else
+               cv = new ClockVector(NULL, this);
+}
+
+void ModelAction::set_try_lock(bool obtainedlock)
+{
+       value = obtainedlock ? VALUE_TRYSUCCESS : VALUE_TRYFAILED;
+}
+
+/**
+ * @brief Get the value read by this load
+ *
+ * We differentiate this function from ModelAction::get_write_value and
+ * ModelAction::get_value for the purpose of RMW's, which may have both a
+ * 'read' and a 'write' value.
+ *
+ * Note: 'this' must be a load.
+ *
+ * @return The value read by this load
+ */
+uint64_t ModelAction::get_reads_from_value() const
+{
+       ASSERT(is_read());
+       if (reads_from)
+               return reads_from->get_write_value();
+       else if (reads_from_promise)
+               return reads_from_promise->get_value();
+       return VALUE_NONE; /* Only for new actions with no reads-from */
+}
+
+/**
+ * @brief Get the value written by this store
+ *
+ * We differentiate this function from ModelAction::get_reads_from_value and
+ * ModelAction::get_value for the purpose of RMW's, which may have both a
+ * 'read' and a 'write' value.
+ *
+ * Note: 'this' must be a store.
+ *
+ * @return The value written by this store
+ */
+uint64_t ModelAction::get_write_value() const
+{
+       ASSERT(is_write());
+       return value;
+}
+
+/**
+ * @brief Get the value returned by this action
+ *
+ * For atomic reads (including RMW), an operation returns the value it read.
+ * For atomic writes, an operation returns the value it wrote. For other
+ * operations, the return value varies (sometimes is a "don't care"), but the
+ * value is simply stored in the "value" field.
+ *
+ * @return This action's return value
+ */
+uint64_t ModelAction::get_return_value() const
+{
+       if (is_read())
+               return get_reads_from_value();
+       else if (is_write())
+               return get_write_value();
+       else
+               return value;
+}
+
+/** @return The Node associated with this ModelAction */
+Node * ModelAction::get_node() const
+{
+       /* UNINIT actions do not have a Node */
+       ASSERT(!is_uninitialized());
+       return node;
+}
+
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ */
+void ModelAction::set_read_from(const ModelAction *act)
+{
+       ASSERT(act);
+       reads_from = act;
+       reads_from_promise = NULL;
+       if (act->is_uninitialized())
+               model->assert_bug("May read from uninitialized atomic:\n"
+                               "    action %d, thread %d, location %p (%s, %s)",
+                               seq_number, id_to_int(tid), location,
+                               get_type_str(), get_mo_str());
+}
+
+/**
+ * Set this action's read-from promise
+ * @param promise The promise to read from
+ */
+void ModelAction::set_read_from_promise(Promise *promise)
+{
+       ASSERT(is_read());
+       reads_from_promise = promise;
+       reads_from = NULL;
+}
+
+/**
+ * Synchronize the current thread with the thread corresponding to the
+ * ModelAction parameter.
+ * @param act The ModelAction to synchronize with
+ * @return True if this is a valid synchronization; false otherwise
+ */
+bool ModelAction::synchronize_with(const ModelAction *act)
+{
+       if (*this < *act)
+               return false;
+       cv->merge(act->cv);
+       return true;
+}
+
+bool ModelAction::has_synchronized_with(const ModelAction *act) const
+{
+       return cv->synchronized_since(act);
+}
+
+/**
+ * Check whether 'this' happens before act, according to the memory-model's
+ * happens before relation. This is checked via the ClockVector constructs.
+ * @return true if this action's thread has synchronized with act's thread
+ * since the execution of act, false otherwise.
+ */
+bool ModelAction::happens_before(const ModelAction *act) const
+{
+       return act->cv->synchronized_since(this);
+}
+
+const char * ModelAction::get_type_str() const
+{
+       switch (this->type) {
+               case MODEL_FIXUP_RELSEQ: return "relseq fixup";
+               case THREAD_CREATE: return "thread create";
+               case THREAD_START: return "thread start";
+               case THREAD_YIELD: return "thread yield";
+               case THREAD_JOIN: return "thread join";
+               case THREAD_FINISH: return "thread finish";
+               case ATOMIC_UNINIT: return "uninitialized";
+               case ATOMIC_READ: return "atomic read";
+               case ATOMIC_WRITE: return "atomic write";
+               case ATOMIC_RMW: return "atomic rmw";
+               case ATOMIC_FENCE: return "fence";
+               case ATOMIC_RMWR: return "atomic rmwr";
+               case ATOMIC_RMWC: return "atomic rmwc";
+               case ATOMIC_INIT: return "init atomic";
+               case ATOMIC_LOCK: return "lock";
+               case ATOMIC_UNLOCK: return "unlock";
+               case ATOMIC_TRYLOCK: return "trylock";
+               case ATOMIC_WAIT: return "wait";
+               case ATOMIC_NOTIFY_ONE: return "notify one";
+         case ATOMIC_NOTIFY_ALL: return "notify all";
+         case ATOMIC_ANNOTATION: return "atomic annotation";
+               default: return "unknown type";
+       };
+}
+
+const char * ModelAction::get_mo_str() const
+{
+       switch (this->order) {
+               case std::memory_order_relaxed: return "relaxed";
+               case std::memory_order_acquire: return "acquire";
+               case std::memory_order_release: return "release";
+               case std::memory_order_acq_rel: return "acq_rel";
+               case std::memory_order_seq_cst: return "seq_cst";
+               default: return "unknown";
+       }
+}
+
+/** @brief Print nicely-formatted info about this ModelAction */
+void ModelAction::print() const
+{
+       const char *type_str = get_type_str(), *mo_str = get_mo_str();
+
+       model_print("%-4d %-2d   %-13s   %7s  %14p   %-#18" PRIx64,
+                       seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value());
+       if (is_read()) {
+               if (reads_from)
+                       model_print("  %-3d", reads_from->get_seq_number());
+               else if (reads_from_promise) {
+                       int idx = reads_from_promise->get_index();
+                       if (idx >= 0)
+                               model_print("  P%-2d", idx);
+                       else
+                               model_print("  P? ");
+               } else
+                       model_print("  ?  ");
+       }
+       if (cv) {
+               if (is_read())
+                       model_print(" ");
+               else
+                       model_print("      ");
+               cv->print();
+       } else
+               model_print("\n");
+}
+
+/** @brief Get a (likely) unique hash for this ModelAction */
+unsigned int ModelAction::hash() const
+{
+       unsigned int hash = (unsigned int)this->type;
+       hash ^= ((unsigned int)this->order) << 3;
+       hash ^= seq_number << 5;
+       hash ^= id_to_int(tid) << 6;
+
+       if (is_read()) {
+              if (reads_from)
+                      hash ^= reads_from->get_seq_number();
+              else if (reads_from_promise)
+                      hash ^= reads_from_promise->get_index();
+              hash ^= get_reads_from_value();
+       }
+       return hash;
+}
+
+/**
+ * @brief Checks the NodeStack to see if a ModelAction is in our may-read-from set
+ * @param write The ModelAction to check for
+ * @return True if the ModelAction is found; false otherwise
+ */
+bool ModelAction::may_read_from(const ModelAction *write) const
+{
+       for (int i = 0; i < node->get_read_from_past_size(); i++)
+               if (node->get_read_from_past(i) == write)
+                       return true;
+       return false;
+}
+
+/**
+ * @brief Checks the NodeStack to see if a Promise is in our may-read-from set
+ * @param promise The Promise to check for
+ * @return True if the Promise is found; false otherwise
+ */
+bool ModelAction::may_read_from(const Promise *promise) const
+{
+       for (int i = 0; i < node->get_read_from_promise_size(); i++)
+               if (node->get_read_from_promise(i) == promise)
+                       return true;
+       return false;
+}
+
+/**
+ * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations.
+ * @return The mutex operated on by this action, if any; otherwise NULL
+ */
+std::mutex * ModelAction::get_mutex() const
+{
+       if (is_trylock() || is_lock() || is_unlock())
+               return (std::mutex *)get_location();
+       else if (is_wait())
+               return (std::mutex *)get_value();
+       else
+               return NULL;
+}
diff --git a/action.h b/action.h
new file mode 100644 (file)
index 0000000..ad3b828
--- /dev/null
+++ b/action.h
@@ -0,0 +1,251 @@
+/** @file action.h
+ *  @brief Models actions taken by threads.
+ */
+
+#ifndef __ACTION_H__
+#define __ACTION_H__
+
+#include <cstddef>
+#include <inttypes.h>
+
+#include "mymemory.h"
+#include "memoryorder.h"
+#include "modeltypes.h"
+
+/* Forward declarations */
+class ClockVector;
+class Thread;
+class Promise;
+
+namespace std {
+       class mutex;
+}
+
+using std::memory_order;
+using std::memory_order_relaxed;
+using std::memory_order_acquire;
+using std::memory_order_release;
+using std::memory_order_acq_rel;
+using std::memory_order_seq_cst;
+
+/**
+ * @brief A recognizable don't-care value for use in the ModelAction::value
+ * field
+ *
+ * Note that this value can be legitimately used by a program, and hence by
+ * iteself does not indicate no value.
+ */
+#define VALUE_NONE 0xdeadbeef
+
+/**
+ * @brief The "location" at which a fence occurs
+ *
+ * We need a non-zero memory location to associate with fences, since our hash
+ * tables don't handle NULL-pointer keys. HACK: Hopefully this doesn't collide
+ * with any legitimate memory locations.
+ */
+#define FENCE_LOCATION ((void *)0x7)
+
+/** @brief Represents an action type, identifying one of several types of
+ * ModelAction */
+typedef enum action_type {
+       MODEL_FIXUP_RELSEQ,   /**< Special ModelAction: finalize a release
+                              *   sequence */
+       THREAD_CREATE,        /**< A thread creation action */
+       THREAD_START,         /**< First action in each thread */
+       THREAD_YIELD,         /**< A thread yield action */
+       THREAD_JOIN,          /**< A thread join action */
+       THREAD_FINISH,        /**< A thread completion action */
+       ATOMIC_UNINIT,        /**< Represents an uninitialized atomic */
+       ATOMIC_READ,          /**< An atomic read action */
+       ATOMIC_WRITE,         /**< An atomic write action */
+       ATOMIC_RMWR,          /**< The read part of an atomic RMW action */
+       ATOMIC_RMW,           /**< The write part of an atomic RMW action */
+       ATOMIC_RMWC,          /**< Convert an atomic RMW action into a READ */
+       ATOMIC_INIT,          /**< Initialization of an atomic object (e.g.,
+                              *   atomic_init()) */
+       ATOMIC_FENCE,         /**< A fence action */
+       ATOMIC_LOCK,          /**< A lock action */
+       ATOMIC_TRYLOCK,       /**< A trylock action */
+       ATOMIC_UNLOCK,        /**< An unlock action */
+       ATOMIC_NOTIFY_ONE,    /**< A notify_one action */
+       ATOMIC_NOTIFY_ALL,    /**< A notify all action */
+       ATOMIC_WAIT,          /**< A wait action */
+       ATOMIC_ANNOTATION     /**< An annotation action to pass information
+                                                                                                        to a trace analysis */
+} action_type_t;
+
+/* Forward declaration */
+class Node;
+class ClockVector;
+
+/**
+ * @brief Represents a single atomic action
+ *
+ * A ModelAction is always allocated as non-snapshotting, because it is used in
+ * multiple executions during backtracking. Except for fake uninitialized
+ * (ATOMIC_UNINIT) ModelActions, each action is assigned a unique sequence
+ * number.
+ */
+class ModelAction {
+public:
+       ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
+       ~ModelAction();
+       void print() const;
+
+       thread_id_t get_tid() const { return tid; }
+       action_type get_type() const { return type; }
+       memory_order get_mo() const { return order; }
+       void * get_location() const { return location; }
+       modelclock_t get_seq_number() const { return seq_number; }
+       uint64_t get_value() const { return value; }
+       uint64_t get_reads_from_value() const;
+       uint64_t get_write_value() const;
+       uint64_t get_return_value() const;
+       const ModelAction * get_reads_from() const { return reads_from; }
+       Promise * get_reads_from_promise() const { return reads_from_promise; }
+       std::mutex * get_mutex() const;
+
+       Node * get_node() const;
+       void set_node(Node *n) { node = n; }
+
+       void set_read_from(const ModelAction *act);
+       void set_read_from_promise(Promise *promise);
+
+       /** Store the most recent fence-release from the same thread
+        *  @param fence The fence-release that occured prior to this */
+       void set_last_fence_release(const ModelAction *fence) { last_fence_release = fence; }
+       /** @return The most recent fence-release from the same thread */
+       const ModelAction * get_last_fence_release() const { return last_fence_release; }
+
+       void copy_from_new(ModelAction *newaction);
+       void set_seq_number(modelclock_t num);
+       void set_try_lock(bool obtainedlock);
+       bool is_thread_start() const;
+       bool is_thread_join() const;
+       bool is_relseq_fixup() const;
+       bool is_mutex_op() const;
+       bool is_lock() const;
+       bool is_trylock() const;
+       bool is_unlock() const;
+       bool is_wait() const;
+       bool is_notify() const;
+       bool is_notify_one() const;
+       bool is_success_lock() const;
+       bool is_failed_trylock() const;
+       bool is_atomic_var() const;
+       bool is_uninitialized() const;
+       bool is_read() const;
+       bool is_write() const;
+       bool is_yield() const;
+       bool could_be_write() const;
+       bool is_rmwr() const;
+       bool is_rmwc() const;
+       bool is_rmw() const;
+       bool is_fence() const;
+       bool is_initialization() const;
+       bool is_annotation() const;
+       bool is_relaxed() const;
+       bool is_acquire() const;
+       bool is_release() const;
+       bool is_seqcst() const;
+       bool same_var(const ModelAction *act) const;
+       bool same_thread(const ModelAction *act) const;
+       bool is_conflicting_lock(const ModelAction *act) const;
+       bool could_synchronize_with(const ModelAction *act) const;
+
+       Thread * get_thread_operand() const;
+
+       void create_cv(const ModelAction *parent = NULL);
+       ClockVector * get_cv() const { return cv; }
+       bool synchronize_with(const ModelAction *act);
+
+       bool has_synchronized_with(const ModelAction *act) const;
+       bool happens_before(const ModelAction *act) const;
+
+       inline bool operator <(const ModelAction& act) const {
+               return get_seq_number() < act.get_seq_number();
+       }
+       inline bool operator >(const ModelAction& act) const {
+               return get_seq_number() > act.get_seq_number();
+       }
+
+       void process_rmw(ModelAction * act);
+       void copy_typeandorder(ModelAction * act);
+
+       void set_sleep_flag() { sleep_flag=true; }
+       bool get_sleep_flag() { return sleep_flag; }
+       unsigned int hash() const;
+
+       bool equals(const ModelAction *x) const { return this == x; }
+       bool equals(const Promise *x) const { return false; }
+
+       bool may_read_from(const ModelAction *write) const;
+       bool may_read_from(const Promise *promise) const;
+       MEMALLOC
+private:
+
+       const char * get_type_str() const;
+       const char * get_mo_str() const;
+
+       /** @brief Type of action (read, write, RMW, fence, thread create, etc.) */
+       action_type type;
+
+       /** @brief The memory order for this operation. */
+       memory_order order;
+
+       /** @brief A pointer to the memory location for this action. */
+       void *location;
+
+       /** @brief The thread id that performed this action. */
+       thread_id_t tid;
+
+       /** @brief The value written (for write or RMW; undefined for read) */
+       uint64_t value;
+
+       /**
+        * @brief The store that this action reads from
+        *
+        * Only valid for reads
+        */
+       const ModelAction *reads_from;
+
+       /**
+        * @brief The promise that this action reads from
+        *
+        * Only valid for reads
+        */
+       Promise *reads_from_promise;
+
+       /** @brief The last fence release from the same thread */
+       const ModelAction *last_fence_release;
+
+       /**
+        * @brief A back reference to a Node in NodeStack
+        *
+        * Only set if this ModelAction is saved on the NodeStack. (A
+        * ModelAction can be thrown away before it ever enters the NodeStack.)
+        */
+       Node *node;
+
+       /**
+        * @brief The sequence number of this action
+        *
+        * Except for ATOMIC_UNINIT actions, this number should be unique and
+        * should represent the action's position in the execution order.
+        */
+       modelclock_t seq_number;
+
+       /**
+        * @brief The clock vector for this operation
+        *
+        * Technically, this is only needed for potentially synchronizing
+        * (e.g., non-relaxed) operations, but it is very handy to have these
+        * vectors for all operations.
+        */
+       ClockVector *cv;
+
+       bool sleep_flag;
+};
+
+#endif /* __ACTION_H__ */
diff --git a/bugmessage.h b/bugmessage.h
new file mode 100644 (file)
index 0000000..bd7d0b6
--- /dev/null
@@ -0,0 +1,21 @@
+#ifndef __BUGMESSAGE_H__
+#define __BUGMESSAGE_H__
+
+#include "common.h"
+#include "mymemory.h"
+
+struct bug_message {
+       bug_message(const char *str) {
+               const char *fmt = "  [BUG] %s\n";
+               msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
+               sprintf(msg, fmt, str);
+       }
+       ~bug_message() { if (msg) snapshot_free(msg); }
+
+       char *msg;
+       void print() { model_print("%s", msg); }
+
+       SNAPSHOTALLOC
+};
+
+#endif /* __BUGMESSAGE_H__ */
diff --git a/clockvector.cc b/clockvector.cc
new file mode 100644 (file)
index 0000000..5f068e9
--- /dev/null
@@ -0,0 +1,101 @@
+#include <cstring>
+#include <stdlib.h>
+
+#include "action.h"
+#include "clockvector.h"
+#include "common.h"
+#include "threads-model.h"
+
+/**
+ * Constructs a new ClockVector, given a parent ClockVector and a first
+ * ModelAction. This constructor can assign appropriate default settings if no
+ * parent and/or action is supplied.
+ * @param parent is the previous ClockVector to inherit (i.e., clock from the
+ * same thread or the parent that created this thread)
+ * @param act is an action with which to update the ClockVector
+ */
+ClockVector::ClockVector(ClockVector *parent, ModelAction *act)
+{
+       ASSERT(act);
+       num_threads = int_to_id(act->get_tid()) + 1;
+       if (parent && parent->num_threads > num_threads)
+               num_threads = parent->num_threads;
+
+       clock = (modelclock_t *)snapshot_calloc(num_threads, sizeof(int));
+       if (parent)
+               std::memcpy(clock, parent->clock, parent->num_threads * sizeof(modelclock_t));
+
+       clock[id_to_int(act->get_tid())] = act->get_seq_number();
+}
+
+/** @brief Destructor */
+ClockVector::~ClockVector()
+{
+       snapshot_free(clock);
+}
+
+/**
+ * Merge a clock vector into this vector, using a pairwise comparison. The
+ * resulting vector length will be the maximum length of the two being merged.
+ * @param cv is the ClockVector being merged into this vector.
+ */
+bool ClockVector::merge(const ClockVector *cv)
+{
+       ASSERT(cv != NULL);
+       bool changed = false;
+       if (cv->num_threads > num_threads) {
+               clock = (modelclock_t *)snapshot_realloc(clock, cv->num_threads * sizeof(modelclock_t));
+               for (int i = num_threads; i < cv->num_threads; i++)
+                       clock[i] = 0;
+               num_threads = cv->num_threads;
+       }
+
+       /* Element-wise maximum */
+       for (int i = 0; i < cv->num_threads; i++)
+               if (cv->clock[i] > clock[i]) {
+                       clock[i] = cv->clock[i];
+                       changed = true;
+               }
+       
+       return changed;
+}
+
+/**
+ * Check whether this vector's thread has synchronized with another action's
+ * thread. This effectively checks the happens-before relation (or actually,
+ * happens after), but it's easier to compare two ModelAction events directly,
+ * using ModelAction::happens_before.
+ *
+ * @see ModelAction::happens_before
+ *
+ * @return true if this ClockVector's thread has synchronized with act's
+ * thread, false otherwise. That is, this function returns:
+ * <BR><CODE>act <= cv[act->tid]</CODE>
+ */
+bool ClockVector::synchronized_since(const ModelAction *act) const
+{
+       int i = id_to_int(act->get_tid());
+
+       if (i < num_threads)
+               return act->get_seq_number() <= clock[i];
+       return false;
+}
+
+/** Gets the clock corresponding to a given thread id from the clock vector. */
+modelclock_t ClockVector::getClock(thread_id_t thread) {
+       int threadid = id_to_int(thread);
+
+       if (threadid < num_threads)
+               return clock[threadid];
+       else
+               return 0;
+}
+
+/** @brief Formats and prints this ClockVector's data. */
+void ClockVector::print() const
+{
+       int i;
+       model_print("(");
+       for (i = 0; i < num_threads; i++)
+               model_print("%2u%s", clock[i], (i == num_threads - 1) ? ")\n" : ", ");
+}
diff --git a/clockvector.h b/clockvector.h
new file mode 100644 (file)
index 0000000..e19a211
--- /dev/null
@@ -0,0 +1,33 @@
+/** @file clockvector.h
+ *  @brief Implements a clock vector.
+ */
+
+#ifndef __CLOCKVECTOR_H__
+#define __CLOCKVECTOR_H__
+
+#include "mymemory.h"
+#include "modeltypes.h"
+
+/* Forward declaration */
+class ModelAction;
+
+class ClockVector {
+public:
+       ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
+       ~ClockVector();
+       bool merge(const ClockVector *cv);
+       bool synchronized_since(const ModelAction *act) const;
+
+       void print() const;
+       modelclock_t getClock(thread_id_t thread);
+
+       SNAPSHOTALLOC
+private:
+       /** @brief Holds the actual clock data, as an array. */
+       modelclock_t *clock;
+
+       /** @brief The number of threads recorded in clock (i.e., its length).  */
+       int num_threads;
+};
+
+#endif /* __CLOCKVECTOR_H__ */
diff --git a/cmodelint.cc b/cmodelint.cc
new file mode 100644 (file)
index 0000000..1632581
--- /dev/null
@@ -0,0 +1,43 @@
+#include "model.h"
+#include "action.h"
+#include "cmodelint.h"
+#include "threads-model.h"
+
+/** Performs a read action.*/
+uint64_t model_read_action(void * obj, memory_order ord) {
+       return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
+}
+
+/** Performs a write action.*/
+void model_write_action(void * obj, memory_order ord, uint64_t val) {
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, ord, obj, val));
+}
+
+/** Performs an init action. */
+void model_init_action(void * obj, uint64_t val) {
+       model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
+}
+
+/**
+ * Performs the read part of a RMW action. The next action must either be the
+ * write part of the RMW action or an explicit close out of the RMW action w/o
+ * a write.
+ */
+uint64_t model_rmwr_action(void *obj, memory_order ord) {
+       return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
+}
+
+/** Performs the write part of a RMW action. */
+void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
+       model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
+}
+
+/** Closes out a RMW action without doing a write. */
+void model_rmwc_action(void *obj, memory_order ord) {
+       model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
+}
+
+/** Issues a fence operation. */
+void model_fence_action(memory_order ord) {
+       model->switch_to_master(new ModelAction(ATOMIC_FENCE, ord, FENCE_LOCATION));
+}
diff --git a/common.cc b/common.cc
new file mode 100644 (file)
index 0000000..26f6d5d
--- /dev/null
+++ b/common.cc
@@ -0,0 +1,173 @@
+#include <execinfo.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+#include <errno.h>
+#include <fcntl.h>
+
+#include <model-assert.h>
+
+#include "common.h"
+#include "model.h"
+#include "stacktrace.h"
+#include "output.h"
+
+#define MAX_TRACE_LEN 100
+
+/** @brief Model-checker output file descriptor; default to stdout until redirected */
+int model_out = STDOUT_FILENO;
+
+#define CONFIG_STACKTRACE
+/** Print a backtrace of the current program state. */
+void print_trace(void)
+{
+#ifdef CONFIG_STACKTRACE
+       print_stacktrace(model_out);
+#else
+       void *array[MAX_TRACE_LEN];
+       char **strings;
+       int size, i;
+
+       size = backtrace(array, MAX_TRACE_LEN);
+       strings = backtrace_symbols(array, size);
+
+       model_print("\nDumping stack trace (%d frames):\n", size);
+
+       for (i = 0; i < size; i++)
+               model_print("\t%s\n", strings[i]);
+
+       free(strings);
+#endif /* CONFIG_STACKTRACE */
+}
+
+void assert_hook(void)
+{
+       model_print("Add breakpoint to line %u in file %s.\n", __LINE__, __FILE__);
+}
+
+void model_assert(bool expr, const char *file, int line)
+{
+       if (!expr) {
+               char msg[100];
+               sprintf(msg, "Program has hit assertion in file %s at line %d\n",
+                               file, line);
+               model->assert_user_bug(msg);
+       }
+}
+
+#ifndef CONFIG_DEBUG
+
+static int fd_user_out; /**< @brief File descriptor from which to read user program output */
+
+/**
+ * @brief Setup output redirecting
+ *
+ * Redirects user program's stdout to a pipe so that we can dump it
+ * selectively, when displaying bugs, etc.
+ * Also connects a file descriptor 'model_out' directly to stdout, for printing
+ * data when needed.
+ *
+ * The model-checker can selectively choose to print/hide the user program
+ * output.
+ * @see clear_program_output
+ * @see print_program_output
+ *
+ * Note that the user program's pipe has limited memory, so if a program will
+ * output much data, we will need to buffer it in user-space during execution.
+ * This also means that if ModelChecker decides not to print an execution, it
+ * should promptly clear the pipe.
+ *
+ * This function should only be called once.
+ */
+void redirect_output()
+{
+       /* Save stdout for later use */
+       model_out = dup(STDOUT_FILENO);
+       if (model_out < 0) {
+               perror("dup");
+               exit(EXIT_FAILURE);
+       }
+
+       /* Redirect program output to a pipe */
+       int pipefd[2];
+       if (pipe(pipefd) < 0) {
+               perror("pipe");
+               exit(EXIT_FAILURE);
+       }
+       if (dup2(pipefd[1], STDOUT_FILENO) < 0) {
+               perror("dup2");
+               exit(EXIT_FAILURE);
+       }
+       close(pipefd[1]);
+
+       /* Save the "read" side of the pipe for use later */
+       if (fcntl(pipefd[0], F_SETFL, O_NONBLOCK) < 0) {
+               perror("fcntl");
+               exit(EXIT_FAILURE);
+       }
+       fd_user_out = pipefd[0];
+}
+
+/**
+ * @brief Wrapper for reading data to buffer
+ *
+ * Besides a simple read, this handles the subtleties of EOF and nonblocking
+ * input (if fd is O_NONBLOCK).
+ *
+ * @param fd The file descriptor to read.
+ * @param buf Buffer to read to.
+ * @param maxlen Maximum data to read to buffer
+ * @return The length of data read. If zero, then we hit EOF or ran out of data
+ * (non-blocking)
+ */
+static ssize_t read_to_buf(int fd, char *buf, size_t maxlen)
+{
+       ssize_t ret = read(fd, buf, maxlen);
+       if (ret < 0) {
+               if (errno == EAGAIN || errno == EWOULDBLOCK) {
+                       return 0;
+               } else {
+                       perror("read");
+                       exit(EXIT_FAILURE);
+               }
+       }
+       return ret;
+}
+
+/** @brief Dump any pending program output without printing */
+void clear_program_output()
+{
+       fflush(stdout);
+       char buf[200];
+       while (read_to_buf(fd_user_out, buf, sizeof(buf)));
+}
+
+/** @brief Print out any pending program output */
+void print_program_output()
+{
+       char buf[200];
+
+       model_print("---- BEGIN PROGRAM OUTPUT ----\n");
+
+       /* Gather all program output */
+       fflush(stdout);
+
+       /* Read program output pipe and write to (real) stdout */
+       ssize_t ret;
+       while (1) {
+               ret = read_to_buf(fd_user_out, buf, sizeof(buf));
+               if (!ret)
+                       break;
+               while (ret > 0) {
+                       ssize_t res = write(model_out, buf, ret);
+                       if (res < 0) {
+                               perror("write");
+                               exit(EXIT_FAILURE);
+                       }
+                       ret -= res;
+               }
+       }
+
+       model_print("---- END PROGRAM OUTPUT   ----\n");
+}
+#endif /* ! CONFIG_DEBUG */
diff --git a/common.h b/common.h
new file mode 100644 (file)
index 0000000..62c16f4
--- /dev/null
+++ b/common.h
@@ -0,0 +1,45 @@
+/** @file common.h
+ *  @brief General purpose macros.
+ */
+
+#ifndef __COMMON_H__
+#define __COMMON_H__
+
+#include <stdio.h>
+#include "config.h"
+
+extern int model_out;
+
+#define model_print(fmt, ...) do { dprintf(model_out, fmt, ##__VA_ARGS__); } while (0)
+
+#ifdef CONFIG_DEBUG
+#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ##__VA_ARGS__); } while (0)
+#define DBG() DEBUG("\n")
+#define DBG_ENABLED() (1)
+#else
+#define DEBUG(fmt, ...)
+#define DBG()
+#define DBG_ENABLED() (0)
+#endif
+
+void assert_hook(void);
+
+#ifdef CONFIG_ASSERT
+#define ASSERT(expr) \
+do { \
+       if (!(expr)) { \
+               fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
+               /* print_trace(); // Trace printing may cause dynamic memory allocation */ \
+               assert_hook();                           \
+               exit(EXIT_FAILURE); \
+       } \
+} while (0)
+#else
+#define ASSERT(expr) \
+       do { } while (0)
+#endif /* CONFIG_ASSERT */
+
+#define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
+
+void print_trace(void);
+#endif /* __COMMON_H__ */
diff --git a/common.mk b/common.mk
new file mode 100644 (file)
index 0000000..bc068df
--- /dev/null
+++ b/common.mk
@@ -0,0 +1,16 @@
+# A few common Makefile items
+
+CC := gcc
+CXX := g++
+
+UNAME := $(shell uname)
+
+LIB_NAME := model
+LIB_SO := lib$(LIB_NAME).so
+
+CPPFLAGS += -Wall -g -O3
+
+# Mac OSX options
+ifeq ($(UNAME), Darwin)
+CPPFLAGS += -D_XOPEN_SOURCE -DMAC
+endif
diff --git a/conditionvariable.cc b/conditionvariable.cc
new file mode 100644 (file)
index 0000000..75af879
--- /dev/null
@@ -0,0 +1,30 @@
+#include <mutex>
+#include "model.h"
+#include <condition_variable>
+#include "action.h"
+
+namespace std {
+
+condition_variable::condition_variable() {
+               
+}
+
+condition_variable::~condition_variable() {
+               
+}
+
+void condition_variable::notify_one() {
+       model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this));
+}
+
+void condition_variable::notify_all() {
+       model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ALL, std::memory_order_seq_cst, this));
+}
+
+void condition_variable::wait(mutex& lock) {
+       model->switch_to_master(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock));
+       //relock as a second action
+       lock.lock();
+}
+}
+
diff --git a/config.h b/config.h
new file mode 100644 (file)
index 0000000..891dfd7
--- /dev/null
+++ b/config.h
@@ -0,0 +1,57 @@
+/** @file config.h
+ * @brief Configuration file.
+ */
+
+#ifndef CONFIG_H
+#define CONFIG_H
+
+/** Turn on debugging. */
+/*             #ifndef CONFIG_DEBUG
+               #define CONFIG_DEBUG
+               #endif
+
+               #ifndef CONFIG_ASSERT
+               #define CONFIG_ASSERT
+               #endif
+*/
+
+/** Turn on support for dumping cyclegraphs as dot files at each
+ *  printed summary.*/
+#define SUPPORT_MOD_ORDER_DUMP 0
+
+/** Do we have a 48 bit virtual address (64 bit machine) or 32 bit addresses.
+ * Set to 1 for 48-bit, 0 for 32-bit. */
+#ifndef BIT48
+#ifdef _LP64
+#define BIT48 1
+#else
+#define BIT48 0
+#endif
+#endif /* BIT48 */
+
+/** Snapshotting configurables */
+
+/** 
+ * If USE_MPROTECT_SNAPSHOT=2, then snapshot by tuned mmap() algorithm
+ * If USE_MPROTECT_SNAPSHOT=1, then snapshot by using mmap() and mprotect()
+ * If USE_MPROTECT_SNAPSHOT=0, then snapshot by using fork() */
+#define USE_MPROTECT_SNAPSHOT 2
+
+/** Size of signal stack */
+#define SIGSTACKSIZE 65536
+
+/** Page size configuration */
+#define PAGESIZE 4096
+
+/** Thread parameters */
+
+/* Size of stack to allocate for a thread. */
+#define STACK_SIZE (1024 * 1024)
+
+/** How many shadow tables of memory to preallocate for data race detector. */
+#define SHADOWBASETABLES 4
+
+/** Enable debugging assertions (via ASSERT()) */
+#define CONFIG_ASSERT
+
+#endif
diff --git a/context.cc b/context.cc
new file mode 100644 (file)
index 0000000..b5ae0ba
--- /dev/null
@@ -0,0 +1,27 @@
+#include "context.h"
+
+#ifdef MAC
+
+int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)
+{
+       /*
+        * Mac OSX swapcontext() clobbers some registers, so use a hand-rolled
+        * version with {get,set}context(). We can avoid the same problem
+        * (where optimizations can break the following code) because we don't
+        * statically link with the C library
+        */
+
+       /* volatile, so that 'i' doesn't get promoted to a register */
+       volatile int i = 0;
+
+       getcontext(oucp);
+
+       if (i == 0) {
+               i = 1;
+               setcontext(ucp);
+       }
+
+       return 0;
+}
+
+#endif /* MAC */
diff --git a/context.h b/context.h
new file mode 100644 (file)
index 0000000..ea32d2f
--- /dev/null
+++ b/context.h
@@ -0,0 +1,24 @@
+/**
+ * @file context.h
+ * @brief ucontext header, since Mac OSX swapcontext() is broken
+ */
+
+#ifndef __CONTEXT_H__
+#define __CONTEXT_H__
+
+#include <ucontext.h>
+
+#ifdef MAC
+
+int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp);
+
+#else /* !MAC */
+
+static inline int model_swapcontext(ucontext_t *oucp, ucontext_t *ucp)
+{
+       return swapcontext(oucp, ucp);
+}
+
+#endif /* !MAC */
+
+#endif /* __CONTEXT_H__ */
diff --git a/cyclegraph.cc b/cyclegraph.cc
new file mode 100644 (file)
index 0000000..7e5e956
--- /dev/null
@@ -0,0 +1,659 @@
+#include "cyclegraph.h"
+#include "action.h"
+#include "common.h"
+#include "promise.h"
+#include "threads-model.h"
+
+/** Initializes a CycleGraph object. */
+CycleGraph::CycleGraph() :
+       discovered(new HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
+       queue(new ModelVector<const CycleNode *>()),
+       hasCycles(false),
+       oldCycles(false)
+{
+}
+
+/** CycleGraph destructor */
+CycleGraph::~CycleGraph()
+{
+       delete queue;
+       delete discovered;
+}
+
+/**
+ * Add a CycleNode to the graph, corresponding to a store ModelAction
+ * @param act The write action that should be added
+ * @param node The CycleNode that corresponds to the store
+ */
+void CycleGraph::putNode(const ModelAction *act, CycleNode *node)
+{
+       actionToNode.put(act, node);
+#if SUPPORT_MOD_ORDER_DUMP
+       nodeList.push_back(node);
+#endif
+}
+
+/**
+ * Add a CycleNode to the graph, corresponding to a Promise
+ * @param promise The Promise that should be added
+ * @param node The CycleNode that corresponds to the Promise
+ */
+void CycleGraph::putNode(const Promise *promise, CycleNode *node)
+{
+       promiseToNode.put(promise, node);
+#if SUPPORT_MOD_ORDER_DUMP
+       nodeList.push_back(node);
+#endif
+}
+
+/**
+ * @brief Remove the Promise node from the graph
+ * @param promise The promise to remove from the graph
+ */
+void CycleGraph::erasePromiseNode(const Promise *promise)
+{
+       promiseToNode.put(promise, NULL);
+#if SUPPORT_MOD_ORDER_DUMP
+       /* Remove the promise node from nodeList */
+       CycleNode *node = getNode_noCreate(promise);
+       for (unsigned int i = 0; i < nodeList.size(); )
+               if (nodeList[i] == node)
+                       nodeList.erase(nodeList.begin() + i);
+               else
+                       i++;
+#endif
+}
+
+/** @return The corresponding CycleNode, if exists; otherwise NULL */
+CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
+{
+       return actionToNode.get(act);
+}
+
+/** @return The corresponding CycleNode, if exists; otherwise NULL */
+CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
+{
+       return promiseToNode.get(promise);
+}
+
+/**
+ * @brief Returns the CycleNode corresponding to a given ModelAction
+ *
+ * Gets (or creates, if none exist) a CycleNode corresponding to a ModelAction
+ *
+ * @param action The ModelAction to find a node for
+ * @return The CycleNode paired with this action
+ */
+CycleNode * CycleGraph::getNode(const ModelAction *action)
+{
+       CycleNode *node = getNode_noCreate(action);
+       if (node == NULL) {
+               node = new CycleNode(action);
+               putNode(action, node);
+       }
+       return node;
+}
+
+/**
+ * @brief Returns a CycleNode corresponding to a promise
+ *
+ * Gets (or creates, if none exist) a CycleNode corresponding to a promised
+ * value.
+ *
+ * @param promise The Promise generated by a reader
+ * @return The CycleNode corresponding to the Promise
+ */
+CycleNode * CycleGraph::getNode(const Promise *promise)
+{
+       CycleNode *node = getNode_noCreate(promise);
+       if (node == NULL) {
+               node = new CycleNode(promise);
+               putNode(promise, node);
+       }
+       return node;
+}
+
+/**
+ * Resolve/satisfy a Promise with a particular store ModelAction, taking care
+ * of the CycleGraph cleanups, including merging any necessary CycleNodes.
+ *
+ * @param promise The Promise to resolve
+ * @param writer The store that will resolve this Promise
+ * @return false if the resolution results in a cycle (or fails in some other
+ * way); true otherwise
+ */
+bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer)
+{
+       CycleNode *promise_node = promiseToNode.get(promise);
+       CycleNode *w_node = actionToNode.get(writer);
+       ASSERT(promise_node);
+
+       if (w_node)
+               return mergeNodes(w_node, promise_node);
+       /* No existing write-node; just convert the promise-node */
+       promise_node->resolvePromise(writer);
+       erasePromiseNode(promise_node->getPromise());
+       putNode(writer, promise_node);
+       return true;
+}
+
+/**
+ * @brief Merge two CycleNodes that represent the same write
+ *
+ * Note that this operation cannot be rolled back.
+ *
+ * @param w_node The write ModelAction node with which to merge
+ * @param p_node The Promise node to merge. Will be destroyed after this
+ * function.
+ *
+ * @return false if the merge cannot succeed; true otherwise
+ */
+bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node)
+{
+       ASSERT(!w_node->is_promise());
+       ASSERT(p_node->is_promise());
+
+       const Promise *promise = p_node->getPromise();
+       if (!promise->is_compatible(w_node->getAction()) ||
+                       !promise->same_value(w_node->getAction()))
+               return false;
+
+       /* Transfer the RMW */
+       CycleNode *promise_rmw = p_node->getRMW();
+       if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw))
+               return false;
+
+       /* Transfer back edges to w_node */
+       while (p_node->getNumBackEdges() > 0) {
+               CycleNode *back = p_node->removeBackEdge();
+               if (back == w_node)
+                       continue;
+               addNodeEdge(back, w_node);
+               if (hasCycles)
+                       return false;
+       }
+
+       /* Transfer forward edges to w_node */
+       while (p_node->getNumEdges() > 0) {
+               CycleNode *forward = p_node->removeEdge();
+               if (forward == w_node)
+                       continue;
+               addNodeEdge(w_node, forward);
+               if (hasCycles)
+                       return false;
+       }
+
+       erasePromiseNode(promise);
+       /* Not deleting p_node, to maintain consistency if mergeNodes() fails */
+
+       return !hasCycles;
+}
+
+/**
+ * Adds an edge between two CycleNodes.
+ * @param fromnode The edge comes from this CycleNode
+ * @param tonode The edge points to this CycleNode
+ * @return True, if new edge(s) are added; otherwise false
+ */
+bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
+{
+       if (fromnode->addEdge(tonode)) {
+               rollbackvector.push_back(fromnode);
+               if (!hasCycles)
+                       hasCycles = checkReachable(tonode, fromnode);
+       } else
+               return false; /* No new edge */
+
+       /*
+        * If the fromnode has a rmwnode that is not the tonode, we should
+        * follow its RMW chain to add an edge at the end, unless we encounter
+        * tonode along the way
+        */
+       CycleNode *rmwnode = fromnode->getRMW();
+       if (rmwnode) {
+               while (rmwnode != tonode && rmwnode->getRMW())
+                       rmwnode = rmwnode->getRMW();
+
+               if (rmwnode != tonode) {
+                       if (rmwnode->addEdge(tonode)) {
+                               if (!hasCycles)
+                                       hasCycles = checkReachable(tonode, rmwnode);
+
+                               rollbackvector.push_back(rmwnode);
+                       }
+               }
+       }
+       return true;
+}
+
+/**
+ * @brief Add an edge between a write and the RMW which reads from it
+ *
+ * Handles special case of a RMW action, where the ModelAction rmw reads from
+ * the ModelAction/Promise from. The key differences are:
+ *  -# No write can occur in between the @a rmw and @a from actions.
+ *  -# Only one RMW action can read from a given write.
+ *
+ * @param from The edge comes from this ModelAction/Promise
+ * @param rmw The edge points to this ModelAction; this action must read from
+ * the ModelAction/Promise from
+ */
+template <typename T>
+void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
+{
+       ASSERT(from);
+       ASSERT(rmw);
+
+       CycleNode *fromnode = getNode(from);
+       CycleNode *rmwnode = getNode(rmw);
+
+       /* We assume that this RMW has no RMW reading from it yet */
+       ASSERT(!rmwnode->getRMW());
+
+       /* Two RMW actions cannot read from the same write. */
+       if (fromnode->setRMW(rmwnode))
+               hasCycles = true;
+       else
+               rmwrollbackvector.push_back(fromnode);
+
+       /* Transfer all outgoing edges from the from node to the rmw node */
+       /* This process should not add a cycle because either:
+        * (1) The rmw should not have any incoming edges yet if it is the
+        * new node or
+        * (2) the fromnode is the new node and therefore it should not
+        * have any outgoing edges.
+        */
+       for (unsigned int i = 0; i < fromnode->getNumEdges(); i++) {
+               CycleNode *tonode = fromnode->getEdge(i);
+               if (tonode != rmwnode) {
+                       if (rmwnode->addEdge(tonode))
+                               rollbackvector.push_back(rmwnode);
+               }
+       }
+
+       addNodeEdge(fromnode, rmwnode);
+}
+/* Instantiate two forms of CycleGraph::addRMWEdge */
+template void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw);
+template void CycleGraph::addRMWEdge(const Promise *from, const ModelAction *rmw);
+
+/**
+ * @brief Adds an edge between objects
+ *
+ * This function will add an edge between any two objects which can be
+ * associated with a CycleNode. That is, if they have a CycleGraph::getNode
+ * implementation.
+ *
+ * The object to is ordered after the object from.
+ *
+ * @param to The edge points to this object, of type T
+ * @param from The edge comes from this object, of type U
+ * @return True, if new edge(s) are added; otherwise false
+ */
+template <typename T, typename U>
+bool CycleGraph::addEdge(const T *from, const U *to)
+{
+       ASSERT(from);
+       ASSERT(to);
+
+       CycleNode *fromnode = getNode(from);
+       CycleNode *tonode = getNode(to);
+
+       return addNodeEdge(fromnode, tonode);
+}
+/* Instantiate four forms of CycleGraph::addEdge */
+template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to);
+template bool CycleGraph::addEdge(const ModelAction *from, const Promise *to);
+template bool CycleGraph::addEdge(const Promise *from, const ModelAction *to);
+template bool CycleGraph::addEdge(const Promise *from, const Promise *to);
+
+#if SUPPORT_MOD_ORDER_DUMP
+
+static void print_node(FILE *file, const CycleNode *node, int label)
+{
+       if (node->is_promise()) {
+               const Promise *promise = node->getPromise();
+               int idx = promise->get_index();
+               fprintf(file, "P%u", idx);
+               if (label) {
+                       int first = 1;
+                       fprintf(file, " [label=\"P%d, T", idx);
+                       for (unsigned int i = 0 ; i < promise->max_available_thread_idx(); i++)
+                               if (promise->thread_is_available(int_to_id(i))) {
+                                       fprintf(file, "%s%u", first ? "": ",", i);
+                                       first = 0;
+                               }
+                       fprintf(file, "\"]");
+               }
+       } else {
+               const ModelAction *act = node->getAction();
+               modelclock_t idx = act->get_seq_number();
+               fprintf(file, "N%u", idx);
+               if (label)
+                       fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid());
+       }
+}
+
+static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, const char *prop)
+{
+       print_node(file, from, 0);
+       fprintf(file, " -> ");
+       print_node(file, to, 0);
+       if (prop && strlen(prop))
+               fprintf(file, " [%s]", prop);
+       fprintf(file, ";\n");
+}
+
+void CycleGraph::dot_print_node(FILE *file, const ModelAction *act)
+{
+       print_node(file, getNode(act), 1);
+}
+
+template <typename T, typename U>
+void CycleGraph::dot_print_edge(FILE *file, const T *from, const U *to, const char *prop)
+{
+       CycleNode *fromnode = getNode(from);
+       CycleNode *tonode = getNode(to);
+
+       print_edge(file, fromnode, tonode, prop);
+}
+/* Instantiate two forms of CycleGraph::dot_print_edge */
+template void CycleGraph::dot_print_edge(FILE *file, const Promise *from, const ModelAction *to, const char *prop);
+template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, const ModelAction *to, const char *prop);
+
+void CycleGraph::dumpNodes(FILE *file) const
+{
+       for (unsigned int i = 0; i < nodeList.size(); i++) {
+               CycleNode *n = nodeList[i];
+               print_node(file, n, 1);
+               fprintf(file, ";\n");
+               if (n->getRMW())
+                       print_edge(file, n, n->getRMW(), "style=dotted");
+               for (unsigned int j = 0; j < n->getNumEdges(); j++)
+                       print_edge(file, n, n->getEdge(j), NULL);
+       }
+}
+
+void CycleGraph::dumpGraphToFile(const char *filename) const
+{
+       char buffer[200];
+       sprintf(buffer, "%s.dot", filename);
+       FILE *file = fopen(buffer, "w");
+       fprintf(file, "digraph %s {\n", filename);
+       dumpNodes(file);
+       fprintf(file, "}\n");
+       fclose(file);
+}
+#endif
+
+/**
+ * Checks whether one CycleNode can reach another.
+ * @param from The CycleNode from which to begin exploration
+ * @param to The CycleNode to reach
+ * @return True, @a from can reach @a to; otherwise, false
+ */
+bool CycleGraph::checkReachable(const CycleNode *from, const CycleNode *to) const
+{
+       discovered->reset();
+       queue->clear();
+       queue->push_back(from);
+       discovered->put(from, from);
+       while (!queue->empty()) {
+               const CycleNode *node = queue->back();
+               queue->pop_back();
+               if (node == to)
+                       return true;
+               for (unsigned int i = 0; i < node->getNumEdges(); i++) {
+                       CycleNode *next = node->getEdge(i);
+                       if (!discovered->contains(next)) {
+                               discovered->put(next, next);
+                               queue->push_back(next);
+                       }
+               }
+       }
+       return false;
+}
+
+/**
+ * Checks whether one ModelAction/Promise can reach another ModelAction/Promise
+ * @param from The ModelAction or Promise from which to begin exploration
+ * @param to The ModelAction or Promise to reach
+ * @return True, @a from can reach @a to; otherwise, false
+ */
+template <typename T, typename U>
+bool CycleGraph::checkReachable(const T *from, const U *to) const
+{
+       CycleNode *fromnode = getNode_noCreate(from);
+       CycleNode *tonode = getNode_noCreate(to);
+
+       if (!fromnode || !tonode)
+               return false;
+
+       return checkReachable(fromnode, tonode);
+}
+/* Instantiate four forms of CycleGraph::checkReachable */
+template bool CycleGraph::checkReachable(const ModelAction *from,
+               const ModelAction *to) const;
+template bool CycleGraph::checkReachable(const ModelAction *from,
+               const Promise *to) const;
+template bool CycleGraph::checkReachable(const Promise *from,
+               const ModelAction *to) const;
+template bool CycleGraph::checkReachable(const Promise *from,
+               const Promise *to) const;
+
+/** @return True, if the promise has failed; false otherwise */
+bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const
+{
+       discovered->reset();
+       queue->clear();
+       CycleNode *from = actionToNode.get(fromact);
+
+       queue->push_back(from);
+       discovered->put(from, from);
+       while (!queue->empty()) {
+               const CycleNode *node = queue->back();
+               queue->pop_back();
+
+               if (node->getPromise() == promise)
+                       return true;
+               if (!node->is_promise() &&
+                               promise->eliminate_thread(node->getAction()->get_tid()))
+                       return true;
+
+               for (unsigned int i = 0; i < node->getNumEdges(); i++) {
+                       CycleNode *next = node->getEdge(i);
+                       if (!discovered->contains(next)) {
+                               discovered->put(next, next);
+                               queue->push_back(next);
+                       }
+               }
+       }
+       return false;
+}
+
+/** @brief Begin a new sequence of graph additions which can be rolled back */
+void CycleGraph::startChanges()
+{
+       ASSERT(rollbackvector.empty());
+       ASSERT(rmwrollbackvector.empty());
+       ASSERT(oldCycles == hasCycles);
+}
+
+/** Commit changes to the cyclegraph. */
+void CycleGraph::commitChanges()
+{
+       rollbackvector.clear();
+       rmwrollbackvector.clear();
+       oldCycles = hasCycles;
+}
+
+/** Rollback changes to the previous commit. */
+void CycleGraph::rollbackChanges()
+{
+       for (unsigned int i = 0; i < rollbackvector.size(); i++)
+               rollbackvector[i]->removeEdge();
+
+       for (unsigned int i = 0; i < rmwrollbackvector.size(); i++)
+               rmwrollbackvector[i]->clearRMW();
+
+       hasCycles = oldCycles;
+       rollbackvector.clear();
+       rmwrollbackvector.clear();
+}
+
+/** @returns whether a CycleGraph contains cycles. */
+bool CycleGraph::checkForCycles() const
+{
+       return hasCycles;
+}
+
+/**
+ * @brief Constructor for a CycleNode
+ * @param act The ModelAction for this node
+ */
+CycleNode::CycleNode(const ModelAction *act) :
+       action(act),
+       promise(NULL),
+       hasRMW(NULL)
+{
+}
+
+/**
+ * @brief Constructor for a Promise CycleNode
+ * @param promise The Promise which was generated
+ */
+CycleNode::CycleNode(const Promise *promise) :
+       action(NULL),
+       promise(promise),
+       hasRMW(NULL)
+{
+}
+
+/**
+ * @param i The index of the edge to return
+ * @returns The CycleNode edge indexed by i
+ */
+CycleNode * CycleNode::getEdge(unsigned int i) const
+{
+       return edges[i];
+}
+
+/** @returns The number of edges leaving this CycleNode */
+unsigned int CycleNode::getNumEdges() const
+{
+       return edges.size();
+}
+
+/**
+ * @param i The index of the back edge to return
+ * @returns The CycleNode back-edge indexed by i
+ */
+CycleNode * CycleNode::getBackEdge(unsigned int i) const
+{
+       return back_edges[i];
+}
+
+/** @returns The number of edges entering this CycleNode */
+unsigned int CycleNode::getNumBackEdges() const
+{
+       return back_edges.size();
+}
+
+/**
+ * @brief Remove an element from a vector
+ * @param v The vector
+ * @param n The element to remove
+ * @return True if the element was found; false otherwise
+ */
+template <typename T>
+static bool vector_remove_node(SnapVector<T>& v, const T n)
+{
+       for (unsigned int i = 0; i < v.size(); i++) {
+               if (v[i] == n) {
+                       v.erase(v.begin() + i);
+                       return true;
+               }
+       }
+       return false;
+}
+
+/**
+ * @brief Remove a (forward) edge from this CycleNode
+ * @return The CycleNode which was popped, if one exists; otherwise NULL
+ */
+CycleNode * CycleNode::removeEdge()
+{
+       if (edges.empty())
+               return NULL;
+
+       CycleNode *ret = edges.back();
+       edges.pop_back();
+       vector_remove_node(ret->back_edges, this);
+       return ret;
+}
+
+/**
+ * @brief Remove a (back) edge from this CycleNode
+ * @return The CycleNode which was popped, if one exists; otherwise NULL
+ */
+CycleNode * CycleNode::removeBackEdge()
+{
+       if (back_edges.empty())
+               return NULL;
+
+       CycleNode *ret = back_edges.back();
+       back_edges.pop_back();
+       vector_remove_node(ret->edges, this);
+       return ret;
+}
+
+/**
+ * Adds an edge from this CycleNode to another CycleNode.
+ * @param node The node to which we add a directed edge
+ * @return True if this edge is a new edge; false otherwise
+ */
+bool CycleNode::addEdge(CycleNode *node)
+{
+       for (unsigned int i = 0; i < edges.size(); i++)
+               if (edges[i] == node)
+                       return false;
+       edges.push_back(node);
+       node->back_edges.push_back(this);
+       return true;
+}
+
+/** @returns the RMW CycleNode that reads from the current CycleNode */
+CycleNode * CycleNode::getRMW() const
+{
+       return hasRMW;
+}
+
+/**
+ * Set a RMW action node that reads from the current CycleNode.
+ * @param node The RMW that reads from the current node
+ * @return True, if this node already was read by another RMW; false otherwise
+ * @see CycleGraph::addRMWEdge
+ */
+bool CycleNode::setRMW(CycleNode *node)
+{
+       if (hasRMW != NULL)
+               return true;
+       hasRMW = node;
+       return false;
+}
+
+/**
+ * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be
+ * used when there's no existing ModelAction CycleNode for this write.
+ *
+ * @param writer The ModelAction which wrote the future value represented by
+ * this CycleNode
+ */
+void CycleNode::resolvePromise(const ModelAction *writer)
+{
+       ASSERT(is_promise());
+       ASSERT(promise->is_compatible(writer));
+       action = writer;
+       promise = NULL;
+       ASSERT(!is_promise());
+}
diff --git a/cyclegraph.h b/cyclegraph.h
new file mode 100644 (file)
index 0000000..7e7d180
--- /dev/null
@@ -0,0 +1,136 @@
+/**
+ * @file cyclegraph.h
+ * @brief Data structure to track ordering constraints on modification order
+ *
+ * Used to determine whether a total order exists that satisfies the ordering
+ * constraints.
+ */
+
+#ifndef __CYCLEGRAPH_H__
+#define __CYCLEGRAPH_H__
+
+#include <inttypes.h>
+#include <stdio.h>
+
+#include "hashtable.h"
+#include "config.h"
+#include "mymemory.h"
+#include "stl-model.h"
+
+class Promise;
+class CycleNode;
+class ModelAction;
+
+/** @brief A graph of Model Actions for tracking cycles. */
+class CycleGraph {
+ public:
+       CycleGraph();
+       ~CycleGraph();
+
+       template <typename T, typename U>
+       bool addEdge(const T *from, const U *to);
+
+       template <typename T>
+       void addRMWEdge(const T *from, const ModelAction *rmw);
+
+       bool checkForCycles() const;
+       bool checkPromise(const ModelAction *from, Promise *p) const;
+
+       template <typename T, typename U>
+       bool checkReachable(const T *from, const U *to) const;
+
+       void startChanges();
+       void commitChanges();
+       void rollbackChanges();
+#if SUPPORT_MOD_ORDER_DUMP
+       void dumpNodes(FILE *file) const;
+       void dumpGraphToFile(const char *filename) const;
+
+       void dot_print_node(FILE *file, const ModelAction *act);
+       template <typename T, typename U>
+       void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop);
+#endif
+
+       bool resolvePromise(const Promise *promise, ModelAction *writer);
+
+       SNAPSHOTALLOC
+ private:
+       bool addNodeEdge(CycleNode *fromnode, CycleNode *tonode);
+       void putNode(const ModelAction *act, CycleNode *node);
+       void putNode(const Promise *promise, CycleNode *node);
+       void erasePromiseNode(const Promise *promise);
+       CycleNode * getNode(const ModelAction *act);
+       CycleNode * getNode(const Promise *promise);
+       CycleNode * getNode_noCreate(const ModelAction *act) const;
+       CycleNode * getNode_noCreate(const Promise *promise) const;
+       bool mergeNodes(CycleNode *node1, CycleNode *node2);
+
+       HashTable<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
+       ModelVector<const CycleNode *> * queue;
+
+
+       /** @brief A table for mapping ModelActions to CycleNodes */
+       HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
+       /** @brief A table for mapping Promises to CycleNodes */
+       HashTable<const Promise *, CycleNode *, uintptr_t, 4> promiseToNode;
+
+#if SUPPORT_MOD_ORDER_DUMP
+       SnapVector<CycleNode *> nodeList;
+#endif
+
+       bool checkReachable(const CycleNode *from, const CycleNode *to) const;
+
+       /** @brief A flag: true if this graph contains cycles */
+       bool hasCycles;
+       /** @brief The previous value of CycleGraph::hasCycles, for rollback */
+       bool oldCycles;
+
+       SnapVector<CycleNode *> rollbackvector;
+       SnapVector<CycleNode *> rmwrollbackvector;
+};
+
+/**
+ * @brief A node within a CycleGraph; corresponds either to one ModelAction or
+ * to a promised future value
+ */
+class CycleNode {
+ public:
+       CycleNode(const ModelAction *act);
+       CycleNode(const Promise *promise);
+       bool addEdge(CycleNode *node);
+       CycleNode * getEdge(unsigned int i) const;
+       unsigned int getNumEdges() const;
+       CycleNode * getBackEdge(unsigned int i) const;
+       unsigned int getNumBackEdges() const;
+       CycleNode * removeEdge();
+       CycleNode * removeBackEdge();
+
+       bool setRMW(CycleNode *);
+       CycleNode * getRMW() const;
+       void clearRMW() { hasRMW = NULL; }
+       const ModelAction * getAction() const { return action; }
+       const Promise * getPromise() const { return promise; }
+       bool is_promise() const { return !action; }
+       void resolvePromise(const ModelAction *writer);
+
+       SNAPSHOTALLOC
+ private:
+       /** @brief The ModelAction that this node represents */
+       const ModelAction *action;
+
+       /** @brief The promise represented by this node; only valid when action
+        * is NULL */
+       const Promise *promise;
+
+       /** @brief The edges leading out from this node */
+       SnapVector<CycleNode *> edges;
+
+       /** @brief The edges leading into this node */
+       SnapVector<CycleNode *> back_edges;
+
+       /** Pointer to a RMW node that reads from this node, or NULL, if none
+        * exists */
+       CycleNode *hasRMW;
+};
+
+#endif /* __CYCLEGRAPH_H__ */
diff --git a/datarace.cc b/datarace.cc
new file mode 100644 (file)
index 0000000..653039b
--- /dev/null
@@ -0,0 +1,363 @@
+#include "datarace.h"
+#include "model.h"
+#include "threads-model.h"
+#include <stdio.h>
+#include <cstring>
+#include "mymemory.h"
+#include "clockvector.h"
+#include "config.h"
+#include "action.h"
+#include "execution.h"
+#include "stl-model.h"
+
+static struct ShadowTable *root;
+static SnapVector<DataRace *> *unrealizedraces;
+static void *memory_base;
+static void *memory_top;
+
+static const ModelExecution * get_execution()
+{
+       return model->get_execution();
+}
+
+/** This function initialized the data race detector. */
+void initRaceDetector()
+{
+       root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
+       memory_base = snapshot_calloc(sizeof(struct ShadowBaseTable) * SHADOWBASETABLES, 1);
+       memory_top = ((char *)memory_base) + sizeof(struct ShadowBaseTable) * SHADOWBASETABLES;
+       unrealizedraces = new SnapVector<DataRace *>();
+}
+
+void * table_calloc(size_t size)
+{
+       if ((((char *)memory_base) + size) > memory_top) {
+               return snapshot_calloc(size, 1);
+       } else {
+               void *tmp = memory_base;
+               memory_base = ((char *)memory_base) + size;
+               return tmp;
+       }
+}
+
+/** This function looks up the entry in the shadow table corresponding to a
+ * given address.*/
+static uint64_t * lookupAddressEntry(const void *address)
+{
+       struct ShadowTable *currtable = root;
+#if BIT48
+       currtable = (struct ShadowTable *) currtable->array[(((uintptr_t)address) >> 32) & MASK16BIT];
+       if (currtable == NULL) {
+               currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address) >> 32) & MASK16BIT] = table_calloc(sizeof(struct ShadowTable)));
+       }
+#endif
+
+       struct ShadowBaseTable *basetable = (struct ShadowBaseTable *)currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT];
+       if (basetable == NULL) {
+               basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address) >> 16) & MASK16BIT] = table_calloc(sizeof(struct ShadowBaseTable)));
+       }
+       return &basetable->array[((uintptr_t)address) & MASK16BIT];
+}
+
+/**
+ * Compares a current clock-vector/thread-ID pair with a clock/thread-ID pair
+ * to check the potential for a data race.
+ * @param clock1 The current clock vector
+ * @param tid1 The current thread; paired with clock1
+ * @param clock2 The clock value for the potentially-racing action
+ * @param tid2 The thread ID for the potentially-racing action
+ * @return true if the current clock allows a race with the event at clock2/tid2
+ */
+static bool clock_may_race(ClockVector *clock1, thread_id_t tid1,
+                           modelclock_t clock2, thread_id_t tid2)
+{
+       return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2;
+}
+
+/**
+ * Expands a record from the compact form to the full form.  This is
+ * necessary for multiple readers or for very large thread ids or time
+ * stamps. */
+static void expandRecord(uint64_t *shadow)
+{
+       uint64_t shadowval = *shadow;
+
+       modelclock_t readClock = READVECTOR(shadowval);
+       thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
+       modelclock_t writeClock = WRITEVECTOR(shadowval);
+       thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
+
+       struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
+       record->writeThread = writeThread;
+       record->writeClock = writeClock;
+
+       if (readClock != 0) {
+               record->capacity = INITCAPACITY;
+               record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * record->capacity);
+               record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * record->capacity);
+               record->numReads = 1;
+               record->thread[0] = readThread;
+               record->readClock[0] = readClock;
+       }
+       *shadow = (uint64_t) record;
+}
+
+/** This function is called when we detect a data race.*/
+static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, const void *address)
+{
+       struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
+       race->oldthread = oldthread;
+       race->oldclock = oldclock;
+       race->isoldwrite = isoldwrite;
+       race->newaction = newaction;
+       race->isnewwrite = isnewwrite;
+       race->address = address;
+       unrealizedraces->push_back(race);
+
+       /* If the race is realized, bail out now. */
+       if (checkDataRaces())
+               model->switch_to_master(NULL);
+}
+
+/**
+ * @brief Check and report data races
+ *
+ * If the trace is feasible (a feasible prefix), clear out the list of
+ * unrealized data races, asserting any realized ones as execution bugs so that
+ * the model-checker will end the execution.
+ *
+ * @return True if any data races were realized
+ */
+bool checkDataRaces()
+{
+       if (get_execution()->isfeasibleprefix()) {
+               bool race_asserted = false;
+               /* Prune the non-racing unrealized dataraces */
+               for (unsigned i = 0; i < unrealizedraces->size(); i++) {
+                       struct DataRace *race = (*unrealizedraces)[i];
+                       if (clock_may_race(race->newaction->get_cv(), race->newaction->get_tid(), race->oldclock, race->oldthread)) {
+                               assert_race(race);
+                               race_asserted = true;
+                       }
+                       snapshot_free(race);
+               }
+               unrealizedraces->clear();
+               return race_asserted;
+       }
+       return false;
+}
+
+/**
+ * @brief Assert a data race
+ *
+ * Asserts a data race which is currently realized, causing the execution to
+ * end and stashing a message in the model-checker's bug list
+ *
+ * @param race The race to report
+ */
+void assert_race(struct DataRace *race)
+{
+       model->assert_bug(
+                       "Data race detected @ address %p:\n"
+                       "    Access 1: %5s in thread %2d @ clock %3u\n"
+                       "    Access 2: %5s in thread %2d @ clock %3u",
+                       race->address,
+                       race->isoldwrite ? "write" : "read",
+                       id_to_int(race->oldthread),
+                       race->oldclock,
+                       race->isnewwrite ? "write" : "read",
+                       id_to_int(race->newaction->get_tid()),
+                       race->newaction->get_seq_number()
+               );
+}
+
+/** This function does race detection for a write on an expanded record. */
+void fullRaceCheckWrite(thread_id_t thread, void *location, uint64_t *shadow, ClockVector *currClock)
+{
+       struct RaceRecord *record = (struct RaceRecord *)(*shadow);
+
+       /* Check for datarace against last read. */
+
+       for (int i = 0; i < record->numReads; i++) {
+               modelclock_t readClock = record->readClock[i];
+               thread_id_t readThread = record->thread[i];
+
+               /* Note that readClock can't actuall be zero here, so it could be
+                        optimized. */
+
+               if (clock_may_race(currClock, thread, readClock, readThread)) {
+                       /* We have a datarace */
+                       reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
+               }
+       }
+
+       /* Check for datarace against last write. */
+
+       modelclock_t writeClock = record->writeClock;
+       thread_id_t writeThread = record->writeThread;
+
+       if (clock_may_race(currClock, thread, writeClock, writeThread)) {
+               /* We have a datarace */
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
+       }
+
+       record->numReads = 0;
+       record->writeThread = thread;
+       modelclock_t ourClock = currClock->getClock(thread);
+       record->writeClock = ourClock;
+}
+
+/** This function does race detection on a write. */
+void raceCheckWrite(thread_id_t thread, void *location)
+{
+       uint64_t *shadow = lookupAddressEntry(location);
+       uint64_t shadowval = *shadow;
+       ClockVector *currClock = get_execution()->get_cv(thread);
+
+       /* Do full record */
+       if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
+               fullRaceCheckWrite(thread, location, shadow, currClock);
+               return;
+       }
+
+       int threadid = id_to_int(thread);
+       modelclock_t ourClock = currClock->getClock(thread);
+
+       /* Thread ID is too large or clock is too large. */
+       if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
+               expandRecord(shadow);
+               fullRaceCheckWrite(thread, location, shadow, currClock);
+               return;
+       }
+
+       /* Check for datarace against last read. */
+
+       modelclock_t readClock = READVECTOR(shadowval);
+       thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
+
+       if (clock_may_race(currClock, thread, readClock, readThread)) {
+               /* We have a datarace */
+               reportDataRace(readThread, readClock, false, get_execution()->get_parent_action(thread), true, location);
+       }
+
+       /* Check for datarace against last write. */
+
+       modelclock_t writeClock = WRITEVECTOR(shadowval);
+       thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
+
+       if (clock_may_race(currClock, thread, writeClock, writeThread)) {
+               /* We have a datarace */
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), true, location);
+       }
+       *shadow = ENCODEOP(0, 0, threadid, ourClock);
+}
+
+/** This function does race detection on a read for an expanded record. */
+void fullRaceCheckRead(thread_id_t thread, const void *location, uint64_t *shadow, ClockVector *currClock)
+{
+       struct RaceRecord *record = (struct RaceRecord *) (*shadow);
+
+       /* Check for datarace against last write. */
+
+       modelclock_t writeClock = record->writeClock;
+       thread_id_t writeThread = record->writeThread;
+
+       if (clock_may_race(currClock, thread, writeClock, writeThread)) {
+               /* We have a datarace */
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
+       }
+
+       /* Shorten vector when possible */
+
+       int copytoindex = 0;
+
+       for (int i = 0; i < record->numReads; i++) {
+               modelclock_t readClock = record->readClock[i];
+               thread_id_t readThread = record->thread[i];
+
+               /*  Note that is not really a datarace check as reads cannott
+                               actually race.  It is just determining that this read subsumes
+                               another in the sense that either this read races or neither
+                               read races. Note that readClock can't actually be zero, so it
+                               could be optimized.  */
+
+               if (clock_may_race(currClock, thread, readClock, readThread)) {
+                       /* Still need this read in vector */
+                       if (copytoindex != i) {
+                               record->readClock[copytoindex] = record->readClock[i];
+                               record->thread[copytoindex] = record->thread[i];
+                       }
+                       copytoindex++;
+               }
+       }
+
+       if (copytoindex >= record->capacity) {
+               int newCapacity = record->capacity * 2;
+               thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t) * newCapacity);
+               modelclock_t *newreadClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t) * newCapacity);
+               std::memcpy(newthread, record->thread, record->capacity * sizeof(thread_id_t));
+               std::memcpy(newreadClock, record->readClock, record->capacity * sizeof(modelclock_t));
+               snapshot_free(record->readClock);
+               snapshot_free(record->thread);
+               record->readClock = newreadClock;
+               record->thread = newthread;
+               record->capacity = newCapacity;
+       }
+
+       modelclock_t ourClock = currClock->getClock(thread);
+
+       record->thread[copytoindex] = thread;
+       record->readClock[copytoindex] = ourClock;
+       record->numReads = copytoindex + 1;
+}
+
+/** This function does race detection on a read. */
+void raceCheckRead(thread_id_t thread, const void *location)
+{
+       uint64_t *shadow = lookupAddressEntry(location);
+       uint64_t shadowval = *shadow;
+       ClockVector *currClock = get_execution()->get_cv(thread);
+
+       /* Do full record */
+       if (shadowval != 0 && !ISSHORTRECORD(shadowval)) {
+               fullRaceCheckRead(thread, location, shadow, currClock);
+               return;
+       }
+
+       int threadid = id_to_int(thread);
+       modelclock_t ourClock = currClock->getClock(thread);
+
+       /* Thread ID is too large or clock is too large. */
+       if (threadid > MAXTHREADID || ourClock > MAXWRITEVECTOR) {
+               expandRecord(shadow);
+               fullRaceCheckRead(thread, location, shadow, currClock);
+               return;
+       }
+
+       /* Check for datarace against last write. */
+
+       modelclock_t writeClock = WRITEVECTOR(shadowval);
+       thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
+
+       if (clock_may_race(currClock, thread, writeClock, writeThread)) {
+               /* We have a datarace */
+               reportDataRace(writeThread, writeClock, true, get_execution()->get_parent_action(thread), false, location);
+       }
+
+       modelclock_t readClock = READVECTOR(shadowval);
+       thread_id_t readThread = int_to_id(RDTHREADID(shadowval));
+
+       if (clock_may_race(currClock, thread, readClock, readThread)) {
+               /* We don't subsume this read... Have to expand record. */
+               expandRecord(shadow);
+               fullRaceCheckRead(thread, location, shadow, currClock);
+               return;
+       }
+
+       *shadow = ENCODEOP(threadid, ourClock, id_to_int(writeThread), writeClock);
+}
+
+bool haveUnrealizedRaces()
+{
+       return !unrealizedraces->empty();
+}
diff --git a/datarace.h b/datarace.h
new file mode 100644 (file)
index 0000000..737a6d6
--- /dev/null
@@ -0,0 +1,94 @@
+/** @file datarace.h
+ *  @brief Data race detection code.
+ */
+
+#ifndef __DATARACE_H__
+#define __DATARACE_H__
+
+#include "config.h"
+#include <stdint.h>
+#include "modeltypes.h"
+
+/* Forward declaration */
+class ModelAction;
+
+struct ShadowTable {
+       void * array[65536];
+};
+
+struct ShadowBaseTable {
+       uint64_t array[65536];
+};
+
+struct DataRace {
+       /* Clock and thread associated with first action.  This won't change in
+                response to synchronization. */
+
+       thread_id_t oldthread;
+       modelclock_t oldclock;
+       /* Record whether this is a write, so we can tell the user. */
+       bool isoldwrite;
+
+       /* Model action associated with second action.  This could change as
+                a result of synchronization. */
+       ModelAction *newaction;
+       /* Record whether this is a write, so we can tell the user. */
+       bool isnewwrite;
+
+       /* Address of data race. */
+       const void *address;
+};
+
+#define MASK16BIT 0xffff
+
+void initRaceDetector();
+void raceCheckWrite(thread_id_t thread, void *location);
+void raceCheckRead(thread_id_t thread, const void *location);
+bool checkDataRaces();
+void assert_race(struct DataRace *race);
+bool haveUnrealizedRaces();
+
+/**
+ * @brief A record of information for detecting data races
+ */
+struct RaceRecord {
+       modelclock_t *readClock;
+       thread_id_t *thread;
+       int capacity;
+       int numReads;
+       thread_id_t writeThread;
+       modelclock_t writeClock;
+};
+
+#define INITCAPACITY 4
+
+#define ISSHORTRECORD(x) ((x)&0x1)
+
+#define THREADMASK 0xff
+#define RDTHREADID(x) (((x)>>1)&THREADMASK)
+#define READMASK 0x07fffff
+#define READVECTOR(x) (((x)>>9)&READMASK)
+
+#define WRTHREADID(x) (((x)>>32)&THREADMASK)
+
+#define WRITEMASK READMASK
+#define WRITEVECTOR(x) (((x)>>40)&WRITEMASK)
+
+/**
+ * The basic encoding idea is that (void *) either:
+ *  -# points to a full record (RaceRecord) or
+ *  -# encodes the information in a 64 bit word. Encoding is as
+ *     follows:
+ *     - lowest bit set to 1
+ *     - next 8 bits are read thread id
+ *     - next 23 bits are read clock vector
+ *     - next 8 bits are write thread id
+ *     - next 23 bits are write clock vector
+ */
+#define ENCODEOP(rdthread, rdtime, wrthread, wrtime) (0x1ULL | ((rdthread)<<1) | ((rdtime) << 9) | (((uint64_t)wrthread)<<32) | (((uint64_t)wrtime)<<40))
+
+#define MAXTHREADID (THREADMASK-1)
+#define MAXREADVECTOR (READMASK-1)
+#define MAXWRITEVECTOR (WRITEMASK-1)
+
+#endif /* __DATARACE_H__ */
diff --git a/doc/Markdown/License.text b/doc/Markdown/License.text
new file mode 100644 (file)
index 0000000..6d76506
--- /dev/null
@@ -0,0 +1,30 @@
+Copyright (c) 2004, John Gruber  
+<http://daringfireball.net/>  
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+* Redistributions of source code must retain the above copyright notice,
+  this list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright
+  notice, this list of conditions and the following disclaimer in the
+  documentation and/or other materials provided with the distribution.
+
+* Neither the name "Markdown" nor the names of its contributors may
+  be used to endorse or promote products derived from this software
+  without specific prior written permission.
+
+This software is provided by the copyright holders and contributors "as
+is" and any express or implied warranties, including, but not limited
+to, the implied warranties of merchantability and fitness for a
+particular purpose are disclaimed. In no event shall the copyright owner
+or contributors be liable for any direct, indirect, incidental, special,
+exemplary, or consequential damages (including, but not limited to,
+procurement of substitute goods or services; loss of use, data, or
+profits; or business interruption) however caused and on any theory of
+liability, whether in contract, strict liability, or tort (including
+negligence or otherwise) arising in any way out of the use of this
+software, even if advised of the possibility of such damage.
diff --git a/doc/Markdown/Markdown Readme.text b/doc/Markdown/Markdown Readme.text
new file mode 100644 (file)
index 0000000..6fbb95f
--- /dev/null
@@ -0,0 +1,341 @@
+Markdown
+========
+
+Version 1.0.1 - Tue 14 Dec 2004
+
+by John Gruber  
+<http://daringfireball.net/>
+
+
+Introduction
+------------
+
+Markdown is a text-to-HTML conversion tool for web writers. Markdown
+allows you to write using an easy-to-read, easy-to-write plain text
+format, then convert it to structurally valid XHTML (or HTML).
+
+Thus, "Markdown" is two things: a plain text markup syntax, and a
+software tool, written in Perl, that converts the plain text markup 
+to HTML.
+
+Markdown works both as a Movable Type plug-in and as a standalone Perl
+script -- which means it can also be used as a text filter in BBEdit
+(or any other application that supporst filters written in Perl).
+
+Full documentation of Markdown's syntax and configuration options is
+available on the web: <http://daringfireball.net/projects/markdown/>.
+(Note: this readme file is formatted in Markdown.)
+
+
+
+Installation and Requirements
+-----------------------------
+
+Markdown requires Perl 5.6.0 or later. Welcome to the 21st Century.
+Markdown also requires the standard Perl library module `Digest::MD5`. 
+
+
+### Movable Type ###
+
+Markdown works with Movable Type version 2.6 or later (including 
+MT 3.0 or later).
+
+1.  Copy the "Markdown.pl" file into your Movable Type "plugins"
+    directory. The "plugins" directory should be in the same directory
+    as "mt.cgi"; if the "plugins" directory doesn't already exist, use
+    your FTP program to create it. Your installation should look like
+    this:
+
+        (mt home)/plugins/Markdown.pl
+
+2.  Once installed, Markdown will appear as an option in Movable Type's
+    Text Formatting pop-up menu. This is selectable on a per-post basis.
+    Markdown translates your posts to HTML when you publish; the posts
+    themselves are stored in your MT database in Markdown format.
+
+3.  If you also install SmartyPants 1.5 (or later), Markdown will offer
+    a second text formatting option: "Markdown with SmartyPants". This
+    option is the same as the regular "Markdown" formatter, except that
+    automatically uses SmartyPants to create typographically correct
+    curly quotes, em-dashes, and ellipses. See the SmartyPants web page
+    for more information: <http://daringfireball.net/projects/smartypants/>
+
+4.  To make Markdown (or "Markdown with SmartyPants") your default
+    text formatting option for new posts, go to Weblog Config ->
+    Preferences.
+
+Note that by default, Markdown produces XHTML output. To configure
+Markdown to produce HTML 4 output, see "Configuration", below.
+
+
+### Blosxom ###
+
+Markdown works with Blosxom version 2.x.
+
+1.  Rename the "Markdown.pl" plug-in to "Markdown" (case is
+    important). Movable Type requires plug-ins to have a ".pl"
+    extension; Blosxom forbids it.
+
+2.  Copy the "Markdown" plug-in file to your Blosxom plug-ins folder.
+    If you're not sure where your Blosxom plug-ins folder is, see the
+    Blosxom documentation for information.
+
+3.  That's it. The entries in your weblog will now automatically be
+    processed by Markdown.
+
+4.  If you'd like to apply Markdown formatting only to certain posts,
+    rather than all of them, see Jason Clark's instructions for using
+    Markdown in conjunction with Blosxom's Meta plugin:
+    
+    <http://jclark.org/weblog/WebDev/Blosxom/Markdown.html>
+
+
+### BBEdit ###
+
+Markdown works with BBEdit 6.1 or later on Mac OS X. (It also works
+with BBEdit 5.1 or later and MacPerl 5.6.1 on Mac OS 8.6 or later.)
+
+1.  Copy the "Markdown.pl" file to appropriate filters folder in your
+    "BBEdit Support" folder. On Mac OS X, this should be:
+
+        BBEdit Support/Unix Support/Unix Filters/
+
+    See the BBEdit documentation for more details on the location of
+    these folders.
+
+    You can rename "Markdown.pl" to whatever you wish.
+
+2.  That's it. To use Markdown, select some text in a BBEdit document,
+    then choose Markdown from the Filters sub-menu in the "#!" menu, or
+    the Filters floating palette
+
+
+
+Configuration
+-------------
+
+By default, Markdown produces XHTML output for tags with empty elements.
+E.g.:
+
+    <br />
+
+Markdown can be configured to produce HTML-style tags; e.g.:
+
+    <br>
+
+
+### Movable Type ###
+
+You need to use a special `MTMarkdownOptions` container tag in each
+Movable Type template where you want HTML 4-style output:
+
+    <MTMarkdownOptions output='html4'>
+        ... put your entry content here ...
+    </MTMarkdownOptions>
+
+The easiest way to use MTMarkdownOptions is probably to put the
+opening tag right after your `<body>` tag, and the closing tag right
+before `</body>`.
+
+To suppress Markdown processing in a particular template, i.e. to
+publish the raw Markdown-formatted text without translation into
+(X)HTML, set the `output` attribute to 'raw':
+
+    <MTMarkdownOptions output='raw'>
+        ... put your entry content here ...
+    </MTMarkdownOptions>
+
+
+### Command-Line ###
+
+Use the `--html4tags` command-line switch to produce HTML output from a
+Unix-style command line. E.g.:
+
+    % perl Markdown.pl --html4tags foo.text
+
+Type `perldoc Markdown.pl`, or read the POD documentation within the
+Markdown.pl source code for more information.
+
+
+
+Bugs
+----
+
+To file bug reports or feature requests please send email to:
+<markdown@daringfireball.net>.
+
+
+
+Version History
+---------------
+
+1.0.1 (14 Dec 2004):
+
++      Changed the syntax rules for code blocks and spans. Previously,
+       backslash escapes for special Markdown characters were processed
+       everywhere other than within inline HTML tags. Now, the contents
+       of code blocks and spans are no longer processed for backslash
+       escapes. This means that code blocks and spans are now treated
+       literally, with no special rules to worry about regarding
+       backslashes.
+
+       **NOTE**: This changes the syntax from all previous versions of
+       Markdown. Code blocks and spans involving backslash characters
+       will now generate different output than before.
+
++      Tweaked the rules for link definitions so that they must occur
+       within three spaces of the left margin. Thus if you indent a link
+       definition by four spaces or a tab, it will now be a code block.
+       
+                  [a]: /url/  "Indented 3 spaces, this is a link def"
+
+                   [b]: /url/  "Indented 4 spaces, this is a code block"
+       
+       **IMPORTANT**: This may affect existing Markdown content if it
+       contains link definitions indented by 4 or more spaces.
+
++      Added `>`, `+`, and `-` to the list of backslash-escapable
+       characters. These should have been done when these characters
+       were added as unordered list item markers.
+
++      Trailing spaces and tabs following HTML comments and `<hr/>` tags
+       are now ignored.
+
++      Inline links using `<` and `>` URL delimiters weren't working:
+
+               like [this](<http://example.com/>)
+
++      Added a bit of tolerance for trailing spaces and tabs after
+       Markdown hr's.
+
++      Fixed bug where auto-links were being processed within code spans:
+
+               like this: `<http://example.com/>`
+
++      Sort-of fixed a bug where lines in the middle of hard-wrapped
+       paragraphs, which lines look like the start of a list item,
+       would accidentally trigger the creation of a list. E.g. a
+       paragraph that looked like this:
+
+               I recommend upgrading to version
+               8. Oops, now this line is treated
+               as a sub-list.
+
+       This is fixed for top-level lists, but it can still happen for
+       sub-lists. E.g., the following list item will not be parsed
+       properly:
+
+               +       I recommend upgrading to version
+                       8. Oops, now this line is treated
+                       as a sub-list.
+
+       Given Markdown's list-creation rules, I'm not sure this can
+       be fixed.
+
++      Standalone HTML comments are now handled; previously, they'd get
+       wrapped in a spurious `<p>` tag.
+
++      Fix for horizontal rules preceded by 2 or 3 spaces.
+
++      `<hr>` HTML tags in must occur within three spaces of left
+       margin. (With 4 spaces or a tab, they should be code blocks, but
+       weren't before this fix.)
+
++      Capitalized "With" in "Markdown With SmartyPants" for
+       consistency with the same string label in SmartyPants.pl.
+       (This fix is specific to the MT plug-in interface.)
+
++      Auto-linked email address can now optionally contain
+       a 'mailto:' protocol. I.e. these are equivalent:
+
+               <mailto:user@example.com>
+               <user@example.com>
+
++      Fixed annoying bug where nested lists would wind up with
+       spurious (and invalid) `<p>` tags.
+
++      You can now write empty links:
+
+               [like this]()
+
+       and they'll be turned into anchor tags with empty href attributes.
+       This should have worked before, but didn't.
+
++      `***this***` and `___this___` are now turned into
+
+               <strong><em>this</em></strong>
+
+       Instead of
+
+               <strong><em>this</strong></em>
+
+       which isn't valid. (Thanks to Michel Fortin for the fix.)
+
++      Added a new substitution in `_EncodeCode()`: s/\$/&#036;/g; This
+       is only for the benefit of Blosxom users, because Blosxom
+       (sometimes?) interpolates Perl scalars in your article bodies.
+
++      Fixed problem for links defined with urls that include parens, e.g.:
+
+               [1]: http://sources.wikipedia.org/wiki/Middle_East_Policy_(Chomsky)
+
+       "Chomsky" was being erroneously treated as the URL's title.
+
++      At some point during 1.0's beta cycle, I changed every sub's
+       argument fetching from this idiom:
+
+               my $text = shift;
+
+       to:
+
+               my $text = shift || return '';
+
+       The idea was to keep Markdown from doing any work in a sub
+       if the input was empty. This introduced a bug, though:
+       if the input to any function was the single-character string
+       "0", it would also evaluate as false and return immediately.
+       How silly. Now fixed.
+
+
+
+Donations
+---------
+
+Donations to support Markdown's development are happily accepted. See:
+<http://daringfireball.net/projects/markdown/> for details.
+
+
+
+Copyright and License
+---------------------
+
+Copyright (c) 2003-2004 John Gruber   
+<http://daringfireball.net/>   
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+* Redistributions of source code must retain the above copyright notice,
+  this list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright
+  notice, this list of conditions and the following disclaimer in the
+  documentation and/or other materials provided with the distribution.
+
+* Neither the name "Markdown" nor the names of its contributors may
+  be used to endorse or promote products derived from this software
+  without specific prior written permission.
+
+This software is provided by the copyright holders and contributors "as
+is" and any express or implied warranties, including, but not limited
+to, the implied warranties of merchantability and fitness for a
+particular purpose are disclaimed. In no event shall the copyright owner
+or contributors be liable for any direct, indirect, incidental, special,
+exemplary, or consequential damages (including, but not limited to,
+procurement of substitute goods or services; loss of use, data, or
+profits; or business interruption) however caused and on any theory of
+liability, whether in contract, strict liability, or tort (including
+negligence or otherwise) arising in any way out of the use of this
+software, even if advised of the possibility of such damage.
diff --git a/doc/Markdown/Markdown.pl b/doc/Markdown/Markdown.pl
new file mode 100755 (executable)
index 0000000..e4c8469
--- /dev/null
@@ -0,0 +1,1450 @@
+#!/usr/bin/perl
+
+#
+# Markdown -- A text-to-HTML conversion tool for web writers
+#
+# Copyright (c) 2004 John Gruber
+# <http://daringfireball.net/projects/markdown/>
+#
+
+
+package Markdown;
+require 5.006_000;
+use strict;
+use warnings;
+
+use Digest::MD5 qw(md5_hex);
+use vars qw($VERSION);
+$VERSION = '1.0.1';
+# Tue 14 Dec 2004
+
+## Disabled; causes problems under Perl 5.6.1:
+# use utf8;
+# binmode( STDOUT, ":utf8" );  # c.f.: http://acis.openlib.org/dev/perl-unicode-struggle.html
+
+
+#
+# Global default settings:
+#
+my $g_empty_element_suffix = " />";     # Change to ">" for HTML output
+my $g_tab_width = 4;
+
+
+#
+# Globals:
+#
+
+# Regex to match balanced [brackets]. See Friedl's
+# "Mastering Regular Expressions", 2nd Ed., pp. 328-331.
+my $g_nested_brackets;
+$g_nested_brackets = qr{
+       (?>                                                             # Atomic matching
+          [^\[\]]+                                                     # Anything other than brackets
+        | 
+          \[
+                (??{ $g_nested_brackets })             # Recursive set of nested brackets
+          \]
+       )*
+}x;
+
+
+# Table of hash values for escaped characters:
+my %g_escape_table;
+foreach my $char (split //, '\\`*_{}[]()>#+-.!') {
+       $g_escape_table{$char} = md5_hex($char);
+}
+
+
+# Global hashes, used by various utility routines
+my %g_urls;
+my %g_titles;
+my %g_html_blocks;
+
+# Used to track when we're inside an ordered or unordered list
+# (see _ProcessListItems() for details):
+my $g_list_level = 0;
+
+
+#### Blosxom plug-in interface ##########################################
+
+# Set $g_blosxom_use_meta to 1 to use Blosxom's meta plug-in to determine
+# which posts Markdown should process, using a "meta-markup: markdown"
+# header. If it's set to 0 (the default), Markdown will process all
+# entries.
+my $g_blosxom_use_meta = 0;
+
+sub start { 1; }
+sub story {
+       my($pkg, $path, $filename, $story_ref, $title_ref, $body_ref) = @_;
+
+       if ( (! $g_blosxom_use_meta) or
+            (defined($meta::markup) and ($meta::markup =~ /^\s*markdown\s*$/i))
+            ){
+                       $$body_ref  = Markdown($$body_ref);
+     }
+     1;
+}
+
+
+#### Movable Type plug-in interface #####################################
+eval {require MT};  # Test to see if we're running in MT.
+unless ($@) {
+    require MT;
+    import  MT;
+    require MT::Template::Context;
+    import  MT::Template::Context;
+
+       eval {require MT::Plugin};  # Test to see if we're running >= MT 3.0.
+       unless ($@) {
+               require MT::Plugin;
+               import  MT::Plugin;
+               my $plugin = new MT::Plugin({
+                       name => "Markdown",
+                       description => "A plain-text-to-HTML formatting plugin. (Version: $VERSION)",
+                       doc_link => 'http://daringfireball.net/projects/markdown/'
+               });
+               MT->add_plugin( $plugin );
+       }
+
+       MT::Template::Context->add_container_tag(MarkdownOptions => sub {
+               my $ctx  = shift;
+               my $args = shift;
+               my $builder = $ctx->stash('builder');
+               my $tokens = $ctx->stash('tokens');
+
+               if (defined ($args->{'output'}) ) {
+                       $ctx->stash('markdown_output', lc $args->{'output'});
+               }
+
+               defined (my $str = $builder->build($ctx, $tokens) )
+                       or return $ctx->error($builder->errstr);
+               $str;           # return value
+       });
+
+       MT->add_text_filter('markdown' => {
+               label     => 'Markdown',
+               docs      => 'http://daringfireball.net/projects/markdown/',
+               on_format => sub {
+                       my $text = shift;
+                       my $ctx  = shift;
+                       my $raw  = 0;
+                   if (defined $ctx) {
+                       my $output = $ctx->stash('markdown_output'); 
+                               if (defined $output  &&  $output =~ m/^html/i) {
+                                       $g_empty_element_suffix = ">";
+                                       $ctx->stash('markdown_output', '');
+                               }
+                               elsif (defined $output  &&  $output eq 'raw') {
+                                       $raw = 1;
+                                       $ctx->stash('markdown_output', '');
+                               }
+                               else {
+                                       $raw = 0;
+                                       $g_empty_element_suffix = " />";
+                               }
+                       }
+                       $text = $raw ? $text : Markdown($text);
+                       $text;
+               },
+       });
+
+       # If SmartyPants is loaded, add a combo Markdown/SmartyPants text filter:
+       my $smartypants;
+
+       {
+               no warnings "once";
+               $smartypants = $MT::Template::Context::Global_filters{'smarty_pants'};
+       }
+
+       if ($smartypants) {
+               MT->add_text_filter('markdown_with_smartypants' => {
+                       label     => 'Markdown With SmartyPants',
+                       docs      => 'http://daringfireball.net/projects/markdown/',
+                       on_format => sub {
+                               my $text = shift;
+                               my $ctx  = shift;
+                               if (defined $ctx) {
+                                       my $output = $ctx->stash('markdown_output'); 
+                                       if (defined $output  &&  $output eq 'html') {
+                                               $g_empty_element_suffix = ">";
+                                       }
+                                       else {
+                                               $g_empty_element_suffix = " />";
+                                       }
+                               }
+                               $text = Markdown($text);
+                               $text = $smartypants->($text, '1');
+                       },
+               });
+       }
+}
+else {
+#### BBEdit/command-line text filter interface ##########################
+# Needs to be hidden from MT (and Blosxom when running in static mode).
+
+    # We're only using $blosxom::version once; tell Perl not to warn us:
+       no warnings 'once';
+    unless ( defined($blosxom::version) ) {
+               use warnings;
+
+               #### Check for command-line switches: #################
+               my %cli_opts;
+               use Getopt::Long;
+               Getopt::Long::Configure('pass_through');
+               GetOptions(\%cli_opts,
+                       'version',
+                       'shortversion',
+                       'html4tags',
+               );
+               if ($cli_opts{'version'}) {             # Version info
+                       print "\nThis is Markdown, version $VERSION.\n";
+                       print "Copyright 2004 John Gruber\n";
+                       print "http://daringfireball.net/projects/markdown/\n\n";
+                       exit 0;
+               }
+               if ($cli_opts{'shortversion'}) {                # Just the version number string.
+                       print $VERSION;
+                       exit 0;
+               }
+               if ($cli_opts{'html4tags'}) {                   # Use HTML tag style instead of XHTML
+                       $g_empty_element_suffix = ">";
+               }
+
+
+               #### Process incoming text: ###########################
+               my $text;
+               {
+                       local $/;               # Slurp the whole file
+                       $text = <>;
+               }
+        print Markdown($text);
+    }
+}
+
+
+
+sub Markdown {
+#
+# Main function. The order in which other subs are called here is
+# essential. Link and image substitutions need to happen before
+# _EscapeSpecialChars(), so that any *'s or _'s in the <a>
+# and <img> tags get encoded.
+#
+       my $text = shift;
+
+       # Clear the global hashes. If we don't clear these, you get conflicts
+       # from other articles when generating a page which contains more than
+       # one article (e.g. an index page that shows the N most recent
+       # articles):
+       %g_urls = ();
+       %g_titles = ();
+       %g_html_blocks = ();
+
+
+       # Standardize line endings:
+       $text =~ s{\r\n}{\n}g;  # DOS to Unix
+       $text =~ s{\r}{\n}g;    # Mac to Unix
+
+       # Make sure $text ends with a couple of newlines:
+       $text .= "\n\n";
+
+       # Convert all tabs to spaces.
+       $text = _Detab($text);
+
+       # Strip any lines consisting only of spaces and tabs.
+       # This makes subsequent regexen easier to write, because we can
+       # match consecutive blank lines with /\n+/ instead of something
+       # contorted like /[ \t]*\n+/ .
+       $text =~ s/^[ \t]+$//mg;
+
+       # Turn block-level HTML blocks into hash entries
+       $text = _HashHTMLBlocks($text);
+
+       # Strip link definitions, store in hashes.
+       $text = _StripLinkDefinitions($text);
+
+       $text = _RunBlockGamut($text);
+
+       $text = _UnescapeSpecialChars($text);
+
+       return $text . "\n";
+}
+
+
+sub _StripLinkDefinitions {
+#
+# Strips link definitions from text, stores the URLs and titles in
+# hash references.
+#
+       my $text = shift;
+       my $less_than_tab = $g_tab_width - 1;
+
+       # Link defs are in the form: ^[id]: url "optional title"
+       while ($text =~ s{
+                                               ^[ ]{0,$less_than_tab}\[(.+)\]: # id = $1
+                                                 [ \t]*
+                                                 \n?                           # maybe *one* newline
+                                                 [ \t]*
+                                               <?(\S+?)>?                      # url = $2
+                                                 [ \t]*
+                                                 \n?                           # maybe one newline
+                                                 [ \t]*
+                                               (?:
+                                                       (?<=\s)                 # lookbehind for whitespace
+                                                       ["(]
+                                                       (.+?)                   # title = $3
+                                                       [")]
+                                                       [ \t]*
+                                               )?      # title is optional
+                                               (?:\n+|\Z)
+                                       }
+                                       {}mx) {
+               $g_urls{lc $1} = _EncodeAmpsAndAngles( $2 );    # Link IDs are case-insensitive
+               if ($3) {
+                       $g_titles{lc $1} = $3;
+                       $g_titles{lc $1} =~ s/"/&quot;/g;
+               }
+       }
+
+       return $text;
+}
+
+
+sub _HashHTMLBlocks {
+       my $text = shift;
+       my $less_than_tab = $g_tab_width - 1;
+
+       # Hashify HTML blocks:
+       # We only want to do this for block-level HTML tags, such as headers,
+       # lists, and tables. That's because we still want to wrap <p>s around
+       # "paragraphs" that are wrapped in non-block-level tags, such as anchors,
+       # phrase emphasis, and spans. The list of tags we're looking for is
+       # hard-coded:
+       my $block_tags_a = qr/p|div|h[1-6]|blockquote|pre|table|dl|ol|ul|script|noscript|form|fieldset|iframe|math|ins|del/;
+       my $block_tags_b = qr/p|div|h[1-6]|blockquote|pre|table|dl|ol|ul|script|noscript|form|fieldset|iframe|math/;
+
+       # First, look for nested blocks, e.g.:
+       #       <div>
+       #               <div>
+       #               tags for inner block must be indented.
+       #               </div>
+       #       </div>
+       #
+       # The outermost tags must start at the left margin for this to match, and
+       # the inner nested divs must be indented.
+       # We need to do this before the next, more liberal match, because the next
+       # match will start at the first `<div>` and stop at the first `</div>`.
+       $text =~ s{
+                               (                                               # save in $1
+                                       ^                                       # start of line  (with /m)
+                                       <($block_tags_a)        # start tag = $2
+                                       \b                                      # word break
+                                       (.*\n)*?                        # any number of lines, minimally matching
+                                       </\2>                           # the matching end tag
+                                       [ \t]*                          # trailing spaces/tabs
+                                       (?=\n+|\Z)      # followed by a newline or end of document
+                               )
+                       }{
+                               my $key = md5_hex($1);
+                               $g_html_blocks{$key} = $1;
+                               "\n\n" . $key . "\n\n";
+                       }egmx;
+
+
+       #
+       # Now match more liberally, simply from `\n<tag>` to `</tag>\n`
+       #
+       $text =~ s{
+                               (                                               # save in $1
+                                       ^                                       # start of line  (with /m)
+                                       <($block_tags_b)        # start tag = $2
+                                       \b                                      # word break
+                                       (.*\n)*?                        # any number of lines, minimally matching
+                                       .*</\2>                         # the matching end tag
+                                       [ \t]*                          # trailing spaces/tabs
+                                       (?=\n+|\Z)      # followed by a newline or end of document
+                               )
+                       }{
+                               my $key = md5_hex($1);
+                               $g_html_blocks{$key} = $1;
+                               "\n\n" . $key . "\n\n";
+                       }egmx;
+       # Special case just for <hr />. It was easier to make a special case than
+       # to make the other regex more complicated.     
+       $text =~ s{
+                               (?:
+                                       (?<=\n\n)               # Starting after a blank line
+                                       |                               # or
+                                       \A\n?                   # the beginning of the doc
+                               )
+                               (                                               # save in $1
+                                       [ ]{0,$less_than_tab}
+                                       <(hr)                           # start tag = $2
+                                       \b                                      # word break
+                                       ([^<>])*?                       # 
+                                       /?>                                     # the matching end tag
+                                       [ \t]*
+                                       (?=\n{2,}|\Z)           # followed by a blank line or end of document
+                               )
+                       }{
+                               my $key = md5_hex($1);
+                               $g_html_blocks{$key} = $1;
+                               "\n\n" . $key . "\n\n";
+                       }egx;
+
+       # Special case for standalone HTML comments:
+       $text =~ s{
+                               (?:
+                                       (?<=\n\n)               # Starting after a blank line
+                                       |                               # or
+                                       \A\n?                   # the beginning of the doc
+                               )
+                               (                                               # save in $1
+                                       [ ]{0,$less_than_tab}
+                                       (?s:
+                                               <!
+                                               (--.*?--\s*)+
+                                               >
+                                       )
+                                       [ \t]*
+                                       (?=\n{2,}|\Z)           # followed by a blank line or end of document
+                               )
+                       }{
+                               my $key = md5_hex($1);
+                               $g_html_blocks{$key} = $1;
+                               "\n\n" . $key . "\n\n";
+                       }egx;
+
+
+       return $text;
+}
+
+
+sub _RunBlockGamut {
+#
+# These are all the transformations that form block-level
+# tags like paragraphs, headers, and list items.
+#
+       my $text = shift;
+
+       $text = _DoHeaders($text);
+
+       # Do Horizontal Rules:
+       $text =~ s{^[ ]{0,2}([ ]?\*[ ]?){3,}[ \t]*$}{\n<hr$g_empty_element_suffix\n}gmx;
+       $text =~ s{^[ ]{0,2}([ ]? -[ ]?){3,}[ \t]*$}{\n<hr$g_empty_element_suffix\n}gmx;
+       $text =~ s{^[ ]{0,2}([ ]? _[ ]?){3,}[ \t]*$}{\n<hr$g_empty_element_suffix\n}gmx;
+
+       $text = _DoLists($text);
+
+       $text = _DoCodeBlocks($text);
+
+       $text = _DoBlockQuotes($text);
+
+       # We already ran _HashHTMLBlocks() before, in Markdown(), but that
+       # was to escape raw HTML in the original Markdown source. This time,
+       # we're escaping the markup we've just created, so that we don't wrap
+       # <p> tags around block-level tags.
+       $text = _HashHTMLBlocks($text);
+
+       $text = _FormParagraphs($text);
+
+       return $text;
+}
+
+
+sub _RunSpanGamut {
+#
+# These are all the transformations that occur *within* block-level
+# tags like paragraphs, headers, and list items.
+#
+       my $text = shift;
+
+       $text = _DoCodeSpans($text);
+
+       $text = _EscapeSpecialChars($text);
+
+       # Process anchor and image tags. Images must come first,
+       # because ![foo][f] looks like an anchor.
+       $text = _DoImages($text);
+       $text = _DoAnchors($text);
+
+       # Make links out of things like `<http://example.com/>`
+       # Must come after _DoAnchors(), because you can use < and >
+       # delimiters in inline links like [this](<url>).
+       $text = _DoAutoLinks($text);
+
+       $text = _EncodeAmpsAndAngles($text);
+
+       $text = _DoItalicsAndBold($text);
+
+       # Do hard breaks:
+       $text =~ s/ {2,}\n/ <br$g_empty_element_suffix\n/g;
+
+       return $text;
+}
+
+
+sub _EscapeSpecialChars {
+       my $text = shift;
+       my $tokens ||= _TokenizeHTML($text);
+
+       $text = '';   # rebuild $text from the tokens
+#      my $in_pre = 0;  # Keep track of when we're inside <pre> or <code> tags.
+#      my $tags_to_skip = qr!<(/?)(?:pre|code|kbd|script|math)[\s>]!;
+
+       foreach my $cur_token (@$tokens) {
+               if ($cur_token->[0] eq "tag") {
+                       # Within tags, encode * and _ so they don't conflict
+                       # with their use in Markdown for italics and strong.
+                       # We're replacing each such character with its
+                       # corresponding MD5 checksum value; this is likely
+                       # overkill, but it should prevent us from colliding
+                       # with the escape values by accident.
+                       $cur_token->[1] =~  s! \* !$g_escape_table{'*'}!gx;
+                       $cur_token->[1] =~  s! _  !$g_escape_table{'_'}!gx;
+                       $text .= $cur_token->[1];
+               } else {
+                       my $t = $cur_token->[1];
+                       $t = _EncodeBackslashEscapes($t);
+                       $text .= $t;
+               }
+       }
+       return $text;
+}
+
+
+sub _DoAnchors {
+#
+# Turn Markdown link shortcuts into XHTML <a> tags.
+#
+       my $text = shift;
+
+       #
+       # First, handle reference-style links: [link text] [id]
+       #
+       $text =~ s{
+               (                                       # wrap whole match in $1
+                 \[
+                   ($g_nested_brackets)        # link text = $2
+                 \]
+
+                 [ ]?                          # one optional space
+                 (?:\n[ ]*)?           # one optional newline followed by spaces
+
+                 \[
+                   (.*?)               # id = $3
+                 \]
+               )
+       }{
+               my $result;
+               my $whole_match = $1;
+               my $link_text   = $2;
+               my $link_id     = lc $3;
+
+               if ($link_id eq "") {
+                       $link_id = lc $link_text;     # for shortcut links like [this][].
+               }
+
+               if (defined $g_urls{$link_id}) {
+                       my $url = $g_urls{$link_id};
+                       $url =~ s! \* !$g_escape_table{'*'}!gx;         # We've got to encode these to avoid
+                       $url =~ s!  _ !$g_escape_table{'_'}!gx;         # conflicting with italics/bold.
+                       $result = "<a href=\"$url\"";
+                       if ( defined $g_titles{$link_id} ) {
+                               my $title = $g_titles{$link_id};
+                               $title =~ s! \* !$g_escape_table{'*'}!gx;
+                               $title =~ s!  _ !$g_escape_table{'_'}!gx;
+                               $result .=  " title=\"$title\"";
+                       }
+                       $result .= ">$link_text</a>";
+               }
+               else {
+                       $result = $whole_match;
+               }
+               $result;
+       }xsge;
+
+       #
+       # Next, inline-style links: [link text](url "optional title")
+       #
+       $text =~ s{
+               (                               # wrap whole match in $1
+                 \[
+                   ($g_nested_brackets)        # link text = $2
+                 \]
+                 \(                    # literal paren
+                       [ \t]*
+                       <?(.*?)>?       # href = $3
+                       [ \t]*
+                       (                       # $4
+                         (['"])        # quote char = $5
+                         (.*?)         # Title = $6
+                         \5            # matching quote
+                       )?                      # title is optional
+                 \)
+               )
+       }{
+               my $result;
+               my $whole_match = $1;
+               my $link_text   = $2;
+               my $url                 = $3;
+               my $title               = $6;
+
+               $url =~ s! \* !$g_escape_table{'*'}!gx;         # We've got to encode these to avoid
+               $url =~ s!  _ !$g_escape_table{'_'}!gx;         # conflicting with italics/bold.
+               $result = "<a href=\"$url\"";
+
+               if (defined $title) {
+                       $title =~ s/"/&quot;/g;
+                       $title =~ s! \* !$g_escape_table{'*'}!gx;
+                       $title =~ s!  _ !$g_escape_table{'_'}!gx;
+                       $result .=  " title=\"$title\"";
+               }
+
+               $result .= ">$link_text</a>";
+
+               $result;
+       }xsge;
+
+       return $text;
+}
+
+
+sub _DoImages {
+#
+# Turn Markdown image shortcuts into <img> tags.
+#
+       my $text = shift;
+
+       #
+       # First, handle reference-style labeled images: ![alt text][id]
+       #
+       $text =~ s{
+               (                               # wrap whole match in $1
+                 !\[
+                   (.*?)               # alt text = $2
+                 \]
+
+                 [ ]?                          # one optional space
+                 (?:\n[ ]*)?           # one optional newline followed by spaces
+
+                 \[
+                   (.*?)               # id = $3
+                 \]
+
+               )
+       }{
+               my $result;
+               my $whole_match = $1;
+               my $alt_text    = $2;
+               my $link_id     = lc $3;
+
+               if ($link_id eq "") {
+                       $link_id = lc $alt_text;     # for shortcut links like ![this][].
+               }
+
+               $alt_text =~ s/"/&quot;/g;
+               if (defined $g_urls{$link_id}) {
+                       my $url = $g_urls{$link_id};
+                       $url =~ s! \* !$g_escape_table{'*'}!gx;         # We've got to encode these to avoid
+                       $url =~ s!  _ !$g_escape_table{'_'}!gx;         # conflicting with italics/bold.
+                       $result = "<img src=\"$url\" alt=\"$alt_text\"";
+                       if (defined $g_titles{$link_id}) {
+                               my $title = $g_titles{$link_id};
+                               $title =~ s! \* !$g_escape_table{'*'}!gx;
+                               $title =~ s!  _ !$g_escape_table{'_'}!gx;
+                               $result .=  " title=\"$title\"";
+                       }
+                       $result .= $g_empty_element_suffix;
+               }
+               else {
+                       # If there's no such link ID, leave intact:
+                       $result = $whole_match;
+               }
+
+               $result;
+       }xsge;
+
+       #
+       # Next, handle inline images:  ![alt text](url "optional title")
+       # Don't forget: encode * and _
+
+       $text =~ s{
+               (                               # wrap whole match in $1
+                 !\[
+                   (.*?)               # alt text = $2
+                 \]
+                 \(                    # literal paren
+                       [ \t]*
+                       <?(\S+?)>?      # src url = $3
+                       [ \t]*
+                       (                       # $4
+                         (['"])        # quote char = $5
+                         (.*?)         # title = $6
+                         \5            # matching quote
+                         [ \t]*
+                       )?                      # title is optional
+                 \)
+               )
+       }{
+               my $result;
+               my $whole_match = $1;
+               my $alt_text    = $2;
+               my $url                 = $3;
+               my $title               = '';
+               if (defined($6)) {
+                       $title          = $6;
+               }
+
+               $alt_text =~ s/"/&quot;/g;
+               $title    =~ s/"/&quot;/g;
+               $url =~ s! \* !$g_escape_table{'*'}!gx;         # We've got to encode these to avoid
+               $url =~ s!  _ !$g_escape_table{'_'}!gx;         # conflicting with italics/bold.
+               $result = "<img src=\"$url\" alt=\"$alt_text\"";
+               if (defined $title) {
+                       $title =~ s! \* !$g_escape_table{'*'}!gx;
+                       $title =~ s!  _ !$g_escape_table{'_'}!gx;
+                       $result .=  " title=\"$title\"";
+               }
+               $result .= $g_empty_element_suffix;
+
+               $result;
+       }xsge;
+
+       return $text;
+}
+
+
+sub _DoHeaders {
+       my $text = shift;
+
+       # Setext-style headers:
+       #         Header 1
+       #         ========
+       #  
+       #         Header 2
+       #         --------
+       #
+       $text =~ s{ ^(.+)[ \t]*\n=+[ \t]*\n+ }{
+               "<h1>"  .  _RunSpanGamut($1)  .  "</h1>\n\n";
+       }egmx;
+
+       $text =~ s{ ^(.+)[ \t]*\n-+[ \t]*\n+ }{
+               "<h2>"  .  _RunSpanGamut($1)  .  "</h2>\n\n";
+       }egmx;
+
+
+       # atx-style headers:
+       #       # Header 1
+       #       ## Header 2
+       #       ## Header 2 with closing hashes ##
+       #       ...
+       #       ###### Header 6
+       #
+       $text =~ s{
+                       ^(\#{1,6})      # $1 = string of #'s
+                       [ \t]*
+                       (.+?)           # $2 = Header text
+                       [ \t]*
+                       \#*                     # optional closing #'s (not counted)
+                       \n+
+               }{
+                       my $h_level = length($1);
+                       "<h$h_level>"  .  _RunSpanGamut($2)  .  "</h$h_level>\n\n";
+               }egmx;
+
+       return $text;
+}
+
+
+sub _DoLists {
+#
+# Form HTML ordered (numbered) and unordered (bulleted) lists.
+#
+       my $text = shift;
+       my $less_than_tab = $g_tab_width - 1;
+
+       # Re-usable patterns to match list item bullets and number markers:
+       my $marker_ul  = qr/[*+-]/;
+       my $marker_ol  = qr/\d+[.]/;
+       my $marker_any = qr/(?:$marker_ul|$marker_ol)/;
+
+       # Re-usable pattern to match any entirel ul or ol list:
+       my $whole_list = qr{
+               (                                                               # $1 = whole list
+                 (                                                             # $2
+                       [ ]{0,$less_than_tab}
+                       (${marker_any})                         # $3 = first list item marker
+                       [ \t]+
+                 )
+                 (?s:.+?)
+                 (                                                             # $4
+                         \z
+                       |
+                         \n{2,}
+                         (?=\S)
+                         (?!                                           # Negative lookahead for another list item marker
+                               [ \t]*
+                               ${marker_any}[ \t]+
+                         )
+                 )
+               )
+       }mx;
+
+       # We use a different prefix before nested lists than top-level lists.
+       # See extended comment in _ProcessListItems().
+       #
+       # Note: There's a bit of duplication here. My original implementation
+       # created a scalar regex pattern as the conditional result of the test on
+       # $g_list_level, and then only ran the $text =~ s{...}{...}egmx
+       # substitution once, using the scalar as the pattern. This worked,
+       # everywhere except when running under MT on my hosting account at Pair
+       # Networks. There, this caused all rebuilds to be killed by the reaper (or
+       # perhaps they crashed, but that seems incredibly unlikely given that the
+       # same script on the same server ran fine *except* under MT. I've spent
+       # more time trying to figure out why this is happening than I'd like to
+       # admit. My only guess, backed up by the fact that this workaround works,
+       # is that Perl optimizes the substition when it can figure out that the
+       # pattern will never change, and when this optimization isn't on, we run
+       # afoul of the reaper. Thus, the slightly redundant code to that uses two
+       # static s/// patterns rather than one conditional pattern.
+
+       if ($g_list_level) {
+               $text =~ s{
+                               ^
+                               $whole_list
+                       }{
+                               my $list = $1;
+                               my $list_type = ($3 =~ m/$marker_ul/) ? "ul" : "ol";
+                               # Turn double returns into triple returns, so that we can make a
+                               # paragraph for the last item in a list, if necessary:
+                               $list =~ s/\n{2,}/\n\n\n/g;
+                               my $result = _ProcessListItems($list, $marker_any);
+                               $result = "<$list_type>\n" . $result . "</$list_type>\n";
+                               $result;
+                       }egmx;
+       }
+       else {
+               $text =~ s{
+                               (?:(?<=\n\n)|\A\n?)
+                               $whole_list
+                       }{
+                               my $list = $1;
+                               my $list_type = ($3 =~ m/$marker_ul/) ? "ul" : "ol";
+                               # Turn double returns into triple returns, so that we can make a
+                               # paragraph for the last item in a list, if necessary:
+                               $list =~ s/\n{2,}/\n\n\n/g;
+                               my $result = _ProcessListItems($list, $marker_any);
+                               $result = "<$list_type>\n" . $result . "</$list_type>\n";
+                               $result;
+                       }egmx;
+       }
+
+
+       return $text;
+}
+
+
+sub _ProcessListItems {
+#
+#      Process the contents of a single ordered or unordered list, splitting it
+#      into individual list items.
+#
+
+       my $list_str = shift;
+       my $marker_any = shift;
+
+
+       # The $g_list_level global keeps track of when we're inside a list.
+       # Each time we enter a list, we increment it; when we leave a list,
+       # we decrement. If it's zero, we're not in a list anymore.
+       #
+       # We do this because when we're not inside a list, we want to treat
+       # something like this:
+       #
+       #               I recommend upgrading to version
+       #               8. Oops, now this line is treated
+       #               as a sub-list.
+       #
+       # As a single paragraph, despite the fact that the second line starts
+       # with a digit-period-space sequence.
+       #
+       # Whereas when we're inside a list (or sub-list), that line will be
+       # treated as the start of a sub-list. What a kludge, huh? This is
+       # an aspect of Markdown's syntax that's hard to parse perfectly
+       # without resorting to mind-reading. Perhaps the solution is to
+       # change the syntax rules such that sub-lists must start with a
+       # starting cardinal number; e.g. "1." or "a.".
+
+       $g_list_level++;
+
+       # trim trailing blank lines:
+       $list_str =~ s/\n{2,}\z/\n/;
+
+
+       $list_str =~ s{
+               (\n)?                                                   # leading line = $1
+               (^[ \t]*)                                               # leading whitespace = $2
+               ($marker_any) [ \t]+                    # list marker = $3
+               ((?s:.+?)                                               # list item text   = $4
+               (\n{1,2}))
+               (?= \n* (\z | \2 ($marker_any) [ \t]+))
+       }{
+               my $item = $4;
+               my $leading_line = $1;
+               my $leading_space = $2;
+
+               if ($leading_line or ($item =~ m/\n{2,}/)) {
+                       $item = _RunBlockGamut(_Outdent($item));
+               }
+               else {
+                       # Recursion for sub-lists:
+                       $item = _DoLists(_Outdent($item));
+                       chomp $item;
+                       $item = _RunSpanGamut($item);
+               }
+
+               "<li>" . $item . "</li>\n";
+       }egmx;
+
+       $g_list_level--;
+       return $list_str;
+}
+
+
+
+sub _DoCodeBlocks {
+#
+#      Process Markdown `<pre><code>` blocks.
+#      
+
+       my $text = shift;
+
+       $text =~ s{
+                       (?:\n\n|\A)
+                       (                   # $1 = the code block -- one or more lines, starting with a space/tab
+                         (?:
+                           (?:[ ]{$g_tab_width} | \t)  # Lines must start with a tab or a tab-width of spaces
+                           .*\n+
+                         )+
+                       )
+                       ((?=^[ ]{0,$g_tab_width}\S)|\Z) # Lookahead for non-space at line-start, or end of doc
+               }{
+                       my $codeblock = $1;
+                       my $result; # return value
+
+                       $codeblock = _EncodeCode(_Outdent($codeblock));
+                       $codeblock = _Detab($codeblock);
+                       $codeblock =~ s/\A\n+//; # trim leading newlines
+                       $codeblock =~ s/\s+\z//; # trim trailing whitespace
+
+                       $result = "\n\n<pre><code>" . $codeblock . "\n</code></pre>\n\n";
+
+                       $result;
+               }egmx;
+
+       return $text;
+}
+
+
+sub _DoCodeSpans {
+#
+#      *       Backtick quotes are used for <code></code> spans.
+# 
+#      *       You can use multiple backticks as the delimiters if you want to
+#              include literal backticks in the code span. So, this input:
+#     
+#         Just type ``foo `bar` baz`` at the prompt.
+#     
+#      Will translate to:
+#     
+#         <p>Just type <code>foo `bar` baz</code> at the prompt.</p>
+#     
+#              There's no arbitrary limit to the number of backticks you
+#              can use as delimters. If you need three consecutive backticks
+#              in your code, use four for delimiters, etc.
+#
+#      *       You can use spaces to get literal backticks at the edges:
+#     
+#         ... type `` `bar` `` ...
+#     
+#      Turns to:
+#     
+#         ... type <code>`bar`</code> ...
+#
+
+       my $text = shift;
+
+       $text =~ s@
+                       (`+)            # $1 = Opening run of `
+                       (.+?)           # $2 = The code block
+                       (?<!`)
+                       \1                      # Matching closer
+                       (?!`)
+               @
+                       my $c = "$2";
+                       $c =~ s/^[ \t]*//g; # leading whitespace
+                       $c =~ s/[ \t]*$//g; # trailing whitespace
+                       $c = _EncodeCode($c);
+                       "<code>$c</code>";
+               @egsx;
+
+       return $text;
+}
+
+
+sub _EncodeCode {
+#
+# Encode/escape certain characters inside Markdown code runs.
+# The point is that in code, these characters are literals,
+# and lose their special Markdown meanings.
+#
+    local $_ = shift;
+
+       # Encode all ampersands; HTML entities are not
+       # entities within a Markdown code span.
+       s/&/&amp;/g;
+
+       # Encode $'s, but only if we're running under Blosxom.
+       # (Blosxom interpolates Perl variables in article bodies.)
+       {
+               no warnings 'once';
+       if (defined($blosxom::version)) {
+               s/\$/&#036;/g;  
+       }
+    }
+
+
+       # Do the angle bracket song and dance:
+       s! <  !&lt;!gx;
+       s! >  !&gt;!gx;
+
+       # Now, escape characters that are magic in Markdown:
+       s! \* !$g_escape_table{'*'}!gx;
+       s! _  !$g_escape_table{'_'}!gx;
+       s! {  !$g_escape_table{'{'}!gx;
+       s! }  !$g_escape_table{'}'}!gx;
+       s! \[ !$g_escape_table{'['}!gx;
+       s! \] !$g_escape_table{']'}!gx;
+       s! \\ !$g_escape_table{'\\'}!gx;
+
+       return $_;
+}
+
+
+sub _DoItalicsAndBold {
+       my $text = shift;
+
+       # <strong> must go first:
+       $text =~ s{ (\*\*|__) (?=\S) (.+?[*_]*) (?<=\S) \1 }
+               {<strong>$2</strong>}gsx;
+
+       $text =~ s{ (\*|_) (?=\S) (.+?) (?<=\S) \1 }
+               {<em>$2</em>}gsx;
+
+       return $text;
+}
+
+
+sub _DoBlockQuotes {
+       my $text = shift;
+
+       $text =~ s{
+                 (                                                             # Wrap whole match in $1
+                       (
+                         ^[ \t]*>[ \t]?                        # '>' at the start of a line
+                           .+\n                                        # rest of the first line
+                         (.+\n)*                                       # subsequent consecutive lines
+                         \n*                                           # blanks
+                       )+
+                 )
+               }{
+                       my $bq = $1;
+                       $bq =~ s/^[ \t]*>[ \t]?//gm;    # trim one level of quoting
+                       $bq =~ s/^[ \t]+$//mg;                  # trim whitespace-only lines
+                       $bq = _RunBlockGamut($bq);              # recurse
+
+                       $bq =~ s/^/  /g;
+                       # These leading spaces screw with <pre> content, so we need to fix that:
+                       $bq =~ s{
+                                       (\s*<pre>.+?</pre>)
+                               }{
+                                       my $pre = $1;
+                                       $pre =~ s/^  //mg;
+                                       $pre;
+                               }egsx;
+
+                       "<blockquote>\n$bq\n</blockquote>\n\n";
+               }egmx;
+
+
+       return $text;
+}
+
+
+sub _FormParagraphs {
+#
+#      Params:
+#              $text - string to process with html <p> tags
+#
+       my $text = shift;
+
+       # Strip leading and trailing lines:
+       $text =~ s/\A\n+//;
+       $text =~ s/\n+\z//;
+
+       my @grafs = split(/\n{2,}/, $text);
+
+       #
+       # Wrap <p> tags.
+       #
+       foreach (@grafs) {
+               unless (defined( $g_html_blocks{$_} )) {
+                       $_ = _RunSpanGamut($_);
+                       s/^([ \t]*)/<p>/;
+                       $_ .= "</p>";
+               }
+       }
+
+       #
+       # Unhashify HTML blocks
+       #
+       foreach (@grafs) {
+               if (defined( $g_html_blocks{$_} )) {
+                       $_ = $g_html_blocks{$_};
+               }
+       }
+
+       return join "\n\n", @grafs;
+}
+
+
+sub _EncodeAmpsAndAngles {
+# Smart processing for ampersands and angle brackets that need to be encoded.
+
+       my $text = shift;
+
+       # Ampersand-encoding based entirely on Nat Irons's Amputator MT plugin:
+       #   http://bumppo.net/projects/amputator/
+       $text =~ s/&(?!#?[xX]?(?:[0-9a-fA-F]+|\w+);)/&amp;/g;
+
+       # Encode naked <'s
+       $text =~ s{<(?![a-z/?\$!])}{&lt;}gi;
+
+       return $text;
+}
+
+
+sub _EncodeBackslashEscapes {
+#
+#   Parameter:  String.
+#   Returns:    The string, with after processing the following backslash
+#               escape sequences.
+#
+    local $_ = shift;
+
+    s! \\\\  !$g_escape_table{'\\'}!gx;                # Must process escaped backslashes first.
+    s! \\`   !$g_escape_table{'`'}!gx;
+    s! \\\*  !$g_escape_table{'*'}!gx;
+    s! \\_   !$g_escape_table{'_'}!gx;
+    s! \\\{  !$g_escape_table{'{'}!gx;
+    s! \\\}  !$g_escape_table{'}'}!gx;
+    s! \\\[  !$g_escape_table{'['}!gx;
+    s! \\\]  !$g_escape_table{']'}!gx;
+    s! \\\(  !$g_escape_table{'('}!gx;
+    s! \\\)  !$g_escape_table{')'}!gx;
+    s! \\>   !$g_escape_table{'>'}!gx;
+    s! \\\#  !$g_escape_table{'#'}!gx;
+    s! \\\+  !$g_escape_table{'+'}!gx;
+    s! \\\-  !$g_escape_table{'-'}!gx;
+    s! \\\.  !$g_escape_table{'.'}!gx;
+    s{ \\!  }{$g_escape_table{'!'}}gx;
+
+    return $_;
+}
+
+
+sub _DoAutoLinks {
+       my $text = shift;
+
+       $text =~ s{<((https?|ftp):[^'">\s]+)>}{<a href="$1">$1</a>}gi;
+
+       # Email addresses: <address@domain.foo>
+       $text =~ s{
+               <
+        (?:mailto:)?
+               (
+                       [-.\w]+
+                       \@
+                       [-a-z0-9]+(\.[-a-z0-9]+)*\.[a-z]+
+               )
+               >
+       }{
+               _EncodeEmailAddress( _UnescapeSpecialChars($1) );
+       }egix;
+
+       return $text;
+}
+
+
+sub _EncodeEmailAddress {
+#
+#      Input: an email address, e.g. "foo@example.com"
+#
+#      Output: the email address as a mailto link, with each character
+#              of the address encoded as either a decimal or hex entity, in
+#              the hopes of foiling most address harvesting spam bots. E.g.:
+#
+#        <a href="&#x6D;&#97;&#105;&#108;&#x74;&#111;:&#102;&#111;&#111;&#64;&#101;
+#       x&#x61;&#109;&#x70;&#108;&#x65;&#x2E;&#99;&#111;&#109;">&#102;&#111;&#111;
+#       &#64;&#101;x&#x61;&#109;&#x70;&#108;&#x65;&#x2E;&#99;&#111;&#109;</a>
+#
+#      Based on a filter by Matthew Wickline, posted to the BBEdit-Talk
+#      mailing list: <http://tinyurl.com/yu7ue>
+#
+
+       my $addr = shift;
+
+       srand;
+       my @encode = (
+               sub { '&#' .                 ord(shift)   . ';' },
+               sub { '&#x' . sprintf( "%X", ord(shift) ) . ';' },
+               sub {                            shift          },
+       );
+
+       $addr = "mailto:" . $addr;
+
+       $addr =~ s{(.)}{
+               my $char = $1;
+               if ( $char eq '@' ) {
+                       # this *must* be encoded. I insist.
+                       $char = $encode[int rand 1]->($char);
+               } elsif ( $char ne ':' ) {
+                       # leave ':' alone (to spot mailto: later)
+                       my $r = rand;
+                       # roughly 10% raw, 45% hex, 45% dec
+                       $char = (
+                               $r > .9   ?  $encode[2]->($char)  :
+                               $r < .45  ?  $encode[1]->($char)  :
+                                                        $encode[0]->($char)
+                       );
+               }
+               $char;
+       }gex;
+
+       $addr = qq{<a href="$addr">$addr</a>};
+       $addr =~ s{">.+?:}{">}; # strip the mailto: from the visible part
+
+       return $addr;
+}
+
+
+sub _UnescapeSpecialChars {
+#
+# Swap back in all the special characters we've hidden.
+#
+       my $text = shift;
+
+       while( my($char, $hash) = each(%g_escape_table) ) {
+               $text =~ s/$hash/$char/g;
+       }
+    return $text;
+}
+
+
+sub _TokenizeHTML {
+#
+#   Parameter:  String containing HTML markup.
+#   Returns:    Reference to an array of the tokens comprising the input
+#               string. Each token is either a tag (possibly with nested,
+#               tags contained therein, such as <a href="<MTFoo>">, or a
+#               run of text between tags. Each element of the array is a
+#               two-element array; the first is either 'tag' or 'text';
+#               the second is the actual value.
+#
+#
+#   Derived from the _tokenize() subroutine from Brad Choate's MTRegex plugin.
+#       <http://www.bradchoate.com/past/mtregex.php>
+#
+
+    my $str = shift;
+    my $pos = 0;
+    my $len = length $str;
+    my @tokens;
+
+    my $depth = 6;
+    my $nested_tags = join('|', ('(?:<[a-z/!$](?:[^<>]') x $depth) . (')*>)' x  $depth);
+    my $match = qr/(?s: <! ( -- .*? -- \s* )+ > ) |  # comment
+                   (?s: <\? .*? \?> ) |              # processing instruction
+                   $nested_tags/ix;                   # nested tags
+
+    while ($str =~ m/($match)/g) {
+        my $whole_tag = $1;
+        my $sec_start = pos $str;
+        my $tag_start = $sec_start - length $whole_tag;
+        if ($pos < $tag_start) {
+            push @tokens, ['text', substr($str, $pos, $tag_start - $pos)];
+        }
+        push @tokens, ['tag', $whole_tag];
+        $pos = pos $str;
+    }
+    push @tokens, ['text', substr($str, $pos, $len - $pos)] if $pos < $len;
+    \@tokens;
+}
+
+
+sub _Outdent {
+#
+# Remove one level of line-leading tabs or spaces
+#
+       my $text = shift;
+
+       $text =~ s/^(\t|[ ]{1,$g_tab_width})//gm;
+       return $text;
+}
+
+
+sub _Detab {
+#
+# Cribbed from a post by Bart Lateur:
+# <http://www.nntp.perl.org/group/perl.macperl.anyperl/154>
+#
+       my $text = shift;
+
+       $text =~ s{(.*?)\t}{$1.(' ' x ($g_tab_width - length($1) % $g_tab_width))}ge;
+       return $text;
+}
+
+
+1;
+
+__END__
+
+
+=pod
+
+=head1 NAME
+
+B<Markdown>
+
+
+=head1 SYNOPSIS
+
+B<Markdown.pl> [ B<--html4tags> ] [ B<--version> ] [ B<-shortversion> ]
+    [ I<file> ... ]
+
+
+=head1 DESCRIPTION
+
+Markdown is a text-to-HTML filter; it translates an easy-to-read /
+easy-to-write structured text format into HTML. Markdown's text format
+is most similar to that of plain text email, and supports features such
+as headers, *emphasis*, code blocks, blockquotes, and links.
+
+Markdown's syntax is designed not as a generic markup language, but
+specifically to serve as a front-end to (X)HTML. You can  use span-level
+HTML tags anywhere in a Markdown document, and you can use block level
+HTML tags (like <div> and <table> as well).
+
+For more information about Markdown's syntax, see:
+
+    http://daringfireball.net/projects/markdown/
+
+
+=head1 OPTIONS
+
+Use "--" to end switch parsing. For example, to open a file named "-z", use:
+
+       Markdown.pl -- -z
+
+=over 4
+
+
+=item B<--html4tags>
+
+Use HTML 4 style for empty element tags, e.g.:
+
+    <br>
+
+instead of Markdown's default XHTML style tags, e.g.:
+
+    <br />
+
+
+=item B<-v>, B<--version>
+
+Display Markdown's version number and copyright information.
+
+
+=item B<-s>, B<--shortversion>
+
+Display the short-form version number.
+
+
+=back
+
+
+
+=head1 BUGS
+
+To file bug reports or feature requests (other than topics listed in the
+Caveats section above) please send email to:
+
+    support@daringfireball.net
+
+Please include with your report: (1) the example input; (2) the output
+you expected; (3) the output Markdown actually produced.
+
+
+=head1 VERSION HISTORY
+
+See the readme file for detailed release notes for this version.
+
+1.0.1 - 14 Dec 2004
+
+1.0 - 28 Aug 2004
+
+
+=head1 AUTHOR
+
+    John Gruber
+    http://daringfireball.net
+
+    PHP port and other contributions by Michel Fortin
+    http://michelf.com
+
+
+=head1 COPYRIGHT AND LICENSE
+
+Copyright (c) 2003-2004 John Gruber   
+<http://daringfireball.net/>   
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+* Redistributions of source code must retain the above copyright notice,
+  this list of conditions and the following disclaimer.
+
+* Redistributions in binary form must reproduce the above copyright
+  notice, this list of conditions and the following disclaimer in the
+  documentation and/or other materials provided with the distribution.
+
+* Neither the name "Markdown" nor the names of its contributors may
+  be used to endorse or promote products derived from this software
+  without specific prior written permission.
+
+This software is provided by the copyright holders and contributors "as
+is" and any express or implied warranties, including, but not limited
+to, the implied warranties of merchantability and fitness for a
+particular purpose are disclaimed. In no event shall the copyright owner
+or contributors be liable for any direct, indirect, incidental, special,
+exemplary, or consequential damages (including, but not limited to,
+procurement of substitute goods or services; loss of use, data, or
+profits; or business interruption) however caused and on any theory of
+liability, whether in contract, strict liability, or tort (including
+negligence or otherwise) arising in any way out of the use of this
+software, even if advised of the possibility of such damage.
+
+=cut
diff --git a/doc/notes/fence.txt b/doc/notes/fence.txt
new file mode 100644 (file)
index 0000000..8256735
--- /dev/null
@@ -0,0 +1,308 @@
+-------------------------------------------------------------------------------
+ Fence support:
+-------------------------------------------------------------------------------
+
+Fences provide a few new modification order constraints as well as an
+interesting extension to release sequences, detailed in 29.3 (p4-p7) and 29.8
+(p2-p4). The specifications are pasted here in Appendix A and are applied to our
+model-checker in these notes.
+
+Section 29.3 details the modification order constraints established by
+sequentially-consistent fences.
+
+Section 29.8 details the behavior of release and acquire fences (note that
+memory_order_seq_cst is both release and acquire).
+
+The text of these rules are provided at the end of this document for reference.
+
+*******************************
+ Backtracking requirements
+*******************************
+
+Because we maintain the seq-cst order as consistent with the execution order,
+seq-cst fences cannot commute with each other, with seq-cst loads, nor with
+seq-cst stores; we backtrack at all such pairs.
+
+Fences extend release/acquire synchronization beyond just
+store-release/load-acquire. We must backtrack with potentially-synchronizing
+fences: that is, with any pair of store- or fence-release and load- or
+fence-acquire, where the release comes after the acquire in the execution order
+(the other ordering is OK, as we will explore both behaviors; where the pair
+synchronize and where they don't).
+
+Note that, for instance, a fence-release may synchronize with a fence-acquire
+only in the presence of a appropriate load/store pair (29.8p2); but the
+synchronization still occurs between the fences, so the backtracking
+requirements are only placed on the release/acquire fences themselves.
+
+*******************************
+ Seq-cst MO constraints (29.3 p4-p7)
+*******************************
+
+The statements given in the specification regarding sequentially consistent
+fences can be transformed into the following 4 modification order constraints.
+
+29.3p4
+
+If
+    is_write(A) && is_read(B) && is_write(W) && is_fence(X) &&
+    is_seqcst(W) && is_seqcst(X) && A != W &&
+    same_loc(W, A, B) &&
+    A --rf-> B &&
+    W --sc-> X --sb-> B
+then
+    W --mo-> A
+
+Intuition/Implementation:
+ * We may (but don't currently) limit our considertion of W to only the most
+   recent (in the SC order) store to the same location as A and B prior to X
+   (note that all prior writes will be ordered prior to W in both SC and MO)
+ * We should consider the "most recent" seq-cst fence X that precedes B
+ * This search can be combined with the r_modification_order search, since we
+   already iterate through the necessary stores W
+
+29.3p5
+
+If
+    is_write(A) && is_read(B) && is_write(W) && is_fence(X) &&
+    is_seqcst(B) && is_seqcst(X) &&
+    same_loc(W, A, B) &&
+    A != W &&
+    A --rf-> B &&
+    W --sb-> X --sc-> B
+then
+    W --mo-> A
+
+Intuition/Implementation:
+ * We only need to examine the "most recent" seq-cst fence X from each thread
+ * We only need to examine the "most recent" qualifying store W that precedes X;
+   all other W will provide a weaker MO constraint
+ * This search can be combined with the r_modification_order search, since we
+   already iterate through the necessary stores W
+
+29.3p6
+
+If
+    is_write(A) && is_read(B) && is_write(W) && is_fence(X) && is_fence(Y) &&
+    is_seqcst(X) && is_seqcst(Y) &&
+    same_loc(W, A, B) &&
+    A != W &&
+    A --rf-> B &&
+    W --sb-> X --sc-> Y --sb-> B
+then
+    W --mo-> A
+
+Intuition/Implementation:
+ * We should consider only the "most recent" fence Y in the same thread as B
+   (prior fences may only yield the same or weaker constraints)
+ * We may then consider the "most recent" seq-cst fence X prior to Y (in SC order)
+   from each thread (prior fences may only yield the same or weaker constraints)
+ * We should consider only the "most recent" store W (to the same location as A,
+   B) in the same thread as X (prior stores may only yield the same or weaker
+   constraints)
+ * This search can be combined with the r_modification_order search, since we
+   already iterate through the necessary stores W
+
+29.3p7
+
+If
+    is_write(A) && is_write(B) && is_fence(X) && is_fence(Y) &&
+    is_seqcst(X) && is_seqcst(Y) &&
+    same_loc(A, B) &&
+    A --sb-> X --sc-> Y --sb-> B
+then
+    A --mo-> B
+
+Intuition/Implementation:
+ * (Similar to 29.3p6 rules, except using A/B write/write) only search for the
+   most recent fence Y in the same thread; search for the most recent (prior to
+   Y) fence X from each thread; search for the most recent store A prior to X
+ * This search can be combined with the w_modification_order search, since we
+   already iterate through the necessary stores A
+
+**********************************************************************
+ Release/acquire synchronization: extended to fences (29.3 p4-p7)
+**********************************************************************
+
+The C++ specification statements regarding release and acquire fences make
+extensions to release sequences, using what they call "hypothetical release
+sequences." These hypothetical release sequences are the same as normal release
+sequences, except that the "head" doesn't have to be a release: it can have any
+memory order (e.g., relaxed). This change actually simplifies our release
+sequences (for the fence case), as we don't actually have to establish a
+contiguous modification order all the way to a release operation; we just need
+to reach the same thread (via a RMW chain, for instance).
+
+The statements given in the specification regarding release and acquire fences
+do not result in totally separable conditions, so I will write down my
+semi-formal notation here along with some simple notes then present my
+implementation notes at the end.
+
+Note that we will use A --rs-> B to denote that B is in the release sequence
+headed by A (we allow A = B, unless otherwise stated). The hypothetical release
+sequence will be similarly denoted A --hrs-> B.
+
+29.8p2
+
+If
+    is_fence(A) && is_write(X) && is_write(W) && is_read(Y) && is_fence(B) &&
+    is_release(A) && is_acquire(B) &&
+    A --sb-> X --hrs-> W --rf-> Y --sb-> B
+then
+    A --sw-> B
+
+Notes:
+ * The fence-release A does not result in any action on its own (i.e., when it
+   is first explored); it only affects later release operations, at which point
+   we may need to associate store X with A. Thus, for every store X, we eagerly
+   record the most recent fence-release, then this record can be utilized during
+   later (hypothetical) release sequence checks.
+ * The fence-acquire B is more troublesome, since there may be many qualifying
+   loads Y (loads from different locations; loads which read from different
+   threads; etc.). Each Y may read from different hypothetical release
+   sequences, ending in a different release A with which B should synchronize.
+   It is difficult (but not impossible) to find good stopping conditions at
+   which we should terminate our search for Y. However, we at least know we only
+   need to consder Y such that:
+       V --sb-> Y --sb-> B
+   where V is a previous fence-acquire.
+
+29.8p3
+
+If
+    is_fence(A) && is_write(X) && is_write(W) && is_read(B) &&
+    is_release(A) && is_acquire(B) &&
+    A --sb-> X --hrs-> W --rf-> B
+then
+    A --sw-> B
+
+Notes:
+ * See the note for fence-release A in 29.8p2
+
+29.8p4
+
+If
+    is_write(A) && is_write(W) && is_read(X) && is_fence(B) &&
+    is_release(A) && is_acquire(B) &&
+    A --rs-> W --rf-> X --sb-> B
+then
+    A --sw-> B
+
+Notes:
+ * See the note for fence-acquire B in 29.8p2. The A, Y, and B in 29.8p2
+   correspond to A, X, and B in this rule (29.8p4).
+
+Summary notes:
+
+Now, noting the overlap in implementation notes between 29.8p2,3,4 and the
+similarity between release sequences and hypothetical release sequences, I can
+extend our release sequence support to provide easy facilities for
+release/acquire fence support.
+
+I extend release sequence support to include fences first by distinguishing the
+'acquire' from the 'load'; previously, release sequence searches were always
+triggered by a load-acquire operation. Now, we may have a *fence*-acquire which
+finds a previous load-*relaxed*, then follows any chain to a release sequence
+(29.8p4). Any release heads found by our existing release sequence support must
+synchronize with the fence-acquire. Any uncertain release sequences can be
+stashed (along with both the fence-acquire and the load-relaxed) as "pending" in
+the existing lists.
+
+Next I extend the release sequence support to include hypothetical release
+sequences. Note that any search for a release sequence can also search for a
+hypothetical release sequence with little additional effort (and even saving
+effort in cases where a fence-release hides a prior store-release, whose release
+sequence may be harder to establish eagerly). Because the "most recent" 
+fence-release is stashed in each ModelAction (see the fence-release note in
+29.8p2), release sequence searches can easily add the most recent fence-release
+to the release_heads vector as it explores a RMW chain. Then, once it reaches a
+thread in which it looks for a store-release, it can perform this interesting
+optimization: if the most recent store-release is sequenced before the most
+recent fence-release, then we can ignore the store-release and simply
+synchronize with the fence-release. This avoids a "contiguous MO" computation.
+
+So, with hypothetical release sequences seamlessly integrated into the release
+sequence code, we easily cover 29.8p3 (fence-release --sw-> load-acquire). Then,
+it's a simple extension to see how 29.8p2 is just a combination of the rules
+described for 29.8p3 and 29.8p4: a fence-acquire triggers a search for loads in
+its same thread; these loads then launch a series of release sequence
+searches--hypothetical (29.8p2) or real (29.8p4)--and synchronizes with all the
+release heads.
+
+The best part about all of the preceding explanations: the lazy fixups, etc.,
+can simply be re-used from existing release sequence code, with slight
+adjustments for dealing the presence of a fence-acquire preceded by a
+load-relaxed.
+
+*******************************
+ Miscellaneous Notes
+*******************************
+
+fence(memory_order_consume) acts like memory_order_release, so if we ever
+support consume, we must alias consume -> release
+
+fence(memory_order_relaxed) is a no-op
+
+**************************************************
+ Appendix A: From the C++11 specification (N3337)
+**************************************************
+
+-------------
+Section 29.3
+-------------
+
+29.3p4
+
+For an atomic operation B that reads the value of an atomic object M, if there
+is a memory_order_seq_cst fence X sequenced before B, then B observes either
+the last memory_order_seq_cst modification of M preceding X in the total order
+S or a later modification of M in its modification order.
+
+29.3p5
+
+For atomic operations A and B on an atomic object M, where A modifies M and B
+takes its value, if there is a memory_order_seq_cst fence X such that A is
+sequenced before X and B follows X in S, then B observes either the effects of
+A or a later modification of M in its modification order.
+
+29.3p6
+
+For atomic operations A and B on an atomic object M, where A modifies M and B
+takes its value, if there are memory_order_seq_cst fences X and Y such that A
+is sequenced before X, Y is sequenced before B, and X precedes Y in S, then B
+observes either the effects of A or a later modification of M in its
+modification order.
+
+29.3p7
+
+For atomic operations A and B on an atomic object M, if there are
+memory_order_seq_cst fences X and Y such that A is sequenced before X, Y is
+sequenced before B, and X precedes Y in S, then B occurs later than A in the
+modification order of M.
+
+-------------
+Section 29.8
+-------------
+
+29.8p2
+
+A release fence A synchronizes with an acquire fence B if there exist atomic
+operations X and Y, both operating on some atomic object M, such that A is
+sequenced before X, X modifies M, Y is sequenced before B, and Y reads the value
+written by X or a value written by any side effect in the hypothetical release
+sequence X would head if it were a release operation.
+
+29.8p3
+
+A release fence A synchronizes with an atomic operation B that performs an
+acquire operation on an atomic object M if there exists an atomic operation X
+such that A is sequenced before X, X modifies M, and B reads the value written
+by X or a value written by any side effect in the hypothetical release sequence
+X would head if it were a release operation.
+
+29.8p4
+
+An atomic operation A that is a release operation on an atomic object M
+synchronizes with an acquire fence B if there exists some atomic operation X on
+M such that X is sequenced before B and reads the value written by A or a value
+written by any side effect in the release sequence headed by A.
diff --git a/doc/notes/release-sequence.txt b/doc/notes/release-sequence.txt
new file mode 100644 (file)
index 0000000..85e8c0c
--- /dev/null
@@ -0,0 +1,99 @@
+-------------------------------------------------------------------------------
+ Release sequence support:
+-------------------------------------------------------------------------------
+
+*******************************
+ From the C++11 specification
+*******************************
+
+1.10.7
+
+A release sequence from a release operation A on an atomic object M is a
+maximal contiguous sub-sequence of side effects in the modification order of
+M, where the first operation is A, and every subsequent operation
+
+- is performed by the same thread that performed A, or
+- is an atomic read-modify-write operation.
+
+29.3.2
+
+An atomic operation A that performs a release operation on an atomic object M
+synchronizes with an atomic operation B that performs an acquire operation on
+M and takes its value from any side effect in the release sequence headed by
+A.
+
+*******************************
+ My Notes
+*******************************
+
+The specification allows for a single acquire to synchronize with more than
+one release operation, as its "reads from" value might be part of more than
+one release sequence.
+
+*******************************
+ Approximate Algorithm
+*******************************
+
+Check read-write chain...
+
+Given:
+current action = curr
+read from = rf
+Cases:
+* rf is NULL: return uncertain
+* rf is RMW:
+       - if rf is release:
+               add rf to release heads
+       - if rf is rel_acq:
+               return certain [note: we don't need to extend release sequence
+               further because this acquire will have synchronized already]
+         else
+               return (recursively) "get release sequence head of rf"
+* if rf is release:
+       add rf to release heads
+       return certain
+* else, rf is relaxed write (NOT RMW)
+  - check same thread
+
+*******************************
+"check same thread"
+*******************************
+
+let release = max{act in S | samethread(act, rf) && isrelease(act) && act <= rf}
+let t = thread(rf) // == thread(release)
+for all threads t_j != t
+       if exists c in S | c !--mo--> release, rf !--mo--> c, c is write, thread(c) == t_j then
+               return certain;
+[ note: need to check "future ordered" condition ]
+add release to release heads
+return certain;
+
+*******************************
+General fixup steps:
+*******************************
+
+1. process action, find read_from
+2. add initial mo_graph edges
+3. assign read_from, calc initial "get_release_seq_heads()"
+4. perform synchronization with all release heads
+
+synchronization => check for new mo_graph edges
+                => check for resolved release sequences
+               => check for failed promises
+mo_graph edges  => check for resolved release sequences
+
+*******************************
+Other notes
+*******************************
+
+"cannot determine" means we need to lazily check conditions in the future
+   - check when future writes satisfy "promises"
+
+Read from future? We require that all release heads are "in the past", so that
+we don't form synchronization against the ordering of the program trace. We
+ensure that some execution is explored in which they are ordered the other way,
+so we declare this execution "infeasible."
+
+=> If we *do* establish a synchronization after the fact:
+   - need to recurse through the execution trace and update clock vectors
+   - more
diff --git a/execution.cc b/execution.cc
new file mode 100644 (file)
index 0000000..53aa521
--- /dev/null
@@ -0,0 +1,2874 @@
+#include <stdio.h>
+#include <algorithm>
+#include <mutex>
+#include <new>
+#include <stdarg.h>
+
+#include "model.h"
+#include "execution.h"
+#include "action.h"
+#include "nodestack.h"
+#include "schedule.h"
+#include "common.h"
+#include "clockvector.h"
+#include "cyclegraph.h"
+#include "promise.h"
+#include "datarace.h"
+#include "threads-model.h"
+#include "bugmessage.h"
+
+#define INITIAL_THREAD_ID      0
+
+/**
+ * Structure for holding small ModelChecker members that should be snapshotted
+ */
+struct model_snapshot_members {
+       model_snapshot_members() :
+               /* First thread created will have id INITIAL_THREAD_ID */
+               next_thread_id(INITIAL_THREAD_ID),
+               used_sequence_numbers(0),
+               next_backtrack(NULL),
+               bugs(),
+               failed_promise(false),
+               too_many_reads(false),
+               no_valid_reads(false),
+               bad_synchronization(false),
+               asserted(false)
+       { }
+
+       ~model_snapshot_members() {
+               for (unsigned int i = 0; i < bugs.size(); i++)
+                       delete bugs[i];
+               bugs.clear();
+       }
+
+       unsigned int next_thread_id;
+       modelclock_t used_sequence_numbers;
+       ModelAction *next_backtrack;
+       SnapVector<bug_message *> bugs;
+       bool failed_promise;
+       bool too_many_reads;
+       bool no_valid_reads;
+       /** @brief Incorrectly-ordered synchronization was made */
+       bool bad_synchronization;
+       bool asserted;
+
+       SNAPSHOTALLOC
+};
+
+/** @brief Constructor */
+ModelExecution::ModelExecution(ModelChecker *m,
+               const struct model_params *params,
+               Scheduler *scheduler,
+               NodeStack *node_stack) :
+       model(m),
+       params(params),
+       scheduler(scheduler),
+       action_trace(),
+       thread_map(2), /* We'll always need at least 2 threads */
+       obj_map(),
+       condvar_waiters_map(),
+       obj_thrd_map(),
+       promises(),
+       futurevalues(),
+       pending_rel_seqs(),
+       thrd_last_action(1),
+       thrd_last_fence_release(),
+       node_stack(node_stack),
+       priv(new struct model_snapshot_members()),
+       mo_graph(new CycleGraph())
+{
+       /* Initialize a model-checker thread, for special ModelActions */
+       model_thread = new Thread(get_next_id());
+       add_thread(model_thread);
+       scheduler->register_engine(this);
+       node_stack->register_engine(this);
+}
+
+/** @brief Destructor */
+ModelExecution::~ModelExecution()
+{
+       for (unsigned int i = 0; i < get_num_threads(); i++)
+               delete get_thread(int_to_id(i));
+
+       for (unsigned int i = 0; i < promises.size(); i++)
+               delete promises[i];
+
+       delete mo_graph;
+       delete priv;
+}
+
+int ModelExecution::get_execution_number() const
+{
+       return model->get_execution_number();
+}
+
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
+{
+       action_list_t *tmp = hash->get(ptr);
+       if (tmp == NULL) {
+               tmp = new action_list_t();
+               hash->put(ptr, tmp);
+       }
+       return tmp;
+}
+
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+{
+       SnapVector<action_list_t> *tmp = hash->get(ptr);
+       if (tmp == NULL) {
+               tmp = new SnapVector<action_list_t>();
+               hash->put(ptr, tmp);
+       }
+       return tmp;
+}
+
+action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
+{
+       SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
+       if (wrv==NULL)
+               return NULL;
+       unsigned int thread=id_to_int(tid);
+       if (thread < wrv->size())
+               return &(*wrv)[thread];
+       else
+               return NULL;
+}
+
+/** @return a thread ID for a new Thread */
+thread_id_t ModelExecution::get_next_id()
+{
+       return priv->next_thread_id++;
+}
+
+/** @return the number of user threads created during this execution */
+unsigned int ModelExecution::get_num_threads() const
+{
+       return priv->next_thread_id;
+}
+
+/** @return a sequence number for a new ModelAction */
+modelclock_t ModelExecution::get_next_seq_num()
+{
+       return ++priv->used_sequence_numbers;
+}
+
+/**
+ * @brief Should the current action wake up a given thread?
+ *
+ * @param curr The current action
+ * @param thread The thread that we might wake up
+ * @return True, if we should wake up the sleeping thread; false otherwise
+ */
+bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
+{
+       const ModelAction *asleep = thread->get_pending();
+       /* Don't allow partial RMW to wake anyone up */
+       if (curr->is_rmwr())
+               return false;
+       /* Synchronizing actions may have been backtracked */
+       if (asleep->could_synchronize_with(curr))
+               return true;
+       /* All acquire/release fences and fence-acquire/store-release */
+       if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
+               return true;
+       /* Fence-release + store can awake load-acquire on the same location */
+       if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
+               ModelAction *fence_release = get_last_fence_release(curr->get_tid());
+               if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
+                       return true;
+       }
+       return false;
+}
+
+void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
+{
+       for (unsigned int i = 0; i < get_num_threads(); i++) {
+               Thread *thr = get_thread(int_to_id(i));
+               if (scheduler->is_sleep_set(thr)) {
+                       if (should_wake_up(curr, thr))
+                               /* Remove this thread from sleep set */
+                               scheduler->remove_sleep(thr);
+               }
+       }
+}
+
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelExecution::set_bad_synchronization()
+{
+       priv->bad_synchronization = true;
+}
+
+bool ModelExecution::assert_bug(const char *msg)
+{
+       priv->bugs.push_back(new bug_message(msg));
+
+       if (isfeasibleprefix()) {
+               set_assert();
+               return true;
+       }
+       return false;
+}
+
+/** @return True, if any bugs have been reported for this execution */
+bool ModelExecution::have_bug_reports() const
+{
+       return priv->bugs.size() != 0;
+}
+
+SnapVector<bug_message *> * ModelExecution::get_bugs() const
+{
+       return &priv->bugs;
+}
+
+/**
+ * Check whether the current trace has triggered an assertion which should halt
+ * its execution.
+ *
+ * @return True, if the execution should be aborted; false otherwise
+ */
+bool ModelExecution::has_asserted() const
+{
+       return priv->asserted;
+}
+
+/**
+ * Trigger a trace assertion which should cause this execution to be halted.
+ * This can be due to a detected bug or due to an infeasibility that should
+ * halt ASAP.
+ */
+void ModelExecution::set_assert()
+{
+       priv->asserted = true;
+}
+
+/**
+ * Check if we are in a deadlock. Should only be called at the end of an
+ * execution, although it should not give false positives in the middle of an
+ * execution (there should be some ENABLED thread).
+ *
+ * @return True if program is in a deadlock; false otherwise
+ */
+bool ModelExecution::is_deadlocked() const
+{
+       bool blocking_threads = false;
+       for (unsigned int i = 0; i < get_num_threads(); i++) {
+               thread_id_t tid = int_to_id(i);
+               if (is_enabled(tid))
+                       return false;
+               Thread *t = get_thread(tid);
+               if (!t->is_model_thread() && t->get_pending())
+                       blocking_threads = true;
+       }
+       return blocking_threads;
+}
+
+/**
+ * @brief Check if we are yield-blocked
+ *
+ * A program can be "yield-blocked" if all threads are ready to execute a
+ * yield.
+ *
+ * @return True if the program is yield-blocked; false otherwise
+ */
+bool ModelExecution::is_yieldblocked() const
+{
+       if (!params->yieldblock)
+               return false;
+
+       for (unsigned int i = 0; i < get_num_threads(); i++) {
+               thread_id_t tid = int_to_id(i);
+               Thread *t = get_thread(tid);
+               if (t->get_pending() && t->get_pending()->is_yield())
+                       return true;
+       }
+       return false;
+}
+
+/**
+ * Check if this is a complete execution. That is, have all thread completed
+ * execution (rather than exiting because sleep sets have forced a redundant
+ * execution).
+ *
+ * @return True if the execution is complete.
+ */
+bool ModelExecution::is_complete_execution() const
+{
+       if (is_yieldblocked())
+               return false;
+       for (unsigned int i = 0; i < get_num_threads(); i++)
+               if (is_enabled(int_to_id(i)))
+                       return false;
+       return true;
+}
+
+/**
+ * @brief Find the last fence-related backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking, as affected by fence
+ * operations. This includes pairs of potentially-synchronizing actions which
+ * occur due to fence-acquire or fence-release, and hence should be explored in
+ * the opposite execution order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act due to fences
+ */
+ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
+{
+       /* Only perform release/acquire fence backtracking for stores */
+       if (!act->is_write())
+               return NULL;
+
+       /* Find a fence-release (or, act is a release) */
+       ModelAction *last_release;
+       if (act->is_release())
+               last_release = act;
+       else
+               last_release = get_last_fence_release(act->get_tid());
+       if (!last_release)
+               return NULL;
+
+       /* Skip past the release */
+       const action_list_t *list = &action_trace;
+       action_list_t::const_reverse_iterator rit;
+       for (rit = list->rbegin(); rit != list->rend(); rit++)
+               if (*rit == last_release)
+                       break;
+       ASSERT(rit != list->rend());
+
+       /* Find a prior:
+        *   load-acquire
+        * or
+        *   load --sb-> fence-acquire */
+       ModelVector<ModelAction *> acquire_fences(get_num_threads(), NULL);
+       ModelVector<ModelAction *> prior_loads(get_num_threads(), NULL);
+       bool found_acquire_fences = false;
+       for ( ; rit != list->rend(); rit++) {
+               ModelAction *prev = *rit;
+               if (act->same_thread(prev))
+                       continue;
+
+               int tid = id_to_int(prev->get_tid());
+
+               if (prev->is_read() && act->same_var(prev)) {
+                       if (prev->is_acquire()) {
+                               /* Found most recent load-acquire, don't need
+                                * to search for more fences */
+                               if (!found_acquire_fences)
+                                       return NULL;
+                       } else {
+                               prior_loads[tid] = prev;
+                       }
+               }
+               if (prev->is_acquire() && prev->is_fence() && !acquire_fences[tid]) {
+                       found_acquire_fences = true;
+                       acquire_fences[tid] = prev;
+               }
+       }
+
+       ModelAction *latest_backtrack = NULL;
+       for (unsigned int i = 0; i < acquire_fences.size(); i++)
+               if (acquire_fences[i] && prior_loads[i])
+                       if (!latest_backtrack || *latest_backtrack < *acquire_fences[i])
+                               latest_backtrack = acquire_fences[i];
+       return latest_backtrack;
+}
+
+/**
+ * @brief Find the last backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking. This primary includes pairs of
+ * synchronizing actions which should be explored in the opposite execution
+ * order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act
+ */
+ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
+{
+       switch (act->get_type()) {
+       case ATOMIC_FENCE:
+               /* Only seq-cst fences can (directly) cause backtracking */
+               if (!act->is_seqcst())
+                       break;
+       case ATOMIC_READ:
+       case ATOMIC_WRITE:
+       case ATOMIC_RMW: {
+               ModelAction *ret = NULL;
+
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map.get(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (prev == act)
+                               continue;
+                       if (prev->could_synchronize_with(act)) {
+                               ret = prev;
+                               break;
+                       }
+               }
+
+               ModelAction *ret2 = get_last_fence_conflict(act);
+               if (!ret2)
+                       return ret;
+               if (!ret)
+                       return ret2;
+               if (*ret < *ret2)
+                       return ret2;
+               return ret;
+       }
+       case ATOMIC_LOCK:
+       case ATOMIC_TRYLOCK: {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map.get(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (act->is_conflicting_lock(prev))
+                               return prev;
+               }
+               break;
+       }
+       case ATOMIC_UNLOCK: {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map.get(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (!act->same_thread(prev) && prev->is_failed_trylock())
+                               return prev;
+               }
+               break;
+       }
+       case ATOMIC_WAIT: {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map.get(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (!act->same_thread(prev) && prev->is_failed_trylock())
+                               return prev;
+                       if (!act->same_thread(prev) && prev->is_notify())
+                               return prev;
+               }
+               break;
+       }
+
+       case ATOMIC_NOTIFY_ALL:
+       case ATOMIC_NOTIFY_ONE: {
+               /* linear search: from most recent to oldest */
+               action_list_t *list = obj_map.get(act->get_location());
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *prev = *rit;
+                       if (!act->same_thread(prev) && prev->is_wait())
+                               return prev;
+               }
+               break;
+       }
+       default:
+               break;
+       }
+       return NULL;
+}
+
+/** This method finds backtracking points where we should try to
+ * reorder the parameter ModelAction against.
+ *
+ * @param the ModelAction to find backtracking points for.
+ */
+void ModelExecution::set_backtracking(ModelAction *act)
+{
+       Thread *t = get_thread(act);
+       ModelAction *prev = get_last_conflict(act);
+       if (prev == NULL)
+               return;
+
+       Node *node = prev->get_node()->get_parent();
+
+       /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
+       int low_tid, high_tid;
+       if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
+               low_tid = id_to_int(act->get_tid());
+               high_tid = low_tid + 1;
+       } else {
+               low_tid = 0;
+               high_tid = get_num_threads();
+       }
+
+       for (int i = low_tid; i < high_tid; i++) {
+               thread_id_t tid = int_to_id(i);
+
+               /* Make sure this thread can be enabled here. */
+               if (i >= node->get_num_threads())
+                       break;
+
+               /* See Dynamic Partial Order Reduction (addendum), POPL '05 */
+               /* Don't backtrack into a point where the thread is disabled or sleeping. */
+               if (node->enabled_status(tid) != THREAD_ENABLED)
+                       continue;
+
+               /* Check if this has been explored already */
+               if (node->has_been_explored(tid))
+                       continue;
+
+               /* See if fairness allows */
+               if (params->fairwindow != 0 && !node->has_priority(tid)) {
+                       bool unfair = false;
+                       for (int t = 0; t < node->get_num_threads(); t++) {
+                               thread_id_t tother = int_to_id(t);
+                               if (node->is_enabled(tother) && node->has_priority(tother)) {
+                                       unfair = true;
+                                       break;
+                               }
+                       }
+                       if (unfair)
+                               continue;
+               }
+
+               /* See if CHESS-like yield fairness allows */
+               if (params->yieldon) {
+                       bool unfair = false;
+                       for (int t = 0; t < node->get_num_threads(); t++) {
+                               thread_id_t tother = int_to_id(t);
+                               if (node->is_enabled(tother) && node->has_priority_over(tid, tother)) {
+                                       unfair = true;
+                                       break;
+                               }
+                       }
+                       if (unfair)
+                               continue;
+               }
+
+               /* Cache the latest backtracking point */
+               set_latest_backtrack(prev);
+
+               /* If this is a new backtracking point, mark the tree */
+               if (!node->set_backtrack(tid))
+                       continue;
+               DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
+                                       id_to_int(prev->get_tid()),
+                                       id_to_int(t->get_id()));
+               if (DBG_ENABLED()) {
+                       prev->print();
+                       act->print();
+               }
+       }
+}
+
+/**
+ * @brief Cache the a backtracking point as the "most recent", if eligible
+ *
+ * Note that this does not prepare the NodeStack for this backtracking
+ * operation, it only caches the action on a per-execution basis
+ *
+ * @param act The operation at which we should explore a different next action
+ * (i.e., backtracking point)
+ * @return True, if this action is now the most recent backtracking point;
+ * false otherwise
+ */
+bool ModelExecution::set_latest_backtrack(ModelAction *act)
+{
+       if (!priv->next_backtrack || *act > *priv->next_backtrack) {
+               priv->next_backtrack = act;
+               return true;
+       }
+       return false;
+}
+
+/**
+ * Returns last backtracking point. The model checker will explore a different
+ * path for this point in the next execution.
+ * @return The ModelAction at which the next execution should diverge.
+ */
+ModelAction * ModelExecution::get_next_backtrack()
+{
+       ModelAction *next = priv->next_backtrack;
+       priv->next_backtrack = NULL;
+       return next;
+}
+
+/**
+ * Processes a read model action.
+ * @param curr is the read model action to process.
+ * @return True if processing this read updates the mo_graph.
+ */
+bool ModelExecution::process_read(ModelAction *curr)
+{
+       Node *node = curr->get_node();
+       while (true) {
+               bool updated = false;
+               switch (node->get_read_from_status()) {
+               case READ_FROM_PAST: {
+                       const ModelAction *rf = node->get_read_from_past();
+                       ASSERT(rf);
+
+                       mo_graph->startChanges();
+
+                       ASSERT(!is_infeasible());
+                       if (!check_recency(curr, rf)) {
+                               if (node->increment_read_from()) {
+                                       mo_graph->rollbackChanges();
+                                       continue;
+                               } else {
+                                       priv->too_many_reads = true;
+                               }
+                       }
+
+                       updated = r_modification_order(curr, rf);
+                       read_from(curr, rf);
+                       mo_graph->commitChanges();
+                       mo_check_promises(curr, true);
+                       break;
+               }
+               case READ_FROM_PROMISE: {
+                       Promise *promise = curr->get_node()->get_read_from_promise();
+                       if (promise->add_reader(curr))
+                               priv->failed_promise = true;
+                       curr->set_read_from_promise(promise);
+                       mo_graph->startChanges();
+                       if (!check_recency(curr, promise))
+                               priv->too_many_reads = true;
+                       updated = r_modification_order(curr, promise);
+                       mo_graph->commitChanges();
+                       break;
+               }
+               case READ_FROM_FUTURE: {
+                       /* Read from future value */
+                       struct future_value fv = node->get_future_value();
+                       Promise *promise = new Promise(this, curr, fv);
+                       curr->set_read_from_promise(promise);
+                       promises.push_back(promise);
+                       mo_graph->startChanges();
+                       updated = r_modification_order(curr, promise);
+                       mo_graph->commitChanges();
+                       break;
+               }
+               default:
+                       ASSERT(false);
+               }
+               get_thread(curr)->set_return_value(curr->get_return_value());
+               return updated;
+       }
+}
+
+/**
+ * Processes a lock, trylock, or unlock model action.  @param curr is
+ * the read model action to process.
+ *
+ * The try lock operation checks whether the lock is taken.  If not,
+ * it falls to the normal lock operation case.  If so, it returns
+ * fail.
+ *
+ * The lock operation has already been checked that it is enabled, so
+ * it just grabs the lock and synchronizes with the previous unlock.
+ *
+ * The unlock operation has to re-enable all of the threads that are
+ * waiting on the lock.
+ *
+ * @return True if synchronization was updated; false otherwise
+ */
+bool ModelExecution::process_mutex(ModelAction *curr)
+{
+       std::mutex *mutex = curr->get_mutex();
+       struct std::mutex_state *state = NULL;
+
+       if (mutex)
+               state = mutex->get_state();
+
+       switch (curr->get_type()) {
+       case ATOMIC_TRYLOCK: {
+               bool success = !state->locked;
+               curr->set_try_lock(success);
+               if (!success) {
+                       get_thread(curr)->set_return_value(0);
+                       break;
+               }
+               get_thread(curr)->set_return_value(1);
+       }
+               //otherwise fall into the lock case
+       case ATOMIC_LOCK: {
+               if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+                       assert_bug("Lock access before initialization");
+               state->locked = get_thread(curr);
+               ModelAction *unlock = get_last_unlock(curr);
+               //synchronize with the previous unlock statement
+               if (unlock != NULL) {
+                       synchronize(unlock, curr);
+                       return true;
+               }
+               break;
+       }
+       case ATOMIC_WAIT:
+       case ATOMIC_UNLOCK: {
+               /* wake up the other threads */
+               for (unsigned int i = 0; i < get_num_threads(); i++) {
+                       Thread *t = get_thread(int_to_id(i));
+                       Thread *curr_thrd = get_thread(curr);
+                       if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
+                               scheduler->wake(t);
+               }
+
+               /* unlock the lock - after checking who was waiting on it */
+               state->locked = NULL;
+
+               if (!curr->is_wait())
+                       break; /* The rest is only for ATOMIC_WAIT */
+
+               /* Should we go to sleep? (simulate spurious failures) */
+               if (curr->get_node()->get_misc() == 0) {
+                       get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->push_back(curr);
+                       /* disable us */
+                       scheduler->sleep(get_thread(curr));
+               }
+               break;
+       }
+       case ATOMIC_NOTIFY_ALL: {
+               action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+               //activate all the waiting threads
+               for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
+                       scheduler->wake(get_thread(*rit));
+               }
+               waiters->clear();
+               break;
+       }
+       case ATOMIC_NOTIFY_ONE: {
+               action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+               int wakeupthread = curr->get_node()->get_misc();
+               action_list_t::iterator it = waiters->begin();
+               advance(it, wakeupthread);
+               scheduler->wake(get_thread(*it));
+               waiters->erase(it);
+               break;
+       }
+
+       default:
+           &nbs