- Compile Cassandra:

- Compile the DMCK tool:

Note: Linux removes some generated temporary folders if the machine is restarted. If you want to run the tests after a restart, you should execute this compilation step again.



### Running the PCTCP tests:

The results for PCTCP method involves three sets of tests where the number of event labels are set to 4, 5 and 6 respectively. The system is tested by running 1000 times using each configuration.

- (Configuration) Set the model checker parameter in the `$HOME/DMCK/cassandra-2.0.0/target-sys.conf` to PCTCPModelChecker on line 48. (The initial configuration already sets it to PCTCPModelChecker.)

- (Configuration) Set the bug-depth parameter in the `$HOME/DMCK/cassandra-2.0.0/pctcp.conf` file on line 10. This repeats the tests with number of event labels 4. 

- (Running tests) The Cassandra system can be tested by running the following commands in the `$HOME/DMCK` folder:

  Note: It took around 510 minutes in our experiments to run the command which initiates 1000 runs to test the Cassandra system with the provided `pctcp.bugDepth` parameter.
  
  To test the system with fewer runs you can modify `pctcp.maxIterations` parameter in the `$HOME/DMCK/cassandra-2.0.0/pctcp.conf` file. It takes around 20 seconds to run a single iteration. (If all Cassandra node messages are not captured by DMCK in a run due to communication nondeterminism, the run is repeated with the same random seed. In such a case, it might take longer time to run the iteration.)

- (Reading the output) The screen output mostly involves DMCK activities such as sending workloads to Cassandra nodes, capturing the Cassandra messages, displaying which message is scheduled next. It is not needed to follow the screen output to get the test results as they will be logged in a file. 

  Results of the tests will be saved in a `$HOME/DMCK/cassandra-2.0.0/Test-<date>.txt` file (similar to sample output file `$HOME/DMCK/sampleOutput/PCTCP-d4.txt`).  It lists the random seed and the priority change points used for each test. At the end of this file, you can find the average number of events, the average number of maximum number of chains, the number of iterations and the elapsed time for running the tests.

  To count the number of runs which hit the bug, you can run the following command to grep in the generated result file. 

- To repeat the tests for each `pctcp.bugDepth = 5` and `pctcp.bugDepth = 6`, set the bug-depth parameter accordingly in `pctcp.conf` as in step 2. Then, run the `dmckRunner.sh` again as in step 3 and read the output as in step 4.  

### Running the random walk tests:

The results for the random walk tests can be reproduced using the following steps:

- (Configuration) The model checker parameter in the `$HOME/DMCK/cassandra-2.0.0/target-sys.conf` file should be set to `RandomModelChecker` on line 48. 

- (Running the tests) The Cassandra system can be tested by running the following commands in the `$HOME/DMCK` folder:

  It took around 500 minutes in our experiments to run the command which initiates 1000 random walk runs to test the Cassandra system.

  To test the system with fewer runs you can modify `random.maxIterations` parameter in the `$HOME/DMCK/cassandra-2.0.0/pctcp.conf` file. It takes around 20 seconds to run a single iteration. 
  (If all Cassandra node messages are not captured by DMCK in a run due to communication nondeterminism, the run is repeated with the same random seed. In such a case, it might take longer time to run the iteration.)
  
- Similar to PCTCP tests, the results of the random walk tests are summarized in a `$HOME/DMCK/cassandra-2.0.0/Test-<date>.txt` file.


## Modification of the test parameters

Cassandra system can be tested with PCTCP and random walk methods using different parameters by modifying the following configurations in `$HOME/DMCK/cassandra-2.0.0/pctcp.conf`.

**Example 1:** The following configuration repeats the single PCTCP test which is found to hit the bug with `pctcp.bugDepth = 5` and `pctcp.randomSeed = 12346395` parameters (as recorded in the sample output file `sampleOutput/PCTCP-d5.txt`).

In file `$HOME/DMCK/cassandra-2.0.0/pctcp.conf`:
  

In file `$HOME/DMCK/cassandra-2.0.0/target-sys.conf`:

Then, run the test in the folder $HOME/DMCK/cassandra-2.0.0:

It takes around 20 seconds to run the test. 

(If all Cassandra node messages are not captured by DMCK in a run due to communication nondeterminism, the run is repeated with the same random seed. In such a case, it might take longer time to run the iteration.)

**Example 2:** The following configuration repeats the single PCTCP test which is found to hit the bug with `pctcp.bugDepth = 6` and `pctcp.randomSeed = 12346547` parameters (as recorded in the sample output file `sampleOutput/PCTCP-d6.txt`).

In file `$HOME/DMCK/cassandra-2.0.0/pctcp.conf`:

In file `$HOME/DMCK/cassandra-2.0.0/target-sys.conf`:

It takes around 20 seconds to run the test.

(If all Cassandra node messages are not captured by DMCK in a run due to communication nondeterminism, the run is repeated with the same random seed. In such a case, it might take longer time to run the iteration.)

## Requirements for the computational environment 

- We performed the experimental evaluation on a virtual machine running Ubuntu 16.04 with 4GB RAM and 4 processor cores hosted on a machine running Windows 7 with 16GB RAM and Intel i5-6600 3.3GHz processor.

- The system can be run on Ubuntu OS (tested with versions 16 and 18) with the following software installed:
  -  Ant build tool
  -  Oracle Java 8
  -  Python 2.7 (python2 is used)
   
Environments that might break the software:

 - Java versions > 8 breaks the software since the Cassandra system under test uses `sun.misc.unsafe` package removed in later releases.
 - Lower CPU and memory configurations might cause the DMCK tool to miss some Cassandra messages to be captured in the timeout defined by the DMCK. This causes testing the system with some incomplete set of messages.