Install dependencies:
sudo apt-get update
sudo apt-get install libtbb-dev libboost-all-dev libgflags-dev
Alternatively, install dependencies using Debian package management system:
cd dependencies
sudo dpkg -i libtbb2_2020.1-2_amd64.deb
sudo dpkg -i libtbb-dev_2020.1-2_amd64.deb
sudo dpkg -i libgflags2.2_2.2.2-1build1_amd64.deb
sudo dpkg -i libgflags-dev_2.2.2-1build1_amd64.deb
sudo dpkg -i libboost1.71-dev_1.71.0-6ubuntu6_amd64.deb
Build tests:
cd src/tervel/tests
make
TEST_SIZE: Test Size
DATA_STRUCTURE: { 0="TBB_QUEUE" , 1="KFIFO_QUEUE", 2="BOOST_STACK", 3="TERVEL_STACK", 4="TBB_MAP", 5="TERVEL_MAP" }
CORRECTNESS_CONDITION: { 0="LINEARIZABILITY" , 1="SEQUENTIAL_CONSISTENCY", 2="QUIESCENT_CONSISTENCY", 3="QUASI_LINEARIZABILITY" }
NUM_THRDS: Number of Threads, set on line 31 in src/tervel/tests/bench/main.cc
K: Quasi-linearization factor, set on line 46 in src/tervel/tests/bench/main.cc
cd src/tervel/tests
./executables/benchmark.x <TEST_SIZE> <DATA_STRUCTURE> <CORRECTNESS_CONDITION>
For example, to test TERVEL_STACK with test size 100 for "QUIESCENT_CONSISTENCY":
./executables/benchmark.x 100 3 2
If the execution is correct, the tool will print "Program Correct Up To This Point". If a correctness violation is detected, the tool will print "Program Not Correct", and a warning will print that indicates the detected error.
WARNINGS:
Incorrect CONSUME: An item was consumed that doesn't exist in the data structure.
Incorrect READ: An item was read that doesn't exist in the data structure.
Incorrect FAIL: A method call failed to consume an item that exists in the data structure.
The runtime of the dynamic analysis tool can be replicated for all experiments except for the k-FIFO queue. The memory requirements for the k-FIFO queue are too large to run in a virtual machine.
Run Script:
cd src/tervel/tests/script
make clean
make
./script
Running the entire script takes approximately 18 hours (RAM = 16 GB, CORES = 4, PROCESSOR = Intel(R) Core(TM) i7-8550U CPU @ 1.80 GHz 1.99 GHz. To replicate a subset of the results, update the for-loop on line 23 of in src/tervel/tests/script/script.cc to set k to the value representing the correctness conditions of interest:
CORRECTNESS_CONDITION: { 0="LINEARIZABILITY" , 1="SEQUENTIAL_CONSISTENCY", 2="QUIESCENT_CONSISTENCY", 3="QUASI_LINEARIZABILITY" }
Each correctness condition takes approximately 4.5 hours to test. The results are printed to src/tervel/tests/script/output.txt
Format of output (for each correctness condition):
<program time> <verification time> (TBB_QUEUE, NUM_THRDS = 32, TEST_SIZE = 10)
<program time> <verification time> (BOOST_STACK, NUM_THRDS = 32, TEST_SIZE = 10)
<program time> <verification time> (TERVEL_STACK, NUM_THRDS = 32, TEST_SIZE = 10)
<program time> <verification time> (TBB_MAP, NUM_THRDS = 32, TEST_SIZE = 10)
<program time> <verification time> (TERVEL_MAP, NUM_THRDS = 32, TEST_SIZE = 10)
<program time> <verification time> (TBB_QUEUE, NUM_THRDS = 32, TEST_SIZE = 100)
<program time> <verification time> (BOOST_STACK, NUM_THRDS = 32, TEST_SIZE = 100)
<program time> <verification time> (TERVEL_STACK, NUM_THRDS = 32, TEST_SIZE = 100)
<program time> <verification time> (TBB_MAP, NUM_THRDS = 32, TEST_SIZE = 100)
<program time> <verification time> (TERVEL_MAP, NUM_THRDS = 32, TEST_SIZE = 100)
<program time> <verification time> (TBB_QUEUE, NUM_THRDS = 32, TEST_SIZE = 1000)
<program time> <verification time> (BOOST_STACK, NUM_THRDS = 32, TEST_SIZE = 1000)
<program time> <verification time> (TERVEL_STACK, NUM_THRDS = 32, TEST_SIZE = 1000)
<program time> <verification time> (TBB_MAP, NUM_THRDS = 32, TEST_SIZE = 1000)
<program time> <verification time> (TERVEL_MAP, NUM_THRDS = 32, TEST_SIZE = 1000)
<program time> <verification time> (TBB_QUEUE, NUM_THRDS = 32, TEST_SIZE = 10000)
<program time> <verification time> (BOOST_STACK, NUM_THRDS = 32, TEST_SIZE = 10000)
<program time> <verification time> (TERVEL_STACK, NUM_THRDS = 32, TEST_SIZE = 10000)
<program time> <verification time> (TBB_MAP, NUM_THRDS = 32, TEST_SIZE = 10000)
<program time> <verification time> (TERVEL_MAP, NUM_THRDS = 32, TEST_SIZE = 10000)
cd RelatedWork/P-Compositionality/linearizability-checker
make stack-test
TEST_SIZE: Test Size, set on line 4891 in RelatedWork/P-Compositionality/linearizability-checker/lt.cc
NUM_THRDS: Number of Threads, set on line 4888 in RelatedWork/P-Compositionality/linearizability-checker/lt.cc
cd RelatedWork/P-Compositionality/linearizability-checker
./lt-stack-test
cd RelatedWork/P-Compositionality/linearizability-checker
Update line 4891 in RelatedWork/P-Compositionality/linearizability-checker/lt.cc as follows:
constexpr WorkerConfiguration worker_configuration = {'\24', 10U};
make stack-test
./lt-stack-test
Results are printed in RelatedWork/P-Compositionality/linearizability-checker/results.txt
Repeat Steps and update line 4891 in RelatedWork/P-Compositionality/linearizability-checker/lt.cc for following cases:
constexpr WorkerConfiguration worker_configuration = {'\24', 100U};constexpr WorkerConfiguration worker_configuration = {'\24', 1000U};constexpr WorkerConfiguration worker_configuration = {'\24', 5000U};(may time out after 25 seconds)