CRDT Model Checking Experiments

Model Checking Experiments

We write a script to automatically conduct comprehensive model checking experiments with the CRDT-TLA.

Requirements

This has been tested on Linux (with JDK 8), but not yet on Windows or Mac.

Experiments

Now, the script checks SEC of the two CRDT protocols:

1. StateAWSet
2. OpAWSet

Parameters

For each of these properties to check, we vary the number of replicas (#Replicas) from 2 to 4 and the number of data (#Data) from 2 to 5.

Because the run time at the scale (3, 5) and (4, 5) is not acceptable, We removed these two scale configurations.

We exit TLC when the number of distinct states TLC examines reaches a given threshold. The threshold is 100, 000, 000,

How to run?

Each of the following command conducts the model checking experiments described above in batch, and it is allowed to set the number of worker threads.

Commands

# Usage Note: In the following three commands, "make" is identical to "make run".
make		# using 10 workers by default (used in our setting)
make WORKERS=2  # using 2 workers
make WORKERS=   # setting the number of workers as that of physical cores in your machine

Output:

The model checking results are stored in the mc_result/YYYYmmdd-HHMMSS directory, consisting of

• Three markdown table containing raw (statistic) data.
• Two LaTeX tables which can be used in paper, one for each protocol to check.

YYYYmmdd-HHMMSS is the timestamp generated when the batch program starts.

A sample model checking result (only the LaTeX tables) is given in mc_result.

To stop:

• Ctrl + C: Stop the individual experiment currently in running
• Ctrl + \: Stop the whole batch of experiments

How is this implemented?

tlcwrapper.py

The tlcwrapper.py script encapsulates the usage of TLC commands.

It accepts two parameters:

• The configuration file. The rules are specified in config.ini.
• The optional TLC log file (MC_out.txt by default).

crdt-batch.py

Run the experiments described above in batch.

It uses tlcwrapper.py to start TLC.

Temp files

TLC generates a subdirectory in the crdt/model directory for each experiment, which is used to store the tla files and cfg files required for TLC.

You can use make clean to delete them.

Any MC files may be helpful for you.

filename	description
MC.cfg / MC.tla	Generated by TLCWrapper.py. Required by TLC.
MC_out.txt	TLC log.
MC_user.txt	User output (using Print or PrintT).
MC_states.dump / MC_states.dot	All states dump (if enabled).
MC_coverage.txt	Coverage information (if enabled).