Skip to content

FORMUS3IC_LAS3 / embb

Go to a project
Commit a053f5cc by lucapegolotti
Options

Split tests from function in linearizability_tester.h

parent 7c9dd335
Inline Side-by-side
Showing with 2344 additions and 2294 deletions
linearizability_tester/CMakeLists.txt
cmake_minimum_required (VERSION 2.6) cmake_minimum_required (VERSION 2.6)
project (Linearizability_tester C CXX) project (EMBB_linearizability_test C CXX)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -lrt") set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11 -lrt")
find_package(Threads REQUIRED) find_package(Threads REQUIRED)
...@@ -42,7 +42,7 @@ set(PROJECT_LINK_LIBS ...@@ -42,7 +42,7 @@ set(PROJECT_LINK_LIBS
) )
ENDIF (WIN32) ENDIF (WIN32)
add_executable(${PROJECT_NAME} lt.cc) add_executable(${PROJECT_NAME} main.cc)
# target_link_libraries(${PROJECT_NAME} ${CMAKE_THREADS_LIBS_INIT}) # target_link_libraries(${PROJECT_NAME} ${CMAKE_THREADS_LIBS_INIT})
target_link_libraries(${PROJECT_NAME} ${CMAKE_THREAD_LIBS_INIT} ${PROJECT_LINK_LIBS}) # ${CMAKE_THREADS_LIBS_INIT}) target_link_libraries(${PROJECT_NAME} ${CMAKE_THREAD_LIBS_INIT} ${PROJECT_LINK_LIBS}) # ${CMAKE_THREADS_LIBS_INIT})
linearizability_tester/README.txt 0 → 100755
Linearizability tester on EMBB data structures
----------------------------------------------
This README.txt gives information on how to compile the linearizability test
and how to implement tests for other future data structures.
The code in this folder is meant to check the linearizability of the
data structures implemented in the EMBB library. The original linearizability
checker was developed by Alex Horn (Oxford) and the original source code is
freely downloadable from the public github repository:
--> https://github.com/ahorn/linearizability-checker
main.cc is the script that runs the test on the structures currently available.
The src folder contains a large part of the code by Alex Horn.
COMPILE INSTRUCTIONS
* On Linux system
Suppose that the embb library was build in ../build (relative path to the current
folder of the linearizability test).
From within the linearizability_tester folder, cd (or mkdir->cd) into the build directory,
then run "cmake .." and "make". The executable of the test should be placed in the
same folder with the name EMBB_linearizability_test.
* On Windows system
Suppose that the embb library was build in ../build (relative path to the current
folder of the linearizability test).
NOTE: the embb library should be build in Release mode, i.e. by running the command
"cmake --build . --config Release" from inside the correct directory.
From within the linearizability_tester folder, cd (or mkdir->cd) into the build directory,
then run "cmake .." and "cmake --build . --config Release". The Visual Studio prompt should
be used.
The executable of the test should be placed in the folder Release
with the name EMBB_linearizability_test.exe.
HOW TO IMPLEMENT TESTS FOR OTHER DATASTRUCTURES
Data structures that support the following functions:
\ No newline at end of file
linearizability_tester/lt.cc → linearizability_tester/main.cc
#include <linearizability_tester.h> #include <linearizability_tester.h>
#include <tests.h>
#include <embb/base/thread.h>
#include <embb/containers/lock_free_stack.h> #include <embb/base/thread.h>
#include <embb/containers/lock_free_mpmc_queue.h> #include <embb/containers/lock_free_stack.h>
#include <embb/containers/lock_free_mpmc_queue.h>
template<std::size_t N, class S>
static void embb_worker_stack( template<std::size_t N, class S>
const WorkerConfiguration& worker_configuration, static void embb_worker_stack(
ConcurrentLog<state::Stack<N>>& concurrent_log, const WorkerConfiguration& worker_configuration,
S& concurrent_stack) ConcurrentLog<state::Stack<N>>& concurrent_log,
{ S& concurrent_stack)
std::random_device rd; {
std::mt19937 gen(rd()); std::random_device rd;
std::uniform_int_distribution<> value_dist('\0', worker_configuration.max_value); std::mt19937 gen(rd());
std::uniform_int_distribution<> percentage_dist(0, 100); std::uniform_int_distribution<> value_dist('\0', worker_configuration.max_value);
std::uniform_int_distribution<> percentage_dist(0, 100);
// each operation returns false
bool ret; // each operation returns false
bool ret;
char value;
unsigned percentage; char value;
EntryPtr<state::Stack<N>> call_entry_ptr; unsigned percentage;
for (unsigned number_of_ops{ 0U }; EntryPtr<state::Stack<N>> call_entry_ptr;
number_of_ops < worker_configuration.number_of_ops; for (unsigned number_of_ops{ 0U };
++number_of_ops) number_of_ops < worker_configuration.number_of_ops;
{ ++number_of_ops)
value = value_dist(rd); {
percentage = percentage_dist(rd); value = value_dist(rd);
if (percentage < 30) percentage = percentage_dist(rd);
{ if (percentage < 30)
call_entry_ptr = concurrent_log.push_back(state::Stack<N>::make_try_push_call(value)); {
ret = concurrent_stack.TryPush(value); call_entry_ptr = concurrent_log.push_back(state::Stack<N>::make_try_push_call(value));
concurrent_log.push_back(call_entry_ptr, state::Stack<N>::make_try_push_ret(ret)); ret = concurrent_stack.TryPush(value);
} concurrent_log.push_back(call_entry_ptr, state::Stack<N>::make_try_push_ret(ret));
else }
{ else
call_entry_ptr = concurrent_log.push_back(state::Stack<N>::make_try_pop_call()); {
ret = concurrent_stack.TryPop(value); call_entry_ptr = concurrent_log.push_back(state::Stack<N>::make_try_pop_call());
concurrent_log.push_back(call_entry_ptr, state::Stack<N>::make_try_pop_ret(ret, value)); ret = concurrent_stack.TryPop(value);
} concurrent_log.push_back(call_entry_ptr, state::Stack<N>::make_try_pop_ret(ret, value));
} }
} }
}
template<std::size_t N, class S>
static void embb_worker_queue( template<std::size_t N, class S>
const WorkerConfiguration& worker_configuration, static void embb_worker_queue(
ConcurrentLog<state::Queue<N>>& concurrent_log, const WorkerConfiguration& worker_configuration,
S& concurrent_queue) ConcurrentLog<state::Queue<N>>& concurrent_log,
{ S& concurrent_queue)
std::random_device rd; {
std::mt19937 gen(rd()); std::random_device rd;
std::uniform_int_distribution<> value_dist('\0', worker_configuration.max_value); std::mt19937 gen(rd());
std::uniform_int_distribution<> percentage_dist(0, 100); std::uniform_int_distribution<> value_dist('\0', worker_configuration.max_value);
std::uniform_int_distribution<> percentage_dist(0, 100);
// each operation returns false
bool ret; // each operation returns false
bool ret;
char value;
unsigned percentage; char value;
EntryPtr<state::Queue<N>> call_entry_ptr; unsigned percentage;
for (unsigned number_of_ops{ 0U }; EntryPtr<state::Queue<N>> call_entry_ptr;
number_of_ops < worker_configuration.number_of_ops; for (unsigned number_of_ops{ 0U };
++number_of_ops) number_of_ops < worker_configuration.number_of_ops;
{ ++number_of_ops)
value = value_dist(rd); {
percentage = percentage_dist(rd); value = value_dist(rd);
if (percentage < 20) percentage = percentage_dist(rd);
{ if (percentage < 20)
call_entry_ptr = concurrent_log.push_back(state::Queue<N>::make_try_enqueue_call(value)); {
ret = concurrent_queue.TryEnqueue(value); call_entry_ptr = concurrent_log.push_back(state::Queue<N>::make_try_enqueue_call(value));
concurrent_log.push_back(call_entry_ptr, state::Queue<N>::make_try_enqueue_ret(ret)); ret = concurrent_queue.TryEnqueue(value);
} concurrent_log.push_back(call_entry_ptr, state::Queue<N>::make_try_enqueue_ret(ret));
else }
{ else
call_entry_ptr = concurrent_log.push_back(state::Queue<N>::make_try_dequeue_call()); {
ret = concurrent_queue.TryDequeue(value); call_entry_ptr = concurrent_log.push_back(state::Queue<N>::make_try_dequeue_call());
concurrent_log.push_back(call_entry_ptr, state::Queue<N>::make_try_dequeue_ret(ret, value)); ret = concurrent_queue.TryDequeue(value);
} concurrent_log.push_back(call_entry_ptr, state::Queue<N>::make_try_dequeue_ret(ret, value));
} }
} }
}
template <class S>
static void embb_experiment_stack(bool is_linearizable) template <class S>
{ static void embb_experiment_stack(bool is_linearizable)
constexpr std::chrono::hours max_duration{ 1 }; {
constexpr std::size_t N = 560000U; constexpr std::chrono::hours max_duration{ 1 };
constexpr unsigned number_of_threads = 4U; constexpr std::size_t N = 560000U;
constexpr WorkerConfiguration worker_configuration = { '\24', 70000U }; constexpr unsigned number_of_threads = 4U;
constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops; constexpr WorkerConfiguration worker_configuration = { '\24', 70000U };
constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops;
std::cout << "embb_experiment_stack : " << (is_linearizable ? "" : "!") << "linearizable" << std::endl;
Result<state::Stack<N>> result;
Result<state::Stack<N>> result; ConcurrentLog<state::Stack<N>> concurrent_log{ 2U * log_size };
ConcurrentLog<state::Stack<N>> concurrent_log{ 2U * log_size }; S concurrent_stack(N);
S concurrent_stack(N);
if (!is_linearizable)
if (!is_linearizable) {
{ bool ok = concurrent_stack.TryPush(5);
bool ok = concurrent_stack.TryPush(5); assert(ok);
assert(ok); }
}
// create history
// create history start_threads(number_of_threads, embb_worker_stack<N, S>, std::cref(worker_configuration),
start_threads(number_of_threads, embb_worker_stack<N, S>, std::cref(worker_configuration), std::ref(concurrent_log), std::ref(concurrent_stack));
std::ref(concurrent_log), std::ref(concurrent_stack));
const std::size_t number_of_entries{ concurrent_log.number_of_entries() };
const std::size_t number_of_entries{ concurrent_log.number_of_entries() }; const LogInfo<state::Stack<N>> log_info{ concurrent_log.info() };
const LogInfo<state::Stack<N>> log_info{ concurrent_log.info() };
// std::cout << log_info << std::endl; auto start = std::chrono::system_clock::now();
auto end = std::chrono::system_clock::now();
auto start = std::chrono::system_clock::now(); std::chrono::seconds seconds;
auto end = std::chrono::system_clock::now();
std::chrono::seconds seconds; start = std::chrono::system_clock::now();
{
start = std::chrono::system_clock::now(); Log<state::Stack<N>> log_copy{ log_info };
{ assert(log_copy.number_of_entries() == number_of_entries);
Log<state::Stack<N>> log_copy{ log_info };
assert(log_copy.number_of_entries() == number_of_entries); LinearizabilityTester<state::Stack<N>, Option::LRU_CACHE> tester{ log_copy.info(), max_duration };
tester.check(result);
LinearizabilityTester<state::Stack<N>, Option::LRU_CACHE> tester{ log_copy.info(), max_duration }; assert(result.is_timeout() || result.is_linearizable() == is_linearizable);
tester.check(result); }
assert(result.is_timeout() || result.is_linearizable() == is_linearizable); end = std::chrono::system_clock::now();
} seconds = std::chrono::duration_cast<std::chrono::seconds>(end - start);
end = std::chrono::system_clock::now(); std::cout << "History length: " << number_of_entries
seconds = std::chrono::duration_cast<std::chrono::seconds>(end - start); << ", elapsed time: "
std::cout << "History length: " << number_of_entries << seconds.count() << " s " << std::endl;
<< ", enabled state cache (LRU=on), O(1) hash: " }
<< seconds.count() << " s " << std::endl;
} template <class S>
static void embb_experiment_queue(bool is_linearizable)
template <class S> {
static void embb_experiment_queue(bool is_linearizable) constexpr std::chrono::hours max_duration{ 1 };
{ constexpr std::size_t N = 560000U;
constexpr std::chrono::hours max_duration{ 1 }; constexpr unsigned number_of_threads = 4U;
constexpr std::size_t N = 560000U; constexpr WorkerConfiguration worker_configuration = { '\24', 70000U };
constexpr unsigned number_of_threads = 4U; constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops;
constexpr WorkerConfiguration worker_configuration = { '\24', 70000U };
constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops;
Result<state::Queue<N>> result;
std::cout << "embb_experiment_queue : " << (is_linearizable ? "" : "!") << "linearizable" << std::endl; ConcurrentLog<state::Queue<N>> concurrent_log{ 2U * log_size };
S concurrent_queue(N);
Result<state::Queue<N>> result;
ConcurrentLog<state::Queue<N>> concurrent_log{ 2U * log_size }; if (!is_linearizable)
S concurrent_queue(N); {
bool ok = concurrent_queue.TryEnqueue(5);
if (!is_linearizable) assert(ok);
{ }
bool ok = concurrent_queue.TryEnqueue(5);
assert(ok); // create history
} start_threads(number_of_threads, embb_worker_queue<N, S>, std::cref(worker_configuration),
std::ref(concurrent_log), std::ref(concurrent_queue));
// create history const std::size_t number_of_entries{ concurrent_log.number_of_entries() };
start_threads(number_of_threads, embb_worker_queue<N, S>, std::cref(worker_configuration), const LogInfo<state::Queue<N>> log_info{ concurrent_log.info() };
std::ref(concurrent_log), std::ref(concurrent_queue)); // std::cout << log_info << std::endl;
const std::size_t number_of_entries{ concurrent_log.number_of_entries() };
const LogInfo<state::Queue<N>> log_info{ concurrent_log.info() }; auto start = std::chrono::system_clock::now();
// std::cout << log_info << std::endl; auto end = std::chrono::system_clock::now();
std::chrono::seconds seconds;
auto start = std::chrono::system_clock::now();
auto end = std::chrono::system_clock::now(); start = std::chrono::system_clock::now();
std::chrono::seconds seconds; {
Log<state::Queue<N>> log_copy{ log_info };
start = std::chrono::system_clock::now(); assert(log_copy.number_of_entries() == number_of_entries);
{ LinearizabilityTester<state::Queue<N>, Option::LRU_CACHE> tester{ log_copy.info(), max_duration };
Log<state::Queue<N>> log_copy{ log_info }; tester.check(result);
assert(log_copy.number_of_entries() == number_of_entries); assert(result.is_timeout() || result.is_linearizable() == is_linearizable);
LinearizabilityTester<state::Queue<N>, Option::LRU_CACHE> tester{ log_copy.info(), max_duration }; }
tester.check(result); end = std::chrono::system_clock::now();
assert(result.is_timeout() || result.is_linearizable() == is_linearizable); seconds = std::chrono::duration_cast<std::chrono::seconds>(end - start);
} std::cout << "History length: " << number_of_entries
end = std::chrono::system_clock::now(); << ", elapsed time: "
seconds = std::chrono::duration_cast<std::chrono::seconds>(end - start); << seconds.count() << " s " << std::endl;
std::cout << "History length: " << number_of_entries }
<< ", enabled state cache (LRU=on), O(1) hash: "
<< seconds.count() << " s " << std::endl;
} int main()
{
int main() // Test functions and structures in linearizability_tester.h
{ run_tests();
test_lru_cache(); embb::base::Thread::SetThreadsMaxCount(255);
test_atomic_op();
test_stack(); std::cout << "Linearizability test on LockFreeMPMCQueue" << std::endl;
test_state_set(); embb_experiment_queue<embb::containers::LockFreeMPMCQueue<char>>(true);
test_bitset();
test_state_set_op(); std::cout << "Linearizability test on LockFreeStack" << std::endl;
test_state_stack(); embb_experiment_stack<embb::containers::LockFreeStack<char>>(true);
test_state_stack_op(); return 0;
}
test_state_queue();
test_state_queue_op();
test_linearizability_empty_log();
test_raw_single_contains_is_linearizable();
test_raw_single_contains_is_not_linearizable();
test_log_copy();
test_single_contains(true);
test_single_contains(false);
// Consider a sequential insert(x) && contains(x) operation
// && their return values on an initially empty set:
for (bool a : {true, false})
for (bool b : {true, false})
{
test_000(a, b);
test_001(a, b);
test_002(a, b);
test_003(a, b);
test_004(a, b);
test_005(a, b);
test_006(a, b);
test_007(a, b);
test_008(a, b);
}
// semantically deeper tests
test_009();
test_010();
test_011();
test_012();
test_013();
test_014();
test_015();
test_016();
test_017();
test_018();
for (bool a : {true, false})
for (bool b : {true, false})
for (bool c : {true, false})
{
test_019(a, b, c);
test_020(a, b, c);
}
test_021();
test_stack_history_000();
test_stack_history_001();
test_stack_history_002();
test_stack_history_003();
test_slice_000();
test_slice_001();
#ifdef _LT_DEBUG_
// debug();
#endif
concurrent_log();
fuzzy_functional_test();
embb::base::Thread::SetThreadsMaxCount(255);
std::cout << "Linearizability experiment on LockFreeMPMCQueue" << std::endl;
embb_experiment_queue<embb::containers::LockFreeMPMCQueue<char>>(true);
std::cout << "Linearizability experiment on LockFreeStack" << std::endl;
embb_experiment_stack<embb::containers::LockFreeStack<char>>(true);
return 0;
}
linearizability_tester/src/linearizability_tester.h
...@@ -10,6 +10,9 @@ ...@@ -10,6 +10,9 @@
// //
// 3) Unit tests and experiments with TBB, EMBB, and etcd. // 3) Unit tests and experiments with TBB, EMBB, and etcd.
#ifndef __LINEARIZABILITY_TESTER
#define __LINEARIZABILITY_TESTER
#include <thread> #include <thread>
#include <atomic> #include <atomic>
#include <mutex> #include <mutex>
...@@ -73,6 +76,8 @@ std::unique_ptr<T> make_unique(Args&& ...args) ...@@ -73,6 +76,8 @@ std::unique_ptr<T> make_unique(Args&& ...args)
using std::make_unique; using std::make_unique;
#endif #endif
/// Linearizability tester /// Linearizability tester
namespace lt namespace lt
{ {
...@@ -2945,2031 +2950,7 @@ namespace lt ...@@ -2945,2031 +2950,7 @@ namespace lt
} }
} }
/************* Unit tests && experiments *************/ #endif
using namespace lt;
static void test_lru_cache()
{
LruCache<char> lru_cache{ 3 };
assert(lru_cache.insert('\1'));
assert(!lru_cache.insert('\1'));
assert(lru_cache.insert('\2'));
assert(lru_cache.insert('\3'));
assert(lru_cache.insert('\1'));
assert(!lru_cache.insert('\3'));
assert(lru_cache.insert('\4'));
assert(lru_cache.insert('\1'));
}
static void test_atomic_op()
{
bool ok;
state::Atomic atomic, new_atomic;
OpPtr<state::Atomic> read_call_op_ptr;
OpPtr<state::Atomic> read_0_ret_op_ptr, read_0_pending_op_ptr;
OpPtr<state::Atomic> read_1_ret_op_ptr;
OpPtr<state::Atomic> read_2_ret_op_ptr;
OpPtr<state::Atomic> write_1_call_op_ptr, write_1_ret_op_ptr, write_1_pending_op_ptr;
OpPtr<state::Atomic> cas_2_succeeded_call_op_ptr, cas_2_succeeded_ret_op_ptr, cas_2_pending_op_ptr;
OpPtr<state::Atomic> cas_2_failed_call_op_ptr, cas_2_failed_ret_op_ptr;
read_call_op_ptr = state::Atomic::make_read_call();
read_0_ret_op_ptr = state::Atomic::make_read_ret('\0');
read_0_pending_op_ptr = state::Atomic::make_read_pending();
read_1_ret_op_ptr = state::Atomic::make_read_ret('\1');
read_2_ret_op_ptr = state::Atomic::make_read_ret('\2');
write_1_call_op_ptr = state::Atomic::make_write_call('\1');
write_1_ret_op_ptr = state::Atomic::make_write_ret();
write_1_pending_op_ptr = state::Atomic::make_write_pending();
cas_2_succeeded_call_op_ptr = state::Atomic::make_cas_call('\1', '\2');
cas_2_succeeded_ret_op_ptr = state::Atomic::make_cas_ret(true);
cas_2_pending_op_ptr = state::Atomic::make_cas_pending();
cas_2_failed_call_op_ptr = state::Atomic::make_cas_call('\2', '\1');
cas_2_failed_ret_op_ptr = state::Atomic::make_cas_ret(false);
Op<state::Atomic>& read_call_op = *read_call_op_ptr;
Op<state::Atomic>& read_0_ret_op = *read_0_ret_op_ptr;
Op<state::Atomic>& read_0_pending_op = *read_0_pending_op_ptr;
Op<state::Atomic>& read_1_ret_op = *read_1_ret_op_ptr;
Op<state::Atomic>& read_2_ret_op = *read_2_ret_op_ptr;
Op<state::Atomic>& write_1_call_op = *write_1_call_op_ptr;
Op<state::Atomic>& write_1_ret_op = *write_1_ret_op_ptr;
Op<state::Atomic>& write_1_pending_op = *write_1_pending_op_ptr;
Op<state::Atomic>& cas_2_succeeded_call_op = *cas_2_succeeded_call_op_ptr;
Op<state::Atomic>& cas_2_succeeded_ret_op = *cas_2_succeeded_ret_op_ptr;
Op<state::Atomic>& cas_2_pending_op = *cas_2_pending_op_ptr;
Op<state::Atomic>& cas_2_failed_call_op = *cas_2_failed_call_op_ptr;
Op<state::Atomic>& cas_2_failed_ret_op = *cas_2_failed_ret_op_ptr;
assert(!read_call_op.is_partitionable());
assert(!read_0_ret_op.is_partitionable());
assert(!read_0_pending_op.is_partitionable());
assert(!read_1_ret_op.is_partitionable());
assert(!read_2_ret_op.is_partitionable());
assert(!write_1_call_op.is_partitionable());
assert(!write_1_ret_op.is_partitionable());
assert(!write_1_pending_op.is_partitionable());
assert(!cas_2_succeeded_call_op.is_partitionable());
assert(!cas_2_succeeded_ret_op.is_partitionable());
assert(!cas_2_pending_op.is_partitionable());
assert(!cas_2_failed_call_op.is_partitionable());
assert(!cas_2_failed_ret_op.is_partitionable());
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_0_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_0_pending_op);
assert(atomic == new_atomic);
assert(ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = write_1_call_op.apply(atomic, write_1_pending_op);
assert(atomic != new_atomic);
assert(ok);
std::tie(ok, new_atomic) = write_1_call_op.apply(atomic, write_1_ret_op);
assert(atomic != new_atomic);
assert(ok);
atomic = new_atomic;
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
assert(atomic == new_atomic);
assert(ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_2_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = cas_2_failed_call_op.apply(atomic, cas_2_failed_ret_op);
assert(atomic == new_atomic);
assert(ok);
std::tie(ok, new_atomic) = cas_2_failed_call_op.apply(atomic, cas_2_succeeded_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = cas_2_succeeded_call_op.apply(atomic, cas_2_pending_op);
assert(atomic != new_atomic);
assert(ok);
std::tie(ok, new_atomic) = cas_2_succeeded_call_op.apply(atomic, cas_2_succeeded_ret_op);
assert(atomic != new_atomic);
assert(ok);
atomic = new_atomic;
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_2_ret_op);
assert(atomic == new_atomic);
assert(ok);
}
/// a few sanity checks
static void test_stack()
{
Entry<state::Set> ret, call;
call.set_op(state::Set::make_contains_call('\1'));
ret.set_op(state::Set::make_ret(true));
call.set_match(&ret);
EntryPtr<state::Set> A{ &call }, B{ &call }, C{ &call };
Stack<state::Set> stack{ 3 };
assert(stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 0U);
stack.push(A, state::Set());
assert(std::get<0>(stack.top()) == A);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 1U);
stack.push(B, state::Set());
assert(std::get<0>(stack.top()) == B);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 2U);
stack.push(C, state::Set());
assert(std::get<0>(stack.top()) == C);
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.size() == 3U);
stack.pop();
assert(std::get<0>(stack.top()) == B);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 2U);
stack.push(C, state::Set());
assert(std::get<0>(stack.top()) == C);
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.size() == 3U);
// pop multiple entries at once
stack.pop(2);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 1U);
stack.pop();
assert(stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 0U);
}
static void test_bitset()
{
constexpr unsigned bits_per_block = static_cast<unsigned>(sizeof(unsigned long) * CHAR_BIT);
constexpr unsigned N = bits_per_block + 7;
FlexibleBitset bitset;
for (unsigned k{ 0U }; k < N; ++k)
assert(!bitset.is_set(k));
assert(bitset.is_empty());
bitset.set(0);
assert(bitset.is_set(0));
assert(!bitset.is_empty());
for (unsigned k{ 1U }; k < N; ++k)
assert(!bitset.is_set(k));
bitset.reset(0);
assert(!bitset.is_set(0));
assert(bitset.is_empty());
bitset.set(1);
assert(!bitset.is_set(0));
assert(bitset.is_set(1));
assert(!bitset.is_empty());
for (unsigned k{ 2U }; k < N; ++k)
assert(!bitset.is_set(k));
bitset.set(N-1);
assert(bitset.is_set(N-1));
assert(!bitset.is_empty());
for (unsigned k{ 2U }; k < N - 1U; ++k)
assert(!bitset.is_set(k));
FlexibleBitset another_bitset;
another_bitset.set(1);
another_bitset.set(N-1);
FlexibleBitset yet_another_bitset(another_bitset);
assert(bitset == another_bitset);
assert(bitset == yet_another_bitset);
assert(!bitset.is_set(bits_per_block - 1U));
assert(bitset.set(bits_per_block - 1U));
assert(bitset.is_set(bits_per_block - 1U));
assert(!bitset.is_set(bits_per_block));
assert(bitset.set(bits_per_block));
assert(bitset.is_set(bits_per_block));
assert(!bitset.is_set(bits_per_block + 1U));
assert(bitset.set(bits_per_block + 1U));
assert(bitset.is_set(bits_per_block + 1U));
assert(!bitset.is_set(2U * bits_per_block - 1U));
assert(bitset.set(2U * bits_per_block - 1U));
assert(bitset.is_set(2U * bits_per_block - 1U));
assert(!bitset.is_set(2U * bits_per_block));
assert(bitset.set(2U * bits_per_block));
assert(bitset.is_set(2U * bits_per_block));
assert(!bitset.is_set(2U * bits_per_block + 1U));
assert(bitset.set(2U * bits_per_block + 1U));
assert(bitset.is_set(2U * bits_per_block + 1U));
bitset = another_bitset;
assert(bitset.set(2U * bits_per_block - 1U));
assert(bitset.reset(2U * bits_per_block - 1U));
assert(bitset == another_bitset);
assert(bitset.set(2U * bits_per_block));
assert(bitset.reset(2U * bits_per_block));
// different number of blocks
assert(bitset != another_bitset);
assert(bitset.set(2U * bits_per_block + 1U));
assert(bitset.reset(2U * bits_per_block + 1U));
// different number of blocks
assert(bitset != another_bitset);
}
static void test_state_set()
{
bool ok;
state::Set set;
assert(!set.contains('\1'));
std::tie(ok, set) = set.insert('\1');
assert(ok);
assert(set.contains('\1'));
// item is already in the set
std::tie(ok, set) = set.insert('\1');
assert(!ok);
assert(set.contains('\1'));
std::tie(ok, set) = set.erase('\1');
assert(ok);
assert(!set.contains('\1'));
// item has been already erased from the set
std::tie(ok, set) = set.erase('\1');
assert(!ok);
assert(!set.contains('\1'));
}
static void test_state_set_op()
{
bool ok;
state::Set set, new_set;
OpPtr<state::Set> empty_op_ptr;
OpPtr<state::Set> contains_op_ptr;
OpPtr<state::Set> insert_op_ptr;
OpPtr<state::Set> erase_op_ptr;
OpPtr<state::Set> true_ret_op_ptr{ state::Set::make_ret(true) };
OpPtr<state::Set> false_ret_op_ptr{ state::Set::make_ret(false) };
const Op<state::Set>& true_ret_op = *true_ret_op_ptr;
const Op<state::Set>& false_ret_op = *false_ret_op_ptr;
empty_op_ptr = state::Set::make_empty_call();
contains_op_ptr = state::Set::make_contains_call('\1');
insert_op_ptr = state::Set::make_insert_call('\1');
erase_op_ptr = state::Set::make_erase_call('\1');
Op<state::Set>& empty_op = *empty_op_ptr;
Op<state::Set>& contains_op = *contains_op_ptr;
Op<state::Set>& insert_op = *insert_op_ptr;
Op<state::Set>& erase_op = *erase_op_ptr;
std::tie(ok, new_set) = empty_op.apply(set, true_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = contains_op.apply(set, false_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = insert_op.apply(set, true_ret_op);
assert(set != new_set);
assert(ok);
set = new_set;
std::tie(ok, new_set) = empty_op.apply(set, false_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = contains_op.apply(set, true_ret_op);
assert(set == new_set);
assert(ok);
// item is already in the set, so insertion is unsuccessful
std::tie(ok, new_set) = insert_op.apply(set, false_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = contains_op.apply(set, true_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = erase_op.apply(set, true_ret_op);
assert(set != new_set);
assert(ok);
assert(std::get<0>(contains_op.apply(set, true_ret_op)));
assert(!std::get<0>(contains_op.apply(set, false_ret_op)));
assert(!std::get<0>(contains_op.apply(new_set, true_ret_op)));
assert(std::get<0>(contains_op.apply(new_set, false_ret_op)));
}
static void test_state_stack()
{
constexpr unsigned N = 2;
state::Stack<N> stack;
state::Stack<N> new_stack;
state::Stack<N> stack_1, stack_2;
assert(stack.is_empty());
assert(!stack.is_full());
new_stack = stack.push('\1');
assert(stack != new_stack);
stack = stack_1 = new_stack;
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.top() == '\1');
new_stack = stack.push('\2');
assert(stack != new_stack);
stack = stack_2 = new_stack;
assert(stack_1 != stack_2);
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.top() == '\2');
new_stack = stack.pop();
assert(new_stack == stack_1);
stack = new_stack;
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.top() == '\1');
new_stack = stack.push('\2');
assert(stack != new_stack);
assert(new_stack == stack_2);
stack = new_stack;
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.top() == '\2');
new_stack = stack.pop();
assert(new_stack == stack_1);
stack = new_stack;
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.top() == '\1');
new_stack = stack.push('\3');
assert(stack != new_stack);
assert(new_stack != stack_1);
assert(new_stack != stack_2);
stack = new_stack;
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.top() == '\3');
}
static void test_state_queue()
{
constexpr unsigned N = 2;
state::Queue<N> queue;
state::Queue<N> new_queue;
state::Queue<N> queue_1, queue_2;
assert(queue.is_empty());
assert(!queue.is_full());
queue.enqueue('\1');
new_queue = queue.enqueue('\1');
assert(queue != new_queue);
queue = queue_1 = new_queue;
assert(!queue.is_empty());
assert(!queue.is_full());
assert(queue.get_value() == '\1');
new_queue = queue.enqueue('\2');
assert(queue != new_queue);
queue = queue_2 = new_queue;
assert(queue_1 != queue_2);
assert(!queue.is_empty());
assert(queue.is_full());
assert(queue.get_value() == '\1');
new_queue = queue.dequeue();
assert(new_queue != queue_1);
queue = new_queue;
assert(!queue.is_empty());
assert(!queue.is_full());
assert(queue.get_value() == '\2');
new_queue = queue.enqueue('\1');
assert(queue != new_queue);
assert(new_queue != queue_2);
queue = new_queue;
assert(!queue.is_empty());
assert(queue.is_full());
assert(queue.get_value() == '\2');
new_queue = queue.dequeue();
assert(new_queue != queue_1);
queue = new_queue;
assert(!queue.is_empty());
assert(!queue.is_full());
assert(queue.get_value() == '\1');
new_queue = queue.enqueue('\3');
assert(queue != new_queue);
assert(new_queue != queue_1);
assert(new_queue != queue_2);
queue = new_queue;
assert(!queue.is_empty());
assert(queue.is_full());
assert(queue.get_value() == '\1');
}
static void test_state_stack_op()
{
constexpr unsigned N = 1;
bool ok;
state::Stack<N> stack, new_stack;
OpPtr<state::Stack<N>> try_push_1_op_ptr, try_push_2_op_ptr;
OpPtr<state::Stack<N>> try_pop_op_ptr;
OpPtr<state::Stack<N>> true_try_push_ret_op_ptr{ state::Stack<N>::make_try_push_ret(true) };
OpPtr<state::Stack<N>> false_try_push_ret_op_ptr{ state::Stack<N>::make_try_push_ret(false) };
const Op<state::Stack<N>>& true_try_push_ret_op = *true_try_push_ret_op_ptr;
const Op<state::Stack<N>>& false_try_push_ret_op = *false_try_push_ret_op_ptr;
OpPtr<state::Stack<N>> true_1_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(true, '\1') };
OpPtr<state::Stack<N>> true_2_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(true, '\2') };
OpPtr<state::Stack<N>> false_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(false, '\0') };
const Op<state::Stack<N>>& true_1_try_pop_ret_op = *true_1_try_pop_ret_op_ptr;
const Op<state::Stack<N>>& true_2_try_pop_ret_op = *true_2_try_pop_ret_op_ptr;
const Op<state::Stack<N>>& false_try_pop_ret_op = *false_try_pop_ret_op_ptr;
try_pop_op_ptr = state::Stack<N>::make_try_pop_call();
Op<state::Stack<N>>& try_pop_op = *try_pop_op_ptr;
std::tie(ok, new_stack) = try_pop_op.apply(stack, false_try_pop_ret_op);
assert(stack == new_stack);
assert(ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_1_try_pop_ret_op);
assert(stack == new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_2_try_pop_ret_op);
assert(stack == new_stack);
assert(!ok);
try_push_2_op_ptr = state::Stack<N>::make_try_push_call('\2');
Op<state::Stack<N>>& try_push_2_op = *try_push_2_op_ptr;
std::tie(ok, new_stack) = try_push_2_op.apply(stack, false_try_push_ret_op);
assert(stack != new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_push_2_op.apply(stack, true_try_push_ret_op);
assert(stack != new_stack);
assert(ok);
stack = new_stack;
try_push_1_op_ptr = state::Stack<N>::make_try_push_call('\1');
Op<state::Stack<N>>& try_push_1_op = *try_push_1_op_ptr;
// stack is full
std::tie(ok, new_stack) = try_push_1_op.apply(stack, false_try_push_ret_op);
assert(stack == new_stack);
assert(ok);
std::tie(ok, new_stack) = try_push_1_op.apply(stack, true_try_push_ret_op);
assert(stack == new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, false_try_pop_ret_op);
assert(stack != new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_1_try_pop_ret_op);
assert(stack != new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_2_try_pop_ret_op);
assert(stack != new_stack);
assert(ok);
}
static void test_state_queue_op()
{
constexpr unsigned N = 1;
bool ok;
state::Queue<N> queue, new_queue;
OpPtr<state::Queue<N>> try_enqueue_1_op_ptr, try_enqueue_2_op_ptr;
OpPtr<state::Queue<N>> try_dequeue_op_ptr;
OpPtr<state::Queue<N>> true_try_enqueue_ret_op_ptr{ state::Queue<N>::make_try_enqueue_ret(true) };
OpPtr<state::Queue<N>> false_try_enqueue_ret_op_ptr{ state::Queue<N>::make_try_enqueue_ret(false) };
const Op<state::Queue<N>>& true_try_enqueue_ret_op = *true_try_enqueue_ret_op_ptr;
const Op<state::Queue<N>>& false_try_enqueue_ret_op = *false_try_enqueue_ret_op_ptr;
OpPtr<state::Queue<N>> true_1_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(true, '\1') };
OpPtr<state::Queue<N>> true_2_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(true, '\2') };
OpPtr<state::Queue<N>> false_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(false, '\0') };
const Op<state::Queue<N>>& true_1_try_dequeue_ret_op = *true_1_try_dequeue_ret_op_ptr;
const Op<state::Queue<N>>& true_2_try_dequeue_ret_op = *true_2_try_dequeue_ret_op_ptr;
const Op<state::Queue<N>>& false_try_dequeue_ret_op = *false_try_dequeue_ret_op_ptr;
try_dequeue_op_ptr = state::Queue<N>::make_try_dequeue_call();
Op<state::Queue<N>>& try_dequeue_op = *try_dequeue_op_ptr;
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, false_try_dequeue_ret_op);
assert(queue == new_queue);
assert(ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_1_try_dequeue_ret_op);
assert(queue == new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_2_try_dequeue_ret_op);
assert(queue == new_queue);
assert(!ok);
try_enqueue_2_op_ptr = state::Queue<N>::make_try_enqueue_call('\2');
Op<state::Queue<N>>& try_enqueue_2_op = *try_enqueue_2_op_ptr;
std::tie(ok, new_queue) = try_enqueue_2_op.apply(queue, false_try_enqueue_ret_op);
assert(queue != new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_enqueue_2_op.apply(queue, true_try_enqueue_ret_op);
assert(queue != new_queue);
assert(ok);
queue = new_queue;
try_enqueue_1_op_ptr = state::Queue<N>::make_try_enqueue_call('\1');
Op<state::Queue<N>>& try_enqueue_1_op = *try_enqueue_1_op_ptr;
// queue is full
std::tie(ok, new_queue) = try_enqueue_1_op.apply(queue, false_try_enqueue_ret_op);
assert(queue == new_queue);
assert(ok);
std::tie(ok, new_queue) = try_enqueue_1_op.apply(queue, true_try_enqueue_ret_op);
assert(queue == new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, false_try_dequeue_ret_op);
assert(queue != new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_1_try_dequeue_ret_op);
assert(queue != new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_2_try_dequeue_ret_op);
assert(queue != new_queue);
assert(ok);
}
/// The empty log is trivially linearizable.
static void test_linearizability_empty_log()
{
std::size_t number_of_entries{ 0U };
LogInfo<state::Set> log_info;
LinearizabilityTester<state::Set> t{ log_info };
assert(log_info.is_empty());
assert(t.check());
}
/// a few sanity checks on the raw entry data structure
static void test_raw_single_contains_is_linearizable()
{
Entry<state::Set> contains_call, contains_ret;
contains_ret.set_op(state::Set::make_ret(false));
contains_ret.prev = &contains_call;
contains_call.set_op(state::Set::make_contains_call('\1'));
contains_call.next = &contains_ret;
contains_call.set_match(&contains_ret);
std::size_t number_of_entries{ 2U };
LogInfo<state::Set> log_info{ &contains_call, number_of_entries };
LinearizabilityTester<state::Set> t{ log_info };
assert(t.check());
}
static void test_raw_single_contains_is_not_linearizable()
{
Entry<state::Set> contains_call, contains_ret;
contains_ret.set_op(state::Set::make_ret(true));
contains_ret.prev = &contains_call;
contains_call.set_op(state::Set::make_contains_call('\1'));
contains_call.next = &contains_ret;
contains_call.set_match(&contains_ret);
std::size_t number_of_entries{ 2U };
LogInfo<state::Set> log_info{ &contains_call, number_of_entries };
LinearizabilityTester<state::Set> t{ log_info };
assert(!t.check());
}
static void test_single_contains(bool ret)
{
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call('\1'));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(ret));
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(log.number_of_entries() == 2U);
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(contains_call_entry_ptr->prev == nullptr);
assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);
assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->next == nullptr);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (!ret));
if (ret)
{
// If log cannot be linearized, then all pointers
// (except the first one) are still the same.
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(contains_call_entry_ptr->prev != nullptr);
assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);
assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->next == nullptr);
}
}
static void test_log_copy()
{
constexpr bool ret = true;
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call('\1'));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(ret));
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(log.number_of_entries() == 2U);
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(contains_call_entry_ptr->prev == nullptr);
assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);
assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->next == nullptr);
Log<state::Set> log_copy{ log.info() };
assert(log_copy.log_head_ptr() != contains_call_entry_ptr);
assert(log_copy.log_head_ptr() != contains_call_entry_ptr);
assert(log_copy.log_head_ptr()->entry_id() == 0U);
assert(&log_copy.log_head_ptr()->op() == &contains_call_entry_ptr->op());
assert(log_copy.log_head_ptr() == log_copy.log_head_ptr()->match()->match());
assert(log_copy.log_head_ptr()->prev == nullptr);
assert(log_copy.number_of_entries() == 2U);
}
// contains(x) : contains_ret
// |---------------------------|
//
// insert(x) : insert_ret
// |---------------------------|
static void test_000(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned contains_entry_id{ 0U };
constexpr unsigned insert_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// contains(x) : contains_ret
// |----------------------------|
//
// insert(x) : insert_ret
// |-------------------------|
static void test_001(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_entry_id{ 0U };
constexpr unsigned contains_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// contains(x) : contains_ret
// |----------------------------|
//
// insert(x) : insert_ret
// |----------------------------------|
static void test_002(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_entry_id{ 0U };
constexpr unsigned contains_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// contains(x) : contains_ret
// |----------------------------------|
//
// insert(x) : insert_ret
// |---------------------------|
static void test_003(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned contains_entry_id{ 0U };
constexpr unsigned insert_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// insert(x) : insert_ret contains(x) : contains_ret
// |------------------------| |---------------------------|
static void test_004(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_entry_id{ 0U };
constexpr unsigned contains_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret && contains_ret));
}
// contains(x) : contains_ret insert(x) : insert_ret
// |---------------------------| |------------------------|
static void test_005(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned contains_entry_id{ 0U };
constexpr unsigned insert_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret && !contains_ret));
}
// insert(x) : insert_ret_0
// |--------------------------|
//
// insert(x) : insert_ret_1
// |--------------------------|
static void test_006(bool insert_ret_0, bool insert_ret_1)
{
constexpr char x = '\1';
constexpr unsigned insert_0_entry_id{ 0U };
constexpr unsigned insert_1_entry_id{ 1U };
EntryPtr<state::Set> insert_call_0_entry_ptr, insert_ret_0_entry_ptr;
EntryPtr<state::Set> insert_call_1_entry_ptr, insert_ret_1_entry_ptr;
Log<state::Set> log{ 4U };
insert_call_0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_call_1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_0_entry_ptr = log.add_ret(insert_call_0_entry_ptr, state::Set::make_ret(insert_ret_0));
insert_ret_1_entry_ptr = log.add_ret(insert_call_1_entry_ptr, state::Set::make_ret(insert_ret_1));
assert(insert_call_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_ret_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_call_1_entry_ptr->entry_id() == insert_1_entry_id);
assert(insert_ret_1_entry_ptr->entry_id() == insert_1_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (!(insert_ret_0 == insert_ret_1)));
}
// insert(x) : insert_ret_0 insert(x) : insert_ret_1
// |--------------------------| |--------------------------|
static void test_007(bool insert_ret_0, bool insert_ret_1)
{
constexpr char x = '\1';
constexpr unsigned insert_0_entry_id{ 0U };
constexpr unsigned insert_1_entry_id{ 1U };
EntryPtr<state::Set> insert_call_0_entry_ptr, insert_ret_0_entry_ptr;
EntryPtr<state::Set> insert_call_1_entry_ptr, insert_ret_1_entry_ptr;
Log<state::Set> log{ 4U };
insert_call_0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_0_entry_ptr = log.add_ret(insert_call_0_entry_ptr, state::Set::make_ret(insert_ret_0));
insert_call_1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_1_entry_ptr = log.add_ret(insert_call_1_entry_ptr, state::Set::make_ret(insert_ret_1));
assert(insert_call_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_ret_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_call_1_entry_ptr->entry_id() == insert_1_entry_id);
assert(insert_ret_1_entry_ptr->entry_id() == insert_1_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret_0 && !insert_ret_1));
}
// insert(x) : insert_ret
// |------------------------------------------|
//
// insert(x) : insert_ret
// |-------------------------------------|
//
// contains(x) : contains_ret
// |----------------------------|
//
static void test_008(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_0_entry_id{ 0U };
constexpr unsigned insert_1_entry_id{ 1U };
constexpr unsigned contains_entry_id{ 2U };
Log<state::Set> log{ 8U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_0_call_entry_ptr, insert_0_ret_entry_ptr;
EntryPtr<state::Set> insert_1_call_entry_ptr, insert_1_ret_entry_ptr;
insert_0_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_1_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_1_ret_entry_ptr = log.add_ret(insert_1_call_entry_ptr, state::Set::make_ret(insert_ret));
insert_0_ret_entry_ptr = log.add_ret(insert_0_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_0_call_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_0_ret_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_1_call_entry_ptr->entry_id() == insert_1_entry_id);
assert(insert_1_ret_entry_ptr->entry_id() == insert_1_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false
// |---------------------|
//
// contains(y) : false
// |---------------------|
//
// insert(x) : false
// |---------------------|
static void test_009()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned contains_x_entry_id{ 0U };
constexpr unsigned contains_y_entry_id{ 1U };
constexpr unsigned insert_x_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false
// |---------------------|
//
// insert(x) : false
// |---------------------|
//
// contains(y) : false
// |---------------------|
static void test_010()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned contains_x_entry_id{ 0U };
constexpr unsigned insert_x_entry_id{ 1U };
constexpr unsigned contains_y_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// Linearizable:
//
// Let x && y be distinct values.
//
// insert(x) : true
// |------------------|
//
// contains(y) : false
// |---------------------|
//
// contains(x) : false
// |---------------------|
static void test_011()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned insert_x_entry_id{ 0U };
constexpr unsigned contains_y_entry_id{ 1U };
constexpr unsigned contains_x_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// Linearizable:
//
// Let x && y be distinct values.
//
// erase(x) : false insert(y) : true
// |------------------| |------------------|
//
// contains(x) : true
// |------------------------------------------------|
//
// contains(y) : false insert(x) : true
// |---------------------| |------------------|
static void test_012()
{
constexpr char x = '\1';
constexpr char y = '\2';
Log<state::Set> log{ 10U };
EntryPtr<state::Set> erase_x_call_entry_ptr, erase_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_y_call_entry_ptr, insert_y_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
erase_x_call_entry_ptr = log.add_call(state::Set::make_erase_call(x));
erase_x_ret_entry_ptr = log.add_ret(erase_x_call_entry_ptr, state::Set::make_ret(false));
insert_y_call_entry_ptr = log.add_call(state::Set::make_insert_call(y));
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_y_ret_entry_ptr = log.add_ret(insert_y_call_entry_ptr, state::Set::make_ret(true));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(true));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// entry id: X0, call: contains(x)
// entry id: X1, call: insert(x)
// entry id: X0, return: ret: 0
// entry id: X2, call: contains(x)
// entry id: X2, return: ret: 0
// entry id: X3, call: insert(x)
// entry id: X3, return: ret: 1
// entry id: X4, call: contains(x)
// entry id: X4, return: ret: 1
// entry id: X1, return: ret: 0
// entry id: X5, call: contains(x)
// entry id: X5, return: ret: 1
static void test_013()
{
constexpr char x = '\1';
Log<state::Set> log{ 12U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_x3_entry_ptr, ret_x3_entry_ptr;
EntryPtr<state::Set> call_x4_entry_ptr, ret_x4_entry_ptr;
EntryPtr<state::Set> call_x5_entry_ptr, ret_x5_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
call_x3_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x3_entry_ptr = log.add_ret(call_x3_entry_ptr, state::Set::make_ret(true));
call_x4_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x4_entry_ptr = log.add_ret(call_x4_entry_ptr, state::Set::make_ret(true));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
call_x5_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x5_entry_ptr = log.add_ret(call_x5_entry_ptr, state::Set::make_ret(true));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// Let x && y be distinct.
//
// entry id: X0, call: contains(x)
// entry id: X1, call: insert(x)
// entry id: X0, return: ret: 0
// entry id: Y0, call: contains(y) <- !linearizable
// entry id: Y0, return: ret: 1
// entry id: X2, call: contains(x)
// entry id: X2, return: ret: 0
// entry id: X3, call: insert(x)
// entry id: X3, return: ret: 1
// entry id: X4, call: contains(x)
// entry id: X4, return: ret: 1
// entry id: X1, return: ret: 0
// entry id: X5, call: contains(x)
// entry id: X5, return: ret: 1
static void test_014()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 2U;
Log<state::Set> log{ 14U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_x3_entry_ptr, ret_x3_entry_ptr;
EntryPtr<state::Set> call_x4_entry_ptr, ret_x4_entry_ptr;
EntryPtr<state::Set> call_x5_entry_ptr, ret_x5_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
call_x3_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x3_entry_ptr = log.add_ret(call_x3_entry_ptr, state::Set::make_ret(true));
call_x4_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x4_entry_ptr = log.add_ret(call_x4_entry_ptr, state::Set::make_ret(true));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
call_x5_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x5_entry_ptr = log.add_ret(call_x5_entry_ptr, state::Set::make_ret(true));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false contains(y) : true
// |---------------------| |--------------------|
//
// insert(x) : true
// |----------------------------|
static void test_015()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned contains_x_entry_id{ 0U };
constexpr unsigned insert_x_entry_id{ 1U };
constexpr unsigned contains_y_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(true));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false contains(y) : true contains(x) : false
// |---------------------| |--------------------| |---------------------|
//
// insert(x) : true
// |------------------------------|
static void test_016()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 2U;
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false contains(y) : true contains(x) : false
// |---------------------| |--------------------| |---------------------|
//
// insert(x) : true
// |-----------------------------------------------------|
static void test_017()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 2U;
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(y) : true insert(x) : true
// |--------------------| |------------------|
//
// insert(x) : false
// |------------------------------------------------|
static void test_018()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 1U;
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
ret_x0_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// Linearizable:
//
// insert(x) : insert_ret
// |------------------------|
//
// contains(x) : contains_ret
// |-----------------------------|
//
// empty() : empty_ret
// |------------------------|
static void test_019(bool insert_ret, bool contains_ret, bool empty_ret)
{
constexpr char x = '\1';
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
EntryPtr<state::Set> call_contains_entry_ptr, ret_contains_entry_ptr;
EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;
call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(x));
call_contains_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(insert_ret));
ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(empty_ret));
ret_contains_entry_ptr = log.add_ret(call_contains_entry_ptr, state::Set::make_ret(contains_ret));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// insert(x) : insert_ret
// |------------------------|
//
// contains(x) : contains_ret contains(x) : contains_ret
// |----------------------------| |----------------------------|
//
// empty() : empty_ret
// |----------------------|
static void test_020(bool insert_ret, bool contains_ret, bool empty_ret)
{
constexpr char x = '\1';
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_contains_0_entry_ptr, ret_contains_0_entry_ptr;
EntryPtr<state::Set> call_contains_1_entry_ptr, ret_contains_1_entry_ptr;
EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;
call_contains_0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_contains_0_entry_ptr = log.add_ret(call_contains_0_entry_ptr, state::Set::make_ret(contains_ret));
call_contains_1_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_contains_1_entry_ptr = log.add_ret(call_contains_1_entry_ptr, state::Set::make_ret(contains_ret));
ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(empty_ret));
ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(insert_ret));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret && !contains_ret));
}
// Linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false
// |---------------------|
//
// insert(y) : true
// |-----------------------------------------------------------|
//
// contains(x) : false empty() : true
// |---------------------| |----------------|
static void test_021()
{
constexpr char x = '\1';
constexpr char y = '\2';
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_contains_0_entry_ptr, ret_contains_0_entry_ptr;
EntryPtr<state::Set> call_contains_1_entry_ptr, ret_contains_1_entry_ptr;
EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;
call_contains_0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(y));
ret_contains_0_entry_ptr = log.add_ret(call_contains_0_entry_ptr, state::Set::make_ret(false));
call_contains_1_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_contains_1_entry_ptr = log.add_ret(call_contains_1_entry_ptr, state::Set::make_ret(false));
call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(true));
ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(1));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// Linearizable:
//
// push(x) : true
// |------------------------|
//
// push(y) : true
// |--------------------|
//
// pop() : (true, x)
// |------------------|
static void test_stack_history_000()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 6U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
assert(!try_push_x_call_entry_ptr->is_partitionable());
assert(!try_push_y_call_entry_ptr->is_partitionable());
assert(!try_pop_x_call_entry_ptr->is_partitionable());
assert(!try_push_x_ret_entry_ptr->is_partitionable());
assert(!try_push_y_ret_entry_ptr->is_partitionable());
assert(!try_pop_x_ret_entry_ptr->is_partitionable());
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(t.check());
}
// push(x):true; push(y):true; pop():x
static void test_stack_history_001()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 6U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
assert(!try_push_x_call_entry_ptr->is_partitionable());
assert(!try_push_y_call_entry_ptr->is_partitionable());
assert(!try_pop_x_call_entry_ptr->is_partitionable());
assert(!try_push_x_ret_entry_ptr->is_partitionable());
assert(!try_push_y_ret_entry_ptr->is_partitionable());
assert(!try_pop_x_ret_entry_ptr->is_partitionable());
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(!t.check());
}
// entry id: 0, thread id: 0x2, call: try_push(x)
// entry id: 0, thread id: 0x2, return: ret: 1
// entry id: 1, thread id: 0x3, call: try_push(y)
// entry id: 2, thread id: 0x4, call: try_pop()
// entry id: 2, thread id: 0x4, return: ret: [ok: 1, value: x]
// entry id: 1, thread id: 0x3, return: ret: 1
static void test_stack_history_002()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 8U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
assert(!try_push_x_call_entry_ptr->is_partitionable());
assert(!try_push_y_call_entry_ptr->is_partitionable());
assert(!try_pop_x_call_entry_ptr->is_partitionable());
assert(!try_push_x_ret_entry_ptr->is_partitionable());
assert(!try_push_y_ret_entry_ptr->is_partitionable());
assert(!try_pop_x_ret_entry_ptr->is_partitionable());
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(t.check());
}
// Linearizable:
//
// push(x) : true pop() : (true, y)
// |----------------| |------------------|
//
// push(y) : true push(z) : true
// |----------------| |---------------------------------|
//
// pop() : (true, x) pop() : (true, z)
// |-------------------| |-------------------|
static void test_stack_history_003()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr char z = '\3';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 12U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_z_call_entry_ptr, try_push_z_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_y_call_entry_ptr, try_pop_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_z_call_entry_ptr, try_pop_z_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_push_z_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(z));
try_pop_y_ret_entry_ptr = log.add_ret(try_pop_y_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, y));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
try_pop_z_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_push_z_ret_entry_ptr = log.add_ret(try_push_z_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_z_ret_entry_ptr = log.add_ret(try_pop_z_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, z));
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(t.check());
}
// Let x = '\0' && y = '\1'.
//
// erase(x) : false insert(y) : true
// |------------------| |------------------|
//
// contains(x) : true
// |------------------------------------------------|
//
// contains(y) : false insert(x) : true
// |---------------------| |------------------|
static void test_slice_000()
{
constexpr char x = '\0';
constexpr char y = '\1';
Log<state::Set> log{ 10U };
EntryPtr<state::Set> erase_x_call_entry_ptr, erase_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_y_call_entry_ptr, insert_y_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
erase_x_call_entry_ptr = log.add_call(state::Set::make_erase_call(x));
erase_x_ret_entry_ptr = log.add_ret(erase_x_call_entry_ptr, state::Set::make_ret(false));
insert_y_call_entry_ptr = log.add_call(state::Set::make_insert_call(y));
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_y_ret_entry_ptr = log.add_ret(insert_y_call_entry_ptr, state::Set::make_ret(true));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(true));
Slicer<state::Set> slicer{ log.info(), 2U };
assert(slicer.sublog_info(x).log_head_ptr() == erase_x_call_entry_ptr);
assert(slicer.sublog_info(y).log_head_ptr() == insert_y_call_entry_ptr);
assert(slicer.sublog_info(x).number_of_entries() == 6U);
assert(slicer.sublog_info(y).number_of_entries() == 4U);
LinearizabilityTester<state::Set> tester_0{ slicer.sublog_info(x) };
assert(tester_0.check());
LinearizabilityTester<state::Set> tester_1{ slicer.sublog_info(y) };
assert(tester_1.check());
}
// Let x = '\0' && y = '\1'.
//
// contains(x) : false
// |---------------------|
//
// contains(y) : false
// |---------------------|
//
// insert(x) : false
// |---------------------|
static void test_slice_001()
{
constexpr char x = '\0';
constexpr char y = '\1';
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));
Slicer<state::Set> slicer{ log.info(), 2U };
assert(slicer.sublog_info(x).log_head_ptr() == contains_x_call_entry_ptr);
assert(slicer.sublog_info(y).log_head_ptr() == contains_y_call_entry_ptr);
assert(slicer.sublog_info(x).number_of_entries() == 4U);
assert(slicer.sublog_info(y).number_of_entries() == 2U);
LinearizabilityTester<state::Set> tester_0{ slicer.sublog_info(x) };
assert(!tester_0.check());
LinearizabilityTester<state::Set> tester_1{ slicer.sublog_info(y) };
assert(tester_1.check());
}
static void debug()
{
constexpr char x = '\1';
Log<state::Set> log{ 2U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(true));
LinearizabilityTester<state::Set> t{ log.info() };
Result<state::Set> result;
t.check(result);
assert(!result.is_linearizable());
std::stringstream os;
result.debug(os);
assert(os.str() == "Linearizable: No\n"
"entry id: 0, thread id: 0, call: contains(1)\n"
"^ previous entries cannot be linearized\n"
"entry id: 0, thread id: 0, return: ret: 1\n"
"^ previous entries cannot be linearized\n");
}
static void concurrent_log()
{
constexpr unsigned number_of_partitions = 1U;
constexpr char x = '\0';
ConcurrentLog<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.push_back(state::Set::make_contains_call(x));
insert_x_call_entry_ptr = log.push_back(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.push_back(contains_x_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.push_back(insert_x_call_entry_ptr, state::Set::make_ret(false));
EntryPtr<state::Set> entry_ptr, log_head_ptr{ log.log_head_ptr() };
assert(log_head_ptr == contains_x_call_entry_ptr);
assert(log_head_ptr->prev == nullptr);
assert(log_head_ptr->next == insert_x_call_entry_ptr);
assert(log_head_ptr->match() == contains_x_ret_entry_ptr);
entry_ptr = log_head_ptr->next;
assert(entry_ptr == insert_x_call_entry_ptr);
assert(entry_ptr->prev == contains_x_call_entry_ptr);
assert(entry_ptr->next == contains_x_ret_entry_ptr);
assert(entry_ptr->match() == insert_x_ret_entry_ptr);
entry_ptr = entry_ptr->next;
assert(entry_ptr == contains_x_ret_entry_ptr);
assert(entry_ptr->prev == insert_x_call_entry_ptr);
assert(entry_ptr->next == insert_x_ret_entry_ptr);
assert(entry_ptr->match() == contains_x_call_entry_ptr);
entry_ptr = entry_ptr->next;
assert(entry_ptr == insert_x_ret_entry_ptr);
assert(entry_ptr->prev == contains_x_ret_entry_ptr);
assert(entry_ptr->next == nullptr);
assert(entry_ptr->match() == insert_x_call_entry_ptr);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
struct WorkerConfiguration
{
const char max_value;
const unsigned number_of_ops;
};
static void returns_always_false_worker(
const WorkerConfiguration& worker_configuration,
ConcurrentLog<state::Set>& concurrent_log)
{
std::random_device rd;
std::mt19937 gen(rd());
std::uniform_int_distribution<> value_dist('\0', worker_configuration.max_value);
std::uniform_int_distribution<> percentage_dist(0, 100);
// each operation returns false
constexpr bool ret = false;
char value;
EntryPtr<state::Set> call_entry_ptr;
for (unsigned number_of_ops{ 0U };
number_of_ops < worker_configuration.number_of_ops;
++number_of_ops)
{
value = value_dist(rd);
if (percentage_dist(rd) < 30)
{
call_entry_ptr = concurrent_log.push_back(state::Set::make_insert_call(value));
concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
}
else if (percentage_dist(rd) < 50)
{
call_entry_ptr = concurrent_log.push_back(state::Set::make_erase_call(value));
concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
}
else
{
call_entry_ptr = concurrent_log.push_back(state::Set::make_contains_call(value));
concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
}
}
}
template<class F, class ...Args>
void start_threads(unsigned number_of_threads, F&& f, Args&&... args)
{
std::vector<Thread> threads(number_of_threads);
for (Thread& thread : threads)
thread = Thread(std::forward<F>(f), std::forward<Args>(args)...);
for (Thread& thread : threads)
thread.join();
}
/// The first "insert" operation should be always marked as non-linearizable.
static void fuzzy_functional_test()
{
constexpr unsigned number_of_threads = 4U;
constexpr WorkerConfiguration worker_configuration = { '\7', 12U };
constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops;
ConcurrentLog<state::Set> concurrent_log{ 2U * log_size };
// create history
start_threads(number_of_threads, returns_always_false_worker,
std::cref(worker_configuration), std::ref(concurrent_log));
LinearizabilityTester<state::Set> tester{ concurrent_log.info() };
assert(!tester.check());
}
linearizability_tester/src/tests.h 0 → 100755
#include <linearizability_tester.h>
using namespace lt;
static void test_lru_cache()
{
LruCache<char> lru_cache{ 3 };
assert(lru_cache.insert('\1'));
assert(!lru_cache.insert('\1'));
assert(lru_cache.insert('\2'));
assert(lru_cache.insert('\3'));
assert(lru_cache.insert('\1'));
assert(!lru_cache.insert('\3'));
assert(lru_cache.insert('\4'));
assert(lru_cache.insert('\1'));
}
static void test_atomic_op()
{
bool ok;
state::Atomic atomic, new_atomic;
OpPtr<state::Atomic> read_call_op_ptr;
OpPtr<state::Atomic> read_0_ret_op_ptr, read_0_pending_op_ptr;
OpPtr<state::Atomic> read_1_ret_op_ptr;
OpPtr<state::Atomic> read_2_ret_op_ptr;
OpPtr<state::Atomic> write_1_call_op_ptr, write_1_ret_op_ptr, write_1_pending_op_ptr;
OpPtr<state::Atomic> cas_2_succeeded_call_op_ptr, cas_2_succeeded_ret_op_ptr, cas_2_pending_op_ptr;
OpPtr<state::Atomic> cas_2_failed_call_op_ptr, cas_2_failed_ret_op_ptr;
read_call_op_ptr = state::Atomic::make_read_call();
read_0_ret_op_ptr = state::Atomic::make_read_ret('\0');
read_0_pending_op_ptr = state::Atomic::make_read_pending();
read_1_ret_op_ptr = state::Atomic::make_read_ret('\1');
read_2_ret_op_ptr = state::Atomic::make_read_ret('\2');
write_1_call_op_ptr = state::Atomic::make_write_call('\1');
write_1_ret_op_ptr = state::Atomic::make_write_ret();
write_1_pending_op_ptr = state::Atomic::make_write_pending();
cas_2_succeeded_call_op_ptr = state::Atomic::make_cas_call('\1', '\2');
cas_2_succeeded_ret_op_ptr = state::Atomic::make_cas_ret(true);
cas_2_pending_op_ptr = state::Atomic::make_cas_pending();
cas_2_failed_call_op_ptr = state::Atomic::make_cas_call('\2', '\1');
cas_2_failed_ret_op_ptr = state::Atomic::make_cas_ret(false);
Op<state::Atomic>& read_call_op = *read_call_op_ptr;
Op<state::Atomic>& read_0_ret_op = *read_0_ret_op_ptr;
Op<state::Atomic>& read_0_pending_op = *read_0_pending_op_ptr;
Op<state::Atomic>& read_1_ret_op = *read_1_ret_op_ptr;
Op<state::Atomic>& read_2_ret_op = *read_2_ret_op_ptr;
Op<state::Atomic>& write_1_call_op = *write_1_call_op_ptr;
Op<state::Atomic>& write_1_ret_op = *write_1_ret_op_ptr;
Op<state::Atomic>& write_1_pending_op = *write_1_pending_op_ptr;
Op<state::Atomic>& cas_2_succeeded_call_op = *cas_2_succeeded_call_op_ptr;
Op<state::Atomic>& cas_2_succeeded_ret_op = *cas_2_succeeded_ret_op_ptr;
Op<state::Atomic>& cas_2_pending_op = *cas_2_pending_op_ptr;
Op<state::Atomic>& cas_2_failed_call_op = *cas_2_failed_call_op_ptr;
Op<state::Atomic>& cas_2_failed_ret_op = *cas_2_failed_ret_op_ptr;
assert(!read_call_op.is_partitionable());
assert(!read_0_ret_op.is_partitionable());
assert(!read_0_pending_op.is_partitionable());
assert(!read_1_ret_op.is_partitionable());
assert(!read_2_ret_op.is_partitionable());
assert(!write_1_call_op.is_partitionable());
assert(!write_1_ret_op.is_partitionable());
assert(!write_1_pending_op.is_partitionable());
assert(!cas_2_succeeded_call_op.is_partitionable());
assert(!cas_2_succeeded_ret_op.is_partitionable());
assert(!cas_2_pending_op.is_partitionable());
assert(!cas_2_failed_call_op.is_partitionable());
assert(!cas_2_failed_ret_op.is_partitionable());
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_0_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_0_pending_op);
assert(atomic == new_atomic);
assert(ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = write_1_call_op.apply(atomic, write_1_pending_op);
assert(atomic != new_atomic);
assert(ok);
std::tie(ok, new_atomic) = write_1_call_op.apply(atomic, write_1_ret_op);
assert(atomic != new_atomic);
assert(ok);
atomic = new_atomic;
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_1_ret_op);
assert(atomic == new_atomic);
assert(ok);
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_2_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = cas_2_failed_call_op.apply(atomic, cas_2_failed_ret_op);
assert(atomic == new_atomic);
assert(ok);
std::tie(ok, new_atomic) = cas_2_failed_call_op.apply(atomic, cas_2_succeeded_ret_op);
assert(atomic == new_atomic);
assert(!ok);
std::tie(ok, new_atomic) = cas_2_succeeded_call_op.apply(atomic, cas_2_pending_op);
assert(atomic != new_atomic);
assert(ok);
std::tie(ok, new_atomic) = cas_2_succeeded_call_op.apply(atomic, cas_2_succeeded_ret_op);
assert(atomic != new_atomic);
assert(ok);
atomic = new_atomic;
std::tie(ok, new_atomic) = read_call_op.apply(atomic, read_2_ret_op);
assert(atomic == new_atomic);
assert(ok);
}
/// a few sanity checks
static void test_stack()
{
Entry<state::Set> ret, call;
call.set_op(state::Set::make_contains_call('\1'));
ret.set_op(state::Set::make_ret(true));
call.set_match(&ret);
EntryPtr<state::Set> A{ &call }, B{ &call }, C{ &call };
Stack<state::Set> stack{ 3 };
assert(stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 0U);
stack.push(A, state::Set());
assert(std::get<0>(stack.top()) == A);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 1U);
stack.push(B, state::Set());
assert(std::get<0>(stack.top()) == B);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 2U);
stack.push(C, state::Set());
assert(std::get<0>(stack.top()) == C);
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.size() == 3U);
stack.pop();
assert(std::get<0>(stack.top()) == B);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 2U);
stack.push(C, state::Set());
assert(std::get<0>(stack.top()) == C);
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.size() == 3U);
// pop multiple entries at once
stack.pop(2);
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 1U);
stack.pop();
assert(stack.is_empty());
assert(!stack.is_full());
assert(stack.size() == 0U);
}
static void test_bitset()
{
constexpr unsigned bits_per_block = static_cast<unsigned>(sizeof(unsigned long) * CHAR_BIT);
constexpr unsigned N = bits_per_block + 7;
FlexibleBitset bitset;
for (unsigned k{ 0U }; k < N; ++k)
assert(!bitset.is_set(k));
assert(bitset.is_empty());
bitset.set(0);
assert(bitset.is_set(0));
assert(!bitset.is_empty());
for (unsigned k{ 1U }; k < N; ++k)
assert(!bitset.is_set(k));
bitset.reset(0);
assert(!bitset.is_set(0));
assert(bitset.is_empty());
bitset.set(1);
assert(!bitset.is_set(0));
assert(bitset.is_set(1));
assert(!bitset.is_empty());
for (unsigned k{ 2U }; k < N; ++k)
assert(!bitset.is_set(k));
bitset.set(N-1);
assert(bitset.is_set(N-1));
assert(!bitset.is_empty());
for (unsigned k{ 2U }; k < N - 1U; ++k)
assert(!bitset.is_set(k));
FlexibleBitset another_bitset;
another_bitset.set(1);
another_bitset.set(N-1);
FlexibleBitset yet_another_bitset(another_bitset);
assert(bitset == another_bitset);
assert(bitset == yet_another_bitset);
assert(!bitset.is_set(bits_per_block - 1U));
assert(bitset.set(bits_per_block - 1U));
assert(bitset.is_set(bits_per_block - 1U));
assert(!bitset.is_set(bits_per_block));
assert(bitset.set(bits_per_block));
assert(bitset.is_set(bits_per_block));
assert(!bitset.is_set(bits_per_block + 1U));
assert(bitset.set(bits_per_block + 1U));
assert(bitset.is_set(bits_per_block + 1U));
assert(!bitset.is_set(2U * bits_per_block - 1U));
assert(bitset.set(2U * bits_per_block - 1U));
assert(bitset.is_set(2U * bits_per_block - 1U));
assert(!bitset.is_set(2U * bits_per_block));
assert(bitset.set(2U * bits_per_block));
assert(bitset.is_set(2U * bits_per_block));
assert(!bitset.is_set(2U * bits_per_block + 1U));
assert(bitset.set(2U * bits_per_block + 1U));
assert(bitset.is_set(2U * bits_per_block + 1U));
bitset = another_bitset;
assert(bitset.set(2U * bits_per_block - 1U));
assert(bitset.reset(2U * bits_per_block - 1U));
assert(bitset == another_bitset);
assert(bitset.set(2U * bits_per_block));
assert(bitset.reset(2U * bits_per_block));
// different number of blocks
assert(bitset != another_bitset);
assert(bitset.set(2U * bits_per_block + 1U));
assert(bitset.reset(2U * bits_per_block + 1U));
// different number of blocks
assert(bitset != another_bitset);
}
static void test_state_set()
{
bool ok;
state::Set set;
assert(!set.contains('\1'));
std::tie(ok, set) = set.insert('\1');
assert(ok);
assert(set.contains('\1'));
// item is already in the set
std::tie(ok, set) = set.insert('\1');
assert(!ok);
assert(set.contains('\1'));
std::tie(ok, set) = set.erase('\1');
assert(ok);
assert(!set.contains('\1'));
// item has been already erased from the set
std::tie(ok, set) = set.erase('\1');
assert(!ok);
assert(!set.contains('\1'));
}
static void test_state_set_op()
{
bool ok;
state::Set set, new_set;
OpPtr<state::Set> empty_op_ptr;
OpPtr<state::Set> contains_op_ptr;
OpPtr<state::Set> insert_op_ptr;
OpPtr<state::Set> erase_op_ptr;
OpPtr<state::Set> true_ret_op_ptr{ state::Set::make_ret(true) };
OpPtr<state::Set> false_ret_op_ptr{ state::Set::make_ret(false) };
const Op<state::Set>& true_ret_op = *true_ret_op_ptr;
const Op<state::Set>& false_ret_op = *false_ret_op_ptr;
empty_op_ptr = state::Set::make_empty_call();
contains_op_ptr = state::Set::make_contains_call('\1');
insert_op_ptr = state::Set::make_insert_call('\1');
erase_op_ptr = state::Set::make_erase_call('\1');
Op<state::Set>& empty_op = *empty_op_ptr;
Op<state::Set>& contains_op = *contains_op_ptr;
Op<state::Set>& insert_op = *insert_op_ptr;
Op<state::Set>& erase_op = *erase_op_ptr;
std::tie(ok, new_set) = empty_op.apply(set, true_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = contains_op.apply(set, false_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = insert_op.apply(set, true_ret_op);
assert(set != new_set);
assert(ok);
set = new_set;
std::tie(ok, new_set) = empty_op.apply(set, false_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = contains_op.apply(set, true_ret_op);
assert(set == new_set);
assert(ok);
// item is already in the set, so insertion is unsuccessful
std::tie(ok, new_set) = insert_op.apply(set, false_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = contains_op.apply(set, true_ret_op);
assert(set == new_set);
assert(ok);
std::tie(ok, new_set) = erase_op.apply(set, true_ret_op);
assert(set != new_set);
assert(ok);
assert(std::get<0>(contains_op.apply(set, true_ret_op)));
assert(!std::get<0>(contains_op.apply(set, false_ret_op)));
assert(!std::get<0>(contains_op.apply(new_set, true_ret_op)));
assert(std::get<0>(contains_op.apply(new_set, false_ret_op)));
}
static void test_state_stack()
{
constexpr unsigned N = 2;
state::Stack<N> stack;
state::Stack<N> new_stack;
state::Stack<N> stack_1, stack_2;
assert(stack.is_empty());
assert(!stack.is_full());
new_stack = stack.push('\1');
assert(stack != new_stack);
stack = stack_1 = new_stack;
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.top() == '\1');
new_stack = stack.push('\2');
assert(stack != new_stack);
stack = stack_2 = new_stack;
assert(stack_1 != stack_2);
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.top() == '\2');
new_stack = stack.pop();
assert(new_stack == stack_1);
stack = new_stack;
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.top() == '\1');
new_stack = stack.push('\2');
assert(stack != new_stack);
assert(new_stack == stack_2);
stack = new_stack;
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.top() == '\2');
new_stack = stack.pop();
assert(new_stack == stack_1);
stack = new_stack;
assert(!stack.is_empty());
assert(!stack.is_full());
assert(stack.top() == '\1');
new_stack = stack.push('\3');
assert(stack != new_stack);
assert(new_stack != stack_1);
assert(new_stack != stack_2);
stack = new_stack;
assert(!stack.is_empty());
assert(stack.is_full());
assert(stack.top() == '\3');
}
static void test_state_queue()
{
constexpr unsigned N = 2;
state::Queue<N> queue;
state::Queue<N> new_queue;
state::Queue<N> queue_1, queue_2;
assert(queue.is_empty());
assert(!queue.is_full());
queue.enqueue('\1');
new_queue = queue.enqueue('\1');
assert(queue != new_queue);
queue = queue_1 = new_queue;
assert(!queue.is_empty());
assert(!queue.is_full());
assert(queue.get_value() == '\1');
new_queue = queue.enqueue('\2');
assert(queue != new_queue);
queue = queue_2 = new_queue;
assert(queue_1 != queue_2);
assert(!queue.is_empty());
assert(queue.is_full());
assert(queue.get_value() == '\1');
new_queue = queue.dequeue();
assert(new_queue != queue_1);
queue = new_queue;
assert(!queue.is_empty());
assert(!queue.is_full());
assert(queue.get_value() == '\2');
new_queue = queue.enqueue('\1');
assert(queue != new_queue);
assert(new_queue != queue_2);
queue = new_queue;
assert(!queue.is_empty());
assert(queue.is_full());
assert(queue.get_value() == '\2');
new_queue = queue.dequeue();
assert(new_queue != queue_1);
queue = new_queue;
assert(!queue.is_empty());
assert(!queue.is_full());
assert(queue.get_value() == '\1');
new_queue = queue.enqueue('\3');
assert(queue != new_queue);
assert(new_queue != queue_1);
assert(new_queue != queue_2);
queue = new_queue;
assert(!queue.is_empty());
assert(queue.is_full());
assert(queue.get_value() == '\1');
}
static void test_state_stack_op()
{
constexpr unsigned N = 1;
bool ok;
state::Stack<N> stack, new_stack;
OpPtr<state::Stack<N>> try_push_1_op_ptr, try_push_2_op_ptr;
OpPtr<state::Stack<N>> try_pop_op_ptr;
OpPtr<state::Stack<N>> true_try_push_ret_op_ptr{ state::Stack<N>::make_try_push_ret(true) };
OpPtr<state::Stack<N>> false_try_push_ret_op_ptr{ state::Stack<N>::make_try_push_ret(false) };
const Op<state::Stack<N>>& true_try_push_ret_op = *true_try_push_ret_op_ptr;
const Op<state::Stack<N>>& false_try_push_ret_op = *false_try_push_ret_op_ptr;
OpPtr<state::Stack<N>> true_1_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(true, '\1') };
OpPtr<state::Stack<N>> true_2_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(true, '\2') };
OpPtr<state::Stack<N>> false_try_pop_ret_op_ptr{ state::Stack<N>::make_try_pop_ret(false, '\0') };
const Op<state::Stack<N>>& true_1_try_pop_ret_op = *true_1_try_pop_ret_op_ptr;
const Op<state::Stack<N>>& true_2_try_pop_ret_op = *true_2_try_pop_ret_op_ptr;
const Op<state::Stack<N>>& false_try_pop_ret_op = *false_try_pop_ret_op_ptr;
try_pop_op_ptr = state::Stack<N>::make_try_pop_call();
Op<state::Stack<N>>& try_pop_op = *try_pop_op_ptr;
std::tie(ok, new_stack) = try_pop_op.apply(stack, false_try_pop_ret_op);
assert(stack == new_stack);
assert(ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_1_try_pop_ret_op);
assert(stack == new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_2_try_pop_ret_op);
assert(stack == new_stack);
assert(!ok);
try_push_2_op_ptr = state::Stack<N>::make_try_push_call('\2');
Op<state::Stack<N>>& try_push_2_op = *try_push_2_op_ptr;
std::tie(ok, new_stack) = try_push_2_op.apply(stack, false_try_push_ret_op);
assert(stack != new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_push_2_op.apply(stack, true_try_push_ret_op);
assert(stack != new_stack);
assert(ok);
stack = new_stack;
try_push_1_op_ptr = state::Stack<N>::make_try_push_call('\1');
Op<state::Stack<N>>& try_push_1_op = *try_push_1_op_ptr;
// stack is full
std::tie(ok, new_stack) = try_push_1_op.apply(stack, false_try_push_ret_op);
assert(stack == new_stack);
assert(ok);
std::tie(ok, new_stack) = try_push_1_op.apply(stack, true_try_push_ret_op);
assert(stack == new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, false_try_pop_ret_op);
assert(stack != new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_1_try_pop_ret_op);
assert(stack != new_stack);
assert(!ok);
std::tie(ok, new_stack) = try_pop_op.apply(stack, true_2_try_pop_ret_op);
assert(stack != new_stack);
assert(ok);
}
static void test_state_queue_op()
{
constexpr unsigned N = 1;
bool ok;
state::Queue<N> queue, new_queue;
OpPtr<state::Queue<N>> try_enqueue_1_op_ptr, try_enqueue_2_op_ptr;
OpPtr<state::Queue<N>> try_dequeue_op_ptr;
OpPtr<state::Queue<N>> true_try_enqueue_ret_op_ptr{ state::Queue<N>::make_try_enqueue_ret(true) };
OpPtr<state::Queue<N>> false_try_enqueue_ret_op_ptr{ state::Queue<N>::make_try_enqueue_ret(false) };
const Op<state::Queue<N>>& true_try_enqueue_ret_op = *true_try_enqueue_ret_op_ptr;
const Op<state::Queue<N>>& false_try_enqueue_ret_op = *false_try_enqueue_ret_op_ptr;
OpPtr<state::Queue<N>> true_1_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(true, '\1') };
OpPtr<state::Queue<N>> true_2_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(true, '\2') };
OpPtr<state::Queue<N>> false_try_dequeue_ret_op_ptr{ state::Queue<N>::make_try_dequeue_ret(false, '\0') };
const Op<state::Queue<N>>& true_1_try_dequeue_ret_op = *true_1_try_dequeue_ret_op_ptr;
const Op<state::Queue<N>>& true_2_try_dequeue_ret_op = *true_2_try_dequeue_ret_op_ptr;
const Op<state::Queue<N>>& false_try_dequeue_ret_op = *false_try_dequeue_ret_op_ptr;
try_dequeue_op_ptr = state::Queue<N>::make_try_dequeue_call();
Op<state::Queue<N>>& try_dequeue_op = *try_dequeue_op_ptr;
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, false_try_dequeue_ret_op);
assert(queue == new_queue);
assert(ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_1_try_dequeue_ret_op);
assert(queue == new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_2_try_dequeue_ret_op);
assert(queue == new_queue);
assert(!ok);
try_enqueue_2_op_ptr = state::Queue<N>::make_try_enqueue_call('\2');
Op<state::Queue<N>>& try_enqueue_2_op = *try_enqueue_2_op_ptr;
std::tie(ok, new_queue) = try_enqueue_2_op.apply(queue, false_try_enqueue_ret_op);
assert(queue != new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_enqueue_2_op.apply(queue, true_try_enqueue_ret_op);
assert(queue != new_queue);
assert(ok);
queue = new_queue;
try_enqueue_1_op_ptr = state::Queue<N>::make_try_enqueue_call('\1');
Op<state::Queue<N>>& try_enqueue_1_op = *try_enqueue_1_op_ptr;
// queue is full
std::tie(ok, new_queue) = try_enqueue_1_op.apply(queue, false_try_enqueue_ret_op);
assert(queue == new_queue);
assert(ok);
std::tie(ok, new_queue) = try_enqueue_1_op.apply(queue, true_try_enqueue_ret_op);
assert(queue == new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, false_try_dequeue_ret_op);
assert(queue != new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_1_try_dequeue_ret_op);
assert(queue != new_queue);
assert(!ok);
std::tie(ok, new_queue) = try_dequeue_op.apply(queue, true_2_try_dequeue_ret_op);
assert(queue != new_queue);
assert(ok);
}
/// The empty log is trivially linearizable.
static void test_linearizability_empty_log()
{
std::size_t number_of_entries{ 0U };
LogInfo<state::Set> log_info;
LinearizabilityTester<state::Set> t{ log_info };
assert(log_info.is_empty());
assert(t.check());
}
/// a few sanity checks on the raw entry data structure
static void test_raw_single_contains_is_linearizable()
{
Entry<state::Set> contains_call, contains_ret;
contains_ret.set_op(state::Set::make_ret(false));
contains_ret.prev = &contains_call;
contains_call.set_op(state::Set::make_contains_call('\1'));
contains_call.next = &contains_ret;
contains_call.set_match(&contains_ret);
std::size_t number_of_entries{ 2U };
LogInfo<state::Set> log_info{ &contains_call, number_of_entries };
LinearizabilityTester<state::Set> t{ log_info };
assert(t.check());
}
static void test_raw_single_contains_is_not_linearizable()
{
Entry<state::Set> contains_call, contains_ret;
contains_ret.set_op(state::Set::make_ret(true));
contains_ret.prev = &contains_call;
contains_call.set_op(state::Set::make_contains_call('\1'));
contains_call.next = &contains_ret;
contains_call.set_match(&contains_ret);
std::size_t number_of_entries{ 2U };
LogInfo<state::Set> log_info{ &contains_call, number_of_entries };
LinearizabilityTester<state::Set> t{ log_info };
assert(!t.check());
}
static void test_single_contains(bool ret)
{
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call('\1'));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(ret));
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(log.number_of_entries() == 2U);
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(contains_call_entry_ptr->prev == nullptr);
assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);
assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->next == nullptr);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (!ret));
if (ret)
{
// If log cannot be linearized, then all pointers
// (except the first one) are still the same.
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(contains_call_entry_ptr->prev != nullptr);
assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);
assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->next == nullptr);
}
}
static void test_log_copy()
{
constexpr bool ret = true;
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call('\1'));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(ret));
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(log.number_of_entries() == 2U);
assert(log.log_head_ptr() == contains_call_entry_ptr);
assert(contains_call_entry_ptr->prev == nullptr);
assert(contains_call_entry_ptr->next == contains_ret_entry_ptr);
assert(contains_call_entry_ptr->match() == contains_ret_entry_ptr);
assert(contains_ret_entry_ptr->match() == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->prev == contains_call_entry_ptr);
assert(contains_ret_entry_ptr->next == nullptr);
Log<state::Set> log_copy{ log.info() };
assert(log_copy.log_head_ptr() != contains_call_entry_ptr);
assert(log_copy.log_head_ptr() != contains_call_entry_ptr);
assert(log_copy.log_head_ptr()->entry_id() == 0U);
assert(&log_copy.log_head_ptr()->op() == &contains_call_entry_ptr->op());
assert(log_copy.log_head_ptr() == log_copy.log_head_ptr()->match()->match());
assert(log_copy.log_head_ptr()->prev == nullptr);
assert(log_copy.number_of_entries() == 2U);
}
// contains(x) : contains_ret
// |---------------------------|
//
// insert(x) : insert_ret
// |---------------------------|
static void test_000(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned contains_entry_id{ 0U };
constexpr unsigned insert_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// contains(x) : contains_ret
// |----------------------------|
//
// insert(x) : insert_ret
// |-------------------------|
static void test_001(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_entry_id{ 0U };
constexpr unsigned contains_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// contains(x) : contains_ret
// |----------------------------|
//
// insert(x) : insert_ret
// |----------------------------------|
static void test_002(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_entry_id{ 0U };
constexpr unsigned contains_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// contains(x) : contains_ret
// |----------------------------------|
//
// insert(x) : insert_ret
// |---------------------------|
static void test_003(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned contains_entry_id{ 0U };
constexpr unsigned insert_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// insert(x) : insert_ret contains(x) : contains_ret
// |------------------------| |---------------------------|
static void test_004(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_entry_id{ 0U };
constexpr unsigned contains_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret && contains_ret));
}
// contains(x) : contains_ret insert(x) : insert_ret
// |---------------------------| |------------------------|
static void test_005(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned contains_entry_id{ 0U };
constexpr unsigned insert_entry_id{ 1U };
Log<state::Set> log{ 4U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_call_entry_ptr, insert_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_entry_ptr = log.add_ret(insert_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_call_entry_ptr->entry_id() == insert_entry_id);
assert(insert_ret_entry_ptr->entry_id() == insert_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret && !contains_ret));
}
// insert(x) : insert_ret_0
// |--------------------------|
//
// insert(x) : insert_ret_1
// |--------------------------|
static void test_006(bool insert_ret_0, bool insert_ret_1)
{
constexpr char x = '\1';
constexpr unsigned insert_0_entry_id{ 0U };
constexpr unsigned insert_1_entry_id{ 1U };
EntryPtr<state::Set> insert_call_0_entry_ptr, insert_ret_0_entry_ptr;
EntryPtr<state::Set> insert_call_1_entry_ptr, insert_ret_1_entry_ptr;
Log<state::Set> log{ 4U };
insert_call_0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_call_1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_0_entry_ptr = log.add_ret(insert_call_0_entry_ptr, state::Set::make_ret(insert_ret_0));
insert_ret_1_entry_ptr = log.add_ret(insert_call_1_entry_ptr, state::Set::make_ret(insert_ret_1));
assert(insert_call_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_ret_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_call_1_entry_ptr->entry_id() == insert_1_entry_id);
assert(insert_ret_1_entry_ptr->entry_id() == insert_1_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (!(insert_ret_0 == insert_ret_1)));
}
// insert(x) : insert_ret_0 insert(x) : insert_ret_1
// |--------------------------| |--------------------------|
static void test_007(bool insert_ret_0, bool insert_ret_1)
{
constexpr char x = '\1';
constexpr unsigned insert_0_entry_id{ 0U };
constexpr unsigned insert_1_entry_id{ 1U };
EntryPtr<state::Set> insert_call_0_entry_ptr, insert_ret_0_entry_ptr;
EntryPtr<state::Set> insert_call_1_entry_ptr, insert_ret_1_entry_ptr;
Log<state::Set> log{ 4U };
insert_call_0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_0_entry_ptr = log.add_ret(insert_call_0_entry_ptr, state::Set::make_ret(insert_ret_0));
insert_call_1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_ret_1_entry_ptr = log.add_ret(insert_call_1_entry_ptr, state::Set::make_ret(insert_ret_1));
assert(insert_call_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_ret_0_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_call_1_entry_ptr->entry_id() == insert_1_entry_id);
assert(insert_ret_1_entry_ptr->entry_id() == insert_1_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret_0 && !insert_ret_1));
}
// insert(x) : insert_ret
// |------------------------------------------|
//
// insert(x) : insert_ret
// |-------------------------------------|
//
// contains(x) : contains_ret
// |----------------------------|
//
static void test_008(bool insert_ret, bool contains_ret)
{
constexpr char x = '\1';
constexpr unsigned insert_0_entry_id{ 0U };
constexpr unsigned insert_1_entry_id{ 1U };
constexpr unsigned contains_entry_id{ 2U };
Log<state::Set> log{ 8U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
EntryPtr<state::Set> insert_0_call_entry_ptr, insert_0_ret_entry_ptr;
EntryPtr<state::Set> insert_1_call_entry_ptr, insert_1_ret_entry_ptr;
insert_0_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_1_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(contains_ret));
insert_1_ret_entry_ptr = log.add_ret(insert_1_call_entry_ptr, state::Set::make_ret(insert_ret));
insert_0_ret_entry_ptr = log.add_ret(insert_0_call_entry_ptr, state::Set::make_ret(insert_ret));
assert(insert_0_call_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_0_ret_entry_ptr->entry_id() == insert_0_entry_id);
assert(insert_1_call_entry_ptr->entry_id() == insert_1_entry_id);
assert(insert_1_ret_entry_ptr->entry_id() == insert_1_entry_id);
assert(contains_call_entry_ptr->entry_id() == contains_entry_id);
assert(contains_ret_entry_ptr->entry_id() == contains_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false
// |---------------------|
//
// contains(y) : false
// |---------------------|
//
// insert(x) : false
// |---------------------|
static void test_009()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned contains_x_entry_id{ 0U };
constexpr unsigned contains_y_entry_id{ 1U };
constexpr unsigned insert_x_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false
// |---------------------|
//
// insert(x) : false
// |---------------------|
//
// contains(y) : false
// |---------------------|
static void test_010()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned contains_x_entry_id{ 0U };
constexpr unsigned insert_x_entry_id{ 1U };
constexpr unsigned contains_y_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// Linearizable:
//
// Let x && y be distinct values.
//
// insert(x) : true
// |------------------|
//
// contains(y) : false
// |---------------------|
//
// contains(x) : false
// |---------------------|
static void test_011()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned insert_x_entry_id{ 0U };
constexpr unsigned contains_y_entry_id{ 1U };
constexpr unsigned contains_x_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// Linearizable:
//
// Let x && y be distinct values.
//
// erase(x) : false insert(y) : true
// |------------------| |------------------|
//
// contains(x) : true
// |------------------------------------------------|
//
// contains(y) : false insert(x) : true
// |---------------------| |------------------|
static void test_012()
{
constexpr char x = '\1';
constexpr char y = '\2';
Log<state::Set> log{ 10U };
EntryPtr<state::Set> erase_x_call_entry_ptr, erase_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_y_call_entry_ptr, insert_y_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
erase_x_call_entry_ptr = log.add_call(state::Set::make_erase_call(x));
erase_x_ret_entry_ptr = log.add_ret(erase_x_call_entry_ptr, state::Set::make_ret(false));
insert_y_call_entry_ptr = log.add_call(state::Set::make_insert_call(y));
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_y_ret_entry_ptr = log.add_ret(insert_y_call_entry_ptr, state::Set::make_ret(true));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(true));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// entry id: X0, call: contains(x)
// entry id: X1, call: insert(x)
// entry id: X0, return: ret: 0
// entry id: X2, call: contains(x)
// entry id: X2, return: ret: 0
// entry id: X3, call: insert(x)
// entry id: X3, return: ret: 1
// entry id: X4, call: contains(x)
// entry id: X4, return: ret: 1
// entry id: X1, return: ret: 0
// entry id: X5, call: contains(x)
// entry id: X5, return: ret: 1
static void test_013()
{
constexpr char x = '\1';
Log<state::Set> log{ 12U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_x3_entry_ptr, ret_x3_entry_ptr;
EntryPtr<state::Set> call_x4_entry_ptr, ret_x4_entry_ptr;
EntryPtr<state::Set> call_x5_entry_ptr, ret_x5_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
call_x3_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x3_entry_ptr = log.add_ret(call_x3_entry_ptr, state::Set::make_ret(true));
call_x4_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x4_entry_ptr = log.add_ret(call_x4_entry_ptr, state::Set::make_ret(true));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
call_x5_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x5_entry_ptr = log.add_ret(call_x5_entry_ptr, state::Set::make_ret(true));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// Let x && y be distinct.
//
// entry id: X0, call: contains(x)
// entry id: X1, call: insert(x)
// entry id: X0, return: ret: 0
// entry id: Y0, call: contains(y) <- !linearizable
// entry id: Y0, return: ret: 1
// entry id: X2, call: contains(x)
// entry id: X2, return: ret: 0
// entry id: X3, call: insert(x)
// entry id: X3, return: ret: 1
// entry id: X4, call: contains(x)
// entry id: X4, return: ret: 1
// entry id: X1, return: ret: 0
// entry id: X5, call: contains(x)
// entry id: X5, return: ret: 1
static void test_014()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 2U;
Log<state::Set> log{ 14U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_x3_entry_ptr, ret_x3_entry_ptr;
EntryPtr<state::Set> call_x4_entry_ptr, ret_x4_entry_ptr;
EntryPtr<state::Set> call_x5_entry_ptr, ret_x5_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
call_x3_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x3_entry_ptr = log.add_ret(call_x3_entry_ptr, state::Set::make_ret(true));
call_x4_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x4_entry_ptr = log.add_ret(call_x4_entry_ptr, state::Set::make_ret(true));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
call_x5_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x5_entry_ptr = log.add_ret(call_x5_entry_ptr, state::Set::make_ret(true));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false contains(y) : true
// |---------------------| |--------------------|
//
// insert(x) : true
// |----------------------------|
static void test_015()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned contains_x_entry_id{ 0U };
constexpr unsigned insert_x_entry_id{ 1U };
constexpr unsigned contains_y_entry_id{ 2U };
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(true));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
assert(contains_x_call_entry_ptr->entry_id() == contains_x_entry_id);
assert(contains_x_ret_entry_ptr->entry_id() == contains_x_entry_id);
assert(insert_x_call_entry_ptr->entry_id() == insert_x_entry_id);
assert(insert_x_ret_entry_ptr->entry_id() == insert_x_entry_id);
assert(contains_y_call_entry_ptr->entry_id() == contains_y_entry_id);
assert(contains_y_ret_entry_ptr->entry_id() == contains_y_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false contains(y) : true contains(x) : false
// |---------------------| |--------------------| |---------------------|
//
// insert(x) : true
// |------------------------------|
static void test_016()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 2U;
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false contains(y) : true contains(x) : false
// |---------------------| |--------------------| |---------------------|
//
// insert(x) : true
// |-----------------------------------------------------|
static void test_017()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 2U;
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_x2_entry_ptr, ret_x2_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x0_entry_ptr = log.add_ret(call_x0_entry_ptr, state::Set::make_ret(false));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x2_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_x2_entry_ptr = log.add_ret(call_x2_entry_ptr, state::Set::make_ret(false));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// !linearizable:
//
// Let x && y be distinct values.
//
// contains(y) : true insert(x) : true
// |--------------------| |------------------|
//
// insert(x) : false
// |------------------------------------------------|
static void test_018()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr unsigned not_linearizable_entry_id = 1U;
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_x0_entry_ptr, ret_x0_entry_ptr;
EntryPtr<state::Set> call_x1_entry_ptr, ret_x1_entry_ptr;
EntryPtr<state::Set> call_y0_entry_ptr, ret_y0_entry_ptr;
call_x0_entry_ptr = log.add_call(state::Set::make_insert_call(x));
call_y0_entry_ptr = log.add_call(state::Set::make_contains_call(y));
ret_y0_entry_ptr = log.add_ret(call_y0_entry_ptr, state::Set::make_ret(true));
call_x1_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_x1_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(true));
ret_x0_entry_ptr = log.add_ret(call_x1_entry_ptr, state::Set::make_ret(false));
assert(call_y0_entry_ptr->entry_id() == not_linearizable_entry_id);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
// Linearizable:
//
// insert(x) : insert_ret
// |------------------------|
//
// contains(x) : contains_ret
// |-----------------------------|
//
// empty() : empty_ret
// |------------------------|
static void test_019(bool insert_ret, bool contains_ret, bool empty_ret)
{
constexpr char x = '\1';
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
EntryPtr<state::Set> call_contains_entry_ptr, ret_contains_entry_ptr;
EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;
call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(x));
call_contains_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(insert_ret));
ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(empty_ret));
ret_contains_entry_ptr = log.add_ret(call_contains_entry_ptr, state::Set::make_ret(contains_ret));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == insert_ret);
}
// insert(x) : insert_ret
// |------------------------|
//
// contains(x) : contains_ret contains(x) : contains_ret
// |----------------------------| |----------------------------|
//
// empty() : empty_ret
// |----------------------|
static void test_020(bool insert_ret, bool contains_ret, bool empty_ret)
{
constexpr char x = '\1';
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_contains_0_entry_ptr, ret_contains_0_entry_ptr;
EntryPtr<state::Set> call_contains_1_entry_ptr, ret_contains_1_entry_ptr;
EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;
call_contains_0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_contains_0_entry_ptr = log.add_ret(call_contains_0_entry_ptr, state::Set::make_ret(contains_ret));
call_contains_1_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(x));
ret_contains_1_entry_ptr = log.add_ret(call_contains_1_entry_ptr, state::Set::make_ret(contains_ret));
ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(empty_ret));
ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(insert_ret));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check() == (insert_ret && !contains_ret));
}
// Linearizable:
//
// Let x && y be distinct values.
//
// contains(x) : false
// |---------------------|
//
// insert(y) : true
// |-----------------------------------------------------------|
//
// contains(x) : false empty() : true
// |---------------------| |----------------|
static void test_021()
{
constexpr char x = '\1';
constexpr char y = '\2';
Log<state::Set> log{ 8U };
EntryPtr<state::Set> call_contains_0_entry_ptr, ret_contains_0_entry_ptr;
EntryPtr<state::Set> call_contains_1_entry_ptr, ret_contains_1_entry_ptr;
EntryPtr<state::Set> call_insert_entry_ptr, ret_insert_entry_ptr;
EntryPtr<state::Set> call_empty_entry_ptr, ret_empty_entry_ptr;
call_contains_0_entry_ptr = log.add_call(state::Set::make_contains_call(x));
call_insert_entry_ptr = log.add_call(state::Set::make_insert_call(y));
ret_contains_0_entry_ptr = log.add_ret(call_contains_0_entry_ptr, state::Set::make_ret(false));
call_contains_1_entry_ptr = log.add_call(state::Set::make_contains_call(x));
ret_contains_1_entry_ptr = log.add_ret(call_contains_1_entry_ptr, state::Set::make_ret(false));
call_empty_entry_ptr = log.add_call(state::Set::make_empty_call());
ret_empty_entry_ptr = log.add_ret(call_empty_entry_ptr, state::Set::make_ret(true));
ret_insert_entry_ptr = log.add_ret(call_insert_entry_ptr, state::Set::make_ret(1));
LinearizabilityTester<state::Set> t{ log.info() };
assert(t.check());
}
// Linearizable:
//
// push(x) : true
// |------------------------|
//
// push(y) : true
// |--------------------|
//
// pop() : (true, x)
// |------------------|
static void test_stack_history_000()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 6U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
assert(!try_push_x_call_entry_ptr->is_partitionable());
assert(!try_push_y_call_entry_ptr->is_partitionable());
assert(!try_pop_x_call_entry_ptr->is_partitionable());
assert(!try_push_x_ret_entry_ptr->is_partitionable());
assert(!try_push_y_ret_entry_ptr->is_partitionable());
assert(!try_pop_x_ret_entry_ptr->is_partitionable());
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(t.check());
}
// push(x):true; push(y):true; pop():x
static void test_stack_history_001()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 6U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
assert(!try_push_x_call_entry_ptr->is_partitionable());
assert(!try_push_y_call_entry_ptr->is_partitionable());
assert(!try_pop_x_call_entry_ptr->is_partitionable());
assert(!try_push_x_ret_entry_ptr->is_partitionable());
assert(!try_push_y_ret_entry_ptr->is_partitionable());
assert(!try_pop_x_ret_entry_ptr->is_partitionable());
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(!t.check());
}
// entry id: 0, thread id: 0x2, call: try_push(x)
// entry id: 0, thread id: 0x2, return: ret: 1
// entry id: 1, thread id: 0x3, call: try_push(y)
// entry id: 2, thread id: 0x4, call: try_pop()
// entry id: 2, thread id: 0x4, return: ret: [ok: 1, value: x]
// entry id: 1, thread id: 0x3, return: ret: 1
static void test_stack_history_002()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 8U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
assert(!try_push_x_call_entry_ptr->is_partitionable());
assert(!try_push_y_call_entry_ptr->is_partitionable());
assert(!try_pop_x_call_entry_ptr->is_partitionable());
assert(!try_push_x_ret_entry_ptr->is_partitionable());
assert(!try_push_y_ret_entry_ptr->is_partitionable());
assert(!try_pop_x_ret_entry_ptr->is_partitionable());
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(t.check());
}
// Linearizable:
//
// push(x) : true pop() : (true, y)
// |----------------| |------------------|
//
// push(y) : true push(z) : true
// |----------------| |---------------------------------|
//
// pop() : (true, x) pop() : (true, z)
// |-------------------| |-------------------|
static void test_stack_history_003()
{
constexpr char x = '\1';
constexpr char y = '\2';
constexpr char z = '\3';
constexpr std::size_t N = 5;
Log<state::Stack<N>> log{ 12U };
EntryPtr<state::Stack<N>> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_push_z_call_entry_ptr, try_push_z_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_y_call_entry_ptr, try_pop_y_ret_entry_ptr;
EntryPtr<state::Stack<N>> try_pop_z_call_entry_ptr, try_pop_z_ret_entry_ptr;
try_push_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(x));
try_push_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(y));
try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_y_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_push_z_call_entry_ptr = log.add_call(state::Stack<N>::make_try_push_call(z));
try_pop_y_ret_entry_ptr = log.add_ret(try_pop_y_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, y));
try_pop_x_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, x));
try_pop_z_call_entry_ptr = log.add_call(state::Stack<N>::make_try_pop_call());
try_push_z_ret_entry_ptr = log.add_ret(try_push_z_call_entry_ptr, state::Stack<N>::make_try_push_ret(true));
try_pop_z_ret_entry_ptr = log.add_ret(try_pop_z_call_entry_ptr, state::Stack<N>::make_try_pop_ret(true, z));
LinearizabilityTester<state::Stack<N>> t{ log.info() };
assert(t.check());
}
// Let x = '\0' && y = '\1'.
//
// erase(x) : false insert(y) : true
// |------------------| |------------------|
//
// contains(x) : true
// |------------------------------------------------|
//
// contains(y) : false insert(x) : true
// |---------------------| |------------------|
static void test_slice_000()
{
constexpr char x = '\0';
constexpr char y = '\1';
Log<state::Set> log{ 10U };
EntryPtr<state::Set> erase_x_call_entry_ptr, erase_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_y_call_entry_ptr, insert_y_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
erase_x_call_entry_ptr = log.add_call(state::Set::make_erase_call(x));
erase_x_ret_entry_ptr = log.add_ret(erase_x_call_entry_ptr, state::Set::make_ret(false));
insert_y_call_entry_ptr = log.add_call(state::Set::make_insert_call(y));
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_y_ret_entry_ptr = log.add_ret(insert_y_call_entry_ptr, state::Set::make_ret(true));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(true));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(true));
Slicer<state::Set> slicer{ log.info(), 2U };
assert(slicer.sublog_info(x).log_head_ptr() == erase_x_call_entry_ptr);
assert(slicer.sublog_info(y).log_head_ptr() == insert_y_call_entry_ptr);
assert(slicer.sublog_info(x).number_of_entries() == 6U);
assert(slicer.sublog_info(y).number_of_entries() == 4U);
LinearizabilityTester<state::Set> tester_0{ slicer.sublog_info(x) };
assert(tester_0.check());
LinearizabilityTester<state::Set> tester_1{ slicer.sublog_info(y) };
assert(tester_1.check());
}
// Let x = '\0' && y = '\1'.
//
// contains(x) : false
// |---------------------|
//
// contains(y) : false
// |---------------------|
//
// insert(x) : false
// |---------------------|
static void test_slice_001()
{
constexpr char x = '\0';
constexpr char y = '\1';
Log<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> contains_y_call_entry_ptr, contains_y_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_y_call_entry_ptr = log.add_call(state::Set::make_contains_call(y));
insert_x_call_entry_ptr = log.add_call(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.add_ret(contains_x_call_entry_ptr, state::Set::make_ret(false));
contains_y_ret_entry_ptr = log.add_ret(contains_y_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.add_ret(insert_x_call_entry_ptr, state::Set::make_ret(false));
Slicer<state::Set> slicer{ log.info(), 2U };
assert(slicer.sublog_info(x).log_head_ptr() == contains_x_call_entry_ptr);
assert(slicer.sublog_info(y).log_head_ptr() == contains_y_call_entry_ptr);
assert(slicer.sublog_info(x).number_of_entries() == 4U);
assert(slicer.sublog_info(y).number_of_entries() == 2U);
LinearizabilityTester<state::Set> tester_0{ slicer.sublog_info(x) };
assert(!tester_0.check());
LinearizabilityTester<state::Set> tester_1{ slicer.sublog_info(y) };
assert(tester_1.check());
}
static void debug()
{
constexpr char x = '\1';
Log<state::Set> log{ 2U };
EntryPtr<state::Set> contains_call_entry_ptr, contains_ret_entry_ptr;
contains_call_entry_ptr = log.add_call(state::Set::make_contains_call(x));
contains_ret_entry_ptr = log.add_ret(contains_call_entry_ptr, state::Set::make_ret(true));
LinearizabilityTester<state::Set> t{ log.info() };
Result<state::Set> result;
t.check(result);
assert(!result.is_linearizable());
std::stringstream os;
result.debug(os);
assert(os.str() == "Linearizable: No\n"
"entry id: 0, thread id: 0, call: contains(1)\n"
"^ previous entries cannot be linearized\n"
"entry id: 0, thread id: 0, return: ret: 1\n"
"^ previous entries cannot be linearized\n");
}
static void concurrent_log()
{
constexpr unsigned number_of_partitions = 1U;
constexpr char x = '\0';
ConcurrentLog<state::Set> log{ 6U };
EntryPtr<state::Set> contains_x_call_entry_ptr, contains_x_ret_entry_ptr;
EntryPtr<state::Set> insert_x_call_entry_ptr, insert_x_ret_entry_ptr;
contains_x_call_entry_ptr = log.push_back(state::Set::make_contains_call(x));
insert_x_call_entry_ptr = log.push_back(state::Set::make_insert_call(x));
contains_x_ret_entry_ptr = log.push_back(contains_x_call_entry_ptr, state::Set::make_ret(false));
insert_x_ret_entry_ptr = log.push_back(insert_x_call_entry_ptr, state::Set::make_ret(false));
EntryPtr<state::Set> entry_ptr, log_head_ptr{ log.log_head_ptr() };
assert(log_head_ptr == contains_x_call_entry_ptr);
assert(log_head_ptr->prev == nullptr);
assert(log_head_ptr->next == insert_x_call_entry_ptr);
assert(log_head_ptr->match() == contains_x_ret_entry_ptr);
entry_ptr = log_head_ptr->next;
assert(entry_ptr == insert_x_call_entry_ptr);
assert(entry_ptr->prev == contains_x_call_entry_ptr);
assert(entry_ptr->next == contains_x_ret_entry_ptr);
assert(entry_ptr->match() == insert_x_ret_entry_ptr);
entry_ptr = entry_ptr->next;
assert(entry_ptr == contains_x_ret_entry_ptr);
assert(entry_ptr->prev == insert_x_call_entry_ptr);
assert(entry_ptr->next == insert_x_ret_entry_ptr);
assert(entry_ptr->match() == contains_x_call_entry_ptr);
entry_ptr = entry_ptr->next;
assert(entry_ptr == insert_x_ret_entry_ptr);
assert(entry_ptr->prev == contains_x_ret_entry_ptr);
assert(entry_ptr->next == nullptr);
assert(entry_ptr->match() == insert_x_call_entry_ptr);
LinearizabilityTester<state::Set> t{ log.info() };
assert(!t.check());
}
struct WorkerConfiguration
{
const char max_value;
const unsigned number_of_ops;
};
static void returns_always_false_worker(
const WorkerConfiguration& worker_configuration,
ConcurrentLog<state::Set>& concurrent_log)
{
std::random_device rd;
std::mt19937 gen(rd());
std::uniform_int_distribution<> value_dist('\0', worker_configuration.max_value);
std::uniform_int_distribution<> percentage_dist(0, 100);
// each operation returns false
constexpr bool ret = false;
char value;
EntryPtr<state::Set> call_entry_ptr;
for (unsigned number_of_ops{ 0U };
number_of_ops < worker_configuration.number_of_ops;
++number_of_ops)
{
value = value_dist(rd);
if (percentage_dist(rd) < 30)
{
call_entry_ptr = concurrent_log.push_back(state::Set::make_insert_call(value));
concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
}
else if (percentage_dist(rd) < 50)
{
call_entry_ptr = concurrent_log.push_back(state::Set::make_erase_call(value));
concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
}
else
{
call_entry_ptr = concurrent_log.push_back(state::Set::make_contains_call(value));
concurrent_log.push_back(call_entry_ptr, state::Set::make_ret(ret));
}
}
}
template<class F, class ...Args>
void start_threads(unsigned number_of_threads, F&& f, Args&&... args)
{
std::vector<Thread> threads(number_of_threads);
for (Thread& thread : threads)
thread = Thread(std::forward<F>(f), std::forward<Args>(args)...);
for (Thread& thread : threads)
thread.join();
}
/// The first "insert" operation should be always marked as non-linearizable.
static void fuzzy_functional_test()
{
constexpr unsigned number_of_threads = 4U;
constexpr WorkerConfiguration worker_configuration = { '\7', 12U };
constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops;
ConcurrentLog<state::Set> concurrent_log{ 2U * log_size };
// create history
start_threads(number_of_threads, returns_always_false_worker,
std::cref(worker_configuration), std::ref(concurrent_log));
LinearizabilityTester<state::Set> tester{ concurrent_log.info() };
assert(!tester.check());
}
void run_tests(){
test_lru_cache();
test_atomic_op();
test_stack();
test_state_set();
test_bitset();
test_state_set_op();
test_state_stack();
test_state_stack_op();
test_state_queue();
test_state_queue_op();
test_linearizability_empty_log();
test_raw_single_contains_is_linearizable();
test_raw_single_contains_is_not_linearizable();
test_log_copy();
test_single_contains(true);
test_single_contains(false);
// Consider a sequential insert(x) && contains(x) operation
// && their return values on an initially empty set:
for (bool a : {true, false})
for (bool b : {true, false})
{
test_000(a, b);
test_001(a, b);
test_002(a, b);
test_003(a, b);
test_004(a, b);
test_005(a, b);
test_006(a, b);
test_007(a, b);
test_008(a, b);
}
// semantically deeper tests
test_009();
test_010();
test_011();
test_012();
test_013();
test_014();
test_015();
test_016();
test_017();
test_018();
for (bool a : {true, false})
for (bool b : {true, false})
for (bool c : {true, false})
{
test_019(a, b, c);
test_020(a, b, c);
}
test_021();
test_stack_history_000();
test_stack_history_001();
test_stack_history_002();
test_stack_history_003();
test_slice_000();
test_slice_001();
#ifdef _LT_DEBUG_
debug();
#endif
concurrent_log();
fuzzy_functional_test();
}
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or sign in to comment