JMCR-Stable/README.md

   1 # Maximal-Causality-Reduction (MCR) Java version
   2
   3 MCR is a stateless model checker powered by an efficient reduction algorithm. It systematically explores the state-space of the program by collecting runtime traces of the program executions and constructing ordering constraints over the traces to generate other possible schedules. It captures the values of the writes and reads to prune redundant explorations. By enforcing at least one read to return a different value, it generates a new schedule which drives the program to reach a new state.
   4
   5 # Getting Started
   6
   7 ## Environment
   8 * z3 installation
   9         * Follow https://github.com/Z3Prover/z3
  10         * Add `z3` to your PATH
  11 * Eclipse (Neon 4.6) & Java 8
  12         * The JDK version tested is 8u101. Higher versions should also be OK. JDK 8u65 was also tested, but it reported an exception related to the lamdba feature. We suggest the users to use JDK 8u101 or higher versions.
  13
  14 ## How to Run
  15 ### run in Eclipse
  16 The tool can be easily used in Eclipse. Create an Eclispe workspace and import all the projects cloned from the Git repository (A build path error may happen. It may need to manually change the JDK version if the error happens). We put all the benchmarks under the folder `mcr-test/`. Users can choose a benchmark and then run it as a junit test. We use java agent for the bytecode instrumentation with the ASM framework. Users need to specify the following VM parameters (click the Run Configurations and choose the JUnit):
  17
  18 ```
  19 -Xmx1g -javaagent:lib/iagent.jar
  20 ```
  21
  22 ### run in terminal
  23
  24 We also support building the project in the terminal (or in Eclipse) using `ant`.
  25
  26 To compile mcr, run `ant ` under `mcr-controller/`, it will generates two jar files into `dist` directory.
  27
  28 To run the tests under `mcr-test/`, run `ant ` and then the bash script `mcr_cmd`.
  29 The usage of `mcr_cmd`:
  30
  31 ```
  32 usage: ./mcr_cmd [options] test_class [parameters]
  33   e.g., ./mcr_cmd [options] edu.tamu.aser.rvtest_simple_tests.Example
  34   options:
  35         --help -h usage
  36         --debug -D print debug information
  37         --static -S using static analysis       (see the ECOOP'17 paper)
  38         --class_path absolute_dir -c absolute_dir
  39                                         if this is not specified, default the current bin/ as the class path
  40         --memmory-model MM -m MM selecting the memory model SC/TSO/PSO  (see the OOPLSA'16 paper)
  41
  42 ```
  43
  44 If `-S` is specified, the tool will first run static analysis to generate the system dependencies graph into `SDGs` and then explore the program. The number of the reads and constraitns as well as the constraints solving times are save to the file under `stats/`.
  45
  46 `-m` selects the executed memory model. We currently support SC/TSO/PSO, and use SC.
  47
  48 ### to run the users' own tests
  49
  50 MCR works with JUnit 4. Given a JUnit 4 test class, it will explore
  51 each of the tests in the test class. To use MCR, you need to add the
  52 following annotation "@RunWith(JUnit4MCRRunner.class)" to the
  53 test class. Users can refer to the benchmarks we put under 'mcr-test/src'
  54 for more ideas about how to write the tests.
  55
  56 ## An Example
  57
  58 The following shows a simple example (See `Example.java` under `mcr-test/src/edu.tamu.aser.rvtest_simple_tests/`).
  59
  60
  61 ```
  62 package edu.tamu.aser.rvtest;
  63 import static org.junit.Assert.*;
  64 import org.junit.Test;
  65 import org.junit.runner.RunWith;
  66 import edu.tamu.aser.exploration.JUnit4MCRRunner;
  67
  68 @RunWith(JUnit4MCRRunner.class)
  69 public class Example {
  70
  71         private static int x, y;
  72         public static void main(String[] args) {
  73                 Thread t1 = new Thread(new Runnable() {
  74                         @Override
  75                         public void run() {
  76                                 int b = x;
  77                                 y = 1;
  78                         }
  79                 });
  80
  81                 t1.start();
  82                 int a = y;
  83                 x = 1;
  84                 t1.join();
  85
  86         }
  87
  88         @Test
  89         public void test() {
  90                 x = 0;
  91                 y = 0;
  92         }
  93 }
  94 ```
  95
  96 After running MCR on the program above, we can generate the following output:
  97
  98 ```
  99 EXPLORING: edu.tamu.aser.rvtest_collection.Example.test: 09:12:12
 100
 101
 102 =============== EXPLORATION STATS ===============
 103 NUMBER OF SCHEDULES: 3
 104 EXPLORATION TIME: 0:00:00
 105 =================================================
 106
 107 ```
 108
 109 ### Explanation of the output
 110
 111
 112 `=============== EXPLORATION STATS ===============`
 113
 114 shows the number of the executions explored for this progam and the time taken.
 115
 116 When an exception is triggered by the program, the tool will print how this error is triggered and how to reproduce it. Take `TestDeadlock.java` under `mcr-test/src/edu.tamu.aser.rvtest_simple_tests/` as an example. Our tool prints out
 117 the buggy trace:
 118
 119 ```
 120 !!! FAILURE DETECTED DURING EXPLORATION OF SCHEDULE #2: Deadlock detected in schedule
 121 The following trace triggered this error:
 122        Thread-1_TestDeadlock.java:67:start
 123        Thread-1_TestDeadlock.java:68:start
 124        Thread-6_TestDeadlock.java:63:read
 125        Thread-6_TestDeadlock.java:29:read
 126        Thread-6_TestDeadlock.java:29:Lock
 127        Thread-6_TestDeadlock.java:35:read
 128        Thread-5_TestDeadlock.java:55:read
 129        Thread-5_TestDeadlock.java:19:read
 130        Thread-5_TestDeadlock.java:19:Lock
 131        Thread-5_TestDeadlock.java:20:write
 132        Thread-5_TestDeadlock.java:21:read
 133        Thread-6_TestDeadlock.java:36:read
 134 ```
 135
 136
 137
 138 # Useful Documents
 139 * [ECOOP'17] [Speeding Up Maximal Causality Reduction with Static Dependency Analysis](https://huangshiyou.github.io/files/Huang-ECOOP-2017-16.pdf)
 140
 141 * [OOPSLA'16] [Maximal Causality Reduction for TSO and PSO](https://huangshiyou.github.io/files/mcr_relax-huang.pdf)
 142
 143 * [PLDI'15] [Stateless Model Checking Concurrent Programs with Maximal Causality Reduction](https://parasol.tamu.edu/~jeff/academic/mcr.pdf)
 144
 145 * [PLDI'14] [Maximal Sound Predictive Race Detection
 146 with Control Flow Abstraction](http://fsl.cs.illinois.edu/FSL/papers/2014/huang-meredith-rosu-2014-pldi/huang-meredith-rosu-2014-pldi-public.pdf)
 147