/jupiter-experiments

Primary LanguageTLA

jupiter-experiments

Model Checking Experiments

We write a script to automatically conduct comprehensive model checking experiments with the jupiter-refinement-project.

Requirements

  • JRE 8 (Not tested on any lower or higher versions)

Experiments

Now, the script checks two kinds of properties:

  1. the refinement relation among a family of Jupiter protocols. Specifically, it checks that
  • AJupiter is a refinement of XJupiter (expressed in AJupiterImplXJupiter),
  • XJupiter is a refinement of CJupiter (expressed in XJupierImplCJupiter), and
  • CJupiter is a refinement of AbsJupiter (expressed in CJupiterImplAbsJupiter).
  1. the correctness of these Jupiter protocols with respect to the weak list specification (WLSpec). Due to the refinement relation above, it only needs to check that
  • AbsJupiter (more precisely, AbsJupiterH) satisfies WLSpec.

Parameters

For each of these four properties to check, we vary the number of client replicas (#Clients) from 1 to 5 and the number of chars (#Chars) allowed to insert from 1 to 5.

For the settings of (#Clients, #Chars) = (3, 3), (2, 4), and (2, 4), we exit TLC when the number of distinct states TLC examines reaches a given threshold. For AbsJupiter, the threshold is 100, 000, 000, while for the others, it is 80, 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

On Linux

# 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

On Windows

cd protocols
python ..\jupiter-cav2019.py ..\mc_result 10

Output:

The model checking results are stored in a subdirectory (named with the timestamps it is generated) in the mc_result directory, consisting of

  • A markdown table containing all raw (statistic) data.
  • Four markdown tables, one for each property to check.
  • Four LaTeX tables which can be used in paper, one for each property to check.

An incomplete sample model checking result (only for (1,1) and (1,2)) is given in 20190207-162510-sample.

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

To stop:

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

Warning: When it is interrupted by Ctrl + C or Ctrl + \, some tables may be incomplete or even be not generated.

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).

jupiter-cav2019.py

Run the experiments described above in batch.

It uses tlcwrapper.py to start TLC.

Temp files

TLC generates a subdirectory in the protocols 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).