The Benefits of Duality in Verifying Concurrent Programs under TSO (Parameterized Verification of TSO Memory Models)

Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo

We study decision problems for the verification of an arbitrary number of finite-state programs running under the classical TSO memory model.

For TSO model, we consider the following decision problem: (COVER) reachability of a configuration with one process in a given control state. We show that the COVER problem is decidable. To this aim, we introduce a novel machine model, called the Dual TSO semantics. Then, we show the decidability of the COVER problem for an arbitrary number of processes running under the Dual TSO semantics. We present a simple backward reachability analysis algorithm for the latter.

To our best of knowledge, our method is the first one that can verify the COVER reachability problems of concurrent programs under TSO memory models.

This page addresses the following issues:

Download and install the tool Dual-TSO (see Section 1)
Reproduce experimental results (see Section 2)
Publication information (see Section 4)
Contact information (see Section 6)

If you encounter problems or bugs when installing or running Dual-TSO, your feedback by email to will be appreciated.

1. How to download and install?

Before download and install, you should check requirements of operation system (see 1.1) and software (see 1.2).

1.1. Operation requirements

Dual-TSO is implemented for Unix environments such as Ubuntu, Fedora, Debian, etc, and the Mac OS system.

1.2. Software requirements

The following softwares are required to be capable of building it:

C++ compiler supporting C++11. For example g++ version 4.8.4 or higher (required)
GNU Autoconf (required)
GNU Make (required)

1.3. Download

We have implemented a prototype as an extension of Memorax TACAS'12 and TACAS'13. The prototype implements the new memory model called the Dual TSO model.

You can download the source code of Dual-TSO for Unix system (tested with OS Ubuntu 14.04 LTS 64 bit).

1.4. Building commands

To produce a configure script as well as Makefile templates:

 
$ cd memorax
$ autoreconf --install

After building the installation files, you should be able to proceed in the same way as above:

$ ./configure
$ make
$ make install

Other information related to installing can be seen in README.md file.

If you have an error related to Latex command when you are installing and you do not want to install Latex packages, you can move forward to the next install command. In this case, you will not have the PDF manual version. The file can be downloaded from manual.pdf.

2. Reproduce experimental results

The Memorax has an option to test with Single Buffer model with fixed number of processes (SB) from TACAS'12 and TACAS'13. The Dual-TSO has two options to test with the Dual model with a fixed number of processes (dual), and the Dual model with parameterized versions (pdual). The commands to run are:

For DUAL: 
  $./src/memorax -a dual reach ./doc/examples/dual-examples/sb.rmm

For PDUAL: 
  $./src/memorax -a pdual reach ./doc/examples/dual-examples/sb.rmm

For SB: 
  $./src/memorax -a sb reach ./doc/examples/dual-examples/sb.rmm

We provide scripts to automatically run all experiments.

$ ./doc/examples/dual-examples/test_sb.sh 
    to repeat all experiments with SB model with a fixed number of processes

$ ./doc/examples/dual-examples/test_dual.sh 
    to repeat all experiments with DUAL model with a fixed number of processes

$ ./doc/examples/dual-examples/test_pdual.sh 
    to repeat all experiments with DUAL model with parameterized versions

Other information related to experiments can be seen in README_experiment.md file.

3. RFF and Limitation

If you would like to run Memorax with SB and/or Dual abstractions on your benchmarks, using --rff option can benefit the performance. Dual-TSO currently only supports input programs presented by finite state transition systems, i.e. finite data domain and finite number of variables. Fence insertion supported by Memorax for SB is currently not supported by Dual and PDual.

4. Papers

You can find the paper The Benefits of Duality in Verifying Concurrent Programs under TSO published at CONCUR 2016 here.
You can find our LMCS journal version A Load-Buffer Semantics for Total Store Ordering, an extended version of the CONCUR'16 paper.

5. Slide

You can find the slide Slide of The Benefits of Duality in Verifying Concurrent Programs under TSO presented at CONCUR 2016 here.

6. Contact

Email: tuan-phong.ngo at it dot uu dot se