Prepare for submit version

DPOR_README

@@ -0,0 +1,210 @@
+Optimal Dynamic Partial Order Reduction for Analysis of Concurrent Programs
+---------------------------------------------------------------------------
+
+Contents:
+---------
+
+1. Introduction
+2. Prerequisites
+3. Quick intro
+4. Tests
+5. Interesting details in the code
+
+1. Introduction
+---------------
+
+The purpose of this readme file is to offer a brief guide around an
+experimental version of the Concuerror tool, which was developed to include an
+algorithm for optimal partial order reduction of the state space generated by
+the exploration of concurrent applications written in the Erlang language.
+
+The experimental functionality, as well as two more similar
+extensions/modifications are enabled with command line options. The tool runs
+the stable version, if these are not provided. The stable version supports a few
+more Erlang built-in functions that require preemption points and has been
+tested and integrated with a GUI. The experimental versions use the command line
+interface.
+
+2. Prerequisites
+----------------
+
+Concuerror is an Erlang application, so you will need an Erlang runtime system
+to run it. Most Linux distributions have suitable packages. To run the original
+Concuerror testsuite you will also need Python. The application startup and
+shutdown relies on a bash script, so it is currently not possible to run
+Concuerror on a Windows machine.
+
+You can build the application using 'make'
+
+3. Quick intro
+--------------
+
+Concuerror expects as input a set of Erlang source modules, a target function
+and a preemption bound. Its output in results.txt are all the traces of the
+program that had some concurrency error.
+
+We explain each briefly the command line options:
+
+- source files : are the files that will be instrumented to include preemption
+                 points before built-in functions that may affect the global
+                 state.
+
+  Option: -f <files>
+
+- target function : is an exported function in one of the files given as
+                    input. This is the function that will be run by the first
+                    process.
+
+  Option: -t <Module> <Name> [<arg1> <arg2>] (arguments are optional. If none is
+                                              given, the function with 0 arity
+                                              will be called)
+
+- preemption bound : designates how many 'unnecessary' preemptions are allowed
+                     in the current run. Concuerror will always allow enabled
+                     processes to run after a process has become blocked (by
+                     trying to execute a receive when no matching messages are
+                     in its mailbox) and will also allow processes to be
+                     interrupted while still being enabled for other processes
+                     to be scheduled instead as many times as the preemption
+                     bound.
+
+  Option: -p <number or 'inf' for infinite bound> (default value is 2)
+
+- versions : by default you will be running the stable version of
+             Concuerror. The following command line options can be used to
+             enable 3 alternative versions, based on the same machinery:
+
+             --dpor_fake : is a 'sanity' check version of Concuerror using the
+                           modified scheduler, but treating all operations as
+                           dependent. Should give results similar to those of
+                           the stable version, with maybe a few more
+                           interleavings.
+
+             --dpor : is our experimental extension. Uses simple source sets to
+                      decide additional interleavings, together with our set of
+                      rules for dependencies between Erlang built-in functions.
+
+             --dpor_flanagan : is a version using the algorithm proposed by
+                               Flanagan and Godefroid, extended with sleep sets
+                               as described in our cited paper.
+
+Examples:
+
+To run stable Concuerror on two modules test.erl and foo.erl in your home
+directory, using test:run/0 as your starting function and infinite preemption
+bound:
+
+  ./concuerror -f ~/test.erl ~/foo.erl -t test run -p inf
+
+To run the same test using our experimental extension:
+
+  ./concuerror -f ~/test.erl ~/foo.erl -t test run -p inf --dpor
+
+You can run ./concuerror --help for description of a few more command line
+options.
+
+4. Tests
+--------
+
+You can instantly run two different testsuites that showcase the experimental
+version:
+
+a) The dpor_tests collection
+
+b) Concuerror's stable testsuite, which has been adapted slightly to run the
+   experimental version instead of the stable one.
+
+Let's go into more details:
+
+a) dpor_tests
+-------------
+
+This is a collection of motivating examples that were used during the
+development of the experimental version. They include toy Erlang programs as
+well as all the examples presented in the paper. The toy tests were written to
+expose dependencies in the supported Erlang built-in functions and to showcase
+the differences and strengths between the different versions of the tool.
+
+The tests output is compared against a stored expected output to decide success
+or failure. A few (less than 5, usually 1) of the tests are expected to fail: in
+these cases a diff of the expected output and the real output should show
+environment related changes, as the traces sometimes include information that is
+environment sensitive.
+
+These tests are in the dpor_tests directory and you can run all of them by:
+
+  dpor_tests/dpor_test
+
+... and a specific test by:
+
+  dpor_tests/dpor_test dpor_tests/dpor_test/src/<test>.erl
+
+The output is written in the dpor_tests/new_results directory and is compared
+with the reference output in dpor_tests/results. If it differs the test is
+reported as FAILED and the output is left for comparison. You can then use a
+(graphical) diff tool (e.g. meld) to see the differences in the outputs.
+
+You can of course run any of the tests with e.g.:
+
+./concuerror -f dpor_tests/src/<test>.erl -t <test> <test> -p inf --dpor
+
+Interesting tests in dpor_tests:
+--------------------------------
+
+- ets_dependencies.erl : This is the simple 2 readers vs 1 writer example.
+- ets_dependencies_n.erl : This is the extended example presented in the paper.
+    You can run this example with a varying number of readers <N> like this:
+
+    T=ets_dependencies
+    ./concuerror -f dpor_tests/src/$T.erl -t $T $T <N> -p inf --dpor
+
+- file_system_example.erl : The file system example written in Erlang
+- independent_receivers.erl : A test with just two interleavings, where stable
+    Concuerror explores 234300 interleavings.
+- register_again.erl : A test showing usage of Erlang built in functions.
+- ring_leader_election_symmetric : An implementation of leader election in a
+    set of processes connected in a ring.
+- ring_leader_election_symmetric_buffer.erl : Same as before, with the
+    difference that here mailboxes are 'modeled' as separate processes in such a
+    way that 'sends' and 'receives' are also interleaved, leading to an
+    explosion in the number of explored interleavings.
+- send_it_ets.erl : An example showing why send operations with the same message
+    to the same process must be also interleaved.
+
+b) Concuerror's stable testsuite
+--------------------------------
+
+Concuerror's stable testsuite has also been run with --dpor to check for any
+missing dependencies. The files are stored in testsuite/suites, including
+reference results. Running the tests creates the testsuite/results (which can
+again be diffed against the reference directory in case of failures).
+
+You can run the suite by:
+
+  make test
+
+87 of the tests are expected to fail because the reference results are those
+obtained by running --dpor_fake. This is to show the difference, which in most
+cases favors --dpor (unless an unsupported instruction is used, in which case
+the program crashes).
+
+The --dpor_fake results are in the dpor directories under each suite. They have
+been compared against the results (stored in the vanilla directories) obtained
+by running the stable version with a few added preemption points. These are in
+turn comparable with the original results (stored in the results directories).
+
+Interesting test in Concuerror's testsuite
+------------------------------------------
+
+- manolis_test_2workers: Corresponds to the rush_hour test presented in the
+    paper.
+
+5. Interesting details in the code
+----------------------------------
+
+Apart from concuerror_rep.erl which has all the replacement functions for the
+actual calls that are found in the instrumented modules, all the main algorithm
+run from concuerror_sched.erl. The dependent/2 boolean function returns true
+when two operations are dependent. The main loop of the algorithm is in the
+explore/1 function. Finally the two different DPOR versions differ in the details
+of add_all_backtracks/1 function.

src/concuerror.erl

@@ -362,6 +362,9 @@ help() ->
      "  --noprogress            Disable progress bar\n"
      "  -q|--quiet              Disable logging (implies --noprogress)\n"
      "  --gui                   Run concuerror with graphics\n"
+     "  --dpor                  Runs the experimental optimal DPOR version\n"
+     "  --dpor_fake             Runs a 'sanity check' experimental version\n"
+     "  --dpor_flanagan         Runs an experimental reference DPOR version\n"
      "  --help                  Show this help message\n"
      "\n"
      "Examples:\n"

testsuite/runtests.py

@@ -31,7 +31,7 @@ def runTest(test):
         files = [test]
     # Create a dir to save the results
     try:
-        os.makedirs(results + "/" + suite + "/dpor_fake")
+        os.makedirs(results + "/" + suite + "/dpor")
     except OSError:
         pass
     # Compile it
@@ -67,12 +67,12 @@ def runScenario(suite, name, modn, funn, preb, files):
     global total_failed
     sema.acquire()
     # Run concuerror
-    os.system("%s --dpor --target %s %s --files %s --output %s/%s/dpor_fake/%s-%s-%s.txt --preb %s --quiet"
+    os.system("%s --dpor --target %s %s --files %s --output %s/%s/dpor/%s-%s-%s.txt --preb %s --quiet"
             % (concuerror, modn, funn, ' '.join(files), results, suite, name,
                funn, preb, preb))
     # Compare the results
-    a = "%s/suites/%s/dpor_fake/%s-%s-%s.txt" % (dirname, suite, name, funn, preb)
-    b = "%s/%s/dpor_fake/%s-%s-%s.txt" % (results, suite, name, funn, preb)
+    a = "%s/suites/%s/dpor/%s-%s-%s.txt" % (dirname, suite, name, funn, preb)
+    b = "%s/%s/dpor/%s-%s-%s.txt" % (results, suite, name, funn, preb)
     equalRes = equalResults(a, b)
     sema.release()
     # Print the results
@@ -177,7 +177,7 @@ def ignoreLine(line):
 print "\nOVERALL SUMMARY for test run"
 print "  %d total tests, which gave rise to" % len(tests)
 print "  %d test cases, of which" % total_tests.value
-print "  %d caused unexpected failures" % total_failed.value
+print "  %d caused expected failures! :-)" % total_failed.value
 
 # Cleanup temp files
 os.system("find %s -name '*.beam' -exec rm {} \;" % dirname)

testsuite/suites/regress/src/exit.erl

@@ -23,6 +23,7 @@ scenarios() ->
 
 %% Here lies is a deadlock
 test1() ->
+    throw(exit_2_is_not_supported),
     Pid = spawn_link(fun() ->
                 process_flag(trap_exit, true),
                 receive _ -> ok end
@@ -31,6 +32,7 @@ test1() ->
 
 %% Here lies is an exception
 test2() ->
+    throw(exit_2_is_not_supported),
     Pid = spawn_link(fun() ->
                 process_flag(trap_exit, true),
                 receive _ -> ok end