Commit state of repository at time of OOPSLA 2015 submission.
authorbdemsky <bdemsky@uci.edu>
Fri, 21 Aug 2015 18:40:52 +0000 (11:40 -0700)
committerbdemsky <bdemsky@uci.edu>
Fri, 4 Sep 2015 05:16:42 +0000 (22:16 -0700)
279 files changed:
.dir-locals.el [new file with mode: 0644]
.gitignore [new file with mode: 0644]
COPYING [new file with mode: 0644]
DEBUGGINGNOTES.txt [new file with mode: 0644]
Doxyfile [new file with mode: 0644]
Makefile [new file with mode: 0644]
benchmarks/.gitignore [new file with mode: 0644]
benchmarks/cdschecker/dekker/bench.sh [new file with mode: 0755]
benchmarks/cdschecker/dekker/dekker-fences.cc.in [new file with mode: 0644]
benchmarks/cdschecker/linuxlock/bench.sh [new file with mode: 0755]
benchmarks/cdschecker/linuxlock/linuxlocks.c.in [new file with mode: 0644]
benchmarks/cdschecker/linuxrwlock/bench.sh [new file with mode: 0755]
benchmarks/cdschecker/linuxrwlock/linuxrwlocks.c.in [new file with mode: 0644]
benchmarks/cdschecker/msqueue/bench.sh [new file with mode: 0755]
benchmarks/cdschecker/msqueue/ms-queue_simple.c.in [new file with mode: 0644]
benchmarks/cdschecker/msqueue/ms-queue_simple.h [new file with mode: 0644]
benchmarks/cdschecker/path.sh [new file with mode: 0755]
benchmarks/cdschecker/seqlock/bench.sh [new file with mode: 0755]
benchmarks/cdschecker/seqlock/seqlock.c.in [new file with mode: 0644]
benchmarks/checkfence/dekker/bench.sh [new file with mode: 0755]
benchmarks/checkfence/dekker/clean.sh [new file with mode: 0755]
benchmarks/checkfence/dekker/dekker-fences.c.in [new file with mode: 0644]
benchmarks/checkfence/dekker/dekkertests.lsl [new file with mode: 0644]
benchmarks/checkfence/linuxlock/bench.sh [new file with mode: 0755]
benchmarks/checkfence/linuxlock/clean.sh [new file with mode: 0755]
benchmarks/checkfence/linuxlock/lin_harness.c [new file with mode: 0755]
benchmarks/checkfence/linuxlock/linuxrwlocksbig.c.in [new file with mode: 0644]
benchmarks/checkfence/linuxlock/locktests.lsl [new file with mode: 0644]
benchmarks/checkfence/linuxrwlock/add_harness.c [new file with mode: 0755]
benchmarks/checkfence/linuxrwlock/bench.sh [new file with mode: 0755]
benchmarks/checkfence/linuxrwlock/clean.sh [new file with mode: 0755]
benchmarks/checkfence/linuxrwlock/llock.c.in [new file with mode: 0644]
benchmarks/checkfence/linuxrwlock/locktests.lsl [new file with mode: 0644]
benchmarks/checkfence/msqueue/bench.sh [new file with mode: 0755]
benchmarks/checkfence/msqueue/clean.sh [new file with mode: 0755]
benchmarks/checkfence/msqueue/msn.c [new file with mode: 0755]
benchmarks/checkfence/msqueue/msn_harness.c.in [new file with mode: 0755]
benchmarks/checkfence/msqueue/tests.lsl [new file with mode: 0644]
benchmarks/checkfence/paths.sh [new file with mode: 0644]
benchmarks/checkfence/seqlock/bench.sh [new file with mode: 0755]
benchmarks/checkfence/seqlock/clean.sh [new file with mode: 0755]
benchmarks/checkfence/seqlock/seqlock.c.in [new file with mode: 0644]
benchmarks/checkfence/seqlock/seqtests.lsl [new file with mode: 0644]
benchmarks/compilesat [new file with mode: 0755]
benchmarks/nidhugg/dekker/bench.sh [new file with mode: 0755]
benchmarks/nidhugg/dekker/benchtso.sh [new file with mode: 0755]
benchmarks/nidhugg/dekker/dekker-fences.cc.in [new file with mode: 0644]
benchmarks/nidhugg/linuxlock/bench.sh [new file with mode: 0755]
benchmarks/nidhugg/linuxlock/benchtso.sh [new file with mode: 0755]
benchmarks/nidhugg/linuxlock/linuxlocks.c.in [new file with mode: 0644]
benchmarks/nidhugg/linuxrwlock/bench.sh [new file with mode: 0755]
benchmarks/nidhugg/linuxrwlock/benchtso.sh [new file with mode: 0755]
benchmarks/nidhugg/linuxrwlock/linuxrwlocks.c.in [new file with mode: 0644]
benchmarks/nidhugg/msqueue/bench.sh [new file with mode: 0755]
benchmarks/nidhugg/msqueue/benchtso.sh [new file with mode: 0755]
benchmarks/nidhugg/msqueue/ms-queue_simple.c.in [new file with mode: 0644]
benchmarks/nidhugg/msqueue/ms-queue_simple.h [new file with mode: 0644]
benchmarks/nidhugg/path.sh [new file with mode: 0755]
benchmarks/nidhugg/seqlock/bench.sh [new file with mode: 0755]
benchmarks/nidhugg/seqlock/benchtso.sh [new file with mode: 0755]
benchmarks/nidhugg/seqlock/seqlock.c.in [new file with mode: 0644]
benchmarks/nidhugg/transform.java [new file with mode: 0644]
benchmarks/runcds [new file with mode: 0755]
benchmarks/runcf [new file with mode: 0755]
benchmarks/runnidd [new file with mode: 0755]
benchmarks/runsat [new file with mode: 0755]
benchmarks/runtsosat [new file with mode: 0755]
benchmarks/satcheck-precompiled/dekker/.gitignore [new file with mode: 0644]
benchmarks/satcheck-precompiled/dekker/bench.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/dekker/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck-precompiled/dekker/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/dekker/clean.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/dekker/dekker-fences.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/dekker/diff.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxlock/.gitignore [new file with mode: 0644]
benchmarks/satcheck-precompiled/linuxlock/bench.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxlock/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck-precompiled/linuxlock/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxlock/clean.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxlock/diff.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/linuxlock/linuxlocks_unannotated.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/linuxrwlock/.gitignore [new file with mode: 0644]
benchmarks/satcheck-precompiled/linuxrwlock/bench.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxrwlock/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck-precompiled/linuxrwlock/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxrwlock/clean.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxrwlock/diff.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks_unannotated.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/msqueueoffset/.gitignore [new file with mode: 0644]
benchmarks/satcheck-precompiled/msqueueoffset/bench.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/msqueueoffset/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck-precompiled/msqueueoffset/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/msqueueoffset/clean.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/msqueueoffset/diff.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.h [new file with mode: 0644]
benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple_unannotated.c [new file with mode: 0644]
benchmarks/satcheck-precompiled/seqlock/.gitignore [new file with mode: 0644]
benchmarks/satcheck-precompiled/seqlock/bench.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/seqlock/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck-precompiled/seqlock/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/seqlock/clean.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/seqlock/diff.sh [new file with mode: 0755]
benchmarks/satcheck-precompiled/seqlock/seqlock.cc [new file with mode: 0644]
benchmarks/satcheck-precompiled/seqlock/seqlock_unannotated.cc [new file with mode: 0644]
benchmarks/satcheck/dekker/.gitignore [new file with mode: 0644]
benchmarks/satcheck/dekker/bench.sh [new file with mode: 0755]
benchmarks/satcheck/dekker/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck/dekker/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck/dekker/clean.sh [new file with mode: 0755]
benchmarks/satcheck/dekker/compile.sh [new file with mode: 0755]
benchmarks/satcheck/dekker/dekker-fences_unannotated.c [new file with mode: 0644]
benchmarks/satcheck/dekker/diff.sh [new file with mode: 0755]
benchmarks/satcheck/linuxlock/.gitignore [new file with mode: 0644]
benchmarks/satcheck/linuxlock/bench.sh [new file with mode: 0755]
benchmarks/satcheck/linuxlock/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck/linuxlock/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck/linuxlock/clean.sh [new file with mode: 0755]
benchmarks/satcheck/linuxlock/compile.sh [new file with mode: 0755]
benchmarks/satcheck/linuxlock/diff.sh [new file with mode: 0755]
benchmarks/satcheck/linuxlock/linuxlocks_unannotated.c [new file with mode: 0644]
benchmarks/satcheck/linuxrwlock/.gitignore [new file with mode: 0644]
benchmarks/satcheck/linuxrwlock/bench.sh [new file with mode: 0755]
benchmarks/satcheck/linuxrwlock/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck/linuxrwlock/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck/linuxrwlock/clean.sh [new file with mode: 0755]
benchmarks/satcheck/linuxrwlock/compile.sh [new file with mode: 0755]
benchmarks/satcheck/linuxrwlock/diff.sh [new file with mode: 0755]
benchmarks/satcheck/linuxrwlock/linuxrwlocks_unannotated.c [new file with mode: 0644]
benchmarks/satcheck/msqueueoffset/.gitignore [new file with mode: 0644]
benchmarks/satcheck/msqueueoffset/bench.sh [new file with mode: 0755]
benchmarks/satcheck/msqueueoffset/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck/msqueueoffset/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck/msqueueoffset/clean.sh [new file with mode: 0755]
benchmarks/satcheck/msqueueoffset/compile.sh [new file with mode: 0755]
benchmarks/satcheck/msqueueoffset/diff.sh [new file with mode: 0755]
benchmarks/satcheck/msqueueoffset/ms-queue-simple.h [new file with mode: 0644]
benchmarks/satcheck/msqueueoffset/ms-queue-simple_unannotated.c [new file with mode: 0644]
benchmarks/satcheck/seqlock/.gitignore [new file with mode: 0644]
benchmarks/satcheck/seqlock/bench.sh [new file with mode: 0755]
benchmarks/satcheck/seqlock/benchmark-config.sh [new file with mode: 0644]
benchmarks/satcheck/seqlock/benchtso.sh [new file with mode: 0755]
benchmarks/satcheck/seqlock/clean.sh [new file with mode: 0755]
benchmarks/satcheck/seqlock/compile.sh [new file with mode: 0755]
benchmarks/satcheck/seqlock/diff.sh [new file with mode: 0755]
benchmarks/satcheck/seqlock/seqlock_unannotated.cc [new file with mode: 0644]
benchmarks/verifycompilesat [new file with mode: 0755]
bin/annotate [new file with mode: 0755]
branchrecord.cc [new file with mode: 0644]
branchrecord.h [new file with mode: 0644]
cgoal.cc [new file with mode: 0644]
cgoal.h [new file with mode: 0644]
change.cc [new file with mode: 0644]
change.h [new file with mode: 0644]
clang/.gitignore [new file with mode: 0644]
clang/COPYING [new file with mode: 0644]
clang/Makefile [new file with mode: 0644]
clang/README.md [new file with mode: 0644]
clang/multi-dep.txt [new file with mode: 0644]
clang/src/add_mc2_annotations.cpp [new file with mode: 0644]
clang/test/apr_1_unannotated.c [new file with mode: 0644]
clang/test/apr_2_unannotated.c [new file with mode: 0644]
clang/test/bitops.c [new file with mode: 0644]
clang/test/bitops_unannotated.c [new file with mode: 0644]
clang/test/linuxrwlocks.c [new file with mode: 0644]
clang/test/linuxrwlocks_unannotated.c [new file with mode: 0644]
clang/test/mcs-lock_unannotated.cc [new file with mode: 0644]
clang/test/minimal-no-braces-if.c [new file with mode: 0644]
clang/test/minimal-no-braces-if_unannotated.c [new file with mode: 0644]
clang/test/ms-queue-simple-offset.c [new file with mode: 0644]
clang/test/ms-queue-simple-offset_unannotated.c [new file with mode: 0644]
clang/test/ms-queue-simple.c [new file with mode: 0644]
clang/test/ms-queue-simple.h [new file with mode: 0644]
clang/test/ms-queue-simple_manual.c [new file with mode: 0644]
clang/test/ms-queue-simple_unannotated.c [new file with mode: 0644]
clang/test/ms-queue_unannotated.c [new file with mode: 0644]
clang/test/seqlock.c [new file with mode: 0644]
clang/test/seqlock_raw_unannotated.c [new file with mode: 0644]
clang/test/seqlock_unannotated.c [new file with mode: 0644]
clang/test/spsc-queue_unannotated.cc [new file with mode: 0644]
clang/test/userprog2_unannotated.c [new file with mode: 0644]
clang/test/userprog_unannotated.c [new file with mode: 0644]
clang/test/various-loads.c [new file with mode: 0644]
clang/test/various-loads_unannotated.c [new file with mode: 0644]
classlist.h [new file with mode: 0644]
cmodelint.cc [new file with mode: 0644]
common.cc [new file with mode: 0644]
common.h [new file with mode: 0644]
common.mk [new file with mode: 0644]
config.h [new file with mode: 0644]
constgen.cc [new file with mode: 0644]
constgen.h [new file with mode: 0644]
constraint.cc [new file with mode: 0644]
constraint.h [new file with mode: 0644]
context.cc [new file with mode: 0644]
context.h [new file with mode: 0644]
eprecord.cc [new file with mode: 0644]
eprecord.h [new file with mode: 0644]
epvalue.cc [new file with mode: 0644]
epvalue.h [new file with mode: 0644]
equalsrecord.cc [new file with mode: 0644]
equalsrecord.h [new file with mode: 0644]
execpoint.cc [new file with mode: 0644]
execpoint.h [new file with mode: 0644]
functionrecord.cc [new file with mode: 0644]
functionrecord.h [new file with mode: 0644]
hashset.h [new file with mode: 0644]
hashtable.h [new file with mode: 0644]
inc_solver.cc [new file with mode: 0644]
inc_solver.h [new file with mode: 0644]
include/atomic [new file with mode: 0644]
include/cmodelint.h [new file with mode: 0644]
include/condition_variable [new file with mode: 0644]
include/cstdatomic [new file with mode: 0644]
include/impatomic.h [new file with mode: 0644]
include/libinterface.h [new file with mode: 0644]
include/memoryorder.h [new file with mode: 0644]
include/model-assert.h [new file with mode: 0644]
include/modeltypes.h [new file with mode: 0644]
include/mutex [new file with mode: 0644]
include/stdatomic.h [new file with mode: 0644]
include/threads.h [new file with mode: 0644]
libinterface.cc [new file with mode: 0644]
libthreads.cc [new file with mode: 0644]
loadrf.cc [new file with mode: 0644]
loadrf.h [new file with mode: 0644]
main.cc [new file with mode: 0644]
malloc.c [new file with mode: 0644]
mcexecution.cc [new file with mode: 0644]
mcexecution.h [new file with mode: 0644]
mcschedule.cc [new file with mode: 0644]
mcschedule.h [new file with mode: 0644]
mcutil.h [new file with mode: 0644]
model.cc [new file with mode: 0644]
model.h [new file with mode: 0644]
mymemory.cc [new file with mode: 0644]
mymemory.h [new file with mode: 0644]
notes [new file with mode: 0644]
output.h [new file with mode: 0644]
params.h [new file with mode: 0644]
planner.cc [new file with mode: 0644]
planner.h [new file with mode: 0644]
run.sh [new file with mode: 0755]
schedulebuilder.cc [new file with mode: 0644]
schedulebuilder.h [new file with mode: 0644]
snapshot-interface.cc [new file with mode: 0644]
snapshot-interface.h [new file with mode: 0644]
snapshot.cc [new file with mode: 0644]
snapshot.h [new file with mode: 0644]
solver_interface.h [new file with mode: 0644]
stacktrace.h [new file with mode: 0644]
stl-model.h [new file with mode: 0644]
storeloadset.cc [new file with mode: 0644]
storeloadset.h [new file with mode: 0644]
test/Makefile [new file with mode: 0644]
test/dekker-fences.c [new file with mode: 0644]
test/function_microbenchmarks.c [new file with mode: 0644]
test/linuxlock.c [new file with mode: 0644]
test/load_in_if_cond.c [new file with mode: 0644]
test/mcs-lock.cc [new file with mode: 0644]
test/ms-queue-freelist.c [new file with mode: 0644]
test/ms-queue-freelist.h [new file with mode: 0644]
test/ms-queue.c [new file with mode: 0644]
test/ms-queue.h [new file with mode: 0644]
test/reference/README.md [new file with mode: 0644]
test/reference/ms-queue-atomics.c [new file with mode: 0644]
test/seqlock.c [new file with mode: 0644]
test/seqlock2.cc [new file with mode: 0644]
test/spsc-queue.cc [new file with mode: 0644]
test/userprog.c [new file with mode: 0644]
test/userprog2.c [new file with mode: 0644]
test/userprog_pointers.c [new file with mode: 0644]
threads-model.h [new file with mode: 0644]
threads.cc [new file with mode: 0644]
valuerecord.cc [new file with mode: 0644]
valuerecord.h [new file with mode: 0644]

diff --git a/.dir-locals.el b/.dir-locals.el
new file mode 100644 (file)
index 0000000..ce85e5f
--- /dev/null
@@ -0,0 +1 @@
+((nil . ((indent-tabs-mode . t))))
\ No newline at end of file
diff --git a/.gitignore b/.gitignore
new file mode 100644 (file)
index 0000000..293af41
--- /dev/null
@@ -0,0 +1,14 @@
+# generic types
+*.o
+*.swp
+*.swo
+*.so
+*~
+*.dot
+.*.d
+*.pdf
+
+# files in this directory
+/tags
+/doc/docs
+/README.html
diff --git a/COPYING b/COPYING
new file mode 100644 (file)
index 0000000..d159169
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,339 @@
+                    GNU GENERAL PUBLIC LICENSE
+                       Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,
+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The licenses for most software are designed to take away your
+freedom to share and change it.  By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users.  This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it.  (Some other Free Software Foundation software is covered by
+the GNU Lesser General Public License instead.)  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+  To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have.  You must make sure that they, too, receive or can get the
+source code.  And you must show them these terms so they know their
+rights.
+
+  We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+  Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software.  If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+  Finally, any free program is threatened constantly by software
+patents.  We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary.  To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                    GNU GENERAL PUBLIC LICENSE
+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+  0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License.  The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language.  (Hereinafter, translation is included without limitation in
+the term "modification".)  Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope.  The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+  1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+  2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+    a) You must cause the modified files to carry prominent notices
+    stating that you changed the files and the date of any change.
+
+    b) You must cause any work that you distribute or publish, that in
+    whole or in part contains or is derived from the Program or any
+    part thereof, to be licensed as a whole at no charge to all third
+    parties under the terms of this License.
+
+    c) If the modified program normally reads commands interactively
+    when run, you must cause it, when started running for such
+    interactive use in the most ordinary way, to print or display an
+    announcement including an appropriate copyright notice and a
+    notice that there is no warranty (or else, saying that you provide
+    a warranty) and that users may redistribute the program under
+    these conditions, and telling the user how to view a copy of this
+    License.  (Exception: if the Program itself is interactive but
+    does not normally print such an announcement, your work based on
+    the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole.  If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works.  But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+  3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+    a) Accompany it with the complete corresponding machine-readable
+    source code, which must be distributed under the terms of Sections
+    1 and 2 above on a medium customarily used for software interchange; or,
+
+    b) Accompany it with a written offer, valid for at least three
+    years, to give any third party, for a charge no more than your
+    cost of physically performing source distribution, a complete
+    machine-readable copy of the corresponding source code, to be
+    distributed under the terms of Sections 1 and 2 above on a medium
+    customarily used for software interchange; or,
+
+    c) Accompany it with the information you received as to the offer
+    to distribute corresponding source code.  (This alternative is
+    allowed only for noncommercial distribution and only if you
+    received the program in object code or executable form with such
+    an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it.  For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable.  However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+  4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License.  Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+  5. You are not required to accept this License, since you have not
+signed it.  However, nothing else grants you permission to modify or
+distribute the Program or its derivative works.  These actions are
+prohibited by law if you do not accept this License.  Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+  6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions.  You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+  7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all.  For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices.  Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+  8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded.  In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+  9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number.  If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation.  If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+  10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission.  For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this.  Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+                            NO WARRANTY
+
+  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+                     END OF TERMS AND CONDITIONS
+
+            How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License along
+    with this program; if not, write to the Free Software Foundation, Inc.,
+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+    Gnomovision version 69, Copyright (C) year name of author
+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary.  Here is a sample; alter the names:
+
+  Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+  `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+  <signature of Ty Coon>, 1 April 1989
+  Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs.  If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library.  If this is what you want to do, use the GNU Lesser General
+Public License instead of this License.
diff --git a/DEBUGGINGNOTES.txt b/DEBUGGINGNOTES.txt
new file mode 100644 (file)
index 0000000..12c3eda
--- /dev/null
@@ -0,0 +1,8 @@
+To run inside MacOS under gdb you need:
+set dont-handle-bad-access 1
+handle SIGBUS nostop noprint
+
+To run in Linux under gdb, use:
+handle SIGSEGV nostop noprint
+
+
diff --git a/Doxyfile b/Doxyfile
new file mode 100644 (file)
index 0000000..65c02c8
--- /dev/null
+++ b/Doxyfile
@@ -0,0 +1,1801 @@
+# Doxyfile 1.8.0
+
+# This file describes the settings to be used by the documentation system
+# doxygen (www.doxygen.org) for a project.
+#
+# All text after a hash (#) is considered a comment and will be ignored.
+# The format is:
+#       TAG = value [value, ...]
+# For lists items can also be appended using:
+#       TAG += value [value, ...]
+# Values that contain spaces should be placed between quotes (" ").
+
+#---------------------------------------------------------------------------
+# Project related configuration options
+#---------------------------------------------------------------------------
+
+# This tag specifies the encoding used for all characters in the config file
+# that follow. The default is UTF-8 which is also the encoding used for all
+# text before the first occurrence of this tag. Doxygen uses libiconv (or the
+# iconv built into libc) for the transcoding. See
+# http://www.gnu.org/software/libiconv for the list of possible encodings.
+
+DOXYFILE_ENCODING      = UTF-8
+
+# The PROJECT_NAME tag is a single word (or sequence of words) that should
+# identify the project. Note that if you do not use Doxywizard you need
+# to put quotes around the project name if it contains spaces.
+
+PROJECT_NAME           = "MC2: A Model Checker for SC"
+
+# The PROJECT_NUMBER tag can be used to enter a project or revision number.
+# This could be handy for archiving the generated documentation or
+# if some version control system is used.
+
+PROJECT_NUMBER         =
+
+# Using the PROJECT_BRIEF tag one can provide an optional one line description
+# for a project that appears at the top of each page and should give viewer
+# a quick idea about the purpose of the project. Keep the description short.
+
+PROJECT_BRIEF          =
+
+# With the PROJECT_LOGO tag one can specify an logo or icon that is
+# included in the documentation. The maximum height of the logo should not
+# exceed 55 pixels and the maximum width should not exceed 200 pixels.
+# Doxygen will copy the logo to the output directory.
+
+PROJECT_LOGO           =
+
+# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute)
+# base path where the generated documentation will be put.
+# If a relative path is entered, it will be relative to the location
+# where doxygen was started. If left blank the current directory will be used.
+
+OUTPUT_DIRECTORY       = doc
+
+# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create
+# 4096 sub-directories (in 2 levels) under the output directory of each output
+# format and will distribute the generated files over these directories.
+# Enabling this option can be useful when feeding doxygen a huge amount of
+# source files, where putting all generated files in the same directory would
+# otherwise cause performance problems for the file system.
+
+CREATE_SUBDIRS         = NO
+
+# The OUTPUT_LANGUAGE tag is used to specify the language in which all
+# documentation generated by doxygen is written. Doxygen will use this
+# information to generate all constant output in the proper language.
+# The default language is English, other supported languages are:
+# Afrikaans, Arabic, Brazilian, Catalan, Chinese, Chinese-Traditional,
+# Croatian, Czech, Danish, Dutch, Esperanto, Farsi, Finnish, French, German,
+# Greek, Hungarian, Italian, Japanese, Japanese-en (Japanese with English
+# messages), Korean, Korean-en, Lithuanian, Norwegian, Macedonian, Persian,
+# Polish, Portuguese, Romanian, Russian, Serbian, Serbian-Cyrillic, Slovak,
+# Slovene, Spanish, Swedish, Ukrainian, and Vietnamese.
+
+OUTPUT_LANGUAGE        = English
+
+# If the BRIEF_MEMBER_DESC tag is set to YES (the default) Doxygen will
+# include brief member descriptions after the members that are listed in
+# the file and class documentation (similar to JavaDoc).
+# Set to NO to disable this.
+
+BRIEF_MEMBER_DESC      = YES
+
+# If the REPEAT_BRIEF tag is set to YES (the default) Doxygen will prepend
+# the brief description of a member or function before the detailed description.
+# Note: if both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the
+# brief descriptions will be completely suppressed.
+
+REPEAT_BRIEF           = YES
+
+# This tag implements a quasi-intelligent brief description abbreviator
+# that is used to form the text in various listings. Each string
+# in this list, if found as the leading text of the brief description, will be
+# stripped from the text and the result after processing the whole list, is
+# used as the annotated text. Otherwise, the brief description is used as-is.
+# If left blank, the following values are used ("$name" is automatically
+# replaced with the name of the entity): "The $name class" "The $name widget"
+# "The $name file" "is" "provides" "specifies" "contains"
+# "represents" "a" "an" "the"
+
+ABBREVIATE_BRIEF       =
+
+# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then
+# Doxygen will generate a detailed section even if there is only a brief
+# description.
+
+ALWAYS_DETAILED_SEC    = NO
+
+# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all
+# inherited members of a class in the documentation of that class as if those
+# members were ordinary class members. Constructors, destructors and assignment
+# operators of the base classes will not be shown.
+
+INLINE_INHERITED_MEMB  = NO
+
+# If the FULL_PATH_NAMES tag is set to YES then Doxygen will prepend the full
+# path before files name in the file list and in the header files. If set
+# to NO the shortest path that makes the file name unique will be used.
+
+FULL_PATH_NAMES        = YES
+
+# If the FULL_PATH_NAMES tag is set to YES then the STRIP_FROM_PATH tag
+# can be used to strip a user-defined part of the path. Stripping is
+# only done if one of the specified strings matches the left-hand part of
+# the path. The tag can be used to show relative paths in the file list.
+# If left blank the directory from which doxygen is run is used as the
+# path to strip.
+
+STRIP_FROM_PATH        =
+
+# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of
+# the path mentioned in the documentation of a class, which tells
+# the reader which header file to include in order to use a class.
+# If left blank only the name of the header file containing the class
+# definition is used. Otherwise one should specify the include paths that
+# are normally passed to the compiler using the -I flag.
+
+STRIP_FROM_INC_PATH    =
+
+# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter
+# (but less readable) file names. This can be useful if your file system
+# doesn't support long names like on DOS, Mac, or CD-ROM.
+
+SHORT_NAMES            = NO
+
+# If the JAVADOC_AUTOBRIEF tag is set to YES then Doxygen
+# will interpret the first line (until the first dot) of a JavaDoc-style
+# comment as the brief description. If set to NO, the JavaDoc
+# comments will behave just like regular Qt-style comments
+# (thus requiring an explicit @brief command for a brief description.)
+
+JAVADOC_AUTOBRIEF      = NO
+
+# If the QT_AUTOBRIEF tag is set to YES then Doxygen will
+# interpret the first line (until the first dot) of a Qt-style
+# comment as the brief description. If set to NO, the comments
+# will behave just like regular Qt-style comments (thus requiring
+# an explicit \brief command for a brief description.)
+
+QT_AUTOBRIEF           = NO
+
+# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make Doxygen
+# treat a multi-line C++ special comment block (i.e. a block of //! or ///
+# comments) as a brief description. This used to be the default behaviour.
+# The new default is to treat a multi-line C++ comment block as a detailed
+# description. Set this tag to YES if you prefer the old behaviour instead.
+
+MULTILINE_CPP_IS_BRIEF = NO
+
+# If the INHERIT_DOCS tag is set to YES (the default) then an undocumented
+# member inherits the documentation from any documented member that it
+# re-implements.
+
+INHERIT_DOCS           = YES
+
+# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce
+# a new page for each member. If set to NO, the documentation of a member will
+# be part of the file/class/namespace that contains it.
+
+SEPARATE_MEMBER_PAGES  = NO
+
+# The TAB_SIZE tag can be used to set the number of spaces in a tab.
+# Doxygen uses this value to replace tabs by spaces in code fragments.
+
+TAB_SIZE               = 5
+
+# This tag can be used to specify a number of aliases that acts
+# as commands in the documentation. An alias has the form "name=value".
+# For example adding "sideeffect=\par Side Effects:\n" will allow you to
+# put the command \sideeffect (or @sideeffect) in the documentation, which
+# will result in a user-defined paragraph with heading "Side Effects:".
+# You can put \n's in the value part of an alias to insert newlines.
+
+ALIASES                =
+
+# This tag can be used to specify a number of word-keyword mappings (TCL only).
+# A mapping has the form "name=value". For example adding
+# "class=itcl::class" will allow you to use the command class in the
+# itcl::class meaning.
+
+TCL_SUBST              =
+
+# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C
+# sources only. Doxygen will then generate output that is more tailored for C.
+# For instance, some of the names that are used will be different. The list
+# of all members will be omitted, etc.
+
+OPTIMIZE_OUTPUT_FOR_C  = NO
+
+# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java
+# sources only. Doxygen will then generate output that is more tailored for
+# Java. For instance, namespaces will be presented as packages, qualified
+# scopes will look different, etc.
+
+OPTIMIZE_OUTPUT_JAVA   = NO
+
+# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran
+# sources only. Doxygen will then generate output that is more tailored for
+# Fortran.
+
+OPTIMIZE_FOR_FORTRAN   = NO
+
+# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL
+# sources. Doxygen will then generate output that is tailored for
+# VHDL.
+
+OPTIMIZE_OUTPUT_VHDL   = NO
+
+# Doxygen selects the parser to use depending on the extension of the files it
+# parses. With this tag you can assign which parser to use for a given extension.
+# Doxygen has a built-in mapping, but you can override or extend it using this
+# tag. The format is ext=language, where ext is a file extension, and language
+# is one of the parsers supported by doxygen: IDL, Java, Javascript, CSharp, C,
+# C++, D, PHP, Objective-C, Python, Fortran, VHDL, C, C++. For instance to make
+# doxygen treat .inc files as Fortran files (default is PHP), and .f files as C
+# (default is Fortran), use: inc=Fortran f=C. Note that for custom extensions
+# you also need to set FILE_PATTERNS otherwise the files are not read by doxygen.
+
+EXTENSION_MAPPING      =
+
+# If MARKDOWN_SUPPORT is enabled (the default) then doxygen pre-processes all
+# comments according to the Markdown format, which allows for more readable
+# documentation. See http://daringfireball.net/projects/markdown/ for details.
+# The output of markdown processing is further processed by doxygen, so you
+# can mix doxygen, HTML, and XML commands with Markdown formatting.
+# Disable only in case of backward compatibilities issues.
+
+MARKDOWN_SUPPORT       = YES
+
+# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want
+# to include (a tag file for) the STL sources as input, then you should
+# set this tag to YES in order to let doxygen match functions declarations and
+# definitions whose arguments contain STL classes (e.g. func(std::string); v.s.
+# func(std::string) {}). This also makes the inheritance and collaboration
+# diagrams that involve STL classes more complete and accurate.
+
+BUILTIN_STL_SUPPORT    = NO
+
+# If you use Microsoft's C++/CLI language, you should set this option to YES to
+# enable parsing support.
+
+CPP_CLI_SUPPORT        = NO
+
+# Set the SIP_SUPPORT tag to YES if your project consists of sip sources only.
+# Doxygen will parse them like normal C++ but will assume all classes use public
+# instead of private inheritance when no explicit protection keyword is present.
+
+SIP_SUPPORT            = NO
+
+# For Microsoft's IDL there are propget and propput attributes to indicate getter
+# and setter methods for a property. Setting this option to YES (the default)
+# will make doxygen replace the get and set methods by a property in the
+# documentation. This will only work if the methods are indeed getting or
+# setting a simple type. If this is not the case, or you want to show the
+# methods anyway, you should set this option to NO.
+
+IDL_PROPERTY_SUPPORT   = YES
+
+# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC
+# tag is set to YES, then doxygen will reuse the documentation of the first
+# member in the group (if any) for the other members of the group. By default
+# all members of a group must be documented explicitly.
+
+DISTRIBUTE_GROUP_DOC   = NO
+
+# Set the SUBGROUPING tag to YES (the default) to allow class member groups of
+# the same type (for instance a group of public functions) to be put as a
+# subgroup of that type (e.g. under the Public Functions section). Set it to
+# NO to prevent subgrouping. Alternatively, this can be done per class using
+# the \nosubgrouping command.
+
+SUBGROUPING            = YES
+
+# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and
+# unions are shown inside the group in which they are included (e.g. using
+# @ingroup) instead of on a separate page (for HTML and Man pages) or
+# section (for LaTeX and RTF).
+
+INLINE_GROUPED_CLASSES = NO
+
+# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and
+# unions with only public data fields will be shown inline in the documentation
+# of the scope in which they are defined (i.e. file, namespace, or group
+# documentation), provided this scope is documented. If set to NO (the default),
+# structs, classes, and unions are shown on a separate page (for HTML and Man
+# pages) or section (for LaTeX and RTF).
+
+INLINE_SIMPLE_STRUCTS  = NO
+
+# When TYPEDEF_HIDES_STRUCT is enabled, a typedef of a struct, union, or enum
+# is documented as struct, union, or enum with the name of the typedef. So
+# typedef struct TypeS {} TypeT, will appear in the documentation as a struct
+# with name TypeT. When disabled the typedef will appear as a member of a file,
+# namespace, or class. And the struct will be named TypeS. This can typically
+# be useful for C code in case the coding convention dictates that all compound
+# types are typedef'ed and only the typedef is referenced, never the tag name.
+
+TYPEDEF_HIDES_STRUCT   = NO
+
+# The SYMBOL_CACHE_SIZE determines the size of the internal cache use to
+# determine which symbols to keep in memory and which to flush to disk.
+# When the cache is full, less often used symbols will be written to disk.
+# For small to medium size projects (<1000 input files) the default value is
+# probably good enough. For larger projects a too small cache size can cause
+# doxygen to be busy swapping symbols to and from disk most of the time
+# causing a significant performance penalty.
+# If the system has enough physical memory increasing the cache will improve the
+# performance by keeping more symbols in memory. Note that the value works on
+# a logarithmic scale so increasing the size by one will roughly double the
+# memory usage. The cache size is given by this formula:
+# 2^(16+SYMBOL_CACHE_SIZE). The valid range is 0..9, the default is 0,
+# corresponding to a cache size of 2^16 = 65536 symbols.
+
+SYMBOL_CACHE_SIZE      = 0
+
+# Similar to the SYMBOL_CACHE_SIZE the size of the symbol lookup cache can be
+# set using LOOKUP_CACHE_SIZE. This cache is used to resolve symbols given
+# their name and scope. Since this can be an expensive process and often the
+# same symbol appear multiple times in the code, doxygen keeps a cache of
+# pre-resolved symbols. If the cache is too small doxygen will become slower.
+# If the cache is too large, memory is wasted. The cache size is given by this
+# formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range is 0..9, the default is 0,
+# corresponding to a cache size of 2^16 = 65536 symbols.
+
+LOOKUP_CACHE_SIZE      = 0
+
+#---------------------------------------------------------------------------
+# Build related configuration options
+#---------------------------------------------------------------------------
+
+# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in
+# documentation are documented, even if no documentation was available.
+# Private class members and static file members will be hidden unless
+# the EXTRACT_PRIVATE and EXTRACT_STATIC tags are set to YES
+
+EXTRACT_ALL            = NO
+
+# If the EXTRACT_PRIVATE tag is set to YES all private members of a class
+# will be included in the documentation.
+
+EXTRACT_PRIVATE        = YES
+
+# If the EXTRACT_PACKAGE tag is set to YES all members with package or internal scope will be included in the documentation.
+
+EXTRACT_PACKAGE        = NO
+
+# If the EXTRACT_STATIC tag is set to YES all static members of a file
+# will be included in the documentation.
+
+EXTRACT_STATIC         = NO
+
+# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs)
+# defined locally in source files will be included in the documentation.
+# If set to NO only classes defined in header files are included.
+
+EXTRACT_LOCAL_CLASSES  = YES
+
+# This flag is only useful for Objective-C code. When set to YES local
+# methods, which are defined in the implementation section but not in
+# the interface are included in the documentation.
+# If set to NO (the default) only methods in the interface are included.
+
+EXTRACT_LOCAL_METHODS  = NO
+
+# If this flag is set to YES, the members of anonymous namespaces will be
+# extracted and appear in the documentation as a namespace called
+# 'anonymous_namespace{file}', where file will be replaced with the base
+# name of the file that contains the anonymous namespace. By default
+# anonymous namespaces are hidden.
+
+EXTRACT_ANON_NSPACES   = NO
+
+# If the HIDE_UNDOC_MEMBERS tag is set to YES, Doxygen will hide all
+# undocumented members of documented classes, files or namespaces.
+# If set to NO (the default) these members will be included in the
+# various overviews, but no documentation section is generated.
+# This option has no effect if EXTRACT_ALL is enabled.
+
+HIDE_UNDOC_MEMBERS     = NO
+
+# If the HIDE_UNDOC_CLASSES tag is set to YES, Doxygen will hide all
+# undocumented classes that are normally visible in the class hierarchy.
+# If set to NO (the default) these classes will be included in the various
+# overviews. This option has no effect if EXTRACT_ALL is enabled.
+
+HIDE_UNDOC_CLASSES     = NO
+
+# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, Doxygen will hide all
+# friend (class|struct|union) declarations.
+# If set to NO (the default) these declarations will be included in the
+# documentation.
+
+HIDE_FRIEND_COMPOUNDS  = NO
+
+# If the HIDE_IN_BODY_DOCS tag is set to YES, Doxygen will hide any
+# documentation blocks found inside the body of a function.
+# If set to NO (the default) these blocks will be appended to the
+# function's detailed documentation block.
+
+HIDE_IN_BODY_DOCS      = NO
+
+# The INTERNAL_DOCS tag determines if documentation
+# that is typed after a \internal command is included. If the tag is set
+# to NO (the default) then the documentation will be excluded.
+# Set it to YES to include the internal documentation.
+
+INTERNAL_DOCS          = NO
+
+# If the CASE_SENSE_NAMES tag is set to NO then Doxygen will only generate
+# file names in lower-case letters. If set to YES upper-case letters are also
+# allowed. This is useful if you have classes or files whose names only differ
+# in case and if your file system supports case sensitive file names. Windows
+# and Mac users are advised to set this option to NO.
+
+CASE_SENSE_NAMES       = NO
+
+# If the HIDE_SCOPE_NAMES tag is set to NO (the default) then Doxygen
+# will show members with their full class and namespace scopes in the
+# documentation. If set to YES the scope will be hidden.
+
+HIDE_SCOPE_NAMES       = NO
+
+# If the SHOW_INCLUDE_FILES tag is set to YES (the default) then Doxygen
+# will put a list of the files that are included by a file in the documentation
+# of that file.
+
+SHOW_INCLUDE_FILES     = YES
+
+# If the FORCE_LOCAL_INCLUDES tag is set to YES then Doxygen
+# will list include files with double quotes in the documentation
+# rather than with sharp brackets.
+
+FORCE_LOCAL_INCLUDES   = NO
+
+# If the INLINE_INFO tag is set to YES (the default) then a tag [inline]
+# is inserted in the documentation for inline members.
+
+INLINE_INFO            = YES
+
+# If the SORT_MEMBER_DOCS tag is set to YES (the default) then doxygen
+# will sort the (detailed) documentation of file and class members
+# alphabetically by member name. If set to NO the members will appear in
+# declaration order.
+
+SORT_MEMBER_DOCS       = YES
+
+# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the
+# brief documentation of file, namespace and class members alphabetically
+# by member name. If set to NO (the default) the members will appear in
+# declaration order.
+
+SORT_BRIEF_DOCS        = NO
+
+# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen
+# will sort the (brief and detailed) documentation of class members so that
+# constructors and destructors are listed first. If set to NO (the default)
+# the constructors will appear in the respective orders defined by
+# SORT_MEMBER_DOCS and SORT_BRIEF_DOCS.
+# This tag will be ignored for brief docs if SORT_BRIEF_DOCS is set to NO
+# and ignored for detailed docs if SORT_MEMBER_DOCS is set to NO.
+
+SORT_MEMBERS_CTORS_1ST = NO
+
+# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the
+# hierarchy of group names into alphabetical order. If set to NO (the default)
+# the group names will appear in their defined order.
+
+SORT_GROUP_NAMES       = NO
+
+# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be
+# sorted by fully-qualified names, including namespaces. If set to
+# NO (the default), the class list will be sorted only by class name,
+# not including the namespace part.
+# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES.
+# Note: This option applies only to the class list, not to the
+# alphabetical list.
+
+SORT_BY_SCOPE_NAME     = NO
+
+# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to
+# do proper type resolution of all parameters of a function it will reject a
+# match between the prototype and the implementation of a member function even
+# if there is only one candidate or it is obvious which candidate to choose
+# by doing a simple string match. By disabling STRICT_PROTO_MATCHING doxygen
+# will still accept a match between prototype and implementation in such cases.
+
+STRICT_PROTO_MATCHING  = NO
+
+# The GENERATE_TODOLIST tag can be used to enable (YES) or
+# disable (NO) the todo list. This list is created by putting \todo
+# commands in the documentation.
+
+GENERATE_TODOLIST      = YES
+
+# The GENERATE_TESTLIST tag can be used to enable (YES) or
+# disable (NO) the test list. This list is created by putting \test
+# commands in the documentation.
+
+GENERATE_TESTLIST      = YES
+
+# The GENERATE_BUGLIST tag can be used to enable (YES) or
+# disable (NO) the bug list. This list is created by putting \bug
+# commands in the documentation.
+
+GENERATE_BUGLIST       = YES
+
+# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or
+# disable (NO) the deprecated list. This list is created by putting
+# \deprecated commands in the documentation.
+
+GENERATE_DEPRECATEDLIST= YES
+
+# The ENABLED_SECTIONS tag can be used to enable conditional
+# documentation sections, marked by \if sectionname ... \endif.
+
+ENABLED_SECTIONS       =
+
+# The MAX_INITIALIZER_LINES tag determines the maximum number of lines
+# the initial value of a variable or macro consists of for it to appear in
+# the documentation. If the initializer consists of more lines than specified
+# here it will be hidden. Use a value of 0 to hide initializers completely.
+# The appearance of the initializer of individual variables and macros in the
+# documentation can be controlled using \showinitializer or \hideinitializer
+# command in the documentation regardless of this setting.
+
+MAX_INITIALIZER_LINES  = 30
+
+# Set the SHOW_USED_FILES tag to NO to disable the list of files generated
+# at the bottom of the documentation of classes and structs. If set to YES the
+# list will mention the files that were used to generate the documentation.
+
+SHOW_USED_FILES        = YES
+
+# If the sources in your project are distributed over multiple directories
+# then setting the SHOW_DIRECTORIES tag to YES will show the directory hierarchy
+# in the documentation. The default is NO.
+
+SHOW_DIRECTORIES       = NO
+
+# Set the SHOW_FILES tag to NO to disable the generation of the Files page.
+# This will remove the Files entry from the Quick Index and from the
+# Folder Tree View (if specified). The default is YES.
+
+SHOW_FILES             = YES
+
+# Set the SHOW_NAMESPACES tag to NO to disable the generation of the
+# Namespaces page.
+# This will remove the Namespaces entry from the Quick Index
+# and from the Folder Tree View (if specified). The default is YES.
+
+SHOW_NAMESPACES        = YES
+
+# The FILE_VERSION_FILTER tag can be used to specify a program or script that
+# doxygen should invoke to get the current version for each file (typically from
+# the version control system). Doxygen will invoke the program by executing (via
+# popen()) the command <command> <input-file>, where <command> is the value of
+# the FILE_VERSION_FILTER tag, and <input-file> is the name of an input file
+# provided by doxygen. Whatever the program writes to standard output
+# is used as the file version. See the manual for examples.
+
+FILE_VERSION_FILTER    =
+
+# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed
+# by doxygen. The layout file controls the global structure of the generated
+# output files in an output format independent way. The create the layout file
+# that represents doxygen's defaults, run doxygen with the -l option.
+# You can optionally specify a file name after the option, if omitted
+# DoxygenLayout.xml will be used as the name of the layout file.
+
+LAYOUT_FILE            =
+
+# The CITE_BIB_FILES tag can be used to specify one or more bib files
+# containing the references data. This must be a list of .bib files. The
+# .bib extension is automatically appended if omitted. Using this command
+# requires the bibtex tool to be installed. See also
+# http://en.wikipedia.org/wiki/BibTeX for more info. For LaTeX the style
+# of the bibliography can be controlled using LATEX_BIB_STYLE. To use this
+# feature you need bibtex and perl available in the search path.
+
+CITE_BIB_FILES         =
+
+#---------------------------------------------------------------------------
+# configuration options related to warning and progress messages
+#---------------------------------------------------------------------------
+
+# The QUIET tag can be used to turn on/off the messages that are generated
+# by doxygen. Possible values are YES and NO. If left blank NO is used.
+
+QUIET                  = NO
+
+# The WARNINGS tag can be used to turn on/off the warning messages that are
+# generated by doxygen. Possible values are YES and NO. If left blank
+# NO is used.
+
+WARNINGS               = YES
+
+# If WARN_IF_UNDOCUMENTED is set to YES, then doxygen will generate warnings
+# for undocumented members. If EXTRACT_ALL is set to YES then this flag will
+# automatically be disabled.
+
+WARN_IF_UNDOCUMENTED   = YES
+
+# If WARN_IF_DOC_ERROR is set to YES, doxygen will generate warnings for
+# potential errors in the documentation, such as not documenting some
+# parameters in a documented function, or documenting parameters that
+# don't exist or using markup commands wrongly.
+
+WARN_IF_DOC_ERROR      = YES
+
+# The WARN_NO_PARAMDOC option can be enabled to get warnings for
+# functions that are documented, but have no documentation for their parameters
+# or return value. If set to NO (the default) doxygen will only warn about
+# wrong or incomplete parameter documentation, but not about the absence of
+# documentation.
+
+WARN_NO_PARAMDOC       = NO
+
+# The WARN_FORMAT tag determines the format of the warning messages that
+# doxygen can produce. The string should contain the $file, $line, and $text
+# tags, which will be replaced by the file and line number from which the
+# warning originated and the warning text. Optionally the format may contain
+# $version, which will be replaced by the version of the file (if it could
+# be obtained via FILE_VERSION_FILTER)
+
+WARN_FORMAT            = "$file:$line: $text"
+
+# The WARN_LOGFILE tag can be used to specify a file to which warning
+# and error messages should be written. If left blank the output is written
+# to stderr.
+
+WARN_LOGFILE           =
+
+#---------------------------------------------------------------------------
+# configuration options related to the input files
+#---------------------------------------------------------------------------
+
+# The INPUT tag can be used to specify the files and/or directories that contain
+# documented source files. You may enter file names like "myfile.cpp" or
+# directories like "/usr/src/myproject". Separate the files or directories
+# with spaces.
+
+INPUT                  = . include/ include/atomic include/condition_variable include/cstdatomic include/mutex
+
+
+# This tag can be used to specify the character encoding of the source files
+# that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
+# also the default input encoding. Doxygen uses libiconv (or the iconv built
+# into libc) for the transcoding. See http://www.gnu.org/software/libiconv for
+# the list of possible encodings.
+
+INPUT_ENCODING         = UTF-8
+
+# If the value of the INPUT tag contains directories, you can use the
+# FILE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp
+# and *.h) to filter out the source-files in the directories. If left
+# blank the following patterns are tested:
+# *.c *.cc *.cxx *.cpp *.c++ *.d *.java *.ii *.ixx *.ipp *.i++ *.inl *.h *.hh
+# *.hxx *.hpp *.h++ *.idl *.odl *.cs *.php *.php3 *.inc *.m *.mm *.dox *.py
+# *.f90 *.f *.for *.vhd *.vhdl
+
+FILE_PATTERNS          =
+
+# The RECURSIVE tag can be used to turn specify whether or not subdirectories
+# should be searched for input files as well. Possible values are YES and NO.
+# If left blank NO is used.
+
+RECURSIVE              = NO
+
+# The EXCLUDE tag can be used to specify files and/or directories that should be
+# excluded from the INPUT source files. This way you can easily exclude a
+# subdirectory from a directory tree whose root is specified with the INPUT tag.
+# Note that relative paths are relative to the directory from which doxygen is
+# run.
+
+EXCLUDE                = malloc.c
+
+# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or
+# directories that are symbolic links (a Unix file system feature) are excluded
+# from the input.
+
+EXCLUDE_SYMLINKS       = NO
+
+# If the value of the INPUT tag contains directories, you can use the
+# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude
+# certain files from those directories. Note that the wildcards are matched
+# against the file with absolute path, so to exclude all test directories
+# for example use the pattern */test/*
+
+EXCLUDE_PATTERNS       =
+
+# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names
+# (namespaces, classes, functions, etc.) that should be excluded from the
+# output. The symbol name can be a fully qualified name, a word, or if the
+# wildcard * is used, a substring. Examples: ANamespace, AClass,
+# AClass::ANamespace, ANamespace::*Test
+
+EXCLUDE_SYMBOLS        =
+
+# The EXAMPLE_PATH tag can be used to specify one or more files or
+# directories that contain example code fragments that are included (see
+# the \include command).
+
+EXAMPLE_PATH           = .
+
+# If the value of the EXAMPLE_PATH tag contains directories, you can use the
+# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp
+# and *.h) to filter out the source-files in the directories. If left
+# blank all files are included.
+
+EXAMPLE_PATTERNS       =
+
+# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be
+# searched for input files to be used with the \include or \dontinclude
+# commands irrespective of the value of the RECURSIVE tag.
+# Possible values are YES and NO. If left blank NO is used.
+
+EXAMPLE_RECURSIVE      = NO
+
+# The IMAGE_PATH tag can be used to specify one or more files or
+# directories that contain image that are included in the documentation (see
+# the \image command).
+
+IMAGE_PATH             =
+
+# The INPUT_FILTER tag can be used to specify a program that doxygen should
+# invoke to filter for each input file. Doxygen will invoke the filter program
+# by executing (via popen()) the command <filter> <input-file>, where <filter>
+# is the value of the INPUT_FILTER tag, and <input-file> is the name of an
+# input file. Doxygen will then use the output that the filter program writes
+# to standard output.
+# If FILTER_PATTERNS is specified, this tag will be
+# ignored.
+
+INPUT_FILTER           =
+
+# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern
+# basis.
+# Doxygen will compare the file name with each pattern and apply the
+# filter if there is a match.
+# The filters are a list of the form:
+# pattern=filter (like *.cpp=my_cpp_filter). See INPUT_FILTER for further
+# info on how filters are used. If FILTER_PATTERNS is empty or if
+# non of the patterns match the file name, INPUT_FILTER is applied.
+
+FILTER_PATTERNS        =
+
+# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using
+# INPUT_FILTER) will be used to filter the input files when producing source
+# files to browse (i.e. when SOURCE_BROWSER is set to YES).
+
+FILTER_SOURCE_FILES    = NO
+
+# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file
+# pattern. A pattern will override the setting for FILTER_PATTERN (if any)
+# and it is also possible to disable source filtering for a specific pattern
+# using *.ext= (so without naming a filter). This option only has effect when
+# FILTER_SOURCE_FILES is enabled.
+
+FILTER_SOURCE_PATTERNS =
+
+#---------------------------------------------------------------------------
+# configuration options related to source browsing
+#---------------------------------------------------------------------------
+
+# If the SOURCE_BROWSER tag is set to YES then a list of source files will
+# be generated. Documented entities will be cross-referenced with these sources.
+# Note: To get rid of all source code in the generated output, make sure also
+# VERBATIM_HEADERS is set to NO.
+
+SOURCE_BROWSER         = NO
+
+# Setting the INLINE_SOURCES tag to YES will include the body
+# of functions and classes directly in the documentation.
+
+INLINE_SOURCES         = NO
+
+# Setting the STRIP_CODE_COMMENTS tag to YES (the default) will instruct
+# doxygen to hide any special comment blocks from generated source code
+# fragments. Normal C and C++ comments will always remain visible.
+
+STRIP_CODE_COMMENTS    = YES
+
+# If the REFERENCED_BY_RELATION tag is set to YES
+# then for each documented function all documented
+# functions referencing it will be listed.
+
+REFERENCED_BY_RELATION = NO
+
+# If the REFERENCES_RELATION tag is set to YES
+# then for each documented function all documented entities
+# called/used by that function will be listed.
+
+REFERENCES_RELATION    = NO
+
+# If the REFERENCES_LINK_SOURCE tag is set to YES (the default)
+# and SOURCE_BROWSER tag is set to YES, then the hyperlinks from
+# functions in REFERENCES_RELATION and REFERENCED_BY_RELATION lists will
+# link to the source code.
+# Otherwise they will link to the documentation.
+
+REFERENCES_LINK_SOURCE = YES
+
+# If the USE_HTAGS tag is set to YES then the references to source code
+# will point to the HTML generated by the htags(1) tool instead of doxygen
+# built-in source browser. The htags tool is part of GNU's global source
+# tagging system (see http://www.gnu.org/software/global/global.html). You
+# will need version 4.8.6 or higher.
+
+USE_HTAGS              = NO
+
+# If the VERBATIM_HEADERS tag is set to YES (the default) then Doxygen
+# will generate a verbatim copy of the header file for each class for
+# which an include is specified. Set to NO to disable this.
+
+VERBATIM_HEADERS       = YES
+
+#---------------------------------------------------------------------------
+# configuration options related to the alphabetical class index
+#---------------------------------------------------------------------------
+
+# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index
+# of all compounds will be generated. Enable this if the project
+# contains a lot of classes, structs, unions or interfaces.
+
+ALPHABETICAL_INDEX     = YES
+
+# If the alphabetical index is enabled (see ALPHABETICAL_INDEX) then
+# the COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns
+# in which this list will be split (can be a number in the range [1..20])
+
+COLS_IN_ALPHA_INDEX    = 5
+
+# In case all classes in a project start with a common prefix, all
+# classes will be put under the same header in the alphabetical index.
+# The IGNORE_PREFIX tag can be used to specify one or more prefixes that
+# should be ignored while generating the index headers.
+
+IGNORE_PREFIX          =
+
+#---------------------------------------------------------------------------
+# configuration options related to the HTML output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_HTML tag is set to YES (the default) Doxygen will
+# generate HTML output.
+
+GENERATE_HTML          = YES
+
+# The HTML_OUTPUT tag is used to specify where the HTML docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `html' will be used as the default path.
+
+HTML_OUTPUT            = docs
+
+# The HTML_FILE_EXTENSION tag can be used to specify the file extension for
+# each generated HTML page (for example: .htm,.php,.asp). If it is left blank
+# doxygen will generate files with .html extension.
+
+HTML_FILE_EXTENSION    = .html
+
+# The HTML_HEADER tag can be used to specify a personal HTML header for
+# each generated HTML page. If it is left blank doxygen will generate a
+# standard header. Note that when using a custom header you are responsible
+#  for the proper inclusion of any scripts and style sheets that doxygen
+# needs, which is dependent on the configuration options used.
+# It is advised to generate a default header using "doxygen -w html
+# header.html footer.html stylesheet.css YourConfigFile" and then modify
+# that header. Note that the header is subject to change so you typically
+# have to redo this when upgrading to a newer version of doxygen or when
+# changing the value of configuration settings such as GENERATE_TREEVIEW!
+
+HTML_HEADER            =
+
+# The HTML_FOOTER tag can be used to specify a personal HTML footer for
+# each generated HTML page. If it is left blank doxygen will generate a
+# standard footer.
+
+HTML_FOOTER            =
+
+# The HTML_STYLESHEET tag can be used to specify a user-defined cascading
+# style sheet that is used by each HTML page. It can be used to
+# fine-tune the look of the HTML output. If the tag is left blank doxygen
+# will generate a default style sheet. Note that doxygen will try to copy
+# the style sheet file to the HTML output directory, so don't put your own
+# style sheet in the HTML output directory as well, or it will be erased!
+
+HTML_STYLESHEET        =
+
+# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or
+# other source files which should be copied to the HTML output directory. Note
+# that these files will be copied to the base HTML output directory. Use the
+# $relpath$ marker in the HTML_HEADER and/or HTML_FOOTER files to load these
+# files. In the HTML_STYLESHEET file, use the file name only. Also note that
+# the files will be copied as-is; there are no commands or markers available.
+
+HTML_EXTRA_FILES       =
+
+# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output.
+# Doxygen will adjust the colors in the style sheet and background images
+# according to this color. Hue is specified as an angle on a colorwheel,
+# see http://en.wikipedia.org/wiki/Hue for more information.
+# For instance the value 0 represents red, 60 is yellow, 120 is green,
+# 180 is cyan, 240 is blue, 300 purple, and 360 is red again.
+# The allowed range is 0 to 359.
+
+HTML_COLORSTYLE_HUE    = 220
+
+# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of
+# the colors in the HTML output. For a value of 0 the output will use
+# grayscales only. A value of 255 will produce the most vivid colors.
+
+HTML_COLORSTYLE_SAT    = 100
+
+# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to
+# the luminance component of the colors in the HTML output. Values below
+# 100 gradually make the output lighter, whereas values above 100 make
+# the output darker. The value divided by 100 is the actual gamma applied,
+# so 80 represents a gamma of 0.8, The value 220 represents a gamma of 2.2,
+# and 100 does not change the gamma.
+
+HTML_COLORSTYLE_GAMMA  = 80
+
+# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML
+# page will contain the date and time when the page was generated. Setting
+# this to NO can help when comparing the output of multiple runs.
+
+HTML_TIMESTAMP         = YES
+
+# If the HTML_ALIGN_MEMBERS tag is set to YES, the members of classes,
+# files or namespaces will be aligned in HTML using tables. If set to
+# NO a bullet list will be used.
+
+HTML_ALIGN_MEMBERS     = YES
+
+# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML
+# documentation will contain sections that can be hidden and shown after the
+# page has loaded. For this to work a browser that supports
+# JavaScript and DHTML is required (for instance Mozilla 1.0+, Firefox
+# Netscape 6.0+, Internet explorer 5.0+, Konqueror, or Safari).
+
+HTML_DYNAMIC_SECTIONS  = NO
+
+# If the GENERATE_DOCSET tag is set to YES, additional index files
+# will be generated that can be used as input for Apple's Xcode 3
+# integrated development environment, introduced with OSX 10.5 (Leopard).
+# To create a documentation set, doxygen will generate a Makefile in the
+# HTML output directory. Running make will produce the docset in that
+# directory and running "make install" will install the docset in
+# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find
+# it at startup.
+# See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html
+# for more information.
+
+GENERATE_DOCSET        = NO
+
+# When GENERATE_DOCSET tag is set to YES, this tag determines the name of the
+# feed. A documentation feed provides an umbrella under which multiple
+# documentation sets from a single provider (such as a company or product suite)
+# can be grouped.
+
+DOCSET_FEEDNAME        = "Doxygen generated docs"
+
+# When GENERATE_DOCSET tag is set to YES, this tag specifies a string that
+# should uniquely identify the documentation set bundle. This should be a
+# reverse domain-name style string, e.g. com.mycompany.MyDocSet. Doxygen
+# will append .docset to the name.
+
+DOCSET_BUNDLE_ID       = org.doxygen.Project
+
+# When GENERATE_PUBLISHER_ID tag specifies a string that should uniquely identify
+# the documentation publisher. This should be a reverse domain-name style
+# string, e.g. com.mycompany.MyDocSet.documentation.
+
+DOCSET_PUBLISHER_ID    = org.doxygen.Publisher
+
+# The GENERATE_PUBLISHER_NAME tag identifies the documentation publisher.
+
+DOCSET_PUBLISHER_NAME  = Publisher
+
+# If the GENERATE_HTMLHELP tag is set to YES, additional index files
+# will be generated that can be used as input for tools like the
+# Microsoft HTML help workshop to generate a compiled HTML help file (.chm)
+# of the generated HTML documentation.
+
+GENERATE_HTMLHELP      = NO
+
+# If the GENERATE_HTMLHELP tag is set to YES, the CHM_FILE tag can
+# be used to specify the file name of the resulting .chm file. You
+# can add a path in front of the file if the result should not be
+# written to the html output directory.
+
+CHM_FILE               =
+
+# If the GENERATE_HTMLHELP tag is set to YES, the HHC_LOCATION tag can
+# be used to specify the location (absolute path including file name) of
+# the HTML help compiler (hhc.exe). If non-empty doxygen will try to run
+# the HTML help compiler on the generated index.hhp.
+
+HHC_LOCATION           =
+
+# If the GENERATE_HTMLHELP tag is set to YES, the GENERATE_CHI flag
+# controls if a separate .chi index file is generated (YES) or that
+# it should be included in the master .chm file (NO).
+
+GENERATE_CHI           = NO
+
+# If the GENERATE_HTMLHELP tag is set to YES, the CHM_INDEX_ENCODING
+# is used to encode HtmlHelp index (hhk), content (hhc) and project file
+# content.
+
+CHM_INDEX_ENCODING     =
+
+# If the GENERATE_HTMLHELP tag is set to YES, the BINARY_TOC flag
+# controls whether a binary table of contents is generated (YES) or a
+# normal table of contents (NO) in the .chm file.
+
+BINARY_TOC             = NO
+
+# The TOC_EXPAND flag can be set to YES to add extra items for group members
+# to the contents of the HTML help documentation and to the tree view.
+
+TOC_EXPAND             = NO
+
+# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and
+# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated
+# that can be used as input for Qt's qhelpgenerator to generate a
+# Qt Compressed Help (.qch) of the generated HTML documentation.
+
+GENERATE_QHP           = NO
+
+# If the QHG_LOCATION tag is specified, the QCH_FILE tag can
+# be used to specify the file name of the resulting .qch file.
+# The path specified is relative to the HTML output folder.
+
+QCH_FILE               =
+
+# The QHP_NAMESPACE tag specifies the namespace to use when generating
+# Qt Help Project output. For more information please see
+# http://doc.trolltech.com/qthelpproject.html#namespace
+
+QHP_NAMESPACE          = org.doxygen.Project
+
+# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating
+# Qt Help Project output. For more information please see
+# http://doc.trolltech.com/qthelpproject.html#virtual-folders
+
+QHP_VIRTUAL_FOLDER     = doc
+
+# If QHP_CUST_FILTER_NAME is set, it specifies the name of a custom filter to
+# add. For more information please see
+# http://doc.trolltech.com/qthelpproject.html#custom-filters
+
+QHP_CUST_FILTER_NAME   =
+
+# The QHP_CUST_FILT_ATTRS tag specifies the list of the attributes of the
+# custom filter to add. For more information please see
+# <a href="http://doc.trolltech.com/qthelpproject.html#custom-filters">
+# Qt Help Project / Custom Filters</a>.
+
+QHP_CUST_FILTER_ATTRS  =
+
+# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this
+# project's
+# filter section matches.
+# <a href="http://doc.trolltech.com/qthelpproject.html#filter-attributes">
+# Qt Help Project / Filter Attributes</a>.
+
+QHP_SECT_FILTER_ATTRS  =
+
+# If the GENERATE_QHP tag is set to YES, the QHG_LOCATION tag can
+# be used to specify the location of Qt's qhelpgenerator.
+# If non-empty doxygen will try to run qhelpgenerator on the generated
+# .qhp file.
+
+QHG_LOCATION           =
+
+# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files
+#  will be generated, which together with the HTML files, form an Eclipse help
+# plugin. To install this plugin and make it available under the help contents
+# menu in Eclipse, the contents of the directory containing the HTML and XML
+# files needs to be copied into the plugins directory of eclipse. The name of
+# the directory within the plugins directory should be the same as
+# the ECLIPSE_DOC_ID value. After copying Eclipse needs to be restarted before
+# the help appears.
+
+GENERATE_ECLIPSEHELP   = NO
+
+# A unique identifier for the eclipse help plugin. When installing the plugin
+# the directory name containing the HTML and XML files should also have
+# this name.
+
+ECLIPSE_DOC_ID         = org.doxygen.Project
+
+# The DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs)
+# at top of each HTML page. The value NO (the default) enables the index and
+# the value YES disables it. Since the tabs have the same information as the
+# navigation tree you can set this option to NO if you already set
+# GENERATE_TREEVIEW to YES.
+
+DISABLE_INDEX          = NO
+
+# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index
+# structure should be generated to display hierarchical information.
+# If the tag value is set to YES, a side panel will be generated
+# containing a tree-like index structure (just like the one that
+# is generated for HTML Help). For this to work a browser that supports
+# JavaScript, DHTML, CSS and frames is required (i.e. any modern browser).
+# Windows users are probably better off using the HTML help feature.
+# Since the tree basically has the same information as the tab index you
+# could consider to set DISABLE_INDEX to NO when enabling this option.
+
+GENERATE_TREEVIEW      = NO
+
+# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values
+# (range [0,1..20]) that doxygen will group on one line in the generated HTML
+# documentation. Note that a value of 0 will completely suppress the enum
+# values from appearing in the overview section.
+
+ENUM_VALUES_PER_LINE   = 4
+
+# By enabling USE_INLINE_TREES, doxygen will generate the Groups, Directories,
+# and Class Hierarchy pages using a tree view instead of an ordered list.
+
+USE_INLINE_TREES       = NO
+
+# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be
+# used to set the initial width (in pixels) of the frame in which the tree
+# is shown.
+
+TREEVIEW_WIDTH         = 250
+
+# When the EXT_LINKS_IN_WINDOW option is set to YES doxygen will open
+# links to external symbols imported via tag files in a separate window.
+
+EXT_LINKS_IN_WINDOW    = NO
+
+# Use this tag to change the font size of Latex formulas included
+# as images in the HTML documentation. The default is 10. Note that
+# when you change the font size after a successful doxygen run you need
+# to manually remove any form_*.png images from the HTML output directory
+# to force them to be regenerated.
+
+FORMULA_FONTSIZE       = 10
+
+# Use the FORMULA_TRANPARENT tag to determine whether or not the images
+# generated for formulas are transparent PNGs. Transparent PNGs are
+# not supported properly for IE 6.0, but are supported on all modern browsers.
+# Note that when changing this option you need to delete any form_*.png files
+# in the HTML output before the changes have effect.
+
+FORMULA_TRANSPARENT    = YES
+
+# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax
+# (see http://www.mathjax.org) which uses client side Javascript for the
+# rendering instead of using prerendered bitmaps. Use this if you do not
+# have LaTeX installed or if you want to formulas look prettier in the HTML
+# output. When enabled you may also need to install MathJax separately and
+# configure the path to it using the MATHJAX_RELPATH option.
+
+USE_MATHJAX            = NO
+
+# When MathJax is enabled you need to specify the location relative to the
+# HTML output directory using the MATHJAX_RELPATH option. The destination
+# directory should contain the MathJax.js script. For instance, if the mathjax
+# directory is located at the same level as the HTML output directory, then
+# MATHJAX_RELPATH should be ../mathjax. The default value points to
+# the MathJax Content Delivery Network so you can quickly see the result without
+# installing MathJax.
+# However, it is strongly recommended to install a local
+# copy of MathJax from http://www.mathjax.org before deployment.
+
+MATHJAX_RELPATH        = http://cdn.mathjax.org/mathjax/latest
+
+# The MATHJAX_EXTENSIONS tag can be used to specify one or MathJax extension
+# names that should be enabled during MathJax rendering.
+
+MATHJAX_EXTENSIONS     =
+
+# When the SEARCHENGINE tag is enabled doxygen will generate a search box
+# for the HTML output. The underlying search engine uses javascript
+# and DHTML and should work on any modern browser. Note that when using
+# HTML help (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets
+# (GENERATE_DOCSET) there is already a search function so this one should
+# typically be disabled. For large projects the javascript based search engine
+# can be slow, then enabling SERVER_BASED_SEARCH may provide a better solution.
+
+SEARCHENGINE           = YES
+
+# When the SERVER_BASED_SEARCH tag is enabled the search engine will be
+# implemented using a PHP enabled web server instead of at the web client
+# using Javascript. Doxygen will generate the search PHP script and index
+# file to put on the web server. The advantage of the server
+# based approach is that it scales better to large projects and allows
+# full text search. The disadvantages are that it is more difficult to setup
+# and does not have live searching capabilities.
+
+SERVER_BASED_SEARCH    = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the LaTeX output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_LATEX tag is set to YES (the default) Doxygen will
+# generate Latex output.
+
+GENERATE_LATEX         = NO
+
+# The LATEX_OUTPUT tag is used to specify where the LaTeX docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `latex' will be used as the default path.
+
+LATEX_OUTPUT           = latex
+
+# The LATEX_CMD_NAME tag can be used to specify the LaTeX command name to be
+# invoked. If left blank `latex' will be used as the default command name.
+# Note that when enabling USE_PDFLATEX this option is only used for
+# generating bitmaps for formulas in the HTML output, but not in the
+# Makefile that is written to the output directory.
+
+LATEX_CMD_NAME         = latex
+
+# The MAKEINDEX_CMD_NAME tag can be used to specify the command name to
+# generate index for LaTeX. If left blank `makeindex' will be used as the
+# default command name.
+
+MAKEINDEX_CMD_NAME     = makeindex
+
+# If the COMPACT_LATEX tag is set to YES Doxygen generates more compact
+# LaTeX documents. This may be useful for small projects and may help to
+# save some trees in general.
+
+COMPACT_LATEX          = NO
+
+# The PAPER_TYPE tag can be used to set the paper type that is used
+# by the printer. Possible values are: a4, letter, legal and
+# executive. If left blank a4wide will be used.
+
+PAPER_TYPE             = a4
+
+# The EXTRA_PACKAGES tag can be to specify one or more names of LaTeX
+# packages that should be included in the LaTeX output.
+
+EXTRA_PACKAGES         =
+
+# The LATEX_HEADER tag can be used to specify a personal LaTeX header for
+# the generated latex document. The header should contain everything until
+# the first chapter. If it is left blank doxygen will generate a
+# standard header. Notice: only use this tag if you know what you are doing!
+
+LATEX_HEADER           =
+
+# The LATEX_FOOTER tag can be used to specify a personal LaTeX footer for
+# the generated latex document. The footer should contain everything after
+# the last chapter. If it is left blank doxygen will generate a
+# standard footer. Notice: only use this tag if you know what you are doing!
+
+LATEX_FOOTER           =
+
+# If the PDF_HYPERLINKS tag is set to YES, the LaTeX that is generated
+# is prepared for conversion to pdf (using ps2pdf). The pdf file will
+# contain links (just like the HTML output) instead of page references
+# This makes the output suitable for online browsing using a pdf viewer.
+
+PDF_HYPERLINKS         = YES
+
+# If the USE_PDFLATEX tag is set to YES, pdflatex will be used instead of
+# plain latex in the generated Makefile. Set this option to YES to get a
+# higher quality PDF documentation.
+
+USE_PDFLATEX           = YES
+
+# If the LATEX_BATCHMODE tag is set to YES, doxygen will add the \\batchmode.
+# command to the generated LaTeX files. This will instruct LaTeX to keep
+# running if errors occur, instead of asking the user for help.
+# This option is also used when generating formulas in HTML.
+
+LATEX_BATCHMODE        = NO
+
+# If LATEX_HIDE_INDICES is set to YES then doxygen will not
+# include the index chapters (such as File Index, Compound Index, etc.)
+# in the output.
+
+LATEX_HIDE_INDICES     = NO
+
+# If LATEX_SOURCE_CODE is set to YES then doxygen will include
+# source code with syntax highlighting in the LaTeX output.
+# Note that which sources are shown also depends on other settings
+# such as SOURCE_BROWSER.
+
+LATEX_SOURCE_CODE      = NO
+
+# The LATEX_BIB_STYLE tag can be used to specify the style to use for the
+# bibliography, e.g. plainnat, or ieeetr. The default style is "plain". See
+# http://en.wikipedia.org/wiki/BibTeX for more info.
+
+LATEX_BIB_STYLE        = plain
+
+#---------------------------------------------------------------------------
+# configuration options related to the RTF output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_RTF tag is set to YES Doxygen will generate RTF output
+# The RTF output is optimized for Word 97 and may not look very pretty with
+# other RTF readers or editors.
+
+GENERATE_RTF           = NO
+
+# The RTF_OUTPUT tag is used to specify where the RTF docs will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `rtf' will be used as the default path.
+
+RTF_OUTPUT             = rtf
+
+# If the COMPACT_RTF tag is set to YES Doxygen generates more compact
+# RTF documents. This may be useful for small projects and may help to
+# save some trees in general.
+
+COMPACT_RTF            = NO
+
+# If the RTF_HYPERLINKS tag is set to YES, the RTF that is generated
+# will contain hyperlink fields. The RTF file will
+# contain links (just like the HTML output) instead of page references.
+# This makes the output suitable for online browsing using WORD or other
+# programs which support those fields.
+# Note: wordpad (write) and others do not support links.
+
+RTF_HYPERLINKS         = NO
+
+# Load style sheet definitions from file. Syntax is similar to doxygen's
+# config file, i.e. a series of assignments. You only have to provide
+# replacements, missing definitions are set to their default value.
+
+RTF_STYLESHEET_FILE    =
+
+# Set optional variables used in the generation of an rtf document.
+# Syntax is similar to doxygen's config file.
+
+RTF_EXTENSIONS_FILE    =
+
+#---------------------------------------------------------------------------
+# configuration options related to the man page output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_MAN tag is set to YES (the default) Doxygen will
+# generate man pages
+
+GENERATE_MAN           = NO
+
+# The MAN_OUTPUT tag is used to specify where the man pages will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `man' will be used as the default path.
+
+MAN_OUTPUT             = man
+
+# The MAN_EXTENSION tag determines the extension that is added to
+# the generated man pages (default is the subroutine's section .3)
+
+MAN_EXTENSION          = .3
+
+# If the MAN_LINKS tag is set to YES and Doxygen generates man output,
+# then it will generate one additional man file for each entity
+# documented in the real man page(s). These additional files
+# only source the real man page, but without them the man command
+# would be unable to find the correct page. The default is NO.
+
+MAN_LINKS              = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the XML output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_XML tag is set to YES Doxygen will
+# generate an XML file that captures the structure of
+# the code including all documentation.
+
+GENERATE_XML           = NO
+
+# The XML_OUTPUT tag is used to specify where the XML pages will be put.
+# If a relative path is entered the value of OUTPUT_DIRECTORY will be
+# put in front of it. If left blank `xml' will be used as the default path.
+
+XML_OUTPUT             = xml
+
+# The XML_SCHEMA tag can be used to specify an XML schema,
+# which can be used by a validating XML parser to check the
+# syntax of the XML files.
+
+XML_SCHEMA             =
+
+# The XML_DTD tag can be used to specify an XML DTD,
+# which can be used by a validating XML parser to check the
+# syntax of the XML files.
+
+XML_DTD                =
+
+# If the XML_PROGRAMLISTING tag is set to YES Doxygen will
+# dump the program listings (including syntax highlighting
+# and cross-referencing information) to the XML output. Note that
+# enabling this will significantly increase the size of the XML output.
+
+XML_PROGRAMLISTING     = YES
+
+#---------------------------------------------------------------------------
+# configuration options for the AutoGen Definitions output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_AUTOGEN_DEF tag is set to YES Doxygen will
+# generate an AutoGen Definitions (see autogen.sf.net) file
+# that captures the structure of the code including all
+# documentation. Note that this feature is still experimental
+# and incomplete at the moment.
+
+GENERATE_AUTOGEN_DEF   = NO
+
+#---------------------------------------------------------------------------
+# configuration options related to the Perl module output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_PERLMOD tag is set to YES Doxygen will
+# generate a Perl module file that captures the structure of
+# the code including all documentation. Note that this
+# feature is still experimental and incomplete at the
+# moment.
+
+GENERATE_PERLMOD       = NO
+
+# If the PERLMOD_LATEX tag is set to YES Doxygen will generate
+# the necessary Makefile rules, Perl scripts and LaTeX code to be able
+# to generate PDF and DVI output from the Perl module output.
+
+PERLMOD_LATEX          = NO
+
+# If the PERLMOD_PRETTY tag is set to YES the Perl module output will be
+# nicely formatted so it can be parsed by a human reader.
+# This is useful
+# if you want to understand what is going on.
+# On the other hand, if this
+# tag is set to NO the size of the Perl module output will be much smaller
+# and Perl will parse it just the same.
+
+PERLMOD_PRETTY         = YES
+
+# The names of the make variables in the generated doxyrules.make file
+# are prefixed with the string contained in PERLMOD_MAKEVAR_PREFIX.
+# This is useful so different doxyrules.make files included by the same
+# Makefile don't overwrite each other's variables.
+
+PERLMOD_MAKEVAR_PREFIX =
+
+#---------------------------------------------------------------------------
+# Configuration options related to the preprocessor
+#---------------------------------------------------------------------------
+
+# If the ENABLE_PREPROCESSING tag is set to YES (the default) Doxygen will
+# evaluate all C-preprocessor directives found in the sources and include
+# files.
+
+ENABLE_PREPROCESSING   = YES
+
+# If the MACRO_EXPANSION tag is set to YES Doxygen will expand all macro
+# names in the source code. If set to NO (the default) only conditional
+# compilation will be performed. Macro expansion can be done in a controlled
+# way by setting EXPAND_ONLY_PREDEF to YES.
+
+MACRO_EXPANSION        = NO
+
+# If the EXPAND_ONLY_PREDEF and MACRO_EXPANSION tags are both set to YES
+# then the macro expansion is limited to the macros specified with the
+# PREDEFINED and EXPAND_AS_DEFINED tags.
+
+EXPAND_ONLY_PREDEF     = NO
+
+# If the SEARCH_INCLUDES tag is set to YES (the default) the includes files
+# pointed to by INCLUDE_PATH will be searched when a #include is found.
+
+SEARCH_INCLUDES        = YES
+
+# The INCLUDE_PATH tag can be used to specify one or more directories that
+# contain include files that are not input files but should be processed by
+# the preprocessor.
+
+INCLUDE_PATH           =
+
+# You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard
+# patterns (like *.h and *.hpp) to filter out the header-files in the
+# directories. If left blank, the patterns specified with FILE_PATTERNS will
+# be used.
+
+INCLUDE_FILE_PATTERNS  =
+
+# The PREDEFINED tag can be used to specify one or more macro names that
+# are defined before the preprocessor is started (similar to the -D option of
+# gcc). The argument of the tag is a list of macros of the form: name
+# or name=definition (no spaces). If the definition and the = are
+# omitted =1 is assumed. To prevent a macro definition from being
+# undefined via #undef or recursively expanded use the := operator
+# instead of the = operator.
+
+PREDEFINED             =
+
+# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then
+# this tag can be used to specify a list of macro names that should be expanded.
+# The macro definition that is found in the sources will be used.
+# Use the PREDEFINED tag if you want to use a different macro definition that
+# overrules the definition found in the source code.
+
+EXPAND_AS_DEFINED      =
+
+# If the SKIP_FUNCTION_MACROS tag is set to YES (the default) then
+# doxygen's preprocessor will remove all references to function-like macros
+# that are alone on a line, have an all uppercase name, and do not end with a
+# semicolon, because these will confuse the parser if not removed.
+
+SKIP_FUNCTION_MACROS   = YES
+
+#---------------------------------------------------------------------------
+# Configuration::additions related to external references
+#---------------------------------------------------------------------------
+
+# The TAGFILES option can be used to specify one or more tagfiles. For each
+# tag file the location of the external documentation should be added. The
+# format of a tag file without this location is as follows:
+#
+# TAGFILES = file1 file2 ...
+# Adding location for the tag files is done as follows:
+#
+# TAGFILES = file1=loc1 "file2 = loc2" ...
+# where "loc1" and "loc2" can be relative or absolute paths
+# or URLs. Note that each tag file must have a unique name (where the name does
+# NOT include the path). If a tag file is not located in the directory in which
+# doxygen is run, you must also specify the path to the tagfile here.
+
+TAGFILES               =
+
+# When a file name is specified after GENERATE_TAGFILE, doxygen will create
+# a tag file that is based on the input files it reads.
+
+GENERATE_TAGFILE       =
+
+# If the ALLEXTERNALS tag is set to YES all external classes will be listed
+# in the class index. If set to NO only the inherited external classes
+# will be listed.
+
+ALLEXTERNALS           = NO
+
+# If the EXTERNAL_GROUPS tag is set to YES all external groups will be listed
+# in the modules index. If set to NO, only the current project's groups will
+# be listed.
+
+EXTERNAL_GROUPS        = YES
+
+# The PERL_PATH should be the absolute path and name of the perl script
+# interpreter (i.e. the result of `which perl').
+
+PERL_PATH              = /usr/bin/perl
+
+#---------------------------------------------------------------------------
+# Configuration options related to the dot tool
+#---------------------------------------------------------------------------
+
+# If the CLASS_DIAGRAMS tag is set to YES (the default) Doxygen will
+# generate a inheritance diagram (in HTML, RTF and LaTeX) for classes with base
+# or super classes. Setting the tag to NO turns the diagrams off. Note that
+# this option also works with HAVE_DOT disabled, but it is recommended to
+# install and use dot, since it yields more powerful graphs.
+
+CLASS_DIAGRAMS         = YES
+
+# You can define message sequence charts within doxygen comments using the \msc
+# command. Doxygen will then run the mscgen tool (see
+# http://www.mcternan.me.uk/mscgen/) to produce the chart and insert it in the
+# documentation. The MSCGEN_PATH tag allows you to specify the directory where
+# the mscgen tool resides. If left empty the tool is assumed to be found in the
+# default search path.
+
+MSCGEN_PATH            =
+
+# If set to YES, the inheritance and collaboration graphs will hide
+# inheritance and usage relations if the target is undocumented
+# or is not a class.
+
+HIDE_UNDOC_RELATIONS   = YES
+
+# If you set the HAVE_DOT tag to YES then doxygen will assume the dot tool is
+# available from the path. This tool is part of Graphviz, a graph visualization
+# toolkit from AT&T and Lucent Bell Labs. The other options in this section
+# have no effect if this option is set to NO (the default)
+
+HAVE_DOT               = NO
+
+# The DOT_NUM_THREADS specifies the number of dot invocations doxygen is
+# allowed to run in parallel. When set to 0 (the default) doxygen will
+# base this on the number of processors available in the system. You can set it
+# explicitly to a value larger than 0 to get control over the balance
+# between CPU load and processing speed.
+
+DOT_NUM_THREADS        = 0
+
+# By default doxygen will use the Helvetica font for all dot files that
+# doxygen generates. When you want a differently looking font you can specify
+# the font name using DOT_FONTNAME. You need to make sure dot is able to find
+# the font, which can be done by putting it in a standard location or by setting
+# the DOTFONTPATH environment variable or by setting DOT_FONTPATH to the
+# directory containing the font.
+
+DOT_FONTNAME           = Helvetica
+
+# The DOT_FONTSIZE tag can be used to set the size of the font of dot graphs.
+# The default size is 10pt.
+
+DOT_FONTSIZE           = 10
+
+# By default doxygen will tell dot to use the Helvetica font.
+# If you specify a different font using DOT_FONTNAME you can use DOT_FONTPATH to
+# set the path where dot can find it.
+
+DOT_FONTPATH           =
+
+# If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for each documented class showing the direct and
+# indirect inheritance relations. Setting this tag to YES will force the
+# CLASS_DIAGRAMS tag to NO.
+
+CLASS_GRAPH            = YES
+
+# If the COLLABORATION_GRAPH and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for each documented class showing the direct and
+# indirect implementation dependencies (inheritance, containment, and
+# class references variables) of the class with other documented classes.
+
+COLLABORATION_GRAPH    = YES
+
+# If the GROUP_GRAPHS and HAVE_DOT tags are set to YES then doxygen
+# will generate a graph for groups, showing the direct groups dependencies
+
+GROUP_GRAPHS           = YES
+
+# If the UML_LOOK tag is set to YES doxygen will generate inheritance and
+# collaboration diagrams in a style similar to the OMG's Unified Modeling
+# Language.
+
+UML_LOOK               = NO
+
+# If the UML_LOOK tag is enabled, the fields and methods are shown inside
+# the class node. If there are many fields or methods and many nodes the
+# graph may become too big to be useful. The UML_LIMIT_NUM_FIELDS
+# threshold limits the number of items for each type to make the size more
+# managable. Set this to 0 for no limit. Note that the threshold may be
+# exceeded by 50% before the limit is enforced.
+
+UML_LIMIT_NUM_FIELDS   = 10
+
+# If set to YES, the inheritance and collaboration graphs will show the
+# relations between templates and their instances.
+
+TEMPLATE_RELATIONS     = NO
+
+# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDE_GRAPH, and HAVE_DOT
+# tags are set to YES then doxygen will generate a graph for each documented
+# file showing the direct and indirect include dependencies of the file with
+# other documented files.
+
+INCLUDE_GRAPH          = YES
+
+# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDED_BY_GRAPH, and
+# HAVE_DOT tags are set to YES then doxygen will generate a graph for each
+# documented header file showing the documented files that directly or
+# indirectly include this file.
+
+INCLUDED_BY_GRAPH      = YES
+
+# If the CALL_GRAPH and HAVE_DOT options are set to YES then
+# doxygen will generate a call dependency graph for every global function
+# or class method. Note that enabling this option will significantly increase
+# the time of a run. So in most cases it will be better to enable call graphs
+# for selected functions only using the \callgraph command.
+
+CALL_GRAPH             = NO
+
+# If the CALLER_GRAPH and HAVE_DOT tags are set to YES then
+# doxygen will generate a caller dependency graph for every global function
+# or class method. Note that enabling this option will significantly increase
+# the time of a run. So in most cases it will be better to enable caller
+# graphs for selected functions only using the \callergraph command.
+
+CALLER_GRAPH           = NO
+
+# If the GRAPHICAL_HIERARCHY and HAVE_DOT tags are set to YES then doxygen
+# will generate a graphical hierarchy of all classes instead of a textual one.
+
+GRAPHICAL_HIERARCHY    = YES
+
+# If the DIRECTORY_GRAPH, SHOW_DIRECTORIES and HAVE_DOT tags are set to YES
+# then doxygen will show the dependencies a directory has on other directories
+# in a graphical way. The dependency relations are determined by the #include
+# relations between the files in the directories.
+
+DIRECTORY_GRAPH        = YES
+
+# The DOT_IMAGE_FORMAT tag can be used to set the image format of the images
+# generated by dot. Possible values are svg, png, jpg, or gif.
+# If left blank png will be used. If you choose svg you need to set
+# HTML_FILE_EXTENSION to xhtml in order to make the SVG files
+# visible in IE 9+ (other browsers do not have this requirement).
+
+DOT_IMAGE_FORMAT       = png
+
+# If DOT_IMAGE_FORMAT is set to svg, then this option can be set to YES to
+# enable generation of interactive SVG images that allow zooming and panning.
+# Note that this requires a modern browser other than Internet Explorer.
+# Tested and working are Firefox, Chrome, Safari, and Opera. For IE 9+ you
+# need to set HTML_FILE_EXTENSION to xhtml in order to make the SVG files
+# visible. Older versions of IE do not have SVG support.
+
+INTERACTIVE_SVG        = NO
+
+# The tag DOT_PATH can be used to specify the path where the dot tool can be
+# found. If left blank, it is assumed the dot tool can be found in the path.
+
+DOT_PATH               =
+
+# The DOTFILE_DIRS tag can be used to specify one or more directories that
+# contain dot files that are included in the documentation (see the
+# \dotfile command).
+
+DOTFILE_DIRS           =
+
+# The MSCFILE_DIRS tag can be used to specify one or more directories that
+# contain msc files that are included in the documentation (see the
+# \mscfile command).
+
+MSCFILE_DIRS           =
+
+# The DOT_GRAPH_MAX_NODES tag can be used to set the maximum number of
+# nodes that will be shown in the graph. If the number of nodes in a graph
+# becomes larger than this value, doxygen will truncate the graph, which is
+# visualized by representing a node as a red box. Note that doxygen if the
+# number of direct children of the root node in a graph is already larger than
+# DOT_GRAPH_MAX_NODES then the graph will not be shown at all. Also note
+# that the size of a graph can be further restricted by MAX_DOT_GRAPH_DEPTH.
+
+DOT_GRAPH_MAX_NODES    = 50
+
+# The MAX_DOT_GRAPH_DEPTH tag can be used to set the maximum depth of the
+# graphs generated by dot. A depth value of 3 means that only nodes reachable
+# from the root by following a path via at most 3 edges will be shown. Nodes
+# that lay further from the root node will be omitted. Note that setting this
+# option to 1 or 2 may greatly reduce the computation time needed for large
+# code bases. Also note that the size of a graph can be further restricted by
+# DOT_GRAPH_MAX_NODES. Using a depth of 0 means no depth restriction.
+
+MAX_DOT_GRAPH_DEPTH    = 0
+
+# Set the DOT_TRANSPARENT tag to YES to generate images with a transparent
+# background. This is disabled by default, because dot on Windows does not
+# seem to support this out of the box. Warning: Depending on the platform used,
+# enabling this option may lead to badly anti-aliased labels on the edges of
+# a graph (i.e. they become hard to read).
+
+DOT_TRANSPARENT        = NO
+
+# Set the DOT_MULTI_TARGETS tag to YES allow dot to generate multiple output
+# files in one run (i.e. multiple -o and -T options on the command line). This
+# makes dot run faster, but since only newer versions of dot (>1.8.10)
+# support this, this feature is disabled by default.
+
+DOT_MULTI_TARGETS      = NO
+
+# If the GENERATE_LEGEND tag is set to YES (the default) Doxygen will
+# generate a legend page explaining the meaning of the various boxes and
+# arrows in the dot generated graphs.
+
+GENERATE_LEGEND        = YES
+
+# If the DOT_CLEANUP tag is set to YES (the default) Doxygen will
+# remove the intermediate dot files that are used to generate
+# the various graphs.
+
+DOT_CLEANUP            = YES
diff --git a/Makefile b/Makefile
new file mode 100644 (file)
index 0000000..639f51a
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,94 @@
+include common.mk
+
+PHONY += directories
+MKDIR_P = mkdir -p
+TSO_DIR = build_tso
+SC_DIR = build_sc
+
+CPP_SOURCES := mymemory.cc context.cc snapshot.cc snapshot-interface.cc libinterface.cc execpoint.cc main.cc cmodelint.cc eprecord.cc epvalue.cc mcexecution.cc model.cc libthreads.cc mcschedule.cc common.cc threads.cc planner.cc cgoal.cc change.cc constgen.cc constraint.cc branchrecord.cc valuerecord.cc storeloadset.cc functionrecord.cc loadrf.cc schedulebuilder.cc equalsrecord.cc inc_solver.cc
+C_SOURCES := malloc.c
+
+TSO_OBJECTS := $(CPP_SOURCES:%.cc=$(TSO_DIR)/%.o) $(C_SOURCES:%.c=$(TSO_DIR)/%.o)
+SC_OBJECTS := $(CPP_SOURCES:%.cc=$(SC_DIR)/%.o) $(C_SOURCES:%.c=$(SC_DIR)/%.o)
+
+CPPFLAGS += -Iinclude -I.
+LDFLAGS := -ldl -lrt -rdynamic
+SHARED := -shared
+
+# Mac OSX options
+ifeq ($(UNAME), Darwin)
+LDFLAGS := -ldl
+SHARED := -Wl,-undefined,dynamic_lookup -dynamiclib
+endif
+
+TESTS_DIR := test
+
+MARKDOWN := doc/Markdown/Markdown.pl
+
+all: directories $(TSO_LIB_SO) $(SC_LIB_SO)
+
+directories: ${TSO_DIR} ${SC_DIR}
+
+${TSO_DIR}:
+       ${MKDIR_P} ${TSO_DIR}
+
+${SC_DIR}:
+       ${MKDIR_P} ${SC_DIR}
+
+debug: CPPFLAGS += -DCONFIG_DEBUG
+debug: all
+
+PHONY += docs
+docs: *.c *.cc *.h
+       doxygen
+
+$(TSO_LIB_SO): $(TSO_OBJECTS)
+       $(CXX) -g $(SHARED) -o $(TSO_LIB_SO) $+ $(LDFLAGS)
+
+$(SC_LIB_SO): $(SC_OBJECTS)
+       $(CXX) -g $(SHARED) -o $(SC_LIB_SO) $+ $(LDFLAGS)
+
+${TSO_DIR}/%.o: %.c
+       $(CC) -fPIC -c $< -o $@ -DTSO -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable
+
+${TSO_DIR}/%.o: %.cc
+       $(CXX) -MMD -DTSO -MF $@.d -o $@ -fPIC -c $< $(CPPFLAGS)
+
+${SC_DIR}/%.o: %.c
+       $(CC) -fPIC -c $< -o $@ -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable
+
+${SC_DIR}/%.o: %.cc
+       $(CXX) -MMD -MF $@.d -fPIC -o $@ -c $< $(CPPFLAGS)
+
+%.pdf: %.dot
+       dot -Tpdf $< -o $@
+
+-include $(TSO_OBJECTS:%=$TSO_DIR/.%.d)
+-include $(SC_OBJECTS:%=$SC_DIR/.%.d)
+
+PHONY += clean
+clean:
+       rm -f *.o *.so *.pdf *.dot dimacs.cnf dimacs.out
+       rm -rf $(TSO_DIR) $(SC_DIR)
+       $(MAKE) -C $(TESTS_DIR) clean
+
+PHONY += mrclean
+mrclean: clean
+       rm -rf docs
+
+PHONY += tags
+tags:
+       ctags -R
+
+PHONE += tests
+tests: $(LIB_SO)
+       $(MAKE) -C $(TESTS_DIR)
+
+PHONY += pdfs
+pdfs: $(patsubst %.dot,%.pdf,$(wildcard *.dot))
+
+.PHONY: $(PHONY)
+
+# A 1-inch margin PDF generated by 'pandoc'
+%.pdf: %.md
+       pandoc -o $@ $< -V header-includes='\usepackage[margin=1in]{geometry}'
diff --git a/benchmarks/.gitignore b/benchmarks/.gitignore
new file mode 100644 (file)
index 0000000..114a7ac
--- /dev/null
@@ -0,0 +1,4 @@
+log
+logall
+
+
diff --git a/benchmarks/cdschecker/dekker/bench.sh b/benchmarks/cdschecker/dekker/bench.sh
new file mode 100755 (executable)
index 0000000..79f6f7a
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+for i in 1 2 3 4 5 6
+do
+echo size= $i
+cat dekker-fences.cc.in | sed s/PROBLEMSIZE/$i/ > dekker-fences.cc
+g++ dekker-fences.cc -O3 -I$CDSCHECKERDIR/include -L$CDSCHECKERDIR -lmodel -o dekker-fences.o
+export LD_LIBRARY_PATH=$CDSCHECKERDIR
+time ./dekker-fences.o -Y
+done
diff --git a/benchmarks/cdschecker/dekker/dekker-fences.cc.in b/benchmarks/cdschecker/dekker/dekker-fences.cc.in
new file mode 100644 (file)
index 0000000..72c30a9
--- /dev/null
@@ -0,0 +1,88 @@
+/*
+ * Dekker's critical section algorithm, implemented with fences.
+ *
+ * URL:
+ *   http://www.justsoftwaresolutions.co.uk/threading/
+ */
+
+#include <atomic>
+#include <threads.h>
+
+#include "librace.h"
+
+std::atomic<bool> flag0, flag1;
+std::atomic<int> turn;
+std::atomic<int> var;
+
+void p0() {
+       flag0.store(true);
+
+       while (flag1.load()) {
+               if (turn.load() !=0)
+               {
+                       flag0.store(false);
+                       while (turn.load() != 0) {
+                               thrd_yield();
+                       }
+                       flag0.store(true);
+               } else
+                       thrd_yield();
+       }
+
+       // critical section
+       var.store(1);
+
+       turn.store(1);
+       flag0.store(false);
+}
+
+void p1() {
+       flag1.store(true);
+
+       while (flag0.load()) {
+               if (turn.load() != 1) {
+                       flag1.store(false);
+                       while (turn.load() != 1) {
+                               thrd_yield();
+                       }
+                       flag1.store(true);
+               } else
+                       thrd_yield();
+       }
+       
+       // critical section
+       var.store(2);
+
+       turn.store(0);
+       flag1.store(false);
+}
+
+void p0l(void *arg) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               p0();
+}
+
+void p1l(void *arg) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               p1();
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t a, b;
+
+       flag0 = false;
+       flag1 = false;
+       turn = 0;
+       var=0;
+       
+       thrd_create(&a, p0l, NULL);
+       thrd_create(&b, p1l, NULL);
+
+       thrd_join(a);
+       thrd_join(b);
+
+       return 0;
+}
diff --git a/benchmarks/cdschecker/linuxlock/bench.sh b/benchmarks/cdschecker/linuxlock/bench.sh
new file mode 100755 (executable)
index 0000000..14c7275
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+for i in 1 2 3 4 5 6 7 8 9
+do
+echo size= $i
+cat linuxlocks.c.in | sed s/PROBLEMSIZE/$i/ > linuxlocks.c
+gcc linuxlocks.c -O3 -I$CDSCHECKERDIR/include -L$CDSCHECKERDIR -lmodel -o linuxlocks.o
+export LD_LIBRARY_PATH=$CDSCHECKERDIR
+time ./linuxlocks.o 
+done
\ No newline at end of file
diff --git a/benchmarks/cdschecker/linuxlock/linuxlocks.c.in b/benchmarks/cdschecker/linuxlock/linuxlocks.c.in
new file mode 100644 (file)
index 0000000..3b62f4b
--- /dev/null
@@ -0,0 +1,54 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       atomic_int lock;
+} lock_t;
+
+static inline bool write_trylock(lock_t *rw) {
+       int oldvalue=0;
+       return atomic_compare_exchange_strong(&rw->lock, &oldvalue, 1);
+}
+
+
+static inline void write_unlock(lock_t *rw)
+{
+       atomic_store(&rw->lock, 0);
+}
+
+lock_t mylock;
+int shareddata;
+
+static void foo() {
+       bool flag=write_trylock(&mylock);
+       if (flag) {
+               write_unlock(&mylock);
+       }
+}
+
+static void a(void *obj)
+{
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               foo();
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t1, t2;
+       atomic_init(&mylock.lock, 0);
+       
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+
+       return 0;
+}
diff --git a/benchmarks/cdschecker/linuxrwlock/bench.sh b/benchmarks/cdschecker/linuxrwlock/bench.sh
new file mode 100755 (executable)
index 0000000..75bce72
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+for i in 1 2 3 4 5 6 7
+do
+echo size= $i
+cat linuxrwlocks.c.in | sed s/PROBLEMSIZE/$i/ > linuxrwlocks.c
+gcc linuxrwlocks.c -O3 -I$CDSCHECKERDIR/include -L$CDSCHECKERDIR -lmodel -o linuxrwlocks.o
+export LD_LIBRARY_PATH=$CDSCHECKERDIR
+time ./linuxrwlocks.o 
+done
\ No newline at end of file
diff --git a/benchmarks/cdschecker/linuxrwlock/linuxrwlocks.c.in b/benchmarks/cdschecker/linuxrwlock/linuxrwlocks.c.in
new file mode 100644 (file)
index 0000000..5fa4a08
--- /dev/null
@@ -0,0 +1,56 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "librace.h"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       atomic_int lock;
+} rwlock_t;
+
+static inline int write_trylock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_seq_cst);
+       if (priorvalue == RW_LOCK_BIAS)
+               return 1;
+
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_seq_cst);
+       return 0;
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add_explicit(&rw->lock, RW_LOCK_BIAS, memory_order_seq_cst);
+}
+
+rwlock_t mylock;
+int shareddata;
+
+static void a(void *obj) {
+       int i;
+       for(i = 0; i < PROBLEMSIZE; i++) {
+               if (write_trylock(&mylock)) {
+                       write_unlock(&mylock);
+               }
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t1, t2;
+       atomic_init(&mylock.lock, RW_LOCK_BIAS);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+
+       return 0;
+}
diff --git a/benchmarks/cdschecker/msqueue/bench.sh b/benchmarks/cdschecker/msqueue/bench.sh
new file mode 100755 (executable)
index 0000000..790d8c7
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+for i in 1 2 3 4 5 6 7 8
+do
+echo size= $i
+cat ms-queue_simple.c.in | sed s/PROBLEMSIZE/$i/ > ms-queue_simple.c
+gcc ms-queue_simple.c -O3 -I$CDSCHECKERDIR/include -L$CDSCHECKERDIR -lmodel -o ms-queue_simple.o
+export LD_LIBRARY_PATH=$CDSCHECKERDIR
+time ./ms-queue_simple.o
+done
diff --git a/benchmarks/cdschecker/msqueue/ms-queue_simple.c.in b/benchmarks/cdschecker/msqueue/ms-queue_simple.c.in
new file mode 100644 (file)
index 0000000..8e0e463
--- /dev/null
@@ -0,0 +1,107 @@
+#include <threads.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <stdatomic.h>
+#define true 1
+#define false 0
+
+
+#include "ms-queue_simple.h"
+
+queue_t queue;
+void init_queue(queue_t *q, int num_threads);
+void enqueue(queue_t *q, unsigned int val);
+bool dequeue(queue_t *q, unsigned int *retVal);
+
+void init_queue(queue_t *q, int num_threads) {
+       struct node *newnode=malloc(sizeof (struct node));
+       atomic_store(&newnode->value, 0);
+
+       atomic_store(&newnode->next, (uintptr_t) NULL);
+               /* initialize queue */
+       atomic_store(&q->head, newnode);
+       
+       atomic_store(&q->tail, newnode);
+}
+
+void enqueue(queue_t *q, unsigned int val) {
+       struct node *tail;
+       struct node * node_ptr = malloc(sizeof(struct node));
+       atomic_store(&node_ptr->value, val);
+       
+       atomic_store(&node_ptr->next, NULL);
+       
+       while (true) {
+               tail = (struct node *) atomic_load(&q->tail);
+               
+               struct node * next = (struct node *) atomic_load( &tail->next);
+               
+               struct node * qtail = (struct node *) atomic_load(&q->tail);
+               if (tail == qtail) {
+                       
+                       if (next == NULL) {
+                               if (atomic_compare_exchange_strong( & tail->next,& next, node_ptr))
+                                       break;
+                       }
+               }
+               struct node * new_tailptr = (struct node *)atomic_load( &tail->next);
+               atomic_compare_exchange_strong(&q->tail, & tail, new_tailptr);
+               thrd_yield();
+       }
+       atomic_compare_exchange_strong(&q->tail, & tail, node_ptr);
+}
+
+bool dequeue(queue_t *q, unsigned int *retVal) {
+       while (true) {
+               struct node * head = (struct node *) atomic_load(&q->head);
+               struct node * tail = (struct node *) atomic_load(&q->tail);
+               struct node * next = (struct node *) atomic_load(&head->next);
+               
+               int t = ((struct node *) atomic_load(&q->head)) == head;
+               if (t) {
+                       if (head == tail) {
+
+                               if (next == NULL) {
+                                       return false; // NULL
+                               }
+                               atomic_compare_exchange_strong(&q->tail, & tail, next);
+                               thrd_yield();
+                       } else {
+                               *retVal = atomic_load(&next->value);
+                               if (atomic_compare_exchange_strong(&q->head,& head, next)) {
+                                       return true;
+                               } else {
+                                       thrd_yield();
+                               }
+                       }
+               }
+       }
+}
+
+static void e(void *param)
+{
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               enqueue(&queue, 1);
+}
+
+static void d(void *param) {
+       int val,i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               dequeue(&queue, &val);
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       // MODEL_ASSERT(queue);
+
+       init_queue(&queue, 2);
+
+       thrd_t t1,t2;
+       thrd_create(&t1, e, NULL);
+       thrd_create(&t2, d, NULL);
+
+
+       return 0;
+}
diff --git a/benchmarks/cdschecker/msqueue/ms-queue_simple.h b/benchmarks/cdschecker/msqueue/ms-queue_simple.h
new file mode 100644 (file)
index 0000000..1d20dfb
--- /dev/null
@@ -0,0 +1,15 @@
+typedef struct node {
+       atomic_int value;
+       atomic_address next;
+} node_t;
+
+typedef struct {
+       atomic_address head;
+       atomic_address tail;
+} queue_t;
+
+//void init_queue(queue_t *q, int num_threads);
+//void enqueue(queue_t *q, unsigned int val);
+//bool dequeue(queue_t *q, unsigned int *retVal);
+int get_thread_num();
+
diff --git a/benchmarks/cdschecker/path.sh b/benchmarks/cdschecker/path.sh
new file mode 100755 (executable)
index 0000000..d83a569
--- /dev/null
@@ -0,0 +1 @@
+CDSCHECKERDIR=~/research/model-checker/
diff --git a/benchmarks/cdschecker/seqlock/bench.sh b/benchmarks/cdschecker/seqlock/bench.sh
new file mode 100755 (executable)
index 0000000..7a65854
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+for i in 1 2 3 4
+do
+echo size= $i
+cat seqlock.c.in | sed s/PROBLEMSIZE/$i/ > seqlock.c
+gcc seqlock.c -O3 -I$CDSCHECKERDIR/include -L$CDSCHECKERDIR -lmodel -o seqlock.o
+export LD_LIBRARY_PATH=$CDSCHECKERDIR
+time ./seqlock.o -Y
+done
\ No newline at end of file
diff --git a/benchmarks/cdschecker/seqlock/seqlock.c.in b/benchmarks/cdschecker/seqlock/seqlock.c.in
new file mode 100644 (file)
index 0000000..52e4d8d
--- /dev/null
@@ -0,0 +1,77 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+#include "threads.h"
+
+atomic_int _seq;
+atomic_int _data;
+
+void seqlock_init() {
+       atomic_store(&_seq, 0);
+       atomic_store(&_data, 0);
+}
+
+int seqlock_read() {
+       int old_seq = atomic_load(&_seq);
+       
+       int c0 = (old_seq % 2 == 1);
+       if (!c0) {
+               int res = atomic_load(&_data);
+               int seq = atomic_load(&_seq);
+    
+               int c1;
+               c1 = seq == old_seq;
+               if (c1) { // relaxed
+                       return res;
+               }
+       }
+       return -1;
+}
+
+int seqlock_write(int new_data) {
+       int old_seq = atomic_load(&_seq);
+       int c2 = (old_seq % 2 == 1);
+       if (!c2) {
+               int new_seq = old_seq + 1;
+               if (atomic_compare_exchange_strong(&_seq, &old_seq, new_seq)) {
+                       atomic_store(&_data, new_data);
+                       atomic_fetch_add(&_seq, 1);
+                       return true;
+               }
+       }
+       return false;
+}
+
+static void a(void *obj) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               seqlock_write(3);
+}
+
+static void b(void *obj) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               int r1=seqlock_read();
+       }
+}
+
+static void c(void *obj) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               int r1=seqlock_read();
+       }
+}
+
+int user_main(int argc, char **argv) {
+       thrd_t t1; thrd_t t2; thrd_t t3;
+       seqlock_init();
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&b, NULL);
+       thrd_create(&t3, (thrd_start_t)&c, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       thrd_join(t3);
+       return 0;
+}
diff --git a/benchmarks/checkfence/dekker/bench.sh b/benchmarks/checkfence/dekker/bench.sh
new file mode 100755 (executable)
index 0000000..ffe72ce
--- /dev/null
@@ -0,0 +1,14 @@
+#!/bin/bash
+source ../paths.sh
+
+for i in 1 2 3 4 5 6 7 8 9 10
+do 
+echo size=$i
+cat dekker-fences.c.in | sed s/PROBLEMSIZE/$i/ > dekker-fences.c
+c2lsl.exe dekker-fences.c dekker-fences.lsl
+time checkfence -i -a memmodel=sc dekker-fences.lsl dekkertests.lsl >> runlog
+echo With loop bounds
+time checkfence -a memmodel=sc dekker-fences.lsl dekkertests.lsl T0.prn >> runlog
+done
+
+
diff --git a/benchmarks/checkfence/dekker/clean.sh b/benchmarks/checkfence/dekker/clean.sh
new file mode 100755 (executable)
index 0000000..1e76a49
--- /dev/null
@@ -0,0 +1,8 @@
+#!/bin/bash
+rm T0.*.htm
+rm T0.bsc*
+rm T0.prn
+rm dekker-fences.c
+rm dekker-fences.i
+rm dekker-fences.lsl
+rm runlog
diff --git a/benchmarks/checkfence/dekker/dekker-fences.c.in b/benchmarks/checkfence/dekker/dekker-fences.c.in
new file mode 100644 (file)
index 0000000..877856a
--- /dev/null
@@ -0,0 +1,75 @@
+#include "lsl_protos.h"
+/*
+ * Dekker's critical section algorithm, implemented with fences.
+ *
+ * URL:
+ *   http://www.justsoftwaresolutions.co.uk/threading/
+ */
+
+
+int flag0, flag1;
+int turn;
+
+int var = 0;
+
+void p0() {
+       flag0 = 1;
+
+       while (flag1) {
+               if (turn != 0) {
+                       flag0=0;
+                       while (turn != 0) {
+                               lsl_assume(false);
+                       }
+                       flag0=1;
+               } else {
+                               lsl_assume(false);
+               }
+       }
+
+       // critical section
+       var=1;
+
+       turn=1;
+       flag0=0;
+}
+
+void p1() {
+       flag1=1;
+
+       while (flag0) {
+               if (turn != 1) {
+                       flag1=0;
+                       while (turn!=1) {
+                               lsl_assume(false);
+                       }
+                       flag1=1;
+               } else {
+                               lsl_assume(false);
+               }
+       }
+       // critical section
+       var=2;
+       turn=0;
+       flag1=0;
+}
+
+void init() {
+       flag0=0;
+       flag1=0;
+       turn=0;
+}
+
+void p0l() {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p0();
+       }
+}
+
+void p1l() {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p1();
+       }
+}
diff --git a/benchmarks/checkfence/dekker/dekkertests.lsl b/benchmarks/checkfence/dekker/dekkertests.lsl
new file mode 100644 (file)
index 0000000..3786396
--- /dev/null
@@ -0,0 +1 @@
+test T0 = init (p0l | p1l )
diff --git a/benchmarks/checkfence/linuxlock/bench.sh b/benchmarks/checkfence/linuxlock/bench.sh
new file mode 100755 (executable)
index 0000000..dc030d9
--- /dev/null
@@ -0,0 +1,14 @@
+#!/bin/bash
+source ../paths.sh
+
+for i in 1 2 3 4 5 6 7 8 9 10 15 20 30 40 50 60
+do 
+echo size=$i
+cat linuxrwlocksbig.c.in | sed s/PROBLEMSIZE/$i/ > linuxrwlocksbig.c
+c2lsl.exe lin_harness.c lin_harness.lsl
+time checkfence -i -a memmodel=sc lin_harness.lsl locktests.lsl >> runlog
+echo With loop bounds
+time checkfence -a memmodel=sc lin_harness.lsl locktests.lsl T0.prn >> runlog
+done
+
+
diff --git a/benchmarks/checkfence/linuxlock/clean.sh b/benchmarks/checkfence/linuxlock/clean.sh
new file mode 100755 (executable)
index 0000000..e431fb1
--- /dev/null
@@ -0,0 +1,8 @@
+#!/bin/bash
+rm T0.*.htm
+rm T0.bsc*
+rm T0.prn
+rm lin_harness.i
+rm lin_harness.lsl
+rm linuxrwlocksbig.c
+rm runlog
\ No newline at end of file
diff --git a/benchmarks/checkfence/linuxlock/lin_harness.c b/benchmarks/checkfence/linuxlock/lin_harness.c
new file mode 100755 (executable)
index 0000000..592dc31
--- /dev/null
@@ -0,0 +1,18 @@
+#include "linuxrwlocksbig.c"
+
+/* ---- harness for queue ---- */
+
+rwlock_t mylock;
+
+void i() 
+{
+  lock_init(&mylock);
+}
+void e()
+{
+  bar(&mylock);
+}
+void d()
+{
+  bar(&mylock);
+}
diff --git a/benchmarks/checkfence/linuxlock/linuxrwlocksbig.c.in b/benchmarks/checkfence/linuxlock/linuxrwlocksbig.c.in
new file mode 100644 (file)
index 0000000..3e3cf11
--- /dev/null
@@ -0,0 +1,38 @@
+#include "lsl_protos.h"
+
+
+#define RW_LOCK_BIAS            0x001000
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef struct rwlock {
+       int lock;
+} rwlock_t;
+
+
+void lock_init(rwlock_t *lock) {
+  lock->lock=0;
+}
+
+int write_trylock(rwlock_t *rw) {
+  return lsl_cas_32(&rw->lock, 0, 1);
+}
+
+
+void write_unlock(rwlock_t *rw) {
+  rw->lock=0;
+}
+
+void foo(rwlock_t *mylock) {
+       int flag=write_trylock(mylock);
+       if (flag) {
+               write_unlock(mylock);
+       }
+}
+
+void bar(rwlock_t *mylock) 
+{  
+       for(int i=0;i<PROBLEMSIZE;i++) 
+               foo(mylock);
+}
diff --git a/benchmarks/checkfence/linuxlock/locktests.lsl b/benchmarks/checkfence/linuxlock/locktests.lsl
new file mode 100644 (file)
index 0000000..3140cda
--- /dev/null
@@ -0,0 +1 @@
+test T0 = i (e | d )
diff --git a/benchmarks/checkfence/linuxrwlock/add_harness.c b/benchmarks/checkfence/linuxrwlock/add_harness.c
new file mode 100755 (executable)
index 0000000..b339149
--- /dev/null
@@ -0,0 +1,18 @@
+#include "llock.c"
+
+/* ---- harness for queue ---- */
+
+rwlock_t mylock;
+
+void i() 
+{
+  lock_init(&mylock);
+}
+void e()
+{
+  bar(&mylock);
+}
+void d()
+{
+  bar(&mylock);
+}
diff --git a/benchmarks/checkfence/linuxrwlock/bench.sh b/benchmarks/checkfence/linuxrwlock/bench.sh
new file mode 100755 (executable)
index 0000000..f0fc17c
--- /dev/null
@@ -0,0 +1,26 @@
+#!/bin/bash
+source ../paths.sh
+
+
+#for i in 1 2 3 4 5 6 7 8 9 10 15
+#do 
+#echo bias set to 0x100
+#echo size=$i
+#cat llock.c.in | sed s/PROBLEMSIZE/$i/ |sed s/TUNELOCK/0x100/ > llock.c
+#c2lsl.exe add_harness.c add_harness.lsl
+#time checkfence -i -a memmodel=sc add_harness.lsl locktests.lsl >> runlog
+#echo Hard loop bounds
+#time checkfence -a memmodel=sc add_harness.lsl locktests.lsl T0.prn >> runlog
+#done
+
+
+for i in 1 2 3 4 5 6 7 8 9 10 15 20 30
+do 
+echo bias set to 100
+echo size=$i
+cat llock.c.in | sed s/PROBLEMSIZE/$i/ |sed s/TUNELOCK/100/ > llock.c
+c2lsl.exe add_harness.c add_harness.lsl
+time checkfence -i -a memmodel=sc add_harness.lsl locktests.lsl >> runlog
+echo Hard loop bounds
+time checkfence -a memmodel=sc add_harness.lsl locktests.lsl T0.prn >> runlog
+done
diff --git a/benchmarks/checkfence/linuxrwlock/clean.sh b/benchmarks/checkfence/linuxrwlock/clean.sh
new file mode 100755 (executable)
index 0000000..fdb1b8e
--- /dev/null
@@ -0,0 +1,8 @@
+#!/bin/bash
+rm T0.*.htm
+rm T0.bsc*
+rm T0.prn
+rm add_harness.i
+rm add_harness.lsl
+rm llock.c
+rm runlog
\ No newline at end of file
diff --git a/benchmarks/checkfence/linuxrwlock/llock.c.in b/benchmarks/checkfence/linuxrwlock/llock.c.in
new file mode 100644 (file)
index 0000000..dd44768
--- /dev/null
@@ -0,0 +1,53 @@
+#include "lsl_protos.h"
+
+
+#define RW_LOCK_BIAS        TUNELOCK
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef struct rwlock {
+       int lock;
+} rwlock_t;
+
+
+void lock_init(rwlock_t *lock) {
+  lock->lock=RW_LOCK_BIAS;
+}
+
+int add(int * ptr, int val) {
+  return lsl_add_32(ptr, val);
+} 
+
+int sub(int * ptr, int val) {
+  return lsl_add_32(ptr, -val);
+} 
+
+int write_trylock(rwlock_t *rw) {
+       int priorvalue=sub(&rw->lock, RW_LOCK_BIAS);
+
+       int flag=priorvalue != RW_LOCK_BIAS;
+
+       if (!flag) {
+               add(&rw->lock, RW_LOCK_BIAS);
+       }
+
+       return flag;
+}
+
+
+void write_unlock(rwlock_t *rw) {
+       add(&rw->lock, RW_LOCK_BIAS);
+}
+
+void foo(rwlock_t *mylock) {
+       int flag=write_trylock(mylock);
+       if (flag) {
+               write_unlock(mylock);
+       }
+}
+
+void bar(rwlock_t *mylock) {
+       for(int i=0;i<PROBLEMSIZE;i++)
+               foo(mylock);
+}
diff --git a/benchmarks/checkfence/linuxrwlock/locktests.lsl b/benchmarks/checkfence/linuxrwlock/locktests.lsl
new file mode 100644 (file)
index 0000000..3140cda
--- /dev/null
@@ -0,0 +1 @@
+test T0 = i (e | d )
diff --git a/benchmarks/checkfence/msqueue/bench.sh b/benchmarks/checkfence/msqueue/bench.sh
new file mode 100755 (executable)
index 0000000..8789e5c
--- /dev/null
@@ -0,0 +1,15 @@
+#!/bin/bash
+source ../paths.sh
+
+for i in 1 2 3 4 5 6 7 8 9
+do 
+echo size=$i
+cat msn_harness.c.in | sed s/PROBLEMSIZE/$i/ > msn_harness.c
+c2lsl.exe msn_harness.c msn_harness.lsl
+time checkfence -i -a memmodel=sc msn_harness.lsl tests.lsl >> runlog
+echo With loop bounds
+time checkfence -a memmodel=sc msn_harness.lsl tests.lsl T0.prn >> runlog
+done
+
+
+
diff --git a/benchmarks/checkfence/msqueue/clean.sh b/benchmarks/checkfence/msqueue/clean.sh
new file mode 100755 (executable)
index 0000000..442a691
--- /dev/null
@@ -0,0 +1,8 @@
+#!/bin/bash
+rm T0.*.htm
+rm T0.bsc*
+rm T0.prn
+rm msn_harness.i
+rm msn_harness.lsl
+rm msn_harness.c
+rm runlog
\ No newline at end of file
diff --git a/benchmarks/checkfence/msqueue/msn.c b/benchmarks/checkfence/msqueue/msn.c
new file mode 100755 (executable)
index 0000000..252e9fc
--- /dev/null
@@ -0,0 +1,72 @@
+#include "lsl_protos.h"
+
+/* ---- data types  ---- */
+
+typedef int value_t;
+
+typedef struct node {
+  struct node *next;
+  value_t value;
+} node_t;
+
+typedef struct queue {
+  node_t *head;
+  node_t *tail;
+} queue_t;
+
+/* ---- operations  ---- */
+
+void init_queue(queue_t *queue) 
+{
+  node_t *node = lsl_malloc_noreuse(sizeof(node_t));
+  node->next = 0;
+  queue->head = queue->tail = node;
+}
+
+void enqueue(queue_t *queue, value_t value)
+{
+  node_t *node;
+  node_t *tail;
+  node_t *next;
+
+  node = lsl_malloc_noreuse(sizeof(node_t));
+  node->value = value;
+  node->next = 0;
+  while (true) {
+    tail = queue->tail;
+    next = tail->next;
+    if (tail == queue->tail)
+      if (next == 0) {
+        if (lsl_cas_64(&tail->next, next, node))
+          break;
+      } else
+        lsl_cas_ptr(&queue->tail, tail, next);
+  }
+  lsl_cas_ptr(&queue->tail, tail, node);
+}
+
+boolean_t dequeue(queue_t *queue, value_t *pvalue)
+{
+  node_t *head;
+  node_t *tail;
+  node_t *next;
+
+  while (true) {
+    head = queue->head;
+    tail = queue->tail;
+    next = head->next;
+    if (head == queue->head) {
+      if (head == tail) {
+        if (next == 0)
+          return false;
+        lsl_cas_ptr(&queue->tail, tail, next);
+      } else {
+        *pvalue = next->value;
+        if (lsl_cas_ptr(&queue->head, head, next))
+          break;
+      } 
+    }
+  }
+  lsl_free_noreuse(head);
+  return true;
+}
diff --git a/benchmarks/checkfence/msqueue/msn_harness.c.in b/benchmarks/checkfence/msqueue/msn_harness.c.in
new file mode 100755 (executable)
index 0000000..69310eb
--- /dev/null
@@ -0,0 +1,21 @@
+#include "msn.c"
+
+queue_t queue;
+
+void i() 
+{
+  init_queue(&queue);
+}
+void e()
+{
+  value_t val = 1;
+       for(int i=0;i<PROBLEMSIZE;i++)
+               enqueue(&queue, val);
+}
+void d()
+{
+  boolean_t res;
+  value_t val;
+       for(int i=0;i<PROBLEMSIZE;i++)
+               res = dequeue(&queue, &val);
+}
diff --git a/benchmarks/checkfence/msqueue/tests.lsl b/benchmarks/checkfence/msqueue/tests.lsl
new file mode 100644 (file)
index 0000000..3b1ce84
--- /dev/null
@@ -0,0 +1 @@
+test T0 = i (e | d)
diff --git a/benchmarks/checkfence/paths.sh b/benchmarks/checkfence/paths.sh
new file mode 100644 (file)
index 0000000..726278a
--- /dev/null
@@ -0,0 +1,4 @@
+export C2LSL_HOME=~/checkfence/c2lsl/
+export PATH=~/checkfence/c2lsl/bin:$PATH
+export CHECKFENCE_HOME=~/checkfence/checkfence
+export PATH=~/checkfence/checkfence/run:$PATH
diff --git a/benchmarks/checkfence/seqlock/bench.sh b/benchmarks/checkfence/seqlock/bench.sh
new file mode 100755 (executable)
index 0000000..85243cf
--- /dev/null
@@ -0,0 +1,11 @@
+#!/bin/bash
+source ../paths.sh
+for i in 1 2 3 4 5 6 7 8 9 10 15 20 25 30 35 40
+do 
+echo size=$i
+cat seqlock.c.in | sed s/PROBLEMSIZE/$i/ > seqlock.c
+c2lsl.exe seqlock.c seqlock.lsl
+time checkfence -i -a memmodel=sc seqlock.lsl seqtests.lsl >> runlog
+echo Hard coded loop bound
+time checkfence -a memmodel=sc seqlock.lsl seqtests.lsl T0.prn >> runlog
+done
diff --git a/benchmarks/checkfence/seqlock/clean.sh b/benchmarks/checkfence/seqlock/clean.sh
new file mode 100755 (executable)
index 0000000..368ffa9
--- /dev/null
@@ -0,0 +1,8 @@
+#!/bin/bash
+rm T0.*.htm
+rm T0.bsc*
+rm T0.prn
+rm seqlock.c
+rm seqlock.lsl
+rm seqlock.i
+rm runlog
\ No newline at end of file
diff --git a/benchmarks/checkfence/seqlock/seqlock.c.in b/benchmarks/checkfence/seqlock/seqlock.c.in
new file mode 100644 (file)
index 0000000..e9690b9
--- /dev/null
@@ -0,0 +1,62 @@
+#include "lsl_protos.h"
+
+int _seq;
+int _data;
+
+void seqlock_init() {
+       _seq=0;
+       _data=0;
+}
+
+int seqlock_read() {
+       int old_seq = _seq;
+       
+       int c0 = (old_seq % 2 == 1);
+       if (!c0) {
+               int res = _data;
+               int seq = _seq;
+               
+               int c1;
+               c1 = seq == old_seq;
+               if (c1) { // relaxed
+                       return res;
+               }
+       }
+       return -1;
+}
+
+
+int seqlock_write(int new_data) {
+       int old_seq = _seq;
+       int c2 = (old_seq % 2 == 1);
+       if (!c2) {
+               int new_seq = old_seq + 1;
+               if (lsl_cas_32(&_seq, old_seq, new_seq)) {
+                       _data = new_data;
+                       lsl_add_32(&_seq, 1);
+                       return 1;
+               }
+       }
+       return 0;
+}
+
+void a() {
+       for(int i=0;i<PROBLEMSIZE;i++)
+               seqlock_write(3);
+}
+
+void b() {
+       for(int i=0;i<PROBLEMSIZE;i++) {
+               int r1 = seqlock_read();
+       }
+}
+
+void c() {
+       for(int i=0;i<PROBLEMSIZE;i++) {
+               int r1 = seqlock_read();
+       }
+}
+
+static void i() {
+       seqlock_init();
+}
diff --git a/benchmarks/checkfence/seqlock/seqtests.lsl b/benchmarks/checkfence/seqlock/seqtests.lsl
new file mode 100644 (file)
index 0000000..f3d2f9f
--- /dev/null
@@ -0,0 +1 @@
+test T0 = i (a | b | c)
diff --git a/benchmarks/compilesat b/benchmarks/compilesat
new file mode 100755 (executable)
index 0000000..0f3db28
--- /dev/null
@@ -0,0 +1,8 @@
+#!/bin/bash
+DIR=`pwd`
+
+for i in dekker linuxlock linuxrwlock msqueueoffset seqlock
+do
+(cd satcheck/$i; ./compile.sh )
+done
+
diff --git a/benchmarks/nidhugg/dekker/bench.sh b/benchmarks/nidhugg/dekker/bench.sh
new file mode 100755 (executable)
index 0000000..dff3eb0
--- /dev/null
@@ -0,0 +1,9 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+for i in 1 2 3 4 5 6
+do
+echo size= $i
+java -cp .. transform $i dekker-fences.cc.in dekker-fences.cc
+time nidhuggc -O3 -std=c++11 -- -sc ./dekker-fences.cc
+done
diff --git a/benchmarks/nidhugg/dekker/benchtso.sh b/benchmarks/nidhugg/dekker/benchtso.sh
new file mode 100755 (executable)
index 0000000..57fd545
--- /dev/null
@@ -0,0 +1,11 @@
+#!/bin/bash
+
+# 4 doesn't work because it takes too long
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+for i in 1 2 3 4 5 6
+do
+echo size= $i
+java -cp .. transform $i dekker-fences.cc.in dekker-fences.cc
+time nidhuggc -O3 -std=c++11 -- -tso ./dekker-fences.cc
+done
diff --git a/benchmarks/nidhugg/dekker/dekker-fences.cc.in b/benchmarks/nidhugg/dekker/dekker-fences.cc.in
new file mode 100644 (file)
index 0000000..2b466f5
--- /dev/null
@@ -0,0 +1,93 @@
+/*
+ * Dekker's critical section algorithm, implemented with fences.
+ *
+ * URL:
+ *   http://www.justsoftwaresolutions.co.uk/threading/
+ */
+
+#include <atomic>
+#include <pthread.h>
+
+std::atomic<bool> flag0, flag1;
+std::atomic<int> turn;
+std::atomic<int> var;
+
+extern "C" {
+void __VERIFIER_assume(int b);
+}
+
+void p0() {
+       flag0.store(true, std::memory_order_relaxed);
+
+       while (flag1.load()) {
+               if (turn.load() !=0)
+               {
+                       flag0.store(false, std::memory_order_relaxed);
+                       while (turn.load() != 0) {
+                               __VERIFIER_assume(0);
+                               //pthread_yield();
+                       }
+                       flag0.store(true, std::memory_order_relaxed);
+               } else
+                               __VERIFIER_assume(0);
+                       ;
+               //                      pthread_yield();
+       }
+
+       // critical section
+       var.store(1, std::memory_order_relaxed);
+
+       turn.store(1, std::memory_order_relaxed);
+       flag0.store(false, std::memory_order_relaxed);
+}
+
+void p1() {
+       flag1.store(true, std::memory_order_relaxed);
+
+       while (flag0.load()) {
+               if (turn.load() != 1) {
+                       flag1.store(false, std::memory_order_relaxed);
+                       while (turn.load() != 1) {
+                               __VERIFIER_assume(0);
+                               //pthread_yield();
+                       }
+                       flag1.store(true, std::memory_order_relaxed);
+               } else
+                       __VERIFIER_assume(0);
+                       ;//pthread_yield();
+       }
+       
+       // critical section
+       var.store(2, std::memory_order_relaxed);
+
+       turn.store(0, std::memory_order_relaxed);
+       flag1.store(false, std::memory_order_relaxed);
+}
+
+void * p0l(void *arg) {
+problemsize            p0();
+       return NULL;
+}
+
+void * p1l(void *arg) {
+problemsize            p1();
+       return NULL;
+}
+
+int main(int argc, char **argv)
+{
+       pthread_t a, b;
+
+       flag0 = false;
+       flag1 = false;
+       turn = 0;
+       var=0;
+       
+       pthread_create(&a, 0, p0l, NULL);
+       pthread_create(&b, 0, p1l, NULL);
+
+       pthread_join(a, 0);
+       pthread_join(b, 0);
+
+       return 0;
+}
diff --git a/benchmarks/nidhugg/linuxlock/bench.sh b/benchmarks/nidhugg/linuxlock/bench.sh
new file mode 100755 (executable)
index 0000000..8c9404b
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+
+for i in 1 2 3 4 5 6 7 8 9
+do
+echo size= $i
+java -cp .. transform $i linuxlocks.c.in linuxlocks.cc
+time nidhuggc -O3 -std=c++11 -- -sc ./linuxlocks.cc
+done
diff --git a/benchmarks/nidhugg/linuxlock/benchtso.sh b/benchmarks/nidhugg/linuxlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..a92b517
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+
+for i in 1 2 3 4 5 6 7 8 9
+do
+echo size= $i
+java -cp .. transform $i linuxlocks.c.in linuxlocks.cc
+time nidhuggc -O3 -std=c++11 -- -tso ./linuxlocks.cc
+done
diff --git a/benchmarks/nidhugg/linuxlock/linuxlocks.c.in b/benchmarks/nidhugg/linuxlock/linuxlocks.c.in
new file mode 100644 (file)
index 0000000..3929127
--- /dev/null
@@ -0,0 +1,55 @@
+#include <stdio.h>
+#include <pthread.h>
+#include <atomic>
+
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       std::atomic<int> lock;
+} lock_t;
+
+static inline bool write_trylock(lock_t *rw) {
+       int oldvalue=0;
+       //      return std::atomic_compare_exchange_strong(&rw->lock, &oldvalue, 1);
+       return rw->lock.compare_exchange_strong(oldvalue, 1);
+}
+
+
+static inline void write_unlock(lock_t *rw)
+{
+       atomic_store_explicit(&rw->lock, 0, std::memory_order_release);
+}
+
+lock_t mylock;
+int shareddata;
+
+static void foo() {
+       bool flag=write_trylock(&mylock);
+       if (flag) {
+               write_unlock(&mylock);
+       }
+}
+
+void * a(void *obj)
+{
+       int i;
+problemsize            foo();
+ return NULL;
+}
+
+int main(int argc, char **argv)
+{
+       pthread_t t1, t2;
+       mylock.lock=0;
+       
+
+       pthread_create(&t1, 0, a, NULL);
+       pthread_create(&t2, 0, a, NULL);
+
+       pthread_join(t1, 0);
+       pthread_join(t2, 0);
+
+       return 0;
+}
diff --git a/benchmarks/nidhugg/linuxrwlock/bench.sh b/benchmarks/nidhugg/linuxrwlock/bench.sh
new file mode 100755 (executable)
index 0000000..5b70978
--- /dev/null
@@ -0,0 +1,9 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+for i in 1 2 3 4 5 6 7
+do
+echo size= $i
+java -cp .. transform $i linuxrwlocks.c.in linuxrwlocks.cc
+time nidhuggc -O3 -std=c++11 -- -sc ./linuxrwlocks.cc
+done
diff --git a/benchmarks/nidhugg/linuxrwlock/benchtso.sh b/benchmarks/nidhugg/linuxrwlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..14c6cb2
--- /dev/null
@@ -0,0 +1,9 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+for i in 1 2 3 4 5 6 7
+do
+echo size= $i
+java -cp .. transform $i linuxrwlocks.c.in linuxrwlocks.cc
+time nidhuggc -O3 -std=c++11 -- -tso ./linuxrwlocks.cc
+done
diff --git a/benchmarks/nidhugg/linuxrwlock/linuxrwlocks.c.in b/benchmarks/nidhugg/linuxrwlock/linuxrwlocks.c.in
new file mode 100644 (file)
index 0000000..78c9423
--- /dev/null
@@ -0,0 +1,51 @@
+#include <stdio.h>
+#include <pthread.h>
+#include <atomic>
+
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       std::atomic<int> lock;
+} rwlock_t;
+
+static inline int write_trylock(rwlock_t *rw)
+{
+       int priorvalue = atomic_fetch_sub(&rw->lock, RW_LOCK_BIAS);
+       if (priorvalue == RW_LOCK_BIAS)
+               return 1;
+
+       atomic_fetch_add(&rw->lock, RW_LOCK_BIAS);
+       return 0;
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       atomic_fetch_add(&rw->lock, RW_LOCK_BIAS);
+}
+
+rwlock_t mylock;
+int shareddata;
+
+void * a(void *obj) {
+problemsize if (write_trylock(&mylock)) {write_unlock(&mylock);}
+ return NULL;
+}
+
+int main(int argc, char **argv)
+{
+       pthread_t t1, t2;
+       mylock.lock = RW_LOCK_BIAS;
+
+       pthread_create(&t1, 0, &a, NULL);
+       pthread_create(&t2, 0, &a, NULL);
+
+       pthread_join(t1, 0);
+       pthread_join(t2, 0);
+
+       return 0;
+}
diff --git a/benchmarks/nidhugg/msqueue/bench.sh b/benchmarks/nidhugg/msqueue/bench.sh
new file mode 100755 (executable)
index 0000000..0cd404c
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+
+for i in 1 2 3 4 5 6 7 8
+do
+echo size= $i
+java -cp .. transform $i ms-queue_simple.c.in ms-queue_simple.cc
+time nidhuggc -O3 -std=c++11 -- -sc ./ms-queue_simple.cc
+done
diff --git a/benchmarks/nidhugg/msqueue/benchtso.sh b/benchmarks/nidhugg/msqueue/benchtso.sh
new file mode 100755 (executable)
index 0000000..14e688b
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+
+for i in 1 2 3 4 5 6 7 8
+do
+echo size= $i
+java -cp .. transform $i ms-queue_simple.c.in ms-queue_simple.cc
+time nidhuggc -O3 -std=c++11 -- -tso ./ms-queue_simple.cc
+done
diff --git a/benchmarks/nidhugg/msqueue/ms-queue_simple.c.in b/benchmarks/nidhugg/msqueue/ms-queue_simple.c.in
new file mode 100644 (file)
index 0000000..384e581
--- /dev/null
@@ -0,0 +1,105 @@
+#include <pthread.h>
+#include <stdlib.h>
+#include <stdio.h>
+#include <atomic>
+#define true 1
+#define false 0
+
+
+#include "ms-queue_simple.h"
+
+queue_t queue;
+void init_queue(queue_t *q, int num_threads);
+void enqueue(queue_t *q, int val);
+bool dequeue(queue_t *q, int *retVal);
+
+void init_queue(queue_t *q, int num_threads) {
+       struct node *newnode=(struct node *) malloc(sizeof (struct node));
+       atomic_store_explicit(&newnode->value, 0, std::memory_order_release);
+
+       newnode->next.store(NULL, std::memory_order_release);
+               /* initialize queue */
+       q->head.store(newnode, std::memory_order_release);
+       
+       q->tail.store( newnode, std::memory_order_release);
+}
+
+void enqueue(queue_t *q, int val) {
+       struct node *tail;
+       struct node * node_ptr = (struct node *) malloc(sizeof(struct node));
+       atomic_store_explicit(&node_ptr->value, val, std::memory_order_release);
+       
+       node_ptr->next.store(NULL, std::memory_order_release);
+       
+       while (true) {
+               tail = (struct node *) atomic_load(&q->tail);
+               
+               struct node * next = (struct node *) atomic_load( &tail->next);
+               
+               struct node * qtail = (struct node *) atomic_load(&q->tail);
+               if (tail == qtail) {
+                       
+                       if (next == NULL) {
+                               if (atomic_compare_exchange_strong( & tail->next,& next, node_ptr))
+                                       break;
+                       }
+               }
+               struct node * new_tailptr = (struct node *)atomic_load( &tail->next);
+               atomic_compare_exchange_strong(&q->tail, & tail, new_tailptr);
+               //thrd_yield();
+       }
+       atomic_compare_exchange_strong(&q->tail, & tail, node_ptr);
+}
+
+bool dequeue(queue_t *q, int *retVal) {
+       while (true) {
+               struct node * head = (struct node *) atomic_load(&q->head);
+               struct node * tail = (struct node *) atomic_load(&q->tail);
+               struct node * next = (struct node *) atomic_load(&head->next);
+               
+               int t = ((struct node *) atomic_load(&q->head)) == head;
+               if (t) {
+                       if (head == tail) {
+
+                               if (next == NULL) {
+                                       return false; // NULL
+                               }
+                               atomic_compare_exchange_strong(&q->tail, & tail, next);
+                               //thrd_yield();
+                       } else {
+                               *retVal = atomic_load(&next->value);
+                               if (atomic_compare_exchange_strong(&q->head,& head, next)) {
+                                       return true;
+                               } else {
+                                       ;//thrd_yield();
+                               }
+                       }
+               }
+       }
+}
+
+void * e(void *param)
+{
+       problemsize enqueue(&queue, 1);
+       return NULL;
+}
+
+void * d(void *param) {
+       int val;
+       problemsize     dequeue(&queue, &val);
+       return NULL;
+}
+
+int main(int argc, char **argv)
+{
+       // MODEL_ASSERT(queue);
+
+       init_queue(&queue,  2);
+
+       pthread_t t1,t2;
+       pthread_create(&t1, 0, e, NULL);
+       pthread_create(&t2, 0, d, NULL);
+
+
+       return 0;
+}
diff --git a/benchmarks/nidhugg/msqueue/ms-queue_simple.h b/benchmarks/nidhugg/msqueue/ms-queue_simple.h
new file mode 100644 (file)
index 0000000..f768163
--- /dev/null
@@ -0,0 +1,15 @@
+typedef struct node {
+       std::atomic<int> value;
+       std::atomic<struct node *> next;
+} node_t;
+
+typedef struct {
+       std::atomic<struct node *> head;
+       std::atomic<struct node *> tail;
+} queue_t;
+
+//void init_queue(queue_t *q, int num_threads);
+//void enqueue(queue_t *q, unsigned int val);
+//bool dequeue(queue_t *q, unsigned int *retVal);
+int get_thread_num();
+
diff --git a/benchmarks/nidhugg/path.sh b/benchmarks/nidhugg/path.sh
new file mode 100755 (executable)
index 0000000..6c9a176
--- /dev/null
@@ -0,0 +1 @@
+NIDHUGG=~/nidhugg/
diff --git a/benchmarks/nidhugg/seqlock/bench.sh b/benchmarks/nidhugg/seqlock/bench.sh
new file mode 100755 (executable)
index 0000000..020ab1e
--- /dev/null
@@ -0,0 +1,10 @@
+#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+
+for i in 1 2 3
+do
+echo size= $i
+java -cp .. transform $i seqlock.c.in seqlock.cc
+time nidhuggc -O3 -std=c++11 -- -sc ./seqlock.cc
+done
diff --git a/benchmarks/nidhugg/seqlock/benchtso.sh b/benchmarks/nidhugg/seqlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..da2381b
--- /dev/null
@@ -0,0 +1,10 @@
+0#!/bin/bash
+source ../path.sh
+export PATH=$PATH:$NIDHUGG/bin/
+
+for i in 1 2 3
+do
+echo size= $i
+java -cp .. transform $i seqlock.c.in seqlock.cc
+time nidhuggc -O3 -std=c++11 -- -tso ./seqlock.cc
+done
diff --git a/benchmarks/nidhugg/seqlock/seqlock.c.in b/benchmarks/nidhugg/seqlock/seqlock.c.in
new file mode 100644 (file)
index 0000000..da76713
--- /dev/null
@@ -0,0 +1,73 @@
+#include <stdio.h>
+#include <pthread.h>
+#include <atomic>
+
+std::atomic<int> _seq;
+std::atomic<int> _data;
+
+void seqlock_init() {
+       atomic_store_explicit(&_seq, 0, std::memory_order_release);
+       atomic_store_explicit(&_data, 0, std::memory_order_release);
+}
+
+int seqlock_read() {
+       int old_seq = atomic_load(&_seq);
+       
+       int c0 = (old_seq % 2 == 1);
+       if (!c0) {
+               int res = atomic_load(&_data);
+               int seq = atomic_load(&_seq);
+    
+               int c1;
+               c1 = seq == old_seq;
+               if (c1) { // relaxed
+                       return res;
+               }
+       }
+       return -1;
+}
+
+int seqlock_write(int new_data) {
+       int old_seq = atomic_load(&_seq);
+       int c2 = (old_seq % 2 == 1);
+       if (!c2) {
+               int new_seq = old_seq + 1;
+               if (atomic_compare_exchange_strong(&_seq, &old_seq, new_seq)) {
+                       atomic_store_explicit(&_data, new_data, std::memory_order_release);
+                       atomic_fetch_add(&_seq, 1);
+                       return true;
+               }
+       }
+       return false;
+}
+
+void * a(void *obj) {
+problemsize            seqlock_write(3);
+ return NULL;
+}
+
+void * b(void *obj) {
+       int r1;
+problemsize            r1=seqlock_read();
+ return NULL;
+}
+
+void * c(void *obj) {
+       int r1;
+problemsize    r1=seqlock_read();
+ return NULL;
+}
+
+int main(int argc, char **argv) {
+       pthread_t t1, t2, t3;
+       seqlock_init();
+
+       pthread_create(&t1, 0,&a, NULL);
+       pthread_create(&t2, 0,&b, NULL);
+       pthread_create(&t3, 0,&c, NULL);
+
+       pthread_join(t1,0);
+       pthread_join(t2,0);
+       pthread_join(t3,0);
+       return 0;
+}
diff --git a/benchmarks/nidhugg/transform.java b/benchmarks/nidhugg/transform.java
new file mode 100644 (file)
index 0000000..d65e384
--- /dev/null
@@ -0,0 +1,29 @@
+import java.io.*;
+
+public class transform {
+       public static void main(String args[]) throws Exception {
+               int num=Integer.parseInt(args[0]);
+               String inputfile=args[1];
+               String output=args[2];
+               BufferedReader br=new BufferedReader(new FileReader(inputfile));
+               FileWriter fw=new FileWriter(output);
+               while(true) {
+                       String input=br.readLine();
+                       if (input==null)
+                               break;
+                       if (input.indexOf("problemsize")!=-1) {
+                               int index=input.indexOf("problemsize");
+                               String str=input.substring(index+12);
+                               fw.write("{\nint index;\n");
+                               fw.write("for (index=0;index<"+num+";index++) {\n");
+                               fw.write(str+"\n");
+                               fw.write("}\n}\n");
+                       } else
+                               fw.write(input+"\n");
+               }
+               br.close();
+               fw.close();
+
+       }
+
+}
diff --git a/benchmarks/runcds b/benchmarks/runcds
new file mode 100755 (executable)
index 0000000..847c39e
--- /dev/null
@@ -0,0 +1,14 @@
+#!/bin/bash
+DIR=`pwd`
+
+echo cdschecker
+for i in cdschecker/*
+do
+echo $i
+cd $i
+./bench.sh
+cd $DIR
+done
+
+
+
diff --git a/benchmarks/runcf b/benchmarks/runcf
new file mode 100755 (executable)
index 0000000..608fa75
--- /dev/null
@@ -0,0 +1,15 @@
+#!/bin/bash
+DIR=`pwd`
+
+
+
+echo checkfence
+for i in checkfence/*
+do
+echo $i
+cd $i
+./bench.sh
+cd $DIR
+done
+
+
diff --git a/benchmarks/runnidd b/benchmarks/runnidd
new file mode 100755 (executable)
index 0000000..702d8fb
--- /dev/null
@@ -0,0 +1,20 @@
+#!/bin/bash
+DIR=`pwd`
+
+echo nidhugg_sc
+for i in nidhugg/*
+do
+echo $i
+cd $i
+./bench.sh
+cd $DIR
+done
+
+echo nidhugg_tso
+for i in nidhugg/*
+do
+echo $i
+cd $i
+./benchtso.sh
+cd $DIR
+done
diff --git a/benchmarks/runsat b/benchmarks/runsat
new file mode 100755 (executable)
index 0000000..ec62696
--- /dev/null
@@ -0,0 +1,13 @@
+#!/bin/bash
+DIR=`pwd`
+BENCHMARKS="dekker linuxlock linuxrwlock msqueueoffset seqlock"
+
+for i in $BENCHMARKS
+do
+echo [SC SATCheck]: Running benchmark $i
+cd satcheck/$i
+echo satcheck > log
+echo $i >> log
+./bench.sh
+cd $DIR
+done
diff --git a/benchmarks/runtsosat b/benchmarks/runtsosat
new file mode 100755 (executable)
index 0000000..8b2c903
--- /dev/null
@@ -0,0 +1,13 @@
+#!/bin/bash
+DIR=`pwd`
+BENCHMARKS="dekker linuxlock linuxrwlock msqueueoffset seqlock"
+
+for i in $BENCHMARKS
+do
+echo [TSO SATCheck]: Running benchmark $i
+cd satcheck/$i
+echo satcheck > log
+echo $i >> log
+./benchtso.sh
+cd $DIR
+done
diff --git a/benchmarks/satcheck-precompiled/dekker/.gitignore b/benchmarks/satcheck-precompiled/dekker/.gitignore
new file mode 100644 (file)
index 0000000..ce592b6
--- /dev/null
@@ -0,0 +1,3 @@
+dekker-fences
+log_file
+logall
diff --git a/benchmarks/satcheck-precompiled/dekker/bench.sh b/benchmarks/satcheck-precompiled/dekker/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/dekker/benchmark-config.sh b/benchmarks/satcheck-precompiled/dekker/benchmark-config.sh
new file mode 100644 (file)
index 0000000..25b2e93
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=dekker-fences
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20 30"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20 30 40"
+RUN_FRONTEND=false
+RUNTIME_FLAGS=-Y
diff --git a/benchmarks/satcheck-precompiled/dekker/benchtso.sh b/benchmarks/satcheck-precompiled/dekker/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/dekker/clean.sh b/benchmarks/satcheck-precompiled/dekker/clean.sh
new file mode 100755 (executable)
index 0000000..a1255ac
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/sh
+rm -f dekker-fences dekker-fences.c dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck-precompiled/dekker/dekker-fences.c b/benchmarks/satcheck-precompiled/dekker/dekker-fences.c
new file mode 100644 (file)
index 0000000..c531933
--- /dev/null
@@ -0,0 +1,199 @@
+/*
+ * Dekker's critical section algorithm, implemented with fences.
+ * Translated to C by Patrick Lam <prof.lam@gmail.com>
+ *
+ * URL:
+ *   http://www.justsoftwaresolutions.co.uk/threading/
+ */
+
+#include <threads.h>
+#include <stdbool.h>
+#include "libinterface.h"
+
+/* atomic */ int flag0, flag1;
+/* atomic */ int turn;
+
+#define true 1
+#define false 0
+#define NULL 0
+
+/* uint32_t */ int var = 0;
+
+void p0() {
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&flag0, true);
+       // std::atomic_thread_fence(std::memory_order_seq_cst);
+
+       MCID _mf1; int f1;
+       MC2_enterLoop();
+       while (true)
+       {
+               _mf1=MC2_nextOpLoad(MCID_NODEP), f1 = load_32(&flag1);
+               MCID _br0;
+               
+               int _cond0 = !f1;
+               MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _mf1);
+               if (_cond0) {
+                       _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
+                       break;
+               }
+
+        else { _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);  MC2_merge(_br0);
+                }      MCID _br1;
+               MCID _m_cond1_m=MC2_nextOpLoad(MCID_NODEP); 
+               int _cond1 = load_32(&turn);
+               MCID _cond1_m = MC2_function_id(2, 1, sizeof(_cond1), _cond1, _m_cond1_m);
+               if (_cond1) {
+                       _br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
+                       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+                       store_32(&flag0, false);
+                       MC2_enterLoop();
+                       while(1) {
+                               MCID _br2;
+                               MCID _m_cond2_m=MC2_nextOpLoad(MCID_NODEP); 
+                               int _cond2 = !load_32(&turn);
+                               MCID _cond2_m = MC2_function_id(3, 1, sizeof(_cond2), _cond2, _m_cond2_m);
+                               if (_cond2) {
+                                       _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
+                                       break;
+                               }
+                else { _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);  MC2_merge(_br2);
+                                }              
+                               MC2_yield();
+                       }
+MC2_exitLoop();
+
+
+                       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+                       store_32(&flag0, true);
+                       MC2_merge(_br1);
+               } else {
+                       _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
+                       MC2_yield();
+                       MC2_merge(_br1);
+               }
+       }
+MC2_exitLoop();
+
+
+       // std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&var, 1);
+
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&turn, 1);
+       // std::atomic_thread_fence(std::memory_order_release);
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&flag0, false);
+}
+
+void p1() {
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&flag1, true);
+       // std::atomic_thread_fence(std::memory_order_seq_cst);
+       
+       int f0;
+       MC2_enterLoop();
+       while (true) {
+               MCID _mf0; _mf0=MC2_nextOpLoad(MCID_NODEP); int f0 = load_32(&flag0);
+               MCID _br3;
+               
+               int _cond3 = !f0;
+               MCID _cond3_m = MC2_function_id(4, 1, sizeof(_cond3), _cond3, _mf0);
+               if (_cond3) {
+                       _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
+                       break;
+               }
+                else { _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);  MC2_merge(_br3);
+                }
+               MCID _br4;
+               MCID _m_cond4_m=MC2_nextOpLoad(MCID_NODEP); 
+               int _cond4 = !load_32(&turn);
+               MCID _cond4_m = MC2_function_id(5, 1, sizeof(_cond4), _cond4, _m_cond4_m);
+               if (_cond4) {
+                       _br4 = MC2_branchUsesID(_cond4_m, 1, 2, true);
+                       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+                       store_32(&flag1, false);
+                       MC2_enterLoop();
+                       while (1) {
+                               MCID _br5;
+                               MCID _m_cond5_m=MC2_nextOpLoad(MCID_NODEP); 
+                               int _cond5 = load_32(&turn);
+                               MCID _cond5_m = MC2_function_id(6, 1, sizeof(_cond5), _cond5, _m_cond5_m);
+                               if (_cond5)
+                                       {_br5 = MC2_branchUsesID(_cond5_m, 1, 2, true);
+                                       break;
+}       else { _br5 = MC2_branchUsesID(_cond5_m, 0, 2, true);  MC2_merge(_br5);
+                                }                      MC2_yield();
+                       }
+MC2_exitLoop();
+
+                       
+                       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+                       store_32(&flag1, true);
+                       // std::atomic_thread_fence(std::memory_order_seq_cst);
+                       MC2_merge(_br4);
+               }
+ else { _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true); MC2_merge(_br4);
+        }      }
+MC2_exitLoop();
+
+
+       // std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&var, 2);
+
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&turn, 0);
+       // std::atomic_thread_fence(std::memory_order_release);
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&flag1, false);
+}
+
+void p0l(void *a) {
+       int i;
+       MC2_enterLoop();
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p0();
+       }
+MC2_exitLoop();
+
+}
+
+
+void p1l(void *a) {
+       int i;
+       MC2_enterLoop();
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p1();
+       }
+MC2_exitLoop();
+
+}
+
+
+int user_main(int argc, char **argv)
+{
+       thrd_t a, b;
+
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&flag0, false);
+
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&flag1, false);
+
+       MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+       store_32(&turn, 0);
+
+       thrd_create(&a, p0l, NULL);
+       thrd_create(&b, p1l, NULL);
+
+       thrd_join(a);
+       thrd_join(b);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c b/benchmarks/satcheck-precompiled/dekker/dekker-fences_unannotated.c
new file mode 100644 (file)
index 0000000..15a6d2c
--- /dev/null
@@ -0,0 +1,134 @@
+/*
+ * Dekker's critical section algorithm, implemented with fences.
+ * Translated to C by Patrick Lam <prof.lam@gmail.com>
+ *
+ * URL:
+ *   http://www.justsoftwaresolutions.co.uk/threading/
+ */
+
+#include <threads.h>
+#include <stdbool.h>
+#include "libinterface.h"
+
+/* atomic */ int flag0, flag1;
+/* atomic */ int turn;
+
+#define true 1
+#define false 0
+#define NULL 0
+
+/* uint32_t */ int var = 0;
+
+void p0() {
+       store_32(&flag0, true);
+       // std::atomic_thread_fence(std::memory_order_seq_cst);
+
+       int f1, t;
+       while (true)
+       {
+               f1 = load_32(&flag1);
+               if (!f1) {
+                       break;
+               }
+
+               
+               t = load_32(&turn);
+
+               if (t) {
+                       store_32(&flag0, false);
+                       while(1) {
+                               t = load_32(&turn);
+                               if (!t) {
+                                       break;
+                               }
+                               
+                               MC2_yield();
+                       }
+
+                       store_32(&flag0, true);
+               } else {
+                       MC2_yield();
+               }
+       }
+
+       // std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       store_32(&var, 1);
+
+       store_32(&turn, 1);
+       // std::atomic_thread_fence(std::memory_order_release);
+       store_32(&flag0, false);
+}
+
+void p1() {
+       store_32(&flag1, true);
+       // std::atomic_thread_fence(std::memory_order_seq_cst);
+       
+       int f0, t;
+       while (true) {
+               int f0 = load_32(&flag0);
+               if (!f0) {
+                       break;
+               }
+               
+               t = load_32(&turn);
+               
+               if (!t) {
+                       store_32(&flag1, false);
+                       while (1) {
+                               t = load_32(&turn);
+                               if (t)
+                                       break;
+                               MC2_yield();
+                       }
+                       
+                       store_32(&flag1, true);
+                       // std::atomic_thread_fence(std::memory_order_seq_cst);
+               }
+       }
+
+       // std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       store_32(&var, 2);
+
+       store_32(&turn, 0);
+       // std::atomic_thread_fence(std::memory_order_release);
+       store_32(&flag1, false);
+}
+
+void p0l(void *a) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p0();
+       }
+}
+
+
+void p1l(void *a) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p1();
+       }
+}
+
+
+int user_main(int argc, char **argv)
+{
+       thrd_t a, b;
+
+       store_32(&flag0, false);
+
+       store_32(&flag1, false);
+
+       store_32(&turn, 0);
+
+       thrd_create(&a, p0l, NULL);
+       thrd_create(&b, p1l, NULL);
+
+       thrd_join(a);
+       thrd_join(b);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/dekker/diff.sh b/benchmarks/satcheck-precompiled/dekker/diff.sh
new file mode 100755 (executable)
index 0000000..e072b49
--- /dev/null
@@ -0,0 +1,3 @@
+#!/bin/sh
+NAME=dekker
+diff -ub ../../satcheck/${NAME}/dekker-fences.c.in dekker-fences.c
diff --git a/benchmarks/satcheck-precompiled/linuxlock/.gitignore b/benchmarks/satcheck-precompiled/linuxlock/.gitignore
new file mode 100644 (file)
index 0000000..797a971
--- /dev/null
@@ -0,0 +1,3 @@
+linuxlocks
+log_file
+logall
diff --git a/benchmarks/satcheck-precompiled/linuxlock/bench.sh b/benchmarks/satcheck-precompiled/linuxlock/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/linuxlock/benchmark-config.sh b/benchmarks/satcheck-precompiled/linuxlock/benchmark-config.sh
new file mode 100644 (file)
index 0000000..698c3be
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=linuxlocks
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20 30 40 50 60 70 80 90 100 150 200 250"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20 30 40 50 60 70 80 90 100"
+RUN_FRONTEND=false
+RUNTIME_FLAGS=
diff --git a/benchmarks/satcheck-precompiled/linuxlock/benchtso.sh b/benchmarks/satcheck-precompiled/linuxlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/linuxlock/clean.sh b/benchmarks/satcheck-precompiled/linuxlock/clean.sh
new file mode 100755 (executable)
index 0000000..9a90971
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f linuxlocks.c linuxlocks dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck-precompiled/linuxlock/diff.sh b/benchmarks/satcheck-precompiled/linuxlock/diff.sh
new file mode 100755 (executable)
index 0000000..b3563be
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=linuxlock
+diff -ub ../../satcheck/$NAME/linuxlocks.c.in linuxlocks.c
+
diff --git a/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c b/benchmarks/satcheck-precompiled/linuxlock/linuxlocks.c
new file mode 100644 (file)
index 0000000..db75025
--- /dev/null
@@ -0,0 +1,78 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+#include <stdbool.h>
+#include "libinterface.h"
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       int lock;
+} rwlock_t;
+
+static inline bool write_trylock(MCID _mrw, rwlock_t *rw, MCID * retval)
+{
+       MCID _rmw0 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+       int priorvalue=rmw_32(CAS, &rw->lock, 0, 1);
+       *retval = _rmw0;
+       return priorvalue;
+}
+
+static inline void write_unlock(MCID _mrw, rwlock_t *rw)
+{
+       MC2_nextOpStoreOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
+       store_32(&rw->lock, 0);
+}
+
+MCID _fn0; rwlock_t * mylock;
+
+static void foo() {
+       MCID _rv0;
+       int flag=write_trylock(MCID_NODEP, mylock, &_rv0);
+       MCID _br0;
+       
+       int _cond0 = flag;
+       MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _rv0);
+       if (_cond0) {_br0 = MC2_branchUsesID(_rv0, 1, 2, true);
+       
+               MC2_merge(_br0);
+       } else {
+               _br0 = MC2_branchUsesID(_rv0, 0, 2, true);
+               write_unlock(MCID_NODEP, mylock);
+               MC2_merge(_br0);
+       }
+}
+
+static void a(void *obj)
+{
+       int i;
+       MC2_enterLoop();
+       for(i=0;i<PROBLEMSIZE;i++)
+               foo();
+MC2_exitLoop();
+
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t1, t2;//, t3, t4;
+       mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
+       _fn0 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 
+       MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
+       store_32(&mylock->lock, 0);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       //thrd_create(&t3, (thrd_start_t)&a, NULL);
+       //thrd_create(&t4, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       //thrd_join(t3);
+       //thrd_join(t4);
+
+
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/linuxlock/linuxlocks_unannotated.c b/benchmarks/satcheck-precompiled/linuxlock/linuxlocks_unannotated.c
new file mode 100644 (file)
index 0000000..926e0e7
--- /dev/null
@@ -0,0 +1,59 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+#include <stdbool.h>
+#include "libinterface.h"
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       int lock;
+} rwlock_t;
+
+static inline bool write_trylock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(CAS, &rw->lock, 0, 1);
+       return priorvalue;
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       store_32(&rw->lock, 0);
+}
+
+rwlock_t * mylock;
+
+static void foo() {
+       int flag=write_trylock(mylock);
+       if (flag) {
+       } else {
+               write_unlock(mylock);
+       }
+}
+
+static void a(void *obj)
+{
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               foo();
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t1, t2;//, t3, t4;
+       mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
+       store_32(&mylock->lock, 0);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       //thrd_create(&t3, (thrd_start_t)&a, NULL);
+       //thrd_create(&t4, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       //thrd_join(t3);
+       //thrd_join(t4);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/.gitignore b/benchmarks/satcheck-precompiled/linuxrwlock/.gitignore
new file mode 100644 (file)
index 0000000..2bb93ae
--- /dev/null
@@ -0,0 +1,4 @@
+linuxrwlocks
+log_file
+logall
+linuxrwlocks
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/bench.sh b/benchmarks/satcheck-precompiled/linuxrwlock/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/benchmark-config.sh b/benchmarks/satcheck-precompiled/linuxrwlock/benchmark-config.sh
new file mode 100644 (file)
index 0000000..c9aa599
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=linuxrwlocks
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20"
+RUN_FRONTEND=false
+RUNTIME_FLAGS=
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/benchtso.sh b/benchmarks/satcheck-precompiled/linuxrwlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/clean.sh b/benchmarks/satcheck-precompiled/linuxrwlock/clean.sh
new file mode 100755 (executable)
index 0000000..3a12299
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f linuxrwlocks.cc linuxrwlocks dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/diff.sh b/benchmarks/satcheck-precompiled/linuxrwlock/diff.sh
new file mode 100755 (executable)
index 0000000..c878fd3
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=linuxrwlock
+diff -ub ../../satcheck/$NAME/linuxrwlocks.c.in linuxrwlocks.c
+
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c b/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks.c
new file mode 100644 (file)
index 0000000..150b68a
--- /dev/null
@@ -0,0 +1,201 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+#include <stdlib.h>
+
+#include "libinterface.h"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       int lock;
+} rwlock_t;
+
+static inline void read_lock(MCID _mrw, rwlock_t *rw)
+{
+       MCID _rmw0 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
+
+       MC2_enterLoop();
+       while (true) {
+               MCID _br0;
+               
+               int _cond0 = priorvalue <= 0;
+               MCID _cond0_m = MC2_function_id(1, 1, sizeof(_cond0), _cond0, _rmw0);
+               if (_cond0) {_br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
+               
+                       MC2_merge(_br0);
+               } else {
+                       _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
+                       break;
+               }
+
+               MCID _rmw1 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
+
+               MC2_enterLoop();
+               while (true) {
+                       MCID _mstatus; _mstatus=MC2_nextOpLoadOffset(_mrw, MC2_OFFSET(rwlock_t *, lock)); int status = load_32(&rw->lock);
+                       MCID _br1;
+                       
+                       int _cond1 = status > 0;
+                       MCID _cond1_m = MC2_function_id(2, 1, sizeof(_cond1), _cond1, _mstatus);
+                       if (_cond1) {_br1 = MC2_branchUsesID(_cond1_m, 1, 2, true);
+                       
+                               MC2_merge(_br1);
+                       } else {
+                               _br1 = MC2_branchUsesID(_cond1_m, 0, 2, true);
+                               break;
+                       }
+                       MC2_yield();
+               }
+MC2_exitLoop();
+
+
+               
+               MCID _rmw2 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+               priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
+       }
+MC2_exitLoop();
+
+}
+
+static inline void write_lock(MCID _mrw, rwlock_t *rw)
+{
+       MCID _rmw3 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+       MC2_enterLoop();
+       while(true) {
+               MCID _br2;
+               
+               int _cond2 = priorvalue != 1048576;
+               MCID _cond2_m = MC2_function_id(3, 1, sizeof(_cond2), _cond2, _rmw3);
+               if (_cond2) {_br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
+               
+                       MC2_merge(_br2);
+               } else {
+                       _br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
+                       break;
+               }
+
+               MCID _rmw4 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+               
+               MC2_enterLoop();
+               while (true) {
+                       MCID _mstatus; _mstatus=MC2_nextOpLoadOffset(_mrw, MC2_OFFSET(rwlock_t *, lock)); int status = load_32(&rw->lock);
+                       MCID _br3;
+                       
+                       int _cond3 = status != 1048576;
+                       MCID _cond3_m = MC2_function_id(4, 1, sizeof(_cond3), _cond3, _mstatus);
+                       if (_cond3) {_br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
+                       
+                               MC2_merge(_br3);
+                       } else {
+                               _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
+                               break;
+                       }
+                       MC2_yield();
+               }
+MC2_exitLoop();
+
+
+               MCID _rmw5 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+               priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+       }
+MC2_exitLoop();
+
+}
+
+static inline bool write_trylock(MCID _mrw, rwlock_t *rw, MCID * retval)
+{
+       MCID _rmw6 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+
+       MCID _fn0; int flag = priorvalue != RW_LOCK_BIAS;
+       _fn0 = MC2_function_id(7, 1, sizeof (flag), (uint64_t)flag, _rmw6); 
+       MCID _br4;
+       
+       int _cond4 = !flag;
+       MCID _cond4_m = MC2_function_id(5, 1, sizeof(_cond4), _cond4, _fn0);
+       if (_cond4) {
+               _br4 = MC2_branchUsesID(_cond4_m, 1, 2, true);
+               MCID _rmw7 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+               MC2_merge(_br4);
+       }
+ else { _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true); MC2_merge(_br4);
+ }
+       *retval = _fn0;
+       return flag;
+}
+
+static inline void read_unlock(MCID _mrw, rwlock_t *rw)
+{
+       MCID _rmw8 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+       rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
+}
+
+static inline void write_unlock(MCID _mrw, rwlock_t *rw)
+{
+       MCID _rmw9 = MC2_nextRMWOffset(_mrw, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP, MCID_NODEP);
+       rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+}
+
+MCID _fn1; rwlock_t * mylock;
+int shareddata;
+
+static void foo() {
+       MCID _rv0;
+       int res = write_trylock(MCID_NODEP, mylock, &_rv0);
+       MCID _br5;
+       
+       int _cond5 = res;
+       MCID _cond5_m = MC2_function_id(6, 1, sizeof(_cond5), _cond5, _rv0);
+       if (_cond5) {
+               _br5 = MC2_branchUsesID(_rv0, 1, 2, true);
+               write_unlock(MCID_NODEP, mylock);
+               MC2_merge(_br5);
+       } else {_br5 = MC2_branchUsesID(_rv0, 0, 2, true);
+       
+               MC2_merge(_br5);
+       }
+}
+
+static void a(void *obj)
+{
+       int i;
+       MC2_enterLoop();
+       for(i=0;i<PROBLEMSIZE;i++)
+               foo();
+MC2_exitLoop();
+
+}
+
+int user_main(int argc, char **argv)
+{
+       mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
+       _fn1 = MC2_function_id(0, 0, sizeof (mylock), (uint64_t)mylock); 
+
+       thrd_t t1, t2;
+       //, t3, t4;
+       MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(rwlock_t *, lock), MCID_NODEP);
+       store_32(&mylock->lock, RW_LOCK_BIAS);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       //      thrd_create(&t3, (thrd_start_t)&a, NULL);
+       //      thrd_create(&t4, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       //      thrd_join(t3);
+       //      thrd_join(t4);
+       free(mylock);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks_unannotated.c b/benchmarks/satcheck-precompiled/linuxrwlock/linuxrwlocks_unannotated.c
new file mode 100644 (file)
index 0000000..10496dc
--- /dev/null
@@ -0,0 +1,128 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+#include <stdlib.h>
+
+#include "libinterface.h"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       int lock;
+} rwlock_t;
+
+static inline void read_lock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
+
+       while (true) {
+               if (priorvalue <= 0) {
+               } else {
+                       break;
+               }
+
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
+
+               while (true) {
+                       int status = load_32(&rw->lock);
+                       if (status > 0) {
+                       } else {
+                               break;
+                       }
+                       MC2_yield();
+               }
+
+               
+               priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
+       }
+}
+
+static inline void write_lock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+       while(true) {
+               if (priorvalue != RW_LOCK_BIAS) {
+               } else {
+                       break;
+               }
+
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+               
+               while (true) {
+                       int status = load_32(&rw->lock);
+                       if (status != RW_LOCK_BIAS) {
+                       } else {
+                               break;
+                       }
+                       MC2_yield();
+               }
+
+               priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+       }
+}
+
+static inline bool write_trylock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+
+       int flag = priorvalue != RW_LOCK_BIAS;
+       if (!flag) {
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+       }
+
+       return flag;
+}
+
+static inline void read_unlock(rwlock_t *rw)
+{
+       rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+}
+
+rwlock_t * mylock;
+int shareddata;
+
+static void foo() {
+       int res = write_trylock(mylock);
+       if (res) {
+               write_unlock(mylock);
+       } else {
+       }
+}
+
+static void a(void *obj)
+{
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               foo();
+}
+
+int user_main(int argc, char **argv)
+{
+       mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
+
+       thrd_t t1, t2;
+       //, t3, t4;
+       store_32(&mylock->lock, RW_LOCK_BIAS);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       //      thrd_create(&t3, (thrd_start_t)&a, NULL);
+       //      thrd_create(&t4, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       //      thrd_join(t3);
+       //      thrd_join(t4);
+       free(mylock);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/.gitignore b/benchmarks/satcheck-precompiled/msqueueoffset/.gitignore
new file mode 100644 (file)
index 0000000..af514b3
--- /dev/null
@@ -0,0 +1,3 @@
+logall
+ms-queue-simple
+log_file
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/bench.sh b/benchmarks/satcheck-precompiled/msqueueoffset/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/benchmark-config.sh b/benchmarks/satcheck-precompiled/msqueueoffset/benchmark-config.sh
new file mode 100644 (file)
index 0000000..a7c1cfc
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=ms-queue-simple
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 11 12 13"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 11 12 13"
+RUN_FRONTEND=false
+RUNTIME_FLAGS=
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/benchtso.sh b/benchmarks/satcheck-precompiled/msqueueoffset/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/clean.sh b/benchmarks/satcheck-precompiled/msqueueoffset/clean.sh
new file mode 100755 (executable)
index 0000000..3a12299
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f linuxrwlocks.cc linuxrwlocks dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/diff.sh b/benchmarks/satcheck-precompiled/msqueueoffset/diff.sh
new file mode 100755 (executable)
index 0000000..d7117e7
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=msqueueoffset
+diff -ub ../../satcheck/$NAME/ms-queue-simple.c.in ms-queue-simple.c
+
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.c b/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.c
new file mode 100644 (file)
index 0000000..e819eb7
--- /dev/null
@@ -0,0 +1,225 @@
+#include <threads.h>
+#include <stdlib.h>
+#include <stdio.h>
+#define true 1
+#define false 0
+#define bool int
+
+#include "ms-queue-simple.h"
+#include "libinterface.h"
+
+void init_queue(MCID _mq, queue_t *q, MCID _mnum_threads, int num_threads);
+void enqueue(MCID _mq, queue_t *q, MCID _mval, unsigned int val);
+bool dequeue(MCID _mq, queue_t *q, MCID _mretVal, unsigned int *retVal, MCID * retval);
+
+queue_t queue;
+
+void init_queue(MCID _mq, queue_t *q, MCID _mnum_threads, int num_threads) {
+       MCID _fn0; struct node *newnode=(struct node *)malloc(sizeof (struct node));
+       _fn0 = MC2_function_id(0, 0, sizeof (newnode), (uint64_t)newnode); 
+       
+       MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(struct node *, value), MCID_NODEP);
+       store_32(&newnode->value, 0);
+
+       
+       MC2_nextOpStoreOffset(_fn0, MC2_OFFSET(struct node *, next), MCID_NODEP);
+       store_64(&newnode->next, (uintptr_t) NULL);
+               /* initialize queue */
+       
+       MC2_nextOpStoreOffset(_mq, MC2_OFFSET(queue_t *, head), _fn0);
+       store_64(&q->head, (uintptr_t) newnode);
+       
+       
+       MC2_nextOpStoreOffset(_mq, MC2_OFFSET(queue_t *, tail), _fn0);
+       store_64(&q->tail, (uintptr_t) newnode);
+}
+
+void enqueue(MCID _mq, queue_t *q, MCID _mval, unsigned int val) {
+       MCID _mtail; struct node *tail;
+       MCID _fn1; struct node * node_ptr; node_ptr = (struct node *)malloc(sizeof(struct node));
+       _fn1 = MC2_function_id(0, 1, sizeof (node_ptr), (uint64_t)node_ptr, _fn1); 
+       
+       MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(struct node *, value), _mval);
+       store_32(&node_ptr->value, val);
+       
+       
+       MC2_nextOpStoreOffset(_fn1, MC2_OFFSET(struct node *, next), MCID_NODEP);
+       store_64(&node_ptr->next, (uintptr_t) NULL);
+                       
+       MC2_enterLoop();
+       while (true) {
+
+               _mtail=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, tail)), tail = (struct node *) load_64(&q->tail);
+
+               MCID _mnext; _mnext=MC2_nextOpLoadOffset(_mtail, MC2_OFFSET(struct node *, next)); struct node * next = (struct node *) load_64(&tail->next);
+               
+               MCID _mqtail; _mqtail=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, tail)); struct node * qtail = (struct node *) load_64(&q->tail);
+
+               MCID _br0;
+               
+               MCID _cond0_m;
+               
+               int _cond0 = MC2_equals(_mtail, (uint64_t)tail, _mqtail, (uint64_t)qtail, &_cond0_m);
+               if (_cond0) {
+                       MCID _br1;
+                       _br0 = MC2_branchUsesID(_cond0_m, 1, 2, true);
+                       
+                       int _cond1 = next;
+                       MCID _cond1_m = MC2_function_id(1, 1, sizeof(_cond1), _cond1, _mnext);
+                       if (_cond1) {
+                               _br1 = MC2_branchUsesID(_mnext, 1, 2, true);
+                               MC2_yield();
+                               MC2_merge(_br1);
+                       } else {
+                               _br1 = MC2_branchUsesID(_mnext, 0, 2, true);
+                               MCID _rmw0 = MC2_nextRMWOffset(_mtail, MC2_OFFSET(struct node *, next), _mnext, _fn1);
+                               struct node * valread = (struct node *) rmw_64(CAS, &tail->next, (uintptr_t) next, (uintptr_t) node_ptr);
+                               
+                               MCID _br2;
+                               
+                               MCID _cond2_m;
+                               
+                               int _cond2 = MC2_equals(_mnext, (uint64_t)next, _rmw0, (uint64_t)valread, &_cond2_m);
+                               if (_cond2) {
+                                       _br2 = MC2_branchUsesID(_cond2_m, 1, 2, true);
+                                       break;
+                               } else {_br2 = MC2_branchUsesID(_cond2_m, 0, 2, true);
+                               
+                                       MC2_merge(_br2);
+                               }
+                               MC2_merge(_br1);
+                       }
+                       MCID _mnew_tailptr; _mnew_tailptr=MC2_nextOpLoadOffset(_mtail, MC2_OFFSET(struct node *, next)); struct node * new_tailptr = (struct node *)load_64(&tail->next);
+                       MCID _rmw1 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, tail), _mtail, _mnew_tailptr);
+                       rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) new_tailptr);
+                       MC2_yield();
+                       MC2_merge(_br0);
+               } else { 
+                       _br0 = MC2_branchUsesID(_cond0_m, 0, 2, true);
+                       MC2_yield();
+                       MC2_merge(_br0);
+               }
+       }
+MC2_exitLoop();
+
+       
+       MCID _rmw2 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, tail), _mtail, _fn1);
+       rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) node_ptr);
+}
+
+bool dequeue(MCID _mq, queue_t *q, MCID _mretVal, unsigned int *retVal, MCID * retval) {
+       MC2_enterLoop();
+       while (true) {
+               MCID _mhead; _mhead=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, head)); struct node * head = (struct node *) load_64(&q->head);
+               MCID _mtail; _mtail=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, tail)); struct node * tail = (struct node *) load_64(&q->tail);
+               MCID _mnext; _mnext=MC2_nextOpLoadOffset(_mhead, MC2_OFFSET(struct node *, next)); struct node * next = (struct node *) load_64(&head->next);
+
+               MCID _mheadr; _mheadr=MC2_nextOpLoadOffset(_mq, MC2_OFFSET(queue_t *, head)); struct node * headr = (struct node *) load_64(&q->head);
+
+               MCID _br3;
+               
+               MCID _cond3_m;
+               
+               int _cond3 = MC2_equals(_mhead, (uint64_t)head, _mheadr, (uint64_t)headr, &_cond3_m);
+               if (_cond3) {
+                       MCID _br4;
+                       _br3 = MC2_branchUsesID(_cond3_m, 1, 2, true);
+                       
+                       MCID _cond4_m;
+                       
+                       int _cond4 = MC2_equals(_mhead, (uint64_t)head, _mtail, (uint64_t)tail, &_cond4_m);
+                       if (_cond4) {
+                               MCID _br5;
+                               _br4 = MC2_branchUsesID(_cond4_m, 1, 2, true);
+                               
+                               int _cond5 = next;
+                               MCID _cond5_m = MC2_function_id(2, 1, sizeof(_cond5), _cond5, _mnext);
+                               if (_cond5) {
+                                       _br5 = MC2_branchUsesID(_mnext, 1, 2, true);
+                                       MC2_yield();
+                                       MC2_merge(_br5);
+                               } else {
+                                       *retval = MCID_NODEP;
+                                       _br5 = MC2_branchUsesID(_mnext, 0, 2, true);
+                                       MC2_exitLoop();
+                                       return false; // NULL
+                               }
+                               MCID _rmw3 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, tail), _mtail, _mnext);
+                               rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
+                               MC2_yield();
+                               MC2_merge(_br4);
+                       } else {
+                               _br4 = MC2_branchUsesID(_cond4_m, 0, 2, true);
+                               _mretVal=MC2_nextOpLoadOffset(_mnext, MC2_OFFSET(struct node *, value)), *retVal = load_32(&next->value);
+                               MCID _rmw4 = MC2_nextRMWOffset(_mq, MC2_OFFSET(queue_t *, head), _mhead, _mnext);
+                               struct node *old_head = (struct node *) rmw_64(CAS, &q->head,
+                                                                                                                                                                                                                        (uintptr_t) head, 
+                                                                                                                                                                                                                        (uintptr_t) next);
+
+                               MCID _br6;
+                               
+                               MCID _cond6_m;
+                               
+                               int _cond6 = MC2_equals(_mhead, (uint64_t)head, _rmw4, (uint64_t)old_head, &_cond6_m);
+                               if (_cond6) {
+                                       *retval = MCID_NODEP;
+                                       _br6 = MC2_branchUsesID(_cond6_m, 1, 2, true);
+                                       MC2_exitLoop();
+                                       return true;
+                               } else {
+                                       _br6 = MC2_branchUsesID(_cond6_m, 0, 2, true);
+                                       MC2_yield();
+                                       MC2_merge(_br6);
+                               }
+                               MC2_merge(_br4);
+                       }
+                       MC2_merge(_br3);
+               } else {
+                       _br3 = MC2_branchUsesID(_cond3_m, 0, 2, true);
+                       MC2_yield();
+                       MC2_merge(_br3);
+               }
+       }
+MC2_exitLoop();
+
+}
+
+/* ms-queue-main */
+bool succ1, succ2;
+
+static void e(void *p) {
+       int i;
+       MC2_enterLoop();
+       for(i=0;i<PROBLEMSIZE;i++) {
+               enqueue(MCID_NODEP, &queue, MCID_NODEP, 1);
+       }
+MC2_exitLoop();
+
+}
+
+static void d(void *p) {
+       unsigned int val;
+       int i;
+       MC2_enterLoop();
+       for(i=0;i<PROBLEMSIZE;i++) {
+               int r;
+               MCID _rv0;
+               r = dequeue(MCID_NODEP, &queue, MCID_NODEP, &val, &_rv0);
+       }
+MC2_exitLoop();
+
+}
+
+int user_main(int argc, char **argv)
+{
+       init_queue(MCID_NODEP, &queue, MCID_NODEP, 2);
+
+       thrd_t t1,t2;
+       thrd_create(&t1, e, NULL);
+       thrd_create(&t2, d, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.h b/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple.h
new file mode 100644 (file)
index 0000000..9f7f11c
--- /dev/null
@@ -0,0 +1,15 @@
+typedef struct node {
+       unsigned int value;
+       struct node * next;
+} node_t;
+
+typedef struct {
+       struct node * head;
+       struct node * tail;
+} queue_t;
+
+//void init_queue(queue_t *q, int num_threads);
+//void enqueue(queue_t *q, unsigned int val);
+//bool dequeue(queue_t *q, unsigned int *retVal);
+int get_thread_num();
+
diff --git a/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple_unannotated.c b/benchmarks/satcheck-precompiled/msqueueoffset/ms-queue-simple_unannotated.c
new file mode 100644 (file)
index 0000000..6fc7d7f
--- /dev/null
@@ -0,0 +1,137 @@
+#include <threads.h>
+#include <stdlib.h>
+#include <stdio.h>
+#define true 1
+#define false 0
+#define bool int
+
+#include "ms-queue-simple.h"
+#include "libinterface.h"
+
+void init_queue(queue_t *q, int num_threads);
+void enqueue(queue_t *q, unsigned int val);
+bool dequeue(queue_t *q, unsigned int *retVal);
+
+queue_t queue;
+
+void init_queue(queue_t *q, int num_threads) {
+       struct node *newnode=(struct node *)malloc(sizeof (struct node));
+       
+       store_32(&newnode->value, 0);
+
+       
+       store_64(&newnode->next, (uintptr_t) NULL);
+               /* initialize queue */
+       
+       store_64(&q->head, (uintptr_t) newnode);
+       
+       
+       store_64(&q->tail, (uintptr_t) newnode);
+}
+
+void enqueue(queue_t *q, unsigned int val) {
+       struct node *tail;
+       struct node * node_ptr; node_ptr = (struct node *)malloc(sizeof(struct node));
+       
+       store_32(&node_ptr->value, val);
+       
+       
+       store_64(&node_ptr->next, (uintptr_t) NULL);
+                       
+       while (true) {
+
+               tail = (struct node *) load_64(&q->tail);
+
+               struct node * next = (struct node *) load_64(&tail->next);
+               
+               struct node * qtail = (struct node *) load_64(&q->tail);
+
+               if (tail == qtail) {
+                       if (next) {
+                               MC2_yield();
+                       } else {
+                               struct node * valread = (struct node *) rmw_64(CAS, &tail->next, (uintptr_t) next, (uintptr_t) node_ptr);
+                               
+                               if (next == valread) {
+                                       break;
+                               } else {
+                               }
+                       }
+                       struct node * new_tailptr = (struct node *)load_64(&tail->next);
+                       rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) new_tailptr);
+                       MC2_yield();
+               } else { 
+                       MC2_yield();
+               }
+       }
+       
+       rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) node_ptr);
+}
+
+bool dequeue(queue_t *q, unsigned int *retVal) {
+       while (true) {
+               struct node * head = (struct node *) load_64(&q->head);
+               struct node * tail = (struct node *) load_64(&q->tail);
+               struct node * next = (struct node *) load_64(&head->next);
+
+               struct node * headr = (struct node *) load_64(&q->head);
+
+               if (head == headr) {
+                       if (head == tail) {
+                               if (next) {
+                                       MC2_yield();
+                               } else {
+                                       return false; // NULL
+                               }
+                               rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
+                               MC2_yield();
+                       } else {
+                               *retVal = load_32(&next->value);
+                               struct node *old_head = (struct node *) rmw_64(CAS, &q->head,
+                                                                                                                                                                                                                        (uintptr_t) head, 
+                                                                                                                                                                                                                        (uintptr_t) next);
+
+                               if (head == old_head) {
+                                       return true;
+                               } else {
+                                       MC2_yield();
+                               }
+                       }
+               } else {
+                       MC2_yield();
+               }
+       }
+}
+
+/* ms-queue-main */
+bool succ1, succ2;
+
+static void e(void *p) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               enqueue(&queue, 1);
+       }
+}
+
+static void d(void *p) {
+       unsigned int val;
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               int r;
+               r = dequeue(&queue, &val);
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       init_queue(&queue, 2);
+
+       thrd_t t1,t2;
+       thrd_create(&t1, e, NULL);
+       thrd_create(&t2, d, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/seqlock/.gitignore b/benchmarks/satcheck-precompiled/seqlock/.gitignore
new file mode 100644 (file)
index 0000000..8710a22
--- /dev/null
@@ -0,0 +1,3 @@
+log_file
+logall
+seqlock
diff --git a/benchmarks/satcheck-precompiled/seqlock/bench.sh b/benchmarks/satcheck-precompiled/seqlock/bench.sh
new file mode 100755 (executable)
index 0000000..a03b573
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.cc -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/seqlock/benchmark-config.sh b/benchmarks/satcheck-precompiled/seqlock/benchmark-config.sh
new file mode 100644 (file)
index 0000000..a737bcf
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=seqlock
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20 25 30 35 40 50 60"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20 25 30 35 40 50 60"
+RUN_FRONTEND=false
+RUNTIME_FLAGS=-Y
diff --git a/benchmarks/satcheck-precompiled/seqlock/benchtso.sh b/benchmarks/satcheck-precompiled/seqlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..3c52574
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.cc -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck-precompiled/seqlock/clean.sh b/benchmarks/satcheck-precompiled/seqlock/clean.sh
new file mode 100755 (executable)
index 0000000..325db38
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f seqlock.cc seqlock dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck-precompiled/seqlock/diff.sh b/benchmarks/satcheck-precompiled/seqlock/diff.sh
new file mode 100755 (executable)
index 0000000..a95a91b
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=seqlock
+diff -ub ../../satcheck/$NAME/seqlock.cc.in seqlock.cc
+
diff --git a/benchmarks/satcheck-precompiled/seqlock/seqlock.cc b/benchmarks/satcheck-precompiled/seqlock/seqlock.cc
new file mode 100644 (file)
index 0000000..1af11a4
--- /dev/null
@@ -0,0 +1,149 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "libinterface.h"
+
+// Sequence for reader consistency check
+/*atomic_*/ int _seq;
+// It needs to be atomic to avoid data races
+/*atomic_*/ int _data;
+
+void seqlock_init() {
+    MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+    store_32(&_seq, 0);
+    MC2_nextOpStore(MCID_NODEP, MCID_NODEP);
+    store_32(&_data, 10);
+}
+
+int seqlock_read(MCID * retval) {
+    MCID _mres; int res;
+       MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq); // acquire
+
+       MCID _br30;
+       
+       int _cond30 = old_seq % 2 == 1;
+       MCID _cond30_m = MC2_function_id(31, 1, sizeof(_cond30), _cond30, _mold_seq);
+       if (_cond30) {
+        _br30 = MC2_branchUsesID(_cond30_m, 1, 2, true);
+        res = -1;
+       MC2_merge(_br30);
+    } else {
+               _br30 = MC2_branchUsesID(_cond30_m, 0, 2, true);
+               _mres=MC2_nextOpLoad(MCID_NODEP), res = load_32(&_data);
+        MCID _mseq; _mseq=MC2_nextOpLoad(MCID_NODEP); int seq = load_32(&_seq);
+    
+        MCID _br31;
+        
+        MCID _cond31_m;
+        
+        int _cond31 = MC2_equals(_mseq, (uint64_t)seq, _mold_seq, (uint64_t)old_seq, &_cond31_m);
+        if (_cond31) {_br31 = MC2_branchUsesID(_cond31_m, 1, 2, true);
+        
+               MC2_merge(_br31);
+        } else {
+            _br31 = MC2_branchUsesID(_cond31_m, 0, 2, true);
+            res = -1;
+               MC2_merge(_br31);
+        }
+       MC2_merge(_br30);
+    }
+    *retval = _mres;
+    return res;
+}
+    
+int seqlock_write(MCID _mnew_data, int new_data, MCID * retval) {
+    MCID _mold_seq; _mold_seq=MC2_nextOpLoad(MCID_NODEP); int old_seq = load_32(&_seq);
+    int res;
+    
+    MCID _br32;
+    
+    int _cond32 = old_seq % 2 == 1;
+    MCID _cond32_m = MC2_function_id(32, 1, sizeof(_cond32), _cond32, _mold_seq);
+    if (_cond32) {
+        _br32 = MC2_branchUsesID(_cond32_m, 1, 2, true);
+        res = 0;
+       MC2_merge(_br32);
+    } else {
+        MCID _fn0; _br32 = MC2_branchUsesID(_cond32_m, 0, 2, true);
+        int new_seq = old_seq + 1;
+        _fn0 = MC2_function_id(33, 1, sizeof (new_seq), (uint64_t)new_seq, _mold_seq); 
+        MCID _rmw0 = MC2_nextRMW(MCID_NODEP, _mold_seq, _fn0);
+        int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
+        
+        MCID _br33;
+        
+        MCID _cond33_m;
+        
+        int _cond33 = MC2_equals(_rmw0, (uint64_t)cas_value, _mold_seq, (uint64_t)old_seq, &_cond33_m);
+        if (_cond33) {
+            // Update the data
+            _br33 = MC2_branchUsesID(_cond33_m, 1, 2, true);
+            MC2_nextOpStore(MCID_NODEP, _mnew_data);
+            store_32(&_data, new_data);
+                       MCID _rmw1 = MC2_nextRMW(MCID_NODEP, MCID_NODEP, MCID_NODEP);
+                       rmw_32(ADD, &_seq, /* dummy */0, 1);
+            res = 1;
+               MC2_merge(_br33);
+        } else {
+            _br33 = MC2_branchUsesID(_cond33_m, 0, 2, true);
+            res = 0;
+               MC2_merge(_br33);
+        }
+       MC2_merge(_br32);
+    }
+    *retval = MCID_NODEP;
+    return res;
+}
+
+static void a(void *obj) {
+       int q;
+    MC2_enterLoop();
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        MCID _rv0;
+        q = seqlock_write(MCID_NODEP, 30, &_rv0);
+       }
+MC2_exitLoop();
+
+
+}
+
+static void b(void *obj) {
+    int r1;
+    MC2_enterLoop();
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        MCID _rv1;
+        r1 = seqlock_read(&_rv1);
+       }
+MC2_exitLoop();
+
+
+}
+
+static void c(void *obj) {
+    int r1;
+    MC2_enterLoop();
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        MCID _rv2;
+        r1 = seqlock_read(&_rv2);
+       }
+MC2_exitLoop();
+
+
+}
+
+int user_main(int argc, char **argv) {
+    thrd_t t1; thrd_t t2; thrd_t t3;
+    seqlock_init();
+
+    thrd_create(&t1, (thrd_start_t)&a, NULL);
+    thrd_create(&t2, (thrd_start_t)&b, NULL);
+    thrd_create(&t3, (thrd_start_t)&c, NULL);
+
+    thrd_join(t1);
+    thrd_join(t2);
+    thrd_join(t3);
+
+
+    return 0;
+}
diff --git a/benchmarks/satcheck-precompiled/seqlock/seqlock_unannotated.cc b/benchmarks/satcheck-precompiled/seqlock/seqlock_unannotated.cc
new file mode 100644 (file)
index 0000000..e380a2e
--- /dev/null
@@ -0,0 +1,95 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "libinterface.h"
+
+// Sequence for reader consistency check
+/*atomic_*/ int _seq;
+// It needs to be atomic to avoid data races
+/*atomic_*/ int _data;
+
+void seqlock_init() {
+    store_32(&_seq, 0);
+    store_32(&_data, 10);
+}
+
+int seqlock_read() {
+    int res;
+       int old_seq = load_32(&_seq); // acquire
+
+       if (old_seq % 2 == 1) {
+        res = -1;
+    } else {
+               res = load_32(&_data);
+        int seq = load_32(&_seq);
+    
+        if (seq == old_seq) {
+        } else {
+            res = -1;
+        }
+    }
+    return res;
+}
+    
+int seqlock_write(int new_data) {
+    int old_seq = load_32(&_seq);
+    int res;
+    
+    if (old_seq % 2 == 1) {
+        res = 0;
+    } else {
+        int new_seq = old_seq + 1;
+        int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
+        
+        if (cas_value == old_seq) {
+            // Update the data
+            store_32(&_data, new_data);
+                       rmw_32(ADD, &_seq, /* dummy */0, 1);
+            res = 1;
+        } else {
+            res = 0;
+        }
+    }
+    return res;
+}
+
+static void a(void *obj) {
+       int q;
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        q = seqlock_write(30);
+       }
+
+}
+
+static void b(void *obj) {
+    int r1;
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        r1 = seqlock_read();
+       }
+
+}
+
+static void c(void *obj) {
+    int r1;
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        r1 = seqlock_read();
+       }
+
+}
+
+int user_main(int argc, char **argv) {
+    thrd_t t1; thrd_t t2; thrd_t t3;
+    seqlock_init();
+
+    thrd_create(&t1, (thrd_start_t)&a, NULL);
+    thrd_create(&t2, (thrd_start_t)&b, NULL);
+    thrd_create(&t3, (thrd_start_t)&c, NULL);
+
+    thrd_join(t1);
+    thrd_join(t2);
+    thrd_join(t3);
+
+
+    return 0;
+}
diff --git a/benchmarks/satcheck/dekker/.gitignore b/benchmarks/satcheck/dekker/.gitignore
new file mode 100644 (file)
index 0000000..dead37e
--- /dev/null
@@ -0,0 +1,4 @@
+dekker-fences
+dekker-fences.c
+log_file
+logall
diff --git a/benchmarks/satcheck/dekker/bench.sh b/benchmarks/satcheck/dekker/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/dekker/benchmark-config.sh b/benchmarks/satcheck/dekker/benchmark-config.sh
new file mode 100644 (file)
index 0000000..195bcbc
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=dekker-fences
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20 30"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20 30 40"
+RUN_FRONTEND=true
+RUNTIME_FLAGS=-Y
diff --git a/benchmarks/satcheck/dekker/benchtso.sh b/benchmarks/satcheck/dekker/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/dekker/clean.sh b/benchmarks/satcheck/dekker/clean.sh
new file mode 100755 (executable)
index 0000000..a1255ac
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/sh
+rm -f dekker-fences dekker-fences.c dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck/dekker/compile.sh b/benchmarks/satcheck/dekker/compile.sh
new file mode 100755 (executable)
index 0000000..5da0c11
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/sh
+. ../path.sh
+. ./benchmark-config.sh
+echo $MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include
+$MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include > ${NAME}.c
diff --git a/benchmarks/satcheck/dekker/dekker-fences_unannotated.c b/benchmarks/satcheck/dekker/dekker-fences_unannotated.c
new file mode 100644 (file)
index 0000000..68ebc84
--- /dev/null
@@ -0,0 +1,127 @@
+/*
+ * Dekker's critical section algorithm, implemented with fences.
+ * Translated to C by Patrick Lam <prof.lam@gmail.com>
+ *
+ * URL:
+ *   http://www.justsoftwaresolutions.co.uk/threading/
+ */
+
+#include <threads.h>
+#include <stdbool.h>
+#include "libinterface.h"
+
+/* atomic */ int flag0, flag1;
+/* atomic */ int turn;
+
+#define true 1
+#define false 0
+#define NULL 0
+
+/* uint32_t */ int var = 0;
+
+void p0() {
+       store_32(&flag0, true);
+       // std::atomic_thread_fence(std::memory_order_seq_cst);
+
+       int f1;
+       while (true)
+       {
+               f1 = load_32(&flag1);
+               if (!f1) {
+                       break;
+               }
+
+               if (load_32(&turn)) {
+                       store_32(&flag0, false);
+                       while(1) {
+                               if (!load_32(&turn)) {
+                                       break;
+                               }
+                               
+                               MC2_yield();
+                       }
+
+                       store_32(&flag0, true);
+               } else {
+                       MC2_yield();
+               }
+       }
+
+       // std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       store_32(&var, 1);
+
+       store_32(&turn, 1);
+       // std::atomic_thread_fence(std::memory_order_release);
+       store_32(&flag0, false);
+}
+
+void p1() {
+       store_32(&flag1, true);
+       // std::atomic_thread_fence(std::memory_order_seq_cst);
+       
+       int f0;
+       while (true) {
+               int f0 = load_32(&flag0);
+               if (!f0) {
+                       break;
+               }
+               
+               if (!load_32(&turn)) {
+                       store_32(&flag1, false);
+                       while (1) {
+                               if (load_32(&turn))
+                                       break;
+                               MC2_yield();
+                       }
+                       
+                       store_32(&flag1, true);
+                       // std::atomic_thread_fence(std::memory_order_seq_cst);
+               }
+       }
+
+       // std::atomic_thread_fence(std::memory_order_acquire);
+
+       // critical section
+       store_32(&var, 2);
+
+       store_32(&turn, 0);
+       // std::atomic_thread_fence(std::memory_order_release);
+       store_32(&flag1, false);
+}
+
+void p0l(void *a) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p0();
+       }
+}
+
+
+void p1l(void *a) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               p1();
+       }
+}
+
+
+int user_main(int argc, char **argv)
+{
+       thrd_t a, b;
+
+       store_32(&flag0, false);
+
+       store_32(&flag1, false);
+
+       store_32(&turn, 0);
+
+       thrd_create(&a, p0l, NULL);
+       thrd_create(&b, p1l, NULL);
+
+       thrd_join(a);
+       thrd_join(b);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck/dekker/diff.sh b/benchmarks/satcheck/dekker/diff.sh
new file mode 100755 (executable)
index 0000000..de3ac5e
--- /dev/null
@@ -0,0 +1,3 @@
+#!/bin/sh
+NAME=dekker
+diff -ub ../../satcheck-precompiled/${NAME}/dekker-fences.c dekker-fences.c
diff --git a/benchmarks/satcheck/linuxlock/.gitignore b/benchmarks/satcheck/linuxlock/.gitignore
new file mode 100644 (file)
index 0000000..0d26fa4
--- /dev/null
@@ -0,0 +1,4 @@
+linuxlocks
+linuxlocks.c
+log_file
+logall
diff --git a/benchmarks/satcheck/linuxlock/bench.sh b/benchmarks/satcheck/linuxlock/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/linuxlock/benchmark-config.sh b/benchmarks/satcheck/linuxlock/benchmark-config.sh
new file mode 100644 (file)
index 0000000..a372bfe
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=linuxlocks
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20 30 40 50 60 70 80 90 100 150 200 250"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20 30 40 50 60 70 80 90 100"
+RUN_FRONTEND=true
+RUNTIME_FLAGS=
diff --git a/benchmarks/satcheck/linuxlock/benchtso.sh b/benchmarks/satcheck/linuxlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/linuxlock/clean.sh b/benchmarks/satcheck/linuxlock/clean.sh
new file mode 100755 (executable)
index 0000000..9a90971
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f linuxlocks.c linuxlocks dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck/linuxlock/compile.sh b/benchmarks/satcheck/linuxlock/compile.sh
new file mode 100755 (executable)
index 0000000..5da0c11
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/sh
+. ../path.sh
+. ./benchmark-config.sh
+echo $MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include
+$MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include > ${NAME}.c
diff --git a/benchmarks/satcheck/linuxlock/diff.sh b/benchmarks/satcheck/linuxlock/diff.sh
new file mode 100755 (executable)
index 0000000..7c3e7be
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=linuxlock
+diff -ub ../../satcheck-precompiled/$NAME/linuxlocks.c linuxlocks.c
+
diff --git a/benchmarks/satcheck/linuxlock/linuxlocks_unannotated.c b/benchmarks/satcheck/linuxlock/linuxlocks_unannotated.c
new file mode 100644 (file)
index 0000000..362080a
--- /dev/null
@@ -0,0 +1,61 @@
+#include <stdlib.h>
+#include <stdio.h>
+#include <threads.h>
+#include <stdbool.h>
+#include "libinterface.h"
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       int lock;
+} rwlock_t;
+
+static inline bool write_trylock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(CAS, &rw->lock, 0, 1);
+       return priorvalue;
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       store_32(&rw->lock, 0);
+}
+
+rwlock_t * mylock;
+
+static void foo() {
+       int flag=write_trylock(mylock);
+       if (flag) {
+       } else {
+               write_unlock(mylock);
+       }
+}
+
+static void a(void *obj)
+{
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               foo();
+}
+
+int user_main(int argc, char **argv)
+{
+       thrd_t t1, t2;//, t3, t4;
+       mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
+       store_32(&mylock->lock, 0);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       //thrd_create(&t3, (thrd_start_t)&a, NULL);
+       //thrd_create(&t4, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       //thrd_join(t3);
+       //thrd_join(t4);
+
+
+
+       return 0;
+}
diff --git a/benchmarks/satcheck/linuxrwlock/.gitignore b/benchmarks/satcheck/linuxrwlock/.gitignore
new file mode 100644 (file)
index 0000000..6f9d7ac
--- /dev/null
@@ -0,0 +1,5 @@
+linuxrwlocks.c
+llinuxrwlocks
+log_file
+logall
+linuxrwlocks
diff --git a/benchmarks/satcheck/linuxrwlock/bench.sh b/benchmarks/satcheck/linuxrwlock/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/linuxrwlock/benchmark-config.sh b/benchmarks/satcheck/linuxrwlock/benchmark-config.sh
new file mode 100644 (file)
index 0000000..f2d4907
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=linuxrwlocks
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20"
+RUN_FRONTEND=true
+RUNTIME_FLAGS=
diff --git a/benchmarks/satcheck/linuxrwlock/benchtso.sh b/benchmarks/satcheck/linuxrwlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/linuxrwlock/clean.sh b/benchmarks/satcheck/linuxrwlock/clean.sh
new file mode 100755 (executable)
index 0000000..3a12299
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f linuxrwlocks.cc linuxrwlocks dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck/linuxrwlock/compile.sh b/benchmarks/satcheck/linuxrwlock/compile.sh
new file mode 100755 (executable)
index 0000000..5da0c11
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/sh
+. ../path.sh
+. ./benchmark-config.sh
+echo $MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include
+$MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include > ${NAME}.c
diff --git a/benchmarks/satcheck/linuxrwlock/diff.sh b/benchmarks/satcheck/linuxrwlock/diff.sh
new file mode 100755 (executable)
index 0000000..32e6fad
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=linuxrwlock
+diff -ub ../../satcheck-precompiled/$NAME/linuxrwlocks.c linuxrwlocks.c
+
diff --git a/benchmarks/satcheck/linuxrwlock/linuxrwlocks_unannotated.c b/benchmarks/satcheck/linuxrwlock/linuxrwlocks_unannotated.c
new file mode 100644 (file)
index 0000000..10496dc
--- /dev/null
@@ -0,0 +1,128 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+#include <stdlib.h>
+
+#include "libinterface.h"
+
+#define RW_LOCK_BIAS            0x00100000
+#define WRITE_LOCK_CMP          RW_LOCK_BIAS
+
+/** Example implementation of linux rw lock along with 2 thread test
+ *  driver... */
+
+typedef union {
+       int lock;
+} rwlock_t;
+
+static inline void read_lock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
+
+       while (true) {
+               if (priorvalue <= 0) {
+               } else {
+                       break;
+               }
+
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
+
+               while (true) {
+                       int status = load_32(&rw->lock);
+                       if (status > 0) {
+                       } else {
+                               break;
+                       }
+                       MC2_yield();
+               }
+
+               
+               priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-1));
+       }
+}
+
+static inline void write_lock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+       while(true) {
+               if (priorvalue != RW_LOCK_BIAS) {
+               } else {
+                       break;
+               }
+
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+               
+               while (true) {
+                       int status = load_32(&rw->lock);
+                       if (status != RW_LOCK_BIAS) {
+                       } else {
+                               break;
+                       }
+                       MC2_yield();
+               }
+
+               priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+       }
+}
+
+static inline bool write_trylock(rwlock_t *rw)
+{
+       int priorvalue=rmw_32(ADD, &rw->lock, /* dummy */ 0, ((unsigned int)-(RW_LOCK_BIAS)));
+
+       int flag = priorvalue != RW_LOCK_BIAS;
+       if (!flag) {
+               rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+       }
+
+       return flag;
+}
+
+static inline void read_unlock(rwlock_t *rw)
+{
+       rmw_32(ADD, &rw->lock, /* dummy */ 0, 1);
+}
+
+static inline void write_unlock(rwlock_t *rw)
+{
+       rmw_32(ADD, &rw->lock, /* dummy */ 0, RW_LOCK_BIAS);
+}
+
+rwlock_t * mylock;
+int shareddata;
+
+static void foo() {
+       int res = write_trylock(mylock);
+       if (res) {
+               write_unlock(mylock);
+       } else {
+       }
+}
+
+static void a(void *obj)
+{
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++)
+               foo();
+}
+
+int user_main(int argc, char **argv)
+{
+       mylock = (rwlock_t*)malloc(sizeof(rwlock_t));
+
+       thrd_t t1, t2;
+       //, t3, t4;
+       store_32(&mylock->lock, RW_LOCK_BIAS);
+
+       thrd_create(&t1, (thrd_start_t)&a, NULL);
+       thrd_create(&t2, (thrd_start_t)&a, NULL);
+       //      thrd_create(&t3, (thrd_start_t)&a, NULL);
+       //      thrd_create(&t4, (thrd_start_t)&a, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+       //      thrd_join(t3);
+       //      thrd_join(t4);
+       free(mylock);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck/msqueueoffset/.gitignore b/benchmarks/satcheck/msqueueoffset/.gitignore
new file mode 100644 (file)
index 0000000..44bf736
--- /dev/null
@@ -0,0 +1,6 @@
+ms-queue-simple.c
+logall
+
+
+ms-queue-simple
+log_file
diff --git a/benchmarks/satcheck/msqueueoffset/bench.sh b/benchmarks/satcheck/msqueueoffset/bench.sh
new file mode 100755 (executable)
index 0000000..2471a37
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/msqueueoffset/benchmark-config.sh b/benchmarks/satcheck/msqueueoffset/benchmark-config.sh
new file mode 100644 (file)
index 0000000..96dc596
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=ms-queue-simple
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 11 12 13"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 11 12 13"
+RUN_FRONTEND=true
+RUNTIME_FLAGS=
diff --git a/benchmarks/satcheck/msqueueoffset/benchtso.sh b/benchmarks/satcheck/msqueueoffset/benchtso.sh
new file mode 100755 (executable)
index 0000000..bf5af51
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.c -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/msqueueoffset/clean.sh b/benchmarks/satcheck/msqueueoffset/clean.sh
new file mode 100755 (executable)
index 0000000..3a12299
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f linuxrwlocks.cc linuxrwlocks dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck/msqueueoffset/compile.sh b/benchmarks/satcheck/msqueueoffset/compile.sh
new file mode 100755 (executable)
index 0000000..5da0c11
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/sh
+. ../path.sh
+. ./benchmark-config.sh
+echo $MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include
+$MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.c -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include > ${NAME}.c
diff --git a/benchmarks/satcheck/msqueueoffset/diff.sh b/benchmarks/satcheck/msqueueoffset/diff.sh
new file mode 100755 (executable)
index 0000000..a835192
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=msqueueoffset
+diff -ub ../../satcheck-precompiled/$NAME/ms-queue-simple.c ms-queue-simple.c
+
diff --git a/benchmarks/satcheck/msqueueoffset/ms-queue-simple.h b/benchmarks/satcheck/msqueueoffset/ms-queue-simple.h
new file mode 100644 (file)
index 0000000..9f7f11c
--- /dev/null
@@ -0,0 +1,15 @@
+typedef struct node {
+       unsigned int value;
+       struct node * next;
+} node_t;
+
+typedef struct {
+       struct node * head;
+       struct node * tail;
+} queue_t;
+
+//void init_queue(queue_t *q, int num_threads);
+//void enqueue(queue_t *q, unsigned int val);
+//bool dequeue(queue_t *q, unsigned int *retVal);
+int get_thread_num();
+
diff --git a/benchmarks/satcheck/msqueueoffset/ms-queue-simple_unannotated.c b/benchmarks/satcheck/msqueueoffset/ms-queue-simple_unannotated.c
new file mode 100644 (file)
index 0000000..6fc7d7f
--- /dev/null
@@ -0,0 +1,137 @@
+#include <threads.h>
+#include <stdlib.h>
+#include <stdio.h>
+#define true 1
+#define false 0
+#define bool int
+
+#include "ms-queue-simple.h"
+#include "libinterface.h"
+
+void init_queue(queue_t *q, int num_threads);
+void enqueue(queue_t *q, unsigned int val);
+bool dequeue(queue_t *q, unsigned int *retVal);
+
+queue_t queue;
+
+void init_queue(queue_t *q, int num_threads) {
+       struct node *newnode=(struct node *)malloc(sizeof (struct node));
+       
+       store_32(&newnode->value, 0);
+
+       
+       store_64(&newnode->next, (uintptr_t) NULL);
+               /* initialize queue */
+       
+       store_64(&q->head, (uintptr_t) newnode);
+       
+       
+       store_64(&q->tail, (uintptr_t) newnode);
+}
+
+void enqueue(queue_t *q, unsigned int val) {
+       struct node *tail;
+       struct node * node_ptr; node_ptr = (struct node *)malloc(sizeof(struct node));
+       
+       store_32(&node_ptr->value, val);
+       
+       
+       store_64(&node_ptr->next, (uintptr_t) NULL);
+                       
+       while (true) {
+
+               tail = (struct node *) load_64(&q->tail);
+
+               struct node * next = (struct node *) load_64(&tail->next);
+               
+               struct node * qtail = (struct node *) load_64(&q->tail);
+
+               if (tail == qtail) {
+                       if (next) {
+                               MC2_yield();
+                       } else {
+                               struct node * valread = (struct node *) rmw_64(CAS, &tail->next, (uintptr_t) next, (uintptr_t) node_ptr);
+                               
+                               if (next == valread) {
+                                       break;
+                               } else {
+                               }
+                       }
+                       struct node * new_tailptr = (struct node *)load_64(&tail->next);
+                       rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) new_tailptr);
+                       MC2_yield();
+               } else { 
+                       MC2_yield();
+               }
+       }
+       
+       rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) node_ptr);
+}
+
+bool dequeue(queue_t *q, unsigned int *retVal) {
+       while (true) {
+               struct node * head = (struct node *) load_64(&q->head);
+               struct node * tail = (struct node *) load_64(&q->tail);
+               struct node * next = (struct node *) load_64(&head->next);
+
+               struct node * headr = (struct node *) load_64(&q->head);
+
+               if (head == headr) {
+                       if (head == tail) {
+                               if (next) {
+                                       MC2_yield();
+                               } else {
+                                       return false; // NULL
+                               }
+                               rmw_64(CAS, &q->tail, (uintptr_t) tail, (uintptr_t) next);
+                               MC2_yield();
+                       } else {
+                               *retVal = load_32(&next->value);
+                               struct node *old_head = (struct node *) rmw_64(CAS, &q->head,
+                                                                                                                                                                                                                        (uintptr_t) head, 
+                                                                                                                                                                                                                        (uintptr_t) next);
+
+                               if (head == old_head) {
+                                       return true;
+                               } else {
+                                       MC2_yield();
+                               }
+                       }
+               } else {
+                       MC2_yield();
+               }
+       }
+}
+
+/* ms-queue-main */
+bool succ1, succ2;
+
+static void e(void *p) {
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               enqueue(&queue, 1);
+       }
+}
+
+static void d(void *p) {
+       unsigned int val;
+       int i;
+       for(i=0;i<PROBLEMSIZE;i++) {
+               int r;
+               r = dequeue(&queue, &val);
+       }
+}
+
+int user_main(int argc, char **argv)
+{
+       init_queue(&queue, 2);
+
+       thrd_t t1,t2;
+       thrd_create(&t1, e, NULL);
+       thrd_create(&t2, d, NULL);
+
+       thrd_join(t1);
+       thrd_join(t2);
+
+       return 0;
+}
diff --git a/benchmarks/satcheck/seqlock/.gitignore b/benchmarks/satcheck/seqlock/.gitignore
new file mode 100644 (file)
index 0000000..16d53f3
--- /dev/null
@@ -0,0 +1,4 @@
+log_file
+logall
+seqlock
+seqlock.cc
diff --git a/benchmarks/satcheck/seqlock/bench.sh b/benchmarks/satcheck/seqlock/bench.sh
new file mode 100755 (executable)
index 0000000..a03b573
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_SC ;
+do
+echo size= $i >> log
+gcc ${NAME}.cc -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -lsc_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/seqlock/benchmark-config.sh b/benchmarks/satcheck/seqlock/benchmark-config.sh
new file mode 100644 (file)
index 0000000..ffd0c5f
--- /dev/null
@@ -0,0 +1,5 @@
+NAME=seqlock
+SIZES_SC="1 2 3 4 5 6 7 8 9 10 15 20 25 30 35 40 50 60"
+SIZES_TSO="1 2 3 4 5 6 7 8 9 10 15 20 25 30 35 40 50 60"
+RUN_FRONTEND=true
+RUNTIME_FLAGS=-Y
diff --git a/benchmarks/satcheck/seqlock/benchtso.sh b/benchmarks/satcheck/seqlock/benchtso.sh
new file mode 100755 (executable)
index 0000000..3c52574
--- /dev/null
@@ -0,0 +1,16 @@
+#!/bin/bash
+source ../path.sh
+source benchmark-config.sh
+export PATH=$MC2DIR:$PATH
+/bin/rm -f log logall
+if [ $RUN_FRONTEND == true ]; then
+ ./compile.sh
+fi
+for i in $SIZES_TSO ;
+do
+echo size= $i >> log
+gcc ${NAME}.cc -DPROBLEMSIZE=$i -O3 -I$MC2DIR/include -L$MC2DIR -ltso_model -o ${NAME}
+export LD_LIBRARY_PATH=$MC2DIR
+export DYLD_LIBRARY_PATH=$MC2DIR
+(time ./${NAME} ${RUNTIME_FLAGS}) >> logall 2>> log
+done
diff --git a/benchmarks/satcheck/seqlock/clean.sh b/benchmarks/satcheck/seqlock/clean.sh
new file mode 100755 (executable)
index 0000000..325db38
--- /dev/null
@@ -0,0 +1,2 @@
+#!/bin/bash
+rm -f seqlock.cc seqlock dimacs.out dimacs.cnf logall log_file
diff --git a/benchmarks/satcheck/seqlock/compile.sh b/benchmarks/satcheck/seqlock/compile.sh
new file mode 100755 (executable)
index 0000000..469e6e3
--- /dev/null
@@ -0,0 +1,5 @@
+#!/bin/sh
+. ../path.sh
+. ./benchmark-config.sh
+echo $MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.cc -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include
+$MC2DIR/clang/build/add_mc2_annotations ${NAME}_unannotated.cc -- -DPROBLEMSIZE=1 -I/usr/include -I$CLANG_INCLUDE_DIR -I$MC2DIR/include > ${NAME}.cc
diff --git a/benchmarks/satcheck/seqlock/diff.sh b/benchmarks/satcheck/seqlock/diff.sh
new file mode 100755 (executable)
index 0000000..7f89e87
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/sh
+NAME=seqlock
+diff -ub ../../satcheck-precompiled/$NAME/seqlock.cc seqlock.cc
+
diff --git a/benchmarks/satcheck/seqlock/seqlock_unannotated.cc b/benchmarks/satcheck/seqlock/seqlock_unannotated.cc
new file mode 100644 (file)
index 0000000..e380a2e
--- /dev/null
@@ -0,0 +1,95 @@
+#include <stdio.h>
+#include <threads.h>
+#include <stdatomic.h>
+
+#include "libinterface.h"
+
+// Sequence for reader consistency check
+/*atomic_*/ int _seq;
+// It needs to be atomic to avoid data races
+/*atomic_*/ int _data;
+
+void seqlock_init() {
+    store_32(&_seq, 0);
+    store_32(&_data, 10);
+}
+
+int seqlock_read() {
+    int res;
+       int old_seq = load_32(&_seq); // acquire
+
+       if (old_seq % 2 == 1) {
+        res = -1;
+    } else {
+               res = load_32(&_data);
+        int seq = load_32(&_seq);
+    
+        if (seq == old_seq) {
+        } else {
+            res = -1;
+        }
+    }
+    return res;
+}
+    
+int seqlock_write(int new_data) {
+    int old_seq = load_32(&_seq);
+    int res;
+    
+    if (old_seq % 2 == 1) {
+        res = 0;
+    } else {
+        int new_seq = old_seq + 1;
+        int cas_value = rmw_32(CAS, &_seq, old_seq, new_seq);
+        
+        if (cas_value == old_seq) {
+            // Update the data
+            store_32(&_data, new_data);
+                       rmw_32(ADD, &_seq, /* dummy */0, 1);
+            res = 1;
+        } else {
+            res = 0;
+        }
+    }
+    return res;
+}
+
+static void a(void *obj) {
+       int q;
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        q = seqlock_write(30);
+       }
+
+}
+
+static void b(void *obj) {
+    int r1;
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        r1 = seqlock_read();
+       }
+
+}
+
+static void c(void *obj) {
+    int r1;
+    for (int i = 0; i < PROBLEMSIZE; i++) {
+        r1 = seqlock_read();
+       }
+
+}
+
+int user_main(int argc, char **argv) {
+    thrd_t t1; thrd_t t2; thrd_t t3;
+    seqlock_init();
+
+    thrd_create(&t1, (thrd_start_t)&a, NULL);
+    thrd_create(&t2, (thrd_start_t)&b, NULL);
+    thrd_create(&t3, (thrd_start_t)&c, NULL);
+
+    thrd_join(t1);
+    thrd_join(t2);
+    thrd_join(t3);
+
+
+    return 0;
+}
diff --git a/benchmarks/verifycompilesat b/benchmarks/verifycompilesat
new file mode 100755 (executable)
index 0000000..6227066
--- /dev/null
@@ -0,0 +1,4 @@
+#!/bin/bash
+# note: should do something about seqlock, which is .cc not .c
+for c in dekker linuxlock linuxrwlock msqueueoffset ; do (. satcheck/$c/benchmark-config.sh; diff -u satcheck-precompiled/$c/$NAME.c satcheck/$c/$NAME.c) done
+for c in seqlock ; do (. satcheck/$c/benchmark-config.sh; diff -u satcheck-precompiled/$c/$NAME.cc satcheck/$c/$NAME.cc) done
diff --git a/bin/annotate b/bin/annotate
new file mode 100755 (executable)
index 0000000..d60ffa5
--- /dev/null
@@ -0,0 +1,7 @@
+#!/bin/bash
+DIR=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
+MC2DIR=`dirname $DIR`
+CLANG_INCLUDE_DIR=/usr/lib/llvm-3.7/lib/clang/3.7.0/include
+
+$MC2DIR/clang/build/add_mc2_annotations $1 -- -DPROBLEMSIZE=1 -I/usr/include -I$MC2DIR/include -I$CLANG_INCLUDE_DIR
+
diff --git a/branchrecord.cc b/branchrecord.cc
new file mode 100644 (file)
index 0000000..e55aa24
--- /dev/null
@@ -0,0 +1,59 @@
+/*      Copyright (c) 2015 Regents of the University of California
+ *
+ *      Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ *      This program is free software; you can redistribute it and/or
+ *      modify it under the terms of the GNU General Public License
+ *      version 2 as published by the Free Software Foundation.
+ */
+
+#include "branchrecord.h"
+#include "mymemory.h"
+#include "constraint.h"
+#include "eprecord.h"
+
+BranchRecord::BranchRecord(EPRecord *r, uint nvars, Constraint **cvars, bool isalwaysexecuted) :
+       branch(r),
+       hasNext(r->getNextRecord()!=NULL),
+       numvars(nvars),
+       numdirections(r->numValues()),
+       alwaysexecuted(isalwaysexecuted),
+       vars((Constraint **)model_malloc(sizeof(Constraint *)*nvars)) {
+       memcpy(vars, cvars, sizeof(Constraint *)*nvars);
+}
+
+BranchRecord::~BranchRecord() {
+       model_free(vars);
+}
+
+Constraint * BranchRecord::getAnyBranch() {
+       if (alwaysexecuted)
+               return &ctrue;
+       else
+               return new Constraint(OR, numvars, vars);
+}
+
+Constraint * BranchRecord::getNewBranch() {
+       return new Constraint(AND, numvars, vars);
+}
+
+Constraint * BranchRecord::getBranch(EPValue *val) {
+       int index=branch->getIndex(val);
+       ASSERT(index>=0);
+       if (!alwaysexecuted)
+               index++;
+       return generateConstraint(numvars, vars, index);
+}
+
+int BranchRecord::getBranchValue(bool * array) {
+       uint value=0;
+       for(int j=numvars-1;j>=0;j--) {
+               value=value<<1;
+               if (array[vars[j]->getVar()])
+                       value|=1;
+       }
+       if (!alwaysexecuted)
+               value--;
+       
+       return value;
+}
diff --git a/branchrecord.h b/branchrecord.h
new file mode 100644 (file)
index 0000000..aa5e4a2
--- /dev/null
@@ -0,0 +1,33 @@
+/*      Copyright (c) 2015 Regents of the University of California
+ *
+ *      Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ *      This program is free software; you can redistribute it and/or
+ *      modify it under the terms of the GNU General Public License
+ *      version 2 as published by the Free Software Foundation.
+ */
+
+#ifndef BRANCHRECORD_H
+#define BRANCHRECORD_H
+#include "classlist.h"
+
+class BranchRecord {
+ public:
+       BranchRecord(EPRecord *record, uint numvars, Constraint **vars, bool isalwaysexecuted);
+       ~BranchRecord();
+       Constraint * getAnyBranch();
+       Constraint * getBranch(EPValue *val);
+       Constraint * getNewBranch();
+       int getBranchValue(bool *array);
+       int numDirections() {return numdirections;}
+       bool hasNextRecord() {return hasNext;}
+       MEMALLOC;
+ private:
+  EPRecord *branch;
+       bool hasNext;
+  uint numvars;
+       uint numdirections;
+       bool alwaysexecuted;
+  Constraint **vars;
+};
+#endif
diff --git a/cgoal.cc b/cgoal.cc
new file mode 100644 (file)
index 0000000..95c26ab
--- /dev/null
+++ b/cgoal.cc
@@ -0,0 +1,61 @@
+/*      Copyright (c) 2015 Regents of the University of California
+ *
+ *      Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ *      This program is free software; you can redistribute it and/or
+ *      modify it under the terms of the GNU General Public License
+ *      version 2 as published by the Free Software Foundation.
+ */
+
+#include "cgoal.h"
+#include "execpoint.h"
+#include "eprecord.h"
+
+CGoal::CGoal(unsigned int _num, uint64_t *vals) :
+       outputvalue(0),
+       num(_num),
+       hash(_num)
+{
+       valarray=(uint64_t *)model_malloc(sizeof(uint64_t)*num);
+       for(unsigned int i=0;i<num;i++) {
+               hash^=(valarray[i]=vals[i]);
+       }
+}
+
+CGoal::~CGoal() {
+       if (valarray)
+               model_free(valarray);
+}
+
+void CGoal::print() {
+       model_print("goal: ");
+       model_print("(");
+       for(uint i=0;i<num;i++) {
+               model_print("%lu",valarray[i]);
+               if ((i+1)!=num)
+                       model_print(", ");
+       }
+       model_print(")");
+}
+
+bool CGoalEquals(CGoal *cg1, CGoal *cg2) {
+       if (cg1==NULL) {
+               return cg2==NULL;
+       }
+       if (cg1->hash!=cg2->hash||
+                       cg1->num!=cg2->num)
+               return false;
+       if (cg1->valarray) {
+               for(unsigned int i=0;i<cg1->num;i++) {
+                       if (cg1->valarray[i]!=cg2->valarray[i])
+                               return false;
+               }
+       }
+
+       return true;
+}
+
+unsigned int CGoalHash(CGoal *cg) {
+       return cg->hash;
+}
+
diff --git a/cgoal.h b/cgoal.h
new file mode 100644 (file)
index 0000000..3374062
--- /dev/null
+++ b/cgoal.h
@@ -0,0 +1,44 @@
+/*      Copyright (c) 2015 Regents of the University of California
+ *
+ *      Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ *      This program is free software; you can redistribute it and/or
+ *      modify it under the terms of the GNU General Public License
+ *      version 2 as published by the Free Software Foundation.
+ */
+
+#ifndef C_GOAL_H
+#define C_GOAL_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "hashset.h"
+#include <stdint.h>
+
+class CGoal {
+ public:
+       CGoal(unsigned int num, uint64_t *vals);
+       ~CGoal();
+       unsigned int getNum() {return num;}
+       uint64_t getValue(unsigned int i) {return valarray[i];}
+       void setOutput(uint64_t _output) { outputvalue=_output;}
+       uint64_t getOutput() {return outputvalue;}
+       void print();
+
+       MEMALLOC;
+ private:
+       uint64_t * valarray;
+       uint64_t outputvalue;
+       unsigned int num;
+       unsigned int hash;
+       
+       friend bool CGoalEquals(CGoal *cg1, CGoal *cg2);
+       friend unsigned int CGoalHash(CGoal *cg);
+};
+
+bool CGoalEquals(CGoal *cg1, CGoal *cg2);
+unsigned int CGoalHash(CGoal *cg);
+
+typedef HashSet<CGoal *, uintptr_t, 0, model_malloc, model_calloc, model_free, CGoalHash, CGoalEquals> CGoalSet;
+typedef HSIterator<CGoal *, uintptr_t, 0, model_malloc, model_calloc, model_free, CGoalHash, CGoalEquals> CGoalIterator;
+
+#endif
diff --git a/change.cc b/change.cc
new file mode 100644 (file)
index 0000000..86de570
--- /dev/null
+++ b/change.cc
@@ -0,0 +1,38 @@
+/*      Copyright (c) 2015 Regents of the University of California
+ *
+ *      Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ *      This program is free software; you can redistribute it and/or
+ *      modify it under the terms of the GNU General Public License
+ *      version 2 as published by the Free Software Foundation.
+ */
+
+#include "change.h"
+
+MCChange::MCChange(EPRecord * _record, uint64_t _val, unsigned int _index) :
+       record(_record),
+       val(_val),
+       index(_index)
+{
+       ASSERT(record->getType()!=BRANCHDIR);
+}
+
+MCChange::~MCChange() {
+}
+
+void MCChange::print() {
+       record->print();
+       model_print("(");
+       model_print("index=%u, val=%lu)\n", index, val);
+}
+
+bool MCChangeEquals(MCChange *mcc1, MCChange *mcc2) {
+       if (mcc1==NULL)
+               return mcc1==mcc2;
+       return (mcc1->record==mcc2->record) && (mcc1->val==mcc2->val) && (mcc1->index == mcc2->index);
+}
+
+unsigned int MCChangeHash(MCChange *mcc) {
+       return ((unsigned int)((uintptr_t)mcc->record))^((unsigned int)mcc->val)^mcc->index;
+}
+
diff --git a/change.h b/change.h
new file mode 100644 (file)
index 0000000..f2e0bef
--- /dev/null
+++ b/change.h
@@ -0,0 +1,42 @@
+/*      Copyright (c) 2015 Regents of the University of California
+ *
+ *      Author: Brian Demsky <bdemsky@uci.edu>
+ *
+ *      This program is free software; you can redistribute it and/or
+ *      modify it under the terms of the GNU General Public License
+ *      version 2 as published by the Free Software Foundation.
+ */
+
+#ifndef CHANGE_H
+#define CHANGE_H
+#include "classlist.h"
+#include "mymemory.h"
+#include <stdint.h>
+#include "eprecord.h"
+
+class MCChange {
+ public:
+       MCChange(EPRecord *record, uint64_t _val, unsigned int _index);
+       ~MCChange();
+       EPRecord *getRecord() {return record;}
+       int getIndex() {return index;}
+       uint64_t getValue() {return val;}
+       bool isRMW() {return record->getType()==RMW;}
+       bool isFunction() {return record->getType()==FUNCTION;}
+       bool isEquals() {return record->getType()==EQUALS;}
+       bool isLoad() {return record->getType()==LOAD;}
+       bool isStore() {return record->getType()==STORE;}
+       void print();
+       MEMALLOC;
+
+ private:
+       EPRecord *record;
+       uint64_t val;
+       unsigned int index;
+       friend bool MCChangeEquals(MCChange *mcc1, MCChange *mcc2);
+       friend unsigned int MCChangeHash(MCChange *mcc);
+};
+
+bool MCChangeEquals(MCChange *mcc1, MCChange *mcc2);
+unsigned int MCChangeHash(MCChange *mcc);
+#endif
diff --git a/clang/.gitignore b/clang/.gitignore
new file mode 100644 (file)
index 0000000..2928847
--- /dev/null
@@ -0,0 +1,4 @@
+build
+*~
+
+
diff --git a/clang/COPYING b/clang/COPYING
new file mode 100644 (file)
index 0000000..b3dcc98
--- /dev/null
@@ -0,0 +1,14 @@
+Copyright (c) 2015 Patrick Lam
+All rights reserved.
+
+Developed by:                  Patrick Lam
+                       University of Waterloo
+                        http://patricklam.ca
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal with the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+    Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimers.
+    Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimers in the documentation and/or other materials provided with the distribution.
+    Neither the names of the University of Waterloo, nor the names of its contributors may be used to endorse or promote products derived from this Software without specific prior written permission. 
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH THE SOFTWARE. 
\ No newline at end of file
diff --git a/clang/Makefile b/clang/Makefile
new file mode 100644 (file)
index 0000000..5b8ed2d
--- /dev/null
@@ -0,0 +1,92 @@
+#-------------------------------------------------------------------------------
+# Sample makefile for building the code samples. Read inline comments for
+# documentation.
+#
+# Eli Bendersky (eliben@gmail.com)
+# This code is in the public domain
+#-------------------------------------------------------------------------------
+
+# The following variables will likely need to be customized, depending on where
+# and how you built LLVM & Clang. They can be overridden by setting them on the
+# make command line: "make VARNAME=VALUE", etc.
+
+LLVM_VERSION := -3.8
+
+# CXX has to be a fairly modern C++ compiler that supports C++11. gcc 4.8 and
+# higher or Clang 3.2 and higher are recommended. Best of all, if you build LLVM
+# from sources, use the same compiler you built LLVM with.
+CXX := clang++$(LLVM_VERSION)
+CXXFLAGS := -fno-rtti -g
+PLUGIN_CXXFLAGS := -fpic
+
+LLVM_CXXFLAGS := `llvm-config$(LLVM_VERSION) --cxxflags`
+LLVM_LDFLAGS := `llvm-config$(LLVM_VERSION) --ldflags --libs --system-libs`
+
+# Plugins shouldn't link LLVM and Clang libs statically, because they are
+# already linked into the main executable (opt or clang). LLVM doesn't like its
+# libs to be linked more than once because it uses globals for configuration
+# and plugin registration, and these trample over each other.
+LLVM_LDFLAGS_NOLIBS := `llvm-config$(LLVM_VERSION) --ldflags`
+PLUGIN_LDFLAGS := -shared
+
+CLANG_INCLUDES := -I/usr/lib/llvm$(LLVM_VERSION)/include
+
+#&n