Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
authorSubramanian Ganapathy <sganapat@uci.edu>
Thu, 21 Jun 2012 18:45:14 +0000 (11:45 -0700)
committerSubramanian Ganapathy <sganapat@uci.edu>
Thu, 21 Jun 2012 18:45:14 +0000 (11:45 -0700)
30 files changed:
.gitignore
Doxyfile [new file with mode: 0644]
Makefile
action.cc
action.h
clockvector.cc
clockvector.h
common.h
cyclegraph.cc [new file with mode: 0644]
cyclegraph.h [new file with mode: 0644]
hashtable.h [new file with mode: 0644]
libatomic.cc
libatomic.h
librace.h
libthreads.h
main.cc
model.cc
model.h
mymemory.cc
mymemory.h
nodestack.cc
nodestack.h
schedule.h
snapshot-interface.cc
snapshot-interface.h
snapshot.cc
snapshot.h
snapshotimp.h
threads.h
userprog.c

index ab5a84ad8ea49a161901625cf3fd22202a3d5851..d4b7fc44362fc1e7b3fe90cc1d994d68ca7a7a29 100644 (file)
@@ -7,3 +7,4 @@
 # files in this directory
 /model
 /tags
+/docs
diff --git a/Doxyfile b/Doxyfile
new file mode 100644 (file)
index 0000000..a6001c3
--- /dev/null
+++ b/Doxyfile
@@ -0,0 +1,1800 @@
+# 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           = "My Project"
+
+# 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       =
+
+# 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                  =
+
+# 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
index de9051cfda92d7d75e1ef4e1b7fbaf6448a3d3e8..ddc89cb2440926aaf0551084fe89c88a3e2bbdfa 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -8,34 +8,43 @@ LIB_SO=lib$(LIB_NAME).so
 USER_O=userprog.o
 USER_H=libthreads.h libatomic.h
 
-MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc
-MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o
-MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h
+MODEL_CC=libthreads.cc schedule.cc libatomic.cc model.cc threads.cc librace.cc action.cc nodestack.cc clockvector.cc main.cc snapshot-interface.cc cyclegraph.cc
+MODEL_O=libthreads.o schedule.o libatomic.o model.o threads.o librace.o action.o nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o
+MODEL_H=libthreads.h schedule.h common.h libatomic.h model.h threads.h librace.h action.h nodestack.h clockvector.h snapshot-interface.h cyclegraph.h hashtable.h
 
 SHMEM_CC=snapshot.cc malloc.c mymemory.cc
 SHMEM_O=snapshot.o malloc.o mymemory.o
 SHMEM_H=snapshot.h snapshotimp.h mymemory.h
 
-CPPFLAGS=-Wall -g
+CPPFLAGS=-Wall -g -O0
 LDFLAGS=-ldl -lrt
+SHARED=-shared
 
 all: $(BIN)
 
 debug: CPPFLAGS += -DCONFIG_DEBUG
 debug: all
 
+mac: CPPFLAGS += -D_XOPEN_SOURCE -DMAC
+mac: LDFLAGS=-ldl
+mac: SHARED=-Wl,-undefined,dynamic_lookup -dynamiclib
+mac: all
+
+docs: *.c *.cc *.h
+       doxygen
+
 $(BIN): $(USER_O) $(LIB_SO)
        $(CXX) -o $(BIN) $(USER_O) -L. -l$(LIB_NAME)
 
 # note: implicit rule for generating $(USER_O) (i.e., userprog.c -> userprog.o)
 
 $(LIB_SO): $(MODEL_O) $(MODEL_H) $(SHMEM_O) $(SHMEM_H)
-       $(CXX) -shared -o $(LIB_SO) $(MODEL_O) $(SHMEM_O) $(LDFLAGS)
+       $(CXX) $(SHARED) -o $(LIB_SO) $(MODEL_O) $(SHMEM_O) $(LDFLAGS)
 
 malloc.o: malloc.c
        $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES $(CPPFLAGS)
 
-mymemory.o: mymemory.h snapshotimp.h mymemory.cc
+mymemory.o: mymemory.h snapshotimp.h snapshot.h mymemory.cc
        $(CXX) -fPIC -c mymemory.cc $(CPPFLAGS)
 
 snapshot.o: mymemory.h snapshot.h snapshotimp.h snapshot.cc
@@ -47,5 +56,8 @@ $(MODEL_O): $(MODEL_CC) $(MODEL_H)
 clean:
        rm -f $(BIN) *.o *.so
 
+mrclean: clean
+       rm -rf docs
+
 tags::
        ctags -R
index 28d95270a7eb19bec65d136034f13e7615edbdec..9f95727c8dcb63b27dfffc9782ab376a644d852b 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -26,17 +26,22 @@ ModelAction::~ModelAction()
                delete cv;
 }
 
-bool ModelAction::is_read()
+bool ModelAction::is_read() const
 {
        return type == ATOMIC_READ;
 }
 
-bool ModelAction::is_write()
+bool ModelAction::is_write() const
 {
        return type == ATOMIC_WRITE;
 }
 
-bool ModelAction::is_acquire()
+bool ModelAction::is_rmw() const
+{
+       return type == ATOMIC_RMW;
+}
+
+bool ModelAction::is_acquire() const
 {
        switch (order) {
        case memory_order_acquire:
@@ -48,7 +53,7 @@ bool ModelAction::is_acquire()
        }
 }
 
-bool ModelAction::is_release()
+bool ModelAction::is_release() const
 {
        switch (order) {
        case memory_order_release:
@@ -60,32 +65,59 @@ bool ModelAction::is_release()
        }
 }
 
-bool ModelAction::same_var(ModelAction *act)
+bool ModelAction::is_seqcst() const
+{
+       return order==memory_order_seq_cst;
+}
+
+bool ModelAction::same_var(const ModelAction *act) const
 {
        return location == act->location;
 }
 
-bool ModelAction::same_thread(ModelAction *act)
+bool ModelAction::same_thread(const ModelAction *act) const
 {
        return tid == act->tid;
 }
 
-bool ModelAction::is_dependent(ModelAction *act)
+/** The is_synchronizing method should only explore interleavings if:
+ *  (1) the operations are seq_cst and don't commute or
+ *  (2) the reordering may establish or break a synchronization relation.
+ *  Other memory operations will be dealt with by using the reads_from
+ *  relation.
+ *
+ *  @param act is the action to consider exploring a reordering.
+ *  @return tells whether we have to explore a reordering.
+ */
+
+bool ModelAction::is_synchronizing(const ModelAction *act) const
 {
-       if (!is_read() && !is_write())
+       //Same thread can't be reordered
+       if (same_thread(act))
                return false;
-       if (!act->is_read() && !act->is_write())
+
+       // Different locations commute
+       if (!same_var(act))
                return false;
-       if (same_var(act) && !same_thread(act) &&
-                       (is_write() || act->is_write()))
+       
+       // Explore interleavings of seqcst writes to guarantee total order
+       // of seq_cst operations that don't commute
+       if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst())
+               return true;
+
+       // Explore synchronizing read/write pairs
+       if (is_read() && is_acquire() && act->is_write() && act->is_release())
+               return true;
+       if (is_write() && is_release() && act->is_read() && act->is_acquire())
                return true;
+
+       // Otherwise handle by reads_from relation
        return false;
 }
 
 void ModelAction::create_cv(ModelAction *parent)
 {
-       if (cv)
-               return;
+       ASSERT(cv == NULL);
 
        if (parent)
                cv = new ClockVector(parent->cv, this);
@@ -101,6 +133,17 @@ void ModelAction::read_from(ModelAction *act)
        value = act->value;
 }
 
+/**
+ * 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(ModelAction *act)
+{
+       return act->cv->synchronized_since(this);
+}
+
 void ModelAction::print(void)
 {
        const char *type_str;
@@ -120,6 +163,9 @@ void ModelAction::print(void)
        case ATOMIC_WRITE:
                type_str = "atomic write";
                break;
+       case ATOMIC_RMW:
+               type_str = "atomic rmw";
+               break;
        default:
                type_str = "unknown type";
        }
index 62141749d5efafc34dc1bbe3fef6656b344571ec..ae4afb29d27f928cbe63a34d79629a6d6310b28b 100644 (file)
--- a/action.h
+++ b/action.h
@@ -1,3 +1,7 @@
+/** @file action.h
+ *  @brief Models actions taken by threads.
+ */
+
 #ifndef __ACTION_H__
 #define __ACTION_H__
 
@@ -14,39 +18,48 @@ typedef enum action_type {
        THREAD_YIELD,
        THREAD_JOIN,
        ATOMIC_READ,
-       ATOMIC_WRITE
+       ATOMIC_WRITE,
+       ATOMIC_RMW
 } action_type_t;
 
 /* Forward declaration */
 class Node;
 class ClockVector;
 
+/**
+ * The ModelAction class encapsulates an atomic action.
+ */
 class ModelAction {
 public:
        ModelAction(action_type_t type, memory_order order, void *loc, int value);
        ~ModelAction();
        void print(void);
 
-       thread_id_t get_tid() { return tid; }
-       action_type get_type() { return type; }
-       memory_order get_mo() { return order; }
-       void * get_location() { return location; }
+       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; }
        int get_seq_number() const { return seq_number; }
 
-       Node * get_node() { return node; }
+       Node * get_node() const { return node; }
        void set_node(Node *n) { node = n; }
 
-       bool is_read();
-       bool is_write();
-       bool is_acquire();
-       bool is_release();
-       bool same_var(ModelAction *act);
-       bool same_thread(ModelAction *act);
-       bool is_dependent(ModelAction *act);
+       bool is_read() const;
+       bool is_write() const;
+       bool is_rmw() 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_synchronizing(const ModelAction *act) const;
 
        void create_cv(ModelAction *parent = NULL);
+       ClockVector * get_cv() const { return cv; }
        void read_from(ModelAction *act);
 
+       bool happens_before(ModelAction *act);
+
        inline bool operator <(const ModelAction& act) const {
                return get_seq_number() < act.get_seq_number();
        }
@@ -56,14 +69,31 @@ public:
 
        MEMALLOC
 private:
+
+       /** Type of action (read, write, thread create, thread yield, thread join) */
        action_type type;
+
+       /** The memory order for this operation. */
        memory_order order;
+
+       /** A pointer to the memory location for this action. */
        void *location;
+
+       /** The thread id that performed this action. */
        thread_id_t tid;
+       
+       /** The value read or written (if RMW, then the value written). This
+        * should probably be something longer. */
        int value;
+
+       /** A back reference to a Node in NodeStack, if this ModelAction is
+        * saved on the NodeStack. */
        Node *node;
+       
        int seq_number;
 
+       /** The clock vector stored with this action; only needed if this
+        * action is a store release? */
        ClockVector *cv;
 };
 
index f411f50d64bcb9ca6c1b7eefe48f871bcc1c1bff..95896ed3a61a7d62b725028b04d7c939245f83a8 100644 (file)
@@ -7,6 +7,14 @@
 #include "clockvector.h"
 #include "common.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)
 {
        num_threads = model->get_num_threads();
@@ -19,11 +27,17 @@ ClockVector::ClockVector(ClockVector *parent, ModelAction *act)
                clock[id_to_int(act->get_tid())] = act->get_seq_number();
 }
 
+/** @brief Destructor */
 ClockVector::~ClockVector()
 {
        MYFREE(clock);
 }
 
+/**
+ * Merge a clock vector into this vector, using a pairwise vector. The
+ * resulting vector length will be the maximum length of the two being merged.
+ * @param cv is the ClockVector being merged into this vector.
+ */
 void ClockVector::merge(ClockVector *cv)
 {
        int *clk = clock;
@@ -49,16 +63,29 @@ void ClockVector::merge(ClockVector *cv)
        clock = clk;
 }
 
-bool ClockVector::happens_before(ModelAction *act, thread_id_t id)
+/**
+ * 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(ModelAction *act) const
 {
-       int i = id_to_int(id);
+       int i = id_to_int(act->get_tid());
 
        if (i < num_threads)
-               return act->get_seq_number() < clock[i];
+               return act->get_seq_number() <= clock[i];
        return false;
 }
 
-void ClockVector::print()
+/** @brief Formats and prints this ClockVector's data. */
+void ClockVector::print() const
 {
        int i;
        printf("CV: (");
index eb7086253d7f97e79b0f1d1ce41ef7b4e988e561..b7d720688a1c6df4a9aad410e1eb4897b08d35ff 100644 (file)
@@ -1,3 +1,7 @@
+/** @file clockvector.h
+ *  @brief Implements a clock vector.
+ */
+
 #ifndef __CLOCKVECTOR_H__
 #define __CLOCKVECTOR_H__
 
@@ -12,13 +16,16 @@ public:
        ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
        ~ClockVector();
        void merge(ClockVector *cv);
-       bool happens_before(ModelAction *act, thread_id_t id);
+       bool synchronized_since(ModelAction *act) const;
 
-       void print();
+       void print() const;
 
        MEMALLOC
 private:
+       /** @brief Holds the actual clock data, as an array. */
        int *clock;
+
+       /** @brief The number of threads recorded in clock (i.e., its length).  */
        int num_threads;
 };
 
index 656ea3798dde73d08b168fdfe54f5d4c72dcc04d..0db1cfe15f722dd8bd487aa98cdb3d16b7cfb79f 100644 (file)
--- a/common.h
+++ b/common.h
@@ -1,3 +1,7 @@
+/** @file common.h
+ *  @brief General purpose macros.
+ */
+
 #ifndef __COMMON_H__
 #define __COMMON_H__
 
@@ -23,7 +27,7 @@
 do { \
        if (!(expr)) { \
                fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
-               exit(1); \
+               exit(EXIT_FAILURE); \
        } \
 } while (0);
 
diff --git a/cyclegraph.cc b/cyclegraph.cc
new file mode 100644 (file)
index 0000000..c1fea4f
--- /dev/null
@@ -0,0 +1,59 @@
+#include "cyclegraph.h"
+
+CycleGraph::CycleGraph() {
+       hasCycles=false;
+}
+
+CycleNode * CycleGraph::getNode(ModelAction * action) {
+       CycleNode *node=actionToNode.get(action);
+       if (node==NULL) {
+               node=new CycleNode(action);
+               actionToNode.put(action, node);
+       }
+       return node;
+}
+
+void CycleGraph::addEdge(ModelAction *from, ModelAction *to) {
+       CycleNode *fromnode=getNode(from);
+       CycleNode *tonode=getNode(to);
+       if (!hasCycles) {
+               // Check for Cycles
+               hasCycles=checkReachable(fromnode, tonode);
+       }
+       fromnode->addEdge(tonode);
+}
+
+bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
+       std::vector<class CycleNode *> queue;
+       HashTable<class CycleNode *, class CycleNode *, uintptr_t, 4> discovered;
+       
+       queue.push_back(from);
+       discovered.put(from, from);
+       while(!queue.empty()) {
+               class CycleNode * node=queue.back();
+               queue.pop_back();
+               if (node==to)
+                       return true;
+               
+               for(unsigned int i=0;i<node->getEdges()->size();i++) {
+                       CycleNode *next=(*node->getEdges())[i];
+                       if (!discovered.contains(next)) {
+                               discovered.put(next,next);
+                               queue.push_back(next);
+                       }
+               }
+       }
+       return false;
+}
+
+CycleNode::CycleNode(ModelAction *modelaction) {
+       action=modelaction;
+}
+
+std::vector<class CycleNode *> * CycleNode::getEdges() {
+       return &edges;
+}
+
+void CycleNode::addEdge(CycleNode * node) {
+       edges.push_back(node);
+}
diff --git a/cyclegraph.h b/cyclegraph.h
new file mode 100644 (file)
index 0000000..818a3e8
--- /dev/null
@@ -0,0 +1,38 @@
+#ifndef CYCLEGRAPH_H
+#define CYCLEGRAPH_H
+
+#include "hashtable.h"
+#include "action.h"
+#include <vector>
+#include <inttypes.h>
+
+class CycleNode;
+
+/** @brief A graph of Model Actions for tracking cycles. */
+class CycleGraph {
+ public:
+       CycleGraph();
+       void addEdge(ModelAction *from, ModelAction *to);
+       bool checkForCycles();
+
+ private:
+       CycleNode * getNode(ModelAction *);
+       HashTable<class ModelAction *, class CycleNode *, uintptr_t, 4> actionToNode;
+       bool checkReachable(CycleNode *from, CycleNode *to);
+       
+       bool hasCycles;
+
+};
+
+class CycleNode {
+ public:
+       CycleNode(ModelAction *action);
+       void addEdge(CycleNode * node);
+       std::vector<class CycleNode *> * getEdges();
+
+ private:
+       ModelAction *action;
+       std::vector<class CycleNode *> edges;
+};
+
+#endif
diff --git a/hashtable.h b/hashtable.h
new file mode 100644 (file)
index 0000000..f372f9e
--- /dev/null
@@ -0,0 +1,143 @@
+#ifndef HASHTABLE_H
+#define HASHTABLE_H
+
+#include <stdlib.h>
+#include <stdio.h>
+
+template<typename _Key, typename _Val>
+       struct hashlistnode {
+               _Key key;
+               _Val val;
+               struct hashlistnode<_Key,_Val> *next;
+       };
+
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift>
+       class HashTable {
+ public:
+       HashTable(unsigned int initialcapacity=1024, double factor=0.5) {
+               // Allocate space for the hash table
+               table = (struct hashlistnode<_Key,_Val> **) calloc(initialcapacity, sizeof(struct hashlistnode<_Key,_Val> *));
+               loadfactor = factor;
+               capacity = initialcapacity;
+               threshold = initialcapacity*loadfactor;
+               mask = (capacity << _Shift)-1;
+               size = 0; // Initial number of elements in the hash
+       }
+
+       ~HashTable() {
+               for(unsigned int i=0;i<capacity;i++) {
+                       struct hashlistnode<_Key,_Val> * bin = table[i];
+                       while(bin!=NULL) {
+                               struct hashlistnode<_Key,_Val> * next=bin->next;
+                               free(bin);
+                               bin=next;
+                       }
+               }
+               free(table);
+       }
+
+       void reset() {
+               for(int i=0;i<capacity;i++) {
+                       struct hashlistnode<_Key,_Val> * bin = table[i];
+                       while(bin!=NULL) {
+                               struct hashlistnode<_Key,_Val> * next=bin->next;
+                               free(bin);
+                               bin=next;
+                       }
+               }
+               memset(table, 0, capacity*sizeof(struct hashlistnode<_Key, _Val> *));
+               size=0;
+       }
+       
+       void put(_Key key, _Val val) {
+               if(size > threshold) {
+                       //Resize
+                       unsigned int newsize = capacity << 1;
+                       resize(newsize);
+               }
+               
+               struct hashlistnode<_Key,_Val> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
+               size++;
+               struct hashlistnode<_Key,_Val> *search = ptr;
+
+               while(search!=NULL) {
+                       if (search->key==key) {
+                               search->val=val;
+                               return;
+                       }
+                       search=search->next;
+               }
+
+               struct hashlistnode<_Key,_Val> *newptr=(struct hashlistnode<_Key,_Val> *)malloc(sizeof(struct hashlistnode<_Key,_Val>));
+               newptr->key=key;
+               newptr->val=val;
+               newptr->next=ptr;
+               table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
+       }
+
+       _Val get(_Key key) {
+               struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+               
+               while(search!=NULL) {
+                       if (search->key==key) {
+                               return search->val;
+                       }
+                       search=search->next;
+               }
+               return (_Val)0;
+       }
+
+       bool contains(_Key key) {
+               struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+               
+               while(search!=NULL) {
+                       if (search->key==key) {
+                               return true;
+                       }
+                       search=search->next;
+               }
+               return false;
+       }
+       
+       void resize(unsigned int newsize) {
+               struct hashlistnode<_Key,_Val> ** oldtable = table;
+               struct hashlistnode<_Key,_Val> ** newtable;
+               unsigned int oldcapacity = capacity;
+               
+               if((newtable = (struct hashlistnode<_Key,_Val> **) calloc(newsize, sizeof(struct hashlistnode<_Key,_Val> *))) == NULL) {
+                       printf("Calloc error %s %d\n", __FILE__, __LINE__);
+                       exit(-1);
+               }
+               
+               table = newtable;          //Update the global hashtable upon resize()
+               capacity = newsize;
+               threshold = newsize * loadfactor;
+               mask = (newsize << _Shift)-1;
+               
+               for(unsigned int i = 0; i < oldcapacity; i++) {
+                       struct hashlistnode<_Key, _Val> * bin = oldtable[i];
+                       
+                       while(bin!=NULL) {
+                               _Key key=bin->key;
+                               struct hashlistnode<_Key, _Val> * next=bin->next;
+                               
+                               unsigned int index = (((_KeyInt)key) & mask) >>_Shift;
+                               struct hashlistnode<_Key, _Val> * tmp=newtable[index];
+                               bin->next=tmp;
+                               newtable[index]=bin;
+                               bin = next;
+                       }
+               }
+               
+               free(oldtable);            //Free the memory of the old hash table
+       }
+       
+ private:
+       struct hashlistnode<_Key,_Val> **table;
+       unsigned int capacity;
+       _KeyInt mask;
+       unsigned int size;
+       unsigned int threshold;
+       double loadfactor;
+};
+#endif
index 88d7fbf79900859575b7b6d3bf1b78609caddd3b..507f6853ca503e75664a86a5711f8f03c5cbc10a 100644 (file)
@@ -5,8 +5,8 @@
 void atomic_store_explicit(struct atomic_object *obj, int value, memory_order order)
 {
        DBG();
-       model->switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
        obj->value = value;
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
 }
 
 int atomic_load_explicit(struct atomic_object *obj, memory_order order)
index 1806f21968b75405c1675a9456b4e79afa6f421f..f24b5fbff35a10a3dcc2c88beca108ecb9093e75 100644 (file)
@@ -1,3 +1,7 @@
+/** @file libatomic.h
+ *  @brief Basic atomic operations to be exposed to user program.
+ */
+
 #ifndef __LIBATOMIC_H__
 #define __LIBATOMIC_H__
 
index a8af6864da2e483a14a58f2571ae36d7a0b62319..591b2925473b9ef608d533d70f2b3d2cf6a928a6 100644 (file)
--- a/librace.h
+++ b/librace.h
@@ -1,3 +1,7 @@
+/** @file librace.h
+ *  @brief Interface to check normal memory operations for data races.
+ */
+
 #ifndef __LIBRACE_H__
 #define __LIBRACE_H__
 
index f6de95bb9fa4f3614f07658b2abe05f8217ec6fa..0c02971342d06ffa903feb01b2d4daadc08754d4 100644 (file)
@@ -1,3 +1,7 @@
+/** @file libthreads.h
+ *  @brief Basic Thread Library Functionality.
+ */
+
 #ifndef __LIBTHREADS_H__
 #define __LIBTHREADS_H__
 
diff --git a/main.cc b/main.cc
index e8a2b3317dc4ebedc235735fef32d272259d4215..b38f7ef4816d003f45d876133dacf0dc0d816bab 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -1,3 +1,7 @@
+/** @file main.cc
+ *  @brief Entry point for the model checker.
+ */
+
 #include "libthreads.h"
 #include "common.h"
 #include "threads.h"
@@ -6,9 +10,11 @@
 #include "model.h"
 #include "snapshot-interface.h"
 
-/*
- * Return 1 if found next thread, 0 otherwise
+/** The thread_system_next function takes the next step in the
+ *  execution.  @return Returns the 1 if there is another step and 0
+ *  otherwise.
  */
+
 static int thread_system_next(void) {
        Thread *curr, *next;
 
@@ -32,12 +38,19 @@ static int thread_system_next(void) {
        return Thread::swap(model->get_system_context(), next);
 }
 
+/** The thread_wait_finish method runs the current execution until we
+ *  have no more steps to take.
+ */
+
 static void thread_wait_finish(void) {
        DBG();
 
        while (!thread_system_next());
 }
 
+
+/** The real_main function contains the main model checking loop. */
+
 void real_main() {
        thrd_t user_thread;
        ucontext_t main_context;
@@ -70,8 +83,9 @@ void real_main() {
 int main_numargs;
 char ** main_args;
 
-/*
- * Main system function
+/**
+ * Main function.  Just initializes snapshotting library and the
+ * snapshotting library calls the real_main function.
  */
 int main(int numargs, char ** args) {
        /* Stash this stuff in case someone wants it eventually */
index 2ffa22a1028a8008c1c60e52e8e9fee627fac766..19d273de50bf67aa60cf6835845b21ac347fc7be 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -6,11 +6,13 @@
 #include "schedule.h"
 #include "snapshot-interface.h"
 #include "common.h"
+#include "clockvector.h"
 
 #define INITIAL_THREAD_ID      0
 
 ModelChecker *model;
 
+/** @brief Constructor */
 ModelChecker::ModelChecker()
        :
        /* Initialize default scheduler */
@@ -32,6 +34,7 @@ ModelChecker::ModelChecker()
 {
 }
 
+/** @brief Destructor */
 ModelChecker::~ModelChecker()
 {
        std::map<int, class Thread *>::iterator it;
@@ -46,6 +49,10 @@ ModelChecker::~ModelChecker()
        delete scheduler;
 }
 
+/**
+ * Restores user program to initial state and resets all model-checker data
+ * structures.
+ */
 void ModelChecker::reset_to_initial_state()
 {
        DEBUG("+++ Resetting to initial state +++\n");
@@ -58,21 +65,33 @@ void ModelChecker::reset_to_initial_state()
        snapshotObject->backTrackBeforeStep(0);
 }
 
+/** @returns a thread ID for a new Thread */
 thread_id_t ModelChecker::get_next_id()
 {
        return next_thread_id++;
 }
 
+/** @returns the number of user threads created during this execution */
 int ModelChecker::get_num_threads()
 {
        return next_thread_id;
 }
 
+/** @returns a sequence number for a new ModelAction */
 int ModelChecker::get_next_seq_num()
 {
        return ++used_sequence_numbers;
 }
 
+/**
+ * Performs the "scheduling" for the model-checker. That is, it checks if the
+ * model-checker has selected a "next thread to run" and returns it, if
+ * available. This function should be called from the Scheduler routine, where
+ * the Scheduler falls back to a default scheduling routine if needed.
+ *
+ * @return The next thread chosen by the model-checker. If the model-checker
+ * makes no selection, retuns NULL.
+ */
 Thread * ModelChecker::schedule_next_thread()
 {
        Thread *t;
@@ -85,12 +104,12 @@ Thread * ModelChecker::schedule_next_thread()
        return t;
 }
 
-/*
- * get_next_replay_thread() - Choose the next thread in the replay sequence
+/**
+ * Choose the next thread in the replay sequence.
  *
- * If we've reached the 'diverge' point, then we pick a thread from the
- *   backtracking set.
- * Otherwise, we simply return the next thread in the sequence.
+ * If the replay sequence has reached the 'diverge' point, returns a thread
+ * from the backtracking set. Otherwise, simply returns the next thread in the
+ * sequence that is being replayed.
  */
 thread_id_t ModelChecker::get_next_replay_thread()
 {
@@ -118,6 +137,13 @@ thread_id_t ModelChecker::get_next_replay_thread()
        return tid;
 }
 
+/**
+ * Queries the model-checker for more executions to explore and, if one
+ * exists, resets the model-checker state to execute a new execution.
+ *
+ * @return If there are more executions to explore, return true. Otherwise,
+ * return false.
+ */
 bool ModelChecker::next_execution()
 {
        DBG();
@@ -154,7 +180,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
        action_list_t::reverse_iterator rit;
        for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
                ModelAction *prev = *rit;
-               if (act->is_dependent(prev))
+               if (act->is_synchronizing(prev))
                        return prev;
        }
        return NULL;
@@ -205,14 +231,28 @@ void ModelChecker::check_current_action(void)
        Node *currnode;
 
        ModelAction *curr = this->current_action;
+       ModelAction *tmp;
        current_action = NULL;
        if (!curr) {
                DEBUG("trying to push NULL action...\n");
                return;
        }
 
-       curr = node_stack->explore_action(curr);
-       curr->create_cv(get_parent_action(curr->get_tid()));
+       tmp = node_stack->explore_action(curr);
+       if (tmp) {
+               /* Discard duplicate ModelAction; use action from NodeStack */
+               delete curr;
+               curr = tmp;
+       } else {
+               /*
+                * Perform one-time actions when pushing new ModelAction onto
+                * NodeStack
+                */
+               curr->create_cv(get_parent_action(curr->get_tid()));
+               /* Build may_read_from set */
+               if (curr->is_read())
+                       build_reads_from_past(curr);
+       }
 
        /* Assign 'creation' parent */
        if (curr->get_type() == THREAD_CREATE) {
@@ -233,6 +273,12 @@ void ModelChecker::check_current_action(void)
        add_action_to_lists(curr);
 }
 
+
+/**
+ * Adds an action to the per-object, per-thread action vector.
+ * @param act is the ModelAction to add.
+ */
+
 void ModelChecker::add_action_to_lists(ModelAction *act)
 {
        action_trace->push_back(act);
@@ -261,11 +307,49 @@ ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
        return parent;
 }
 
+/**
+ * Build up an initial set of all past writes that this 'read' action may read
+ * from. This set is determined by the clock vector's "happens before"
+ * relationship.
+ * @param curr is the current ModelAction that we are exploring; it must be a
+ * 'read' operation.
+ */
+void ModelChecker::build_reads_from_past(ModelAction *curr)
+{
+       std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
+       unsigned int i;
+
+       ASSERT(curr->is_read());
+
+       for (i = 0; i < thrd_lists->size(); i++) {
+               action_list_t *list = &(*thrd_lists)[i];
+               action_list_t::reverse_iterator rit;
+               for (rit = list->rbegin(); rit != list->rend(); rit++) {
+                       ModelAction *act = *rit;
+
+                       /* Only consider 'write' actions */
+                       if (!act->is_write())
+                               continue;
+
+                       DEBUG("Adding action to may_read_from:\n");
+                       if (DBG_ENABLED()) {
+                               act->print();
+                               curr->print();
+                       }
+                       curr->get_node()->add_read_from(act);
+
+                       /* Include at most one act that "happens before" curr */
+                       if (act->happens_before(curr))
+                               break;
+               }
+       }
+}
+
 void ModelChecker::print_summary(void)
 {
        printf("\n");
        printf("Number of executions: %d\n", num_executions);
-       printf("Total nodes created: %d\n", Node::get_total_nodes());
+       printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 
        scheduler->print();
 
diff --git a/model.h b/model.h
index d89a8a2b123b1743c58f3c5d7c883c87263b45b9..ab961f840b03613492a4da2b8585453bbe6b2847 100644 (file)
--- a/model.h
+++ b/model.h
@@ -1,3 +1,7 @@
+/** @file model.h
+ *  @brief Core model checker. 
+ */
+
 #ifndef __MODEL_H__
 #define __MODEL_H__
 
 /* Forward declaration */
 class NodeStack;
 
+/** @brief The central structure for model-checking */
 class ModelChecker {
 public:
        ModelChecker();
        ~ModelChecker();
+
+       /** The scheduler to use: tracks the running/ready Threads */
        class Scheduler *scheduler;
 
+       /** Stores the context for the main model-checking system thread (call
+        * once)
+        * @param ctxt The system context structure
+        */
        void set_system_context(ucontext_t *ctxt) { system_context = ctxt; }
+
+       /** @returns the context for the main model-checking system thread */
        ucontext_t * get_system_context(void) { return system_context; }
 
+       /**
+        * Stores the ModelAction for the current thread action.  Call this
+        * immediately before switching from user- to system-context to pass
+        * data between them.
+        * @param act The ModelAction created by the user-thread action
+        */
        void set_current_action(ModelAction *act) { current_action = act; }
        void check_current_action(void);
        void print_summary(void);
@@ -59,6 +78,7 @@ private:
        void add_action_to_lists(ModelAction *act);
        ModelAction * get_last_action(thread_id_t tid);
        ModelAction * get_parent_action(thread_id_t tid);
+       void build_reads_from_past(ModelAction *curr);
 
        void print_list(action_list_t *list);
 
index 80c1b953ff6855e24d058ddffa6589f29a6dda1f..88018e269093c531a67bde16d27de8a95d6d6305 100644 (file)
@@ -3,10 +3,18 @@
 #include "snapshotimp.h"
 #include <stdio.h>
 #include <dlfcn.h>
+#include <unistd.h>
+#include <cstring>
+#define REQUESTS_BEFORE_ALLOC 1024
+size_t allocatedReqs[ REQUESTS_BEFORE_ALLOC ] = { 0 };
+int nextRequest = 0;
+int howManyFreed = 0;
 #if !USE_MPROTECT_SNAPSHOT
 static mspace sStaticSpace = NULL;
 #endif
 
+/** Non-snapshotting malloc for our use. */
+
 void *MYMALLOC(size_t size) {
 #if USE_MPROTECT_SNAPSHOT
        static void *(*mallocp)(size_t size);
@@ -18,7 +26,7 @@ void *MYMALLOC(size_t size) {
                mallocp = ( void * ( * )( size_t ) )dlsym(RTLD_NEXT, "malloc");
                if ((error = dlerror()) != NULL) {
                        fputs(error, stderr);
-                       exit(1);
+                       exit(EXIT_FAILURE);
                }
        }
        ptr = mallocp(size);     
@@ -28,11 +36,44 @@ void *MYMALLOC(size_t size) {
                createSharedLibrary();
        }
        if( NULL == sStaticSpace )
-               sStaticSpace = create_mspace_with_base( ( void * )( sTheRecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct Snapshot_t ), 1 );
+               sStaticSpace = create_mspace_with_base( ( void * )( sTheRecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct Snapshot ), 1 );
        return mspace_malloc( sStaticSpace, size );
 #endif
 }
 
+void *system_malloc( size_t size ){
+       static void *(*mallocp)(size_t size);
+       char *error;
+       void *ptr;
+
+       /* get address of libc malloc */
+       if (!mallocp) {
+               mallocp = ( void * ( * )( size_t ) )dlsym(RTLD_NEXT, "malloc");
+               if ((error = dlerror()) != NULL) {
+                       fputs(error, stderr);
+                       exit(EXIT_FAILURE);
+               }
+       }
+       ptr = mallocp(size);
+       return ptr;
+}
+
+void system_free( void * ptr ){
+       static void (*freep)(void *);
+       char *error;
+
+       /* get address of libc free */
+       if (!freep) {
+               freep = ( void  ( * )( void * ) )dlsym(RTLD_NEXT, "free");
+               if ((error = dlerror()) != NULL) {
+                       fputs(error, stderr);
+                       exit(EXIT_FAILURE);
+               }
+       }
+       freep(ptr);
+}
+
+/** Non-snapshotting free for our use. */
 void MYFREE(void *ptr) {
 #if USE_MPROTECT_SNAPSHOT
        static void (*freep)(void *);
@@ -43,7 +84,7 @@ void MYFREE(void *ptr) {
                freep = ( void  ( * )( void * ) )dlsym(RTLD_NEXT, "free");
                if ((error = dlerror()) != NULL) {
                        fputs(error, stderr);
-                       exit(1);
+                       exit(EXIT_FAILURE);
                }
        }
        freep(ptr);
@@ -51,29 +92,95 @@ void MYFREE(void *ptr) {
        mspace_free( sStaticSpace, ptr );
 #endif
 }
+
+
+/** This global references the mspace for the snapshotting heap */
 mspace mySpace = NULL;
+
+/** This global references the unaligned memory address that was malloced for the snapshotting heap */
 void * basemySpace = NULL;
 
+/** Adding the fix for not able to allocate through a reimplemented calloc at the beginning before instantiating our allocator
+A bit circumspect about adding an sbrk. linux docs say to avoid using it... */
+
+void * HandleEarlyAllocationRequest( size_t sz ){
+       if( 0 == mySpace ){
+               void * returnAddress = sbrk( sz );
+               if( nextRequest >= REQUESTS_BEFORE_ALLOC ){
+                       exit( EXIT_FAILURE );
+               }
+               allocatedReqs[ nextRequest++ ] = ( size_t )returnAddress;
+               return returnAddress;
+       }
+       return NULL;
+}
+
+/** The fact that I am not expecting more than a handful requests is implicit in my not using a binary search here*/
+
+bool DontFree( void * ptr ){
+       if( howManyFreed == nextRequest ) return false; //a minor optimization to reduce the number of instructions executed on each free call....
+       if( NULL == ptr ) return true;
+       for( int i =  nextRequest - 1; i >= 0; --i ){
+               if( allocatedReqs[ i ] ==  ( size_t )ptr ) {
+                       ++howManyFreed;
+                       return true;
+               }
+       }
+       return false;
+}
+
+/** Snapshotting malloc implementation for user programs. */
+
 void *malloc( size_t size ) {
+       void * earlyReq = HandleEarlyAllocationRequest( size );
+       if( earlyReq ) return earlyReq;
        return mspace_malloc( mySpace, size );
 }
 
+/** Snapshotting free implementation for user programs. */
+
 void free( void * ptr ){
+       if( DontFree( ptr ) ) return;
        mspace_free( mySpace, ptr );
 }
 
+/** Snapshotting realloc implementation for user programs. */
+
+void *realloc( void *ptr, size_t size ){
+       return mspace_realloc( mySpace, ptr, size );
+}
+
+/** Snapshotting calloc implementation for user programs. */
+
+void * calloc( size_t num, size_t size ){
+       void * earlyReq = HandleEarlyAllocationRequest( size * num );
+       if( earlyReq ) {
+               std::memset( earlyReq, 0, size * num );
+               return earlyReq;
+       }
+       return mspace_calloc( mySpace, num, size );
+}
+
+/** Snapshotting new operator for user programs. */
+
 void * operator new(size_t size) throw(std::bad_alloc) {
        return malloc(size);
 }
 
+/** Snapshotting delete operator for user programs. */
+
 void operator delete(void *p) throw() {
        free(p);
 }
 
+/** Snapshotting new[] operator for user programs. */
+
 void * operator new[](size_t size) throw(std::bad_alloc) {
        return malloc(size);
 }
 
+/** Snapshotting delete[] operator for user programs. */
+
 void operator delete[](void *p, size_t size) {
        free(p);
 }
index 90b27844f5f8e025c68ef8be56d50f93cbdf2a72..56e690436d1e573da00bf287e6aff2388f476c0c 100644 (file)
@@ -1,8 +1,15 @@
+/** @file mymemory.h
+ *  @brief Memory allocation functions.
+ */
+
 #ifndef _MY_MEMORY_H
 #define _MY_MEMORY_H
 #include <stdlib.h>
 #include <limits>
 
+/** MEMALLOC declares the allocators for a class to allocate
+ *     memory in the non-snapshotting heap. */
+
 #define MEMALLOC \
        void * operator new(size_t size) { \
                return MYMALLOC(size);\
                MYFREE(p);\
        }
 
-/* Empty define; represents opposite of MEMALLOC */
+/** SNAPSHOTALLOC declares the allocators for a class to allocate
+ *     memory in the snapshotting heap. */
+
 #define SNAPSHOTALLOC
 
 void *MYMALLOC(size_t size);
 void MYFREE(void *ptr);
 
-/*
-The following code example is taken from the book
-The C++ Standard Library - A Tutorial and Reference
-by Nicolai M. Josuttis, Addison-Wesley, 1999
-© Copyright Nicolai M. Josuttis 1999
-Permission to copy, use, modify, sell and distribute this software
-is granted provided this copyright notice appears in all copies.
-This software is provided "as is" without express or implied
-warranty, and with no claim as to its suitability for any purpose.
-*/
+void system_free( void * ptr );
+void *system_malloc( size_t size );
+
+/** @brief Provides a non-snapshotting allocator for use in STL classes.
+ *
+ * The code was adapted from a code example from the book The C++
+ * Standard Library - A Tutorial and Reference by Nicolai M. Josuttis,
+ * Addison-Wesley, 1999 Â© Copyright Nicolai M. Josuttis 1999
+ * Permission to copy, use, modify, sell and distribute this software
+ * is granted provided this copyright notice appears in all copies.
+ * This software is provided "as is" without express or implied
+ * warranty, and with no claim as to its suitability for any purpose.
+ */
+
 template <class T>
    class MyAlloc {
      public:
@@ -101,12 +114,14 @@ template <class T>
        }
    };
 
-// return that all specializations of this allocator are interchangeable
+/** Return that all specializations of this allocator are interchangeable. */
  template <class T1, class T2>
  bool operator== (const MyAlloc<T1>&,
                   const MyAlloc<T2>&) throw() {
      return true;
  }
+
+/** Return that all specializations of this allocator are interchangeable. */
  template <class T1, class T2>
  bool operator!= (const MyAlloc<T1>&,
                   const MyAlloc<T2>&) throw() {
@@ -119,6 +134,8 @@ extern "C" {
 typedef void * mspace;
 extern void* mspace_malloc(mspace msp, size_t bytes);
 extern void mspace_free(mspace msp, void* mem);
+extern void* mspace_realloc(mspace msp, void* mem, size_t newsize);
+extern void* mspace_calloc(mspace msp, size_t n_elements, size_t elem_size);
 extern mspace create_mspace_with_base(void* base, size_t capacity, int locked);
 extern mspace create_mspace(size_t capacity, int locked);
 extern mspace mySpace;
index df5fc633ac37aba0b6df464f51be996ab8403eb6..87b3ee531fbe2d10a7b52f229f23e7ea90196e9d 100644 (file)
@@ -3,23 +3,25 @@
 #include "common.h"
 #include "model.h"
 
-int Node::total_nodes = 0;
-
+/** @brief Node constructor */
 Node::Node(ModelAction *act, int nthreads)
        : action(act),
        num_threads(nthreads),
        explored_children(num_threads),
-       backtrack(num_threads)
+       backtrack(num_threads),
+       numBacktracks(0),
+       may_read_from()
 {
-       total_nodes++;
 }
 
+/** @brief Node desctructor */
 Node::~Node()
 {
        if (action)
                delete action;
 }
 
+/** Prints debugging info for the ModelAction associated with this Node */
 void Node::print()
 {
        if (action)
@@ -28,33 +30,54 @@ void Node::print()
                printf("******** empty action ********\n");
 }
 
+/**
+ * Checks if the Thread associated with this thread ID has been explored from
+ * this Node already.
+ * @param tid is the thread ID to check
+ * @return true if this thread choice has been explored already, false
+ * otherwise
+ */
 bool Node::has_been_explored(thread_id_t tid)
 {
        int id = id_to_int(tid);
        return explored_children[id];
 }
 
+/**
+ * Checks if the backtracking set is empty.
+ * @return true if the backtracking set is empty
+ */
 bool Node::backtrack_empty()
 {
-       unsigned int i;
-       for (i = 0; i < backtrack.size(); i++)
-               if (backtrack[i] == true)
-                       return false;
-       return true;
+       return numBacktracks == 0;
 }
 
+/**
+ * Explore a child Node using a given ModelAction. This updates both the
+ * Node-internal and the ModelAction data to associate the ModelAction with
+ * this Node.
+ * @param act is the ModelAction to explore
+ */
 void Node::explore_child(ModelAction *act)
 {
        act->set_node(this);
        explore(act->get_tid());
 }
 
+/**
+ * Records a backtracking reference for a thread choice within this Node.
+ * Provides feedback as to whether this thread choice is already set for
+ * backtracking.
+ * @return false if the thread was already set to be backtracked, true
+ * otherwise
+ */
 bool Node::set_backtrack(thread_id_t id)
 {
        int i = id_to_int(id);
        if (backtrack[i])
                return false;
        backtrack[i] = true;
+       numBacktracks++;
        return true;
 }
 
@@ -68,6 +91,7 @@ thread_id_t Node::get_next_backtrack()
        if (i >= backtrack.size())
                return THREAD_ID_T_NONE;
        backtrack[i] = false;
+       numBacktracks--;
        return int_to_id(i);
 }
 
@@ -76,10 +100,22 @@ bool Node::is_enabled(Thread *t)
        return id_to_int(t->get_id()) < num_threads;
 }
 
+/**
+ * Add an action to the may_read_from set.
+ * @param act is the action to add
+ */
+void Node::add_read_from(ModelAction *act)
+{
+       may_read_from.insert(act);
+}
+
 void Node::explore(thread_id_t tid)
 {
        int i = id_to_int(tid);
-       backtrack[i] = false;
+       if (backtrack[i]) {
+               backtrack[i] = false;
+               numBacktracks--;
+       }
        explored_children[i] = true;
 }
 
@@ -94,8 +130,10 @@ static void clear_node_list(node_list_t *list, node_list_t::iterator start,
 }
 
 NodeStack::NodeStack()
+       : total_nodes(0)
 {
        node_list.push_back(new Node());
+       total_nodes++;
        iter = node_list.begin();
 }
 
@@ -124,21 +162,21 @@ ModelAction * NodeStack::explore_action(ModelAction *act)
        ASSERT(!node_list.empty());
 
        if (get_head()->has_been_explored(act->get_tid())) {
-               /* Discard duplicate ModelAction */
-               delete act;
-               iter++;
-       } else { /* Diverging from previous execution */
-               /* Clear out remainder of list */
-               node_list_t::iterator it = iter;
-               it++;
-               clear_node_list(&node_list, it, node_list.end());
-
-               /* Record action */
-               get_head()->explore_child(act);
-               node_list.push_back(new Node(act, model->get_num_threads()));
                iter++;
+               return (*iter)->get_action();
        }
-       return (*iter)->get_action();
+
+       /* Diverging from previous execution; clear out remainder of list */
+       node_list_t::iterator it = iter;
+       it++;
+       clear_node_list(&node_list, it, node_list.end());
+
+       /* Record action */
+       get_head()->explore_child(act);
+       node_list.push_back(new Node(act, model->get_num_threads()));
+       total_nodes++;
+       iter++;
+       return NULL;
 }
 
 Node * NodeStack::get_head()
index cf3c6db146675c0cb7f41d994f988925209fc976..74ac245f3b3b00331a3328482d7c21c47bdc7cdb 100644 (file)
@@ -1,14 +1,21 @@
+/** @file nodestack.h
+ *  @brief Stack of operations for use in backtracking.
+*/
+
 #ifndef __NODESTACK_H__
 #define __NODESTACK_H__
 
 #include <list>
 #include <vector>
+#include <set>
 #include <cstddef>
 #include "threads.h"
 #include "mymemory.h"
 
 class ModelAction;
 
+typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction * > > action_set_t;
+
 class Node {
 public:
        Node(ModelAction *act = NULL, int nthreads = 1);
@@ -24,19 +31,23 @@ public:
        bool is_enabled(Thread *t);
        ModelAction * get_action() { return action; }
 
-       void print();
+       void add_read_from(ModelAction *act);
 
-       static int get_total_nodes() { return total_nodes; }
+       void print();
 
        MEMALLOC
 private:
        void explore(thread_id_t tid);
 
-       static int total_nodes;
        ModelAction *action;
        int num_threads;
        std::vector< bool, MyAlloc<bool> > explored_children;
        std::vector< bool, MyAlloc<bool> > backtrack;
+       int numBacktracks;
+
+       /** The set of ModelActions that this the action at this Node may read
+        *  from. Only meaningful if this Node represents a 'read' action. */
+       action_set_t may_read_from;
 };
 
 typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
@@ -50,12 +61,16 @@ public:
        Node * get_next();
        void reset_execution();
 
+       int get_total_nodes() { return total_nodes; }
+
        void print();
 
        MEMALLOC
 private:
        node_list_t node_list;
        node_list_t::iterator iter;
+
+       int total_nodes;
 };
 
 #endif /* __NODESTACK_H__ */
index f4965369b2a62be67a124ae29a44b4172c28f0eb..cba4b11a6d597011910ceec3a55324d5edf136f4 100644 (file)
@@ -1,3 +1,7 @@
+/** @file schedule.h
+ *     @brief Thread scheduler.
+ */
+
 #ifndef __SCHEDULE_H__
 #define __SCHEDULE_H__
 
@@ -7,6 +11,8 @@
 /* Forward declaration */
 class Thread;
 
+/** @brief The Scheduler class performs the mechanics of Thread execution
+ * scheduling. */
 class Scheduler {
 public:
        Scheduler();
index 2ef7e4ba94f9ef88b250b9dce1d5d3b3ff551efd..baedf4753a806b5ac47b8079f9227dba4bce3706 100644 (file)
 #include <cassert>
 #include <vector>
 #include <utility>
+#include <inttypes.h>
+#include "common.h"
+
 
 #define MYBINARYNAME "model"
 #define MYLIBRARYNAME "libmodel.so"
-#define PROCNAME      "/proc/*/maps"
-#define REPLACEPOS             6
-
-typedef std::basic_string<char, std::char_traits<char>, MyAlloc<char> > MyString;
+#define MAPFILE_FORMAT "/proc/%d/maps"
 
 SnapshotStack * snapshotObject;
 
-/*This looks like it might leak memory...  Subramanian should fix this. */
+#ifdef MAC
+/** The SnapshotGlobalSegments function computes the memory regions
+ *     that may contain globals and then configures the snapshotting
+ *     library to snapshot them.
+ */
+static void SnapshotGlobalSegments(){
+       int pid = getpid();
+       char buf[9000], execname[100];
+       FILE *map;
 
-typedef std::basic_stringstream< char, std::char_traits< char >, MyAlloc< char > > MyStringStream;
-std::vector< MyString, MyAlloc< MyString> > splitString( MyString input, char delim ){
-       std::vector< MyString, MyAlloc< MyString > > splits;
-       MyStringStream ss( input );     
-       MyString item;
-       while( std::getline( ss, item, delim ) ){
-               splits.push_back( item );       
+       sprintf(execname, "vmmap -interleaved %d", pid);
+       map=popen(execname, "r");
+
+       if (!map) {
+               perror("popen");
+               exit(EXIT_FAILURE);
        }
-       return splits;
-}
 
-bool checkPermissions( MyString permStr ){
-       return permStr.find("w") != MyString::npos;
-}
-static void takeSegmentSnapshot( const MyString & lineText ){
-       std::vector< MyString, MyAlloc< MyString > > firstSplit = splitString( lineText, ' ' );
-       if( checkPermissions( firstSplit[ 1 ] ) ){
-               std::vector< MyString, MyAlloc< MyString > > secondSplit = splitString( firstSplit[ 0 ], '-' );    
-               size_t val1 = 0, val2 = 0;
-               sscanf( secondSplit[ 0 ].c_str(), "%zx", &val1 );
-               sscanf( secondSplit[ 1 ].c_str(), "%zx", &val2 );
-               size_t len = ( val2 - val1 ) / PAGESIZE;    
-               if( 0 != len ){
-                       addMemoryRegionToSnapShot( ( void * )val1, len );        
+       /* Wait for correct part */
+       while (fgets(buf, sizeof(buf), map)) {
+               if (strstr(buf, "==== regions for process"))
+                       break;
+       }
+
+       while (fgets(buf, sizeof(buf), map)) {
+               char regionname[200] = "";
+               char type[23];
+               char smstr[23];
+               char r, w, x;
+               char mr, mw, mx;
+               int size;
+               void *begin, *end;
+
+               //Skip out at the end of the section
+               if (buf[0]=='\n')
+                       break;
+               
+               sscanf(buf, "%22s %p-%p [%5dK] %c%c%c/%c%c%c SM=%3s %200s\n", &type, &begin, &end, &size, &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
+
+               if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) {
+                       size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
+                       if (len != 0)
+                               addMemoryRegionToSnapShot(begin, len);
+                       DEBUG("%s\n", buf);
+                       DEBUG("%45s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p);
                }
        }
+       pclose(map);
 }
-void SnapshotGlobalSegments(){
-       MyString fn = PROCNAME;
-       static char sProcessSize[ 12 ] = { 0 };
-       std::pair< const char *, bool > dataSect[ 2 ];
-       dataSect[ 0 ] = std::make_pair( MYBINARYNAME, false );
-       dataSect[ 1 ] = std::make_pair( MYLIBRARYNAME, false );
-       static pid_t sProcID = 0;
-       if( 0 == sProcID ) {
-               sProcID = getpid();     
-               sprintf( sProcessSize, "%d", sProcID );
+#else
+/** The SnapshotGlobalSegments function computes the memory regions
+ *     that may contain globals and then configures the snapshotting
+ *     library to snapshot them.
+ */
+static void SnapshotGlobalSegments(){
+       int pid = getpid();
+       char buf[9000], filename[100];
+       FILE *map;
+
+       sprintf(filename, MAPFILE_FORMAT, pid);
+       map = fopen(filename, "r");
+       if (!map) {
+               perror("fopen");
+               exit(EXIT_FAILURE);
        }
-       fn.replace( REPLACEPOS, 1, sProcessSize );
-       std::ifstream procName( fn.c_str() );
-       if( procName.is_open() ){
-               MyString line;
-               while( procName.good() ){
-                       getline( procName, line );
-                       int i;
-                       for( i = 0; i < 2; ++i ){
-                               if( MyString::npos != line.find( dataSect[ i ].first ) ) break;                 
-                       }
-                       if( i >= 2 || dataSect[ i ].second == true ) continue;
-                       dataSect[ i ].second = true;
-                       if( !procName.good() )return;
-                       getline( procName, line );
-                       takeSegmentSnapshot( line );    
-               }       
+       while (fgets(buf, sizeof(buf), map)) {
+               char regionname[200] = "";
+               char r, w, x, p;
+               void *begin, *end;
+
+               sscanf(buf, "%p-%p %c%c%c%c %*x %*x:%*x %*u %200s\n", &begin, &end, &r, &w, &x, &p, regionname);
+               if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) {
+                       size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
+                       if (len != 0)
+                               addMemoryRegionToSnapShot(begin, len);
+                       DEBUG("%45s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p);
+               }
        }
+       fclose(map);
 }
+#endif
 
-//class definition of SnapshotStack.....
-//declaration of constructor....
 SnapshotStack::SnapshotStack(){
        SnapshotGlobalSegments();
        stack=NULL;
 }
-       
+
 SnapshotStack::~SnapshotStack(){
 }
-       
+
+
+/** This method returns to the last snapshot before the inputted
+ * sequence number.  This function must be called from the model
+ * checking thread and not from a snapshotted stack.  
+ * @param seqindex is the sequence number to rollback before.  
+ * @return is the sequence number we actually rolled back to.
+ */
+               
 int SnapshotStack::backTrackBeforeStep(int seqindex) {
        while(true) {
                if (stack->index<=seqindex) {
@@ -102,6 +131,9 @@ int SnapshotStack::backTrackBeforeStep(int seqindex) {
        }
 }
 
+/** This method takes a snapshot at the given sequence number.
+ */
+
 void SnapshotStack::snapshotStep(int seqindex) {
        struct stackEntry *tmp=(struct stackEntry *)MYMALLOC(sizeof(struct stackEntry));
        tmp->next=stack;
index e9746e1ebb35468ff20e0ea68fd9ee364a0e7cd6..5f54edb87f00f3299c20b1dc7beb9b5f4149107d 100644 (file)
@@ -1,3 +1,8 @@
+/** @file snapshot-interface.h
+ *  @brief C++ layer on top of snapshotting system.
+ */
+
+
 #ifndef __SNAPINTERFACE_H
 #define __SNAPINTERFACE_H
 #include "mymemory.h"
@@ -9,8 +14,6 @@ void initSnapShotLibrary(unsigned int numbackingpages,
                unsigned int numsnapshots, unsigned int nummemoryregions,
                unsigned int numheappages, VoidFuncPtr entryPoint);
 
-void SnapshotGlobalSegments();
-
 struct stackEntry {
   struct stackEntry *next;
   snapshot_id snapshotid;
index 7cea7d6191ca457b5c7b98cd1e45dc2c15596e22..5fb1a85ebd4c4e633e1da3812b97776a893dccd8 100644 (file)
 #include <sys/wait.h>
 #include <ucontext.h>
 
-//extern declaration definition
-#define FAILURE(mesg) { printf("failed in the API: %s with errno relative message: %s\n", mesg, strerror( errno ) ); exit( -1 ); }
+#define FAILURE(mesg) { printf("failed in the API: %s with errno relative message: %s\n", mesg, strerror( errno ) ); exit(EXIT_FAILURE); }
+
+#ifdef CONFIG_SSDEBUG
+#define SSDEBUG                printf
+#else
+#define SSDEBUG(...)   do { } while (0)
+#endif
+
+/* extern declaration definition */
 #if USE_MPROTECT_SNAPSHOT
 struct SnapShot * snapshotrecord = NULL;
-struct Snapshot_t * sTheRecord = NULL;
 #else
-struct Snapshot_t * sTheRecord = NULL;
+struct Snapshot * sTheRecord = NULL;
 #endif
-void DumpIntoLog( const char * filename, const char * message ){
-#if SSDEBUG
-       static pid_t thePID = getpid();
-       char newFn[ 1024 ] ={ 0 };
-       sprintf( newFn,"%s-%d.txt", filename, thePID );
-       FILE * myFile = fopen( newFn, "w+" );
-       fprintf( myFile, "the message %s: the process id %d\n", message, thePID );
-       fflush( myFile );
-       fclose( myFile );
-       myFile = NULL;
-#endif
-}
+
 #if !USE_MPROTECT_SNAPSHOT
 static ucontext_t savedSnapshotContext;
 static ucontext_t savedUserSnapshotContext;
 static snapshot_id snapshotid = 0;
 #endif
-/* Initialize snapshot data structure */
+
+/** PageAlignedAdressUpdate return a page aligned address for the
+ * address being added as a side effect the numBytes are also changed.
+ */
+static void * PageAlignAddressUpward(void * addr) {
+       return (void *)((((uintptr_t)addr)+PAGESIZE-1)&~(PAGESIZE-1));
+}
+
 #if USE_MPROTECT_SNAPSHOT
-void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions) {
+
+/** ReturnPageAlignedAddress returns a page aligned address for the
+ * address being added as a side effect the numBytes are also changed.
+ */
+static void * ReturnPageAlignedAddress(void * addr) {
+       return (void *)(((uintptr_t)addr)&~(PAGESIZE-1));
+}
+
+/** The initSnapShotRecord method initialized the snapshotting data
+ *  structures for the mprotect based snapshot. 
+ */
+static void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions) {
        snapshotrecord=( struct SnapShot * )MYMALLOC(sizeof(struct SnapShot));
        snapshotrecord->regionsToSnapShot=( struct MemoryRegion * )MYMALLOC(sizeof(struct MemoryRegion)*nummemoryregions);
        snapshotrecord->backingStoreBasePtr= ( struct SnapShotPage * )MYMALLOC( sizeof( struct SnapShotPage ) * (numbackingpages + 1) );
@@ -59,15 +72,17 @@ void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots,
        snapshotrecord->maxBackingPages=numbackingpages;
        snapshotrecord->maxSnapShots=numsnapshots;
 }
-#endif //nothing to initialize for the fork based snapshotting.
 
-void HandlePF( int sig, siginfo_t *si, void * unused){
-#if USE_MPROTECT_SNAPSHOT
+/** HandlePF is the page fault handler for mprotect based snapshotting
+ * algorithm.
+ */
+static void HandlePF( int sig, siginfo_t *si, void * unused){
        if( si->si_code == SEGV_MAPERR ){
                printf("Real Fault at %p\n", si->si_addr);
                exit( EXIT_FAILURE );
        }
        void* addr = ReturnPageAlignedAddress(si->si_addr);
+
        unsigned int backingpage=snapshotrecord->lastBackingPage++; //Could run out of pages...
        if (backingpage==snapshotrecord->maxBackingPages) {
                printf("Out of backing pages at %p\n", si->si_addr);
@@ -83,43 +98,34 @@ void HandlePF( int sig, siginfo_t *si, void * unused){
                perror("mprotect");
                // Handle error by quitting?
        }
-#endif //nothing to handle for non snapshotting case.
-}
-
-//Return a page aligned address for the address being added
-//as a side effect the numBytes are also changed.
-void * ReturnPageAlignedAddress(void * addr) {
-       return (void *)(((uintptr_t)addr)&~(PAGESIZE-1));
 }
+#endif //nothing to handle for non snapshotting case.
 
-//Return a page aligned address for the address being added
-//as a side effect the numBytes are also changed.
-void * PageAlignAddressUpward(void * addr) {
-       return (void *)((((uintptr_t)addr)+PAGESIZE-1)&~(PAGESIZE-1));
-}
-#ifdef __cplusplus
-extern "C" {
-#endif
-       void createSharedLibrary(){
+void createSharedLibrary(){
 #if !USE_MPROTECT_SNAPSHOT
-               //step 1. create shared memory.
-               if( sTheRecord ) return;
-               int fd = shm_open( "/ModelChecker-Snapshotter", O_RDWR | O_CREAT, 0777 ); //universal permissions.
-               if( -1 == fd ) FAILURE("shm_open");
-               if( -1 == ftruncate( fd, ( size_t )SHARED_MEMORY_DEFAULT + ( size_t )STACK_SIZE_DEFAULT ) ) FAILURE( "ftruncate" );
-               char * memMapBase = ( char * ) mmap( 0, ( size_t )SHARED_MEMORY_DEFAULT + ( size_t )STACK_SIZE_DEFAULT, PROT_READ | PROT_WRITE, MAP_SHARED, fd, 0 );
-               if( MAP_FAILED == memMapBase ) FAILURE("mmap");
-               sTheRecord = ( struct Snapshot_t * )memMapBase;
-               sTheRecord->mSharedMemoryBase = memMapBase + sizeof( struct Snapshot_t );
-               sTheRecord->mStackBase = ( char * )memMapBase + ( size_t )SHARED_MEMORY_DEFAULT;
-               sTheRecord->mStackSize = STACK_SIZE_DEFAULT;
-               sTheRecord->mIDToRollback = -1;
-               sTheRecord->currSnapShotID = 0;
+       //step 1. create shared memory.
+       if ( sTheRecord )
+               return;
+       int fd = shm_open( "/ModelChecker-Snapshotter", O_RDWR | O_CREAT, 0777 ); //universal permissions.
+       if ( -1 == fd )
+               FAILURE("shm_open");
+       if ( -1 == ftruncate( fd, SHARED_MEMORY_DEFAULT + STACK_SIZE_DEFAULT ) )
+               FAILURE( "ftruncate" );
+       void * memMapBase = mmap( 0, SHARED_MEMORY_DEFAULT + STACK_SIZE_DEFAULT, PROT_READ | PROT_WRITE, MAP_SHARED, fd, 0 );
+       if( MAP_FAILED == memMapBase )
+               FAILURE("mmap");
+       sTheRecord = ( struct Snapshot * )memMapBase;
+       sTheRecord->mSharedMemoryBase = (void *)((uintptr_t)memMapBase + sizeof(struct Snapshot));
+       sTheRecord->mStackBase = (void *)((uintptr_t)memMapBase + SHARED_MEMORY_DEFAULT);
+       sTheRecord->mStackSize = STACK_SIZE_DEFAULT;
+       sTheRecord->mIDToRollback = -1;
+       sTheRecord->currSnapShotID = 0;
 #endif
-       }
-#ifdef __cplusplus
 }
-#endif
+
+/** The initSnapShotLibrary function initializes the Snapshot library.
+ *  @param entryPoint the function that should run the program.
+ */
 void initSnapShotLibrary(unsigned int numbackingpages,
                unsigned int numsnapshots, unsigned int nummemoryregions,
                unsigned int numheappages, VoidFuncPtr entryPoint) {
@@ -135,50 +141,56 @@ void initSnapShotLibrary(unsigned int numbackingpages,
        sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
        sigemptyset( &sa.sa_mask );
        sa.sa_sigaction = HandlePF;
+#ifdef MAC
+       if( sigaction( SIGBUS, &sa, NULL ) == -1 ){
+               printf("SIGACTION CANNOT BE INSTALLED\n");
+               exit(EXIT_FAILURE);
+       }
+#endif
        if( sigaction( SIGSEGV, &sa, NULL ) == -1 ){
                printf("SIGACTION CANNOT BE INSTALLED\n");
-               exit(-1);
+               exit(EXIT_FAILURE);
        }
+
        initSnapShotRecord(numbackingpages, numsnapshots, nummemoryregions);
 
+       // EVIL HACK: We need to make sure that calls into the HandlePF method don't cause dynamic links
+       // The problem is that we end up protecting state in the dynamic linker...
+       // Solution is to call our signal handler before we start protecting stuff...
+
+       siginfo_t si;
+       memset(&si, 0, sizeof(si));
+       si.si_addr=ss.ss_sp;
+       HandlePF(SIGSEGV, &si, NULL);
+       snapshotrecord->lastBackingPage--; //remove the fake page we copied
+
        basemySpace=MYMALLOC((numheappages+1)*PAGESIZE);
        void * pagealignedbase=PageAlignAddressUpward(basemySpace);
        mySpace = create_mspace_with_base(pagealignedbase,  numheappages*PAGESIZE, 1 );
        addMemoryRegionToSnapShot(pagealignedbase, numheappages);
        entryPoint();
 #else
-       //add a signal to indicate that the process is going to terminate.
-       struct sigaction sa;
-       sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART;
-       sigemptyset( &sa.sa_mask );
-       sa.sa_sigaction = HandlePF;
-       if( sigaction( SIGUSR1, &sa, NULL ) == -1 ){
-               printf("SIGACTION CANNOT BE INSTALLED\n");
-               exit(-1);
-       }
+
+       basemySpace=system_malloc((numheappages+1)*PAGESIZE);
+       void * pagealignedbase=PageAlignAddressUpward(basemySpace);
+       mySpace = create_mspace_with_base(pagealignedbase,  numheappages*PAGESIZE, 1 );
        createSharedLibrary();
 
        //step 2 setup the stack context.
-
-       int alreadySwapped = 0;
-       getcontext( &savedSnapshotContext );
-       if( !alreadySwapped ){
-               alreadySwapped = 1;
-               ucontext_t currentContext, swappedContext, newContext;
-               getcontext( &newContext );
-               newContext.uc_stack.ss_sp = sTheRecord->mStackBase;
-               newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
-               newContext.uc_link = &currentContext;
-               makecontext( &newContext, entryPoint, 0 );
-               swapcontext( &swappedContext, &newContext );
-       }
+       ucontext_t newContext;
+       getcontext( &newContext );
+       newContext.uc_stack.ss_sp = sTheRecord->mStackBase;
+       newContext.uc_stack.ss_size = STACK_SIZE_DEFAULT;
+       makecontext( &newContext, entryPoint, 0 );
+       /* switch to a new entryPoint context, on a new stack */
+       swapcontext(&savedSnapshotContext, &newContext);
 
        //add the code to take a snapshot here...
        //to return to user process, do a second swapcontext...
        pid_t forkedID = 0;
        snapshotid = sTheRecord->currSnapShotID;
        bool swapContext = false;
-       while( !sTheRecord->mbFinalize ){
+       while( true ){
                sTheRecord->currSnapShotID=snapshotid+1;
                forkedID = fork();
                if( 0 == forkedID ){
@@ -195,17 +207,16 @@ void initSnapShotLibrary(unsigned int numbackingpages,
                } else {
                        int status;
                        int retVal;
-#if SSDEBUG
-                       char mesg[ 1024 ] = { 0 };
-                       sprintf( mesg, "The process id of child is %d and the process id of this process is %d and snapshot id is %d", forkedID, getpid(), snapshotid );
-                       DumpIntoLog( "ModelSnapshot", mesg );
-#endif
+
+                       SSDEBUG("The process id of child is %d and the process id of this process is %d and snapshot id is %d",
+                               forkedID, getpid(), snapshotid );
+
                        do {
                                retVal=waitpid( forkedID, &status, 0 );
                        } while( -1 == retVal && errno == EINTR );
 
                        if( sTheRecord->mIDToRollback != snapshotid )
-                               exit(0);
+                               exit(EXIT_SUCCESS);
                        else{
                                swapContext = true;
                        }
@@ -214,33 +225,38 @@ void initSnapShotLibrary(unsigned int numbackingpages,
 
 #endif
 }
-/* This function assumes that addr is page aligned */
+
+/** The addMemoryRegionToSnapShot function assumes that addr is page aligned. 
+ */
 void addMemoryRegionToSnapShot( void * addr, unsigned int numPages) {
 #if USE_MPROTECT_SNAPSHOT
        unsigned int memoryregion=snapshotrecord->lastRegion++;
        if (memoryregion==snapshotrecord->maxRegions) {
                printf("Exceeded supported number of memory regions!\n");
-               exit(-1);
+               exit(EXIT_FAILURE);
        }
 
        snapshotrecord->regionsToSnapShot[ memoryregion ].basePtr=addr;
        snapshotrecord->regionsToSnapShot[ memoryregion ].sizeInPages=numPages;
 #endif //NOT REQUIRED IN THE CASE OF FORK BASED SNAPSHOTS.
 }
-//take snapshot
+
+/** The takeSnapshot function takes a snapshot.
+ * @return The snapshot identifier.
+ */
 snapshot_id takeSnapshot( ){
 #if USE_MPROTECT_SNAPSHOT
        for(unsigned int region=0; region<snapshotrecord->lastRegion;region++) {
                if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ ) == -1 ){
                        perror("mprotect");
                        printf("Failed to mprotect inside of takeSnapShot\n");
-                       exit(-1);
+                       exit(EXIT_FAILURE);
                }
        }
        unsigned int snapshot=snapshotrecord->lastSnapShot++;
        if (snapshot==snapshotrecord->maxSnapShots) {
                printf("Out of snapshots\n");
-               exit(-1);
+               exit(EXIT_FAILURE);
        }
        snapshotrecord->snapShots[snapshot].firstBackingPage=snapshotrecord->lastBackingPage;
 
@@ -250,6 +266,10 @@ snapshot_id takeSnapshot( ){
        return snapshotid;
 #endif
 }
+
+/** The rollBack function rollback to the given snapshot identifier.
+ *  @param theID is the snapshot identifier to rollback to.
+ */
 void rollBack( snapshot_id theID ){
 #if USE_MPROTECT_SNAPSHOT
        std::map< void *, bool, std::less< void * >, MyAlloc< std::pair< const void *, bool > > > duplicateMap;
@@ -257,7 +277,7 @@ void rollBack( snapshot_id theID ){
                if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ | PROT_WRITE ) == -1 ){
                        perror("mprotect");
                        printf("Failed to mprotect inside of takeSnapShot\n");
-                       exit(-1);
+                       exit(EXIT_FAILURE);
                }
        }
        for(unsigned int page=snapshotrecord->snapShots[theID].firstBackingPage; page<snapshotrecord->lastBackingPage; page++) {
@@ -281,17 +301,10 @@ void rollBack( snapshot_id theID ){
        getcontext( &sTheRecord->mContextToRollback );
        if( !sTemp ){
                sTemp = 1;
-#if SSDEBUG
-               DumpIntoLog( "ModelSnapshot", "Invoked rollback" );
-#endif
-               exit( 0 );
+               SSDEBUG("Invoked rollback");
+               exit(EXIT_SUCCESS);
        }
-#endif
-}
-
-void finalize(){
-#if !USE_MPROTECT_SNAPSHOT
-       sTheRecord->mbFinalize = true;
+       sTheRecord->mIDToRollback = -1;
 #endif
 }
 
index 39e294a8c60f1c0d781fdafb43a6162b6475f1af..cbbe0070fb92328f6690ba604cebbb19f8466fce 100644 (file)
@@ -1,3 +1,7 @@
+/** @file snapshot.h
+ *     @brief Snapshotting interface header file.
+ */
+
 #ifndef _SNAPSHOT_H
 #define _SNAPSHOT_H
 
@@ -10,7 +14,7 @@
 #define USE_MPROTECT_SNAPSHOT 1
 
 /* Size of signal stack */
-#define SIGSTACKSIZE 16384
+#define SIGSTACKSIZE 32768
 
 void addMemoryRegionToSnapShot( void * ptr, unsigned int numPages );
 
@@ -18,13 +22,6 @@ snapshot_id takeSnapshot( );
 
 void rollBack( snapshot_id theSnapShot );
 
-void finalize();
-
-#ifdef __cplusplus
-extern "C" {
-#endif
 void createSharedLibrary();
-#ifdef __cplusplus
-};  /* end of extern "C" */
-#endif
+
 #endif
index 8d935f238b81e3d43cf5ea1d7fdac07f583bc470..e9f6d8bd50a4ab1493a8d0264c275fdfeade3b8b 100644 (file)
@@ -1,3 +1,7 @@
+/** @file snapshotimp.h
+ *     @brief Snapshotting implementation header file..
+ */
+
 #ifndef _SNAPSHOTIMP_H
 #define _SNAPSHOTIMP_H
 #include "snapshot.h"
 #include <sys/mman.h>
 #include <sys/types.h>
 #include <csignal>
-#define SHARED_MEMORY_DEFAULT ( 100 * ( 1 << 20 ) ) // 100mb for the shared memory
-#define STACK_SIZE_DEFAULT  ( ( 1 << 20 ) * 20 ) //20 mb out of the above 100 mb for my stack.
+#define SHARED_MEMORY_DEFAULT  (100 * ((size_t)1 << 20)) // 100mb for the shared memory
+#define STACK_SIZE_DEFAULT      (((size_t)1 << 20) * 20)  // 20 mb out of the above 100 mb for my stack
 
 #if USE_MPROTECT_SNAPSHOT
 //Each snapshotrecord lists the firstbackingpage that must be written to revert to that snapshot
 struct SnapShotRecord {
-  unsigned int firstBackingPage;
+       unsigned int firstBackingPage;
 };
 
 //Backing store page struct
 struct SnapShotPage {
-  char data[PAGESIZE];
+       char data[PAGESIZE];
 };
 
 //List the base address of the corresponding page in the backing store so we know where to copy it to
 struct BackingPageRecord {
-  void * basePtrOfPage;
+       void * basePtrOfPage;
 };
 
 //Stuct for each memory region
 struct MemoryRegion {
-  void * basePtr; //base of memory region
-  int sizeInPages; //size of memory region in pages
+       void * basePtr; //base of memory region
+       int sizeInPages; //size of memory region in pages
 };
 
 //Primary struct for snapshotting system....
 struct SnapShot {
-  struct MemoryRegion * regionsToSnapShot; //This pointer references an array of memory regions to snapshot
-  struct SnapShotPage * backingStore; //This pointer references an array of snapshotpage's that form the backing store
-  void * backingStoreBasePtr; //This pointer references an array of snapshotpage's that form the backing store
-  struct BackingPageRecord * backingRecords; //This pointer references an array of backingpagerecord's (same number of elements as backingstore
-  struct SnapShotRecord * snapShots; //This pointer references the snapshot array
-  
-  unsigned int lastSnapShot; //Stores the next snapshot record we should use
-  unsigned int lastBackingPage; //Stores the next backingpage we should use
-  unsigned int lastRegion; //Stores the next memory region to be used
+       struct MemoryRegion * regionsToSnapShot; //This pointer references an array of memory regions to snapshot
+       struct SnapShotPage * backingStore; //This pointer references an array of snapshotpage's that form the backing store
+       void * backingStoreBasePtr; //This pointer references an array of snapshotpage's that form the backing store
+       struct BackingPageRecord * backingRecords; //This pointer references an array of backingpagerecord's (same number of elements as backingstore
+       struct SnapShotRecord * snapShots; //This pointer references the snapshot array
+
+       unsigned int lastSnapShot; //Stores the next snapshot record we should use
+       unsigned int lastBackingPage; //Stores the next backingpage we should use
+       unsigned int lastRegion; //Stores the next memory region to be used
 
-  unsigned int maxRegions; //Stores the max number of memory regions we support
-  unsigned int maxBackingPages; //Stores the total number of backing pages
-  unsigned int maxSnapShots; //Stores the total number of snapshots we allow
+       unsigned int maxRegions; //Stores the max number of memory regions we support
+       unsigned int maxBackingPages; //Stores the total number of backing pages
+       unsigned int maxSnapShots; //Stores the total number of snapshots we allow
 };
 
 //Global reference to snapshot data structure
 extern struct SnapShot * snapshotrecord;
-void * ReturnPageAlignedAddress( void *);
-void * PageAlignAddressUpward( void *);
 #else
-struct Snapshot_t{
-char *mSharedMemoryBase;
-char *mStackBase;
-size_t mStackSize;
-snapshot_id mIDToRollback;
-ucontext_t mContextToRollback;
-snapshot_id currSnapShotID;
-volatile bool mbFinalize;
+struct Snapshot {
+       void *mSharedMemoryBase;
+       void *mStackBase;
+       size_t mStackSize;
+       snapshot_id mIDToRollback;
+       ucontext_t mContextToRollback;
+       snapshot_id currSnapShotID;
 };
-extern struct Snapshot_t * sTheRecord;
+extern struct Snapshot * sTheRecord;
 #endif
 #endif
index 7d2189b49d9f098a775b1cc158390cf76f49cbf4..a97a04c704449963981fe443a711c64abc716fb3 100644 (file)
--- a/threads.h
+++ b/threads.h
@@ -1,3 +1,7 @@
+/** @file threads.h
+ *  @brief Model Checker Thread class.
+ */
+
 #ifndef __THREADS_H__
 #define __THREADS_H__
 
@@ -18,6 +22,7 @@ typedef enum thread_state {
 
 class ModelAction;
 
+/** @brief A Thread is created for each user-space thread */
 class Thread {
 public:
        Thread(thrd_t *t, void (*func)(void *), void *a);
index 2854ddc4a6b73bdf366b63262ed63ff3c8911eff..33319b1ce873c891b4bce429790196280b3acc12 100644 (file)
@@ -1,4 +1,5 @@
 #include <stdio.h>
+#include <stdlib.h>
 
 #include "libthreads.h"
 #include "libatomic.h"
@@ -30,15 +31,18 @@ static void a(atomic_int *obj)
 void user_main()
 {
        thrd_t t1, t2;
-       atomic_int obj;
+       atomic_int *obj;
 
-       atomic_init(&obj, 0);
+       obj = malloc(sizeof(*obj));
+
+       atomic_init(obj, 0);
 
        printf("Thread %d: creating 2 threads\n", thrd_current());
-       thrd_create(&t1, (thrd_start_t)&a, &obj);
-       thrd_create(&t2, (thrd_start_t)&a, &obj);
+       thrd_create(&t1, (thrd_start_t)&a, obj);
+       thrd_create(&t2, (thrd_start_t)&a, obj);
 
        thrd_join(t1);
        thrd_join(t2);
+       free(obj);
        printf("Thread %d is finished\n", thrd_current());
 }