From a053f5cc9bcf585c04b55c3ca31cb5abb502a37e Mon Sep 17 00:00:00 2001 From: lucapegolotti Date: Mon, 14 Mar 2016 14:21:16 +0100 Subject: [PATCH] Split tests from function in linearizability_tester.h --- linearizability_tester/CMakeLists.txt | 4 ++-- linearizability_tester/README.txt | 39 +++++++++++++++++++++++++++++++++++++++ linearizability_tester/lt.cc | 267 --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- linearizability_tester/main.cc | 192 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ linearizability_tester/src/linearizability_tester.h | 2031 ++++++--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- linearizability_tester/src/tests.h | 2103 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 6 files changed, 2342 insertions(+), 2294 deletions(-) create mode 100755 linearizability_tester/README.txt delete mode 100644 linearizability_tester/lt.cc create mode 100644 linearizability_tester/main.cc create mode 100755 linearizability_tester/src/tests.h diff --git a/linearizability_tester/CMakeLists.txt b/linearizability_tester/CMakeLists.txt index e7813c5..cc1df9f 100644 --- a/linearizability_tester/CMakeLists.txt +++ b/linearizability_tester/CMakeLists.txt @@ -1,5 +1,5 @@ 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") find_package(Threads REQUIRED) @@ -42,7 +42,7 @@ set(PROJECT_LINK_LIBS ) 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_THREAD_LIBS_INIT} ${PROJECT_LINK_LIBS}) # ${CMAKE_THREADS_LIBS_INIT}) diff --git a/linearizability_tester/README.txt b/linearizability_tester/README.txt new file mode 100755 index 0000000..8bed8fc --- /dev/null +++ b/linearizability_tester/README.txt @@ -0,0 +1,39 @@ +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 diff --git a/linearizability_tester/lt.cc b/linearizability_tester/lt.cc deleted file mode 100644 index 8cb5a85..0000000 --- a/linearizability_tester/lt.cc +++ /dev/null @@ -1,267 +0,0 @@ -#include - -#include -#include -#include - -template -static void embb_worker_stack( - const WorkerConfiguration& worker_configuration, - ConcurrentLog>& concurrent_log, - S& concurrent_stack) -{ - 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 - bool ret; - - char value; - unsigned percentage; - EntryPtr> call_entry_ptr; - for (unsigned number_of_ops{ 0U }; - number_of_ops < worker_configuration.number_of_ops; - ++number_of_ops) - { - value = value_dist(rd); - percentage = percentage_dist(rd); - if (percentage < 30) - { - call_entry_ptr = concurrent_log.push_back(state::Stack::make_try_push_call(value)); - ret = concurrent_stack.TryPush(value); - concurrent_log.push_back(call_entry_ptr, state::Stack::make_try_push_ret(ret)); - } - else - { - call_entry_ptr = concurrent_log.push_back(state::Stack::make_try_pop_call()); - ret = concurrent_stack.TryPop(value); - concurrent_log.push_back(call_entry_ptr, state::Stack::make_try_pop_ret(ret, value)); - } - } -} - -template -static void embb_worker_queue( - const WorkerConfiguration& worker_configuration, - ConcurrentLog>& concurrent_log, - S& concurrent_queue) -{ - 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 - bool ret; - - char value; - unsigned percentage; - EntryPtr> call_entry_ptr; - for (unsigned number_of_ops{ 0U }; - number_of_ops < worker_configuration.number_of_ops; - ++number_of_ops) - { - value = value_dist(rd); - percentage = percentage_dist(rd); - if (percentage < 20) - { - call_entry_ptr = concurrent_log.push_back(state::Queue::make_try_enqueue_call(value)); - ret = concurrent_queue.TryEnqueue(value); - concurrent_log.push_back(call_entry_ptr, state::Queue::make_try_enqueue_ret(ret)); - } - else - { - call_entry_ptr = concurrent_log.push_back(state::Queue::make_try_dequeue_call()); - ret = concurrent_queue.TryDequeue(value); - concurrent_log.push_back(call_entry_ptr, state::Queue::make_try_dequeue_ret(ret, value)); - } - } -} - -template -static void embb_experiment_stack(bool is_linearizable) -{ - constexpr std::chrono::hours max_duration{ 1 }; - constexpr std::size_t N = 560000U; - constexpr unsigned number_of_threads = 4U; - 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> result; - ConcurrentLog> concurrent_log{ 2U * log_size }; - S concurrent_stack(N); - - if (!is_linearizable) - { - bool ok = concurrent_stack.TryPush(5); - assert(ok); - } - - // create history - start_threads(number_of_threads, embb_worker_stack, std::cref(worker_configuration), - std::ref(concurrent_log), std::ref(concurrent_stack)); - - const std::size_t number_of_entries{ concurrent_log.number_of_entries() }; - const LogInfo> 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(); - std::chrono::seconds seconds; - - start = std::chrono::system_clock::now(); - { - Log> log_copy{ log_info }; - assert(log_copy.number_of_entries() == number_of_entries); - - LinearizabilityTester, Option::LRU_CACHE> tester{ log_copy.info(), max_duration }; - tester.check(result); - assert(result.is_timeout() || result.is_linearizable() == is_linearizable); - } - end = std::chrono::system_clock::now(); - seconds = std::chrono::duration_cast(end - start); - std::cout << "History length: " << number_of_entries - << ", enabled state cache (LRU=on), O(1) hash: " - << seconds.count() << " s " << std::endl; -} - -template -static void embb_experiment_queue(bool is_linearizable) -{ - constexpr std::chrono::hours max_duration{ 1 }; - constexpr std::size_t N = 560000U; - constexpr unsigned number_of_threads = 4U; - constexpr WorkerConfiguration worker_configuration = { '\24', 70000U }; - constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops; - - std::cout << "embb_experiment_queue : " << (is_linearizable ? "" : "!") << "linearizable" << std::endl; - - Result> result; - ConcurrentLog> concurrent_log{ 2U * log_size }; - S concurrent_queue(N); - - if (!is_linearizable) - { - bool ok = concurrent_queue.TryEnqueue(5); - assert(ok); - } - - // create history - start_threads(number_of_threads, embb_worker_queue, std::cref(worker_configuration), - std::ref(concurrent_log), std::ref(concurrent_queue)); - const std::size_t number_of_entries{ concurrent_log.number_of_entries() }; - const LogInfo> 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(); - std::chrono::seconds seconds; - - start = std::chrono::system_clock::now(); - { - Log> log_copy{ log_info }; - assert(log_copy.number_of_entries() == number_of_entries); - LinearizabilityTester, Option::LRU_CACHE> tester{ log_copy.info(), max_duration }; - tester.check(result); - assert(result.is_timeout() || result.is_linearizable() == is_linearizable); - } - end = std::chrono::system_clock::now(); - seconds = std::chrono::duration_cast(end - start); - std::cout << "History length: " << number_of_entries - << ", enabled state cache (LRU=on), O(1) hash: " - << seconds.count() << " s " << std::endl; -} - - -int main() -{ - - 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(); - - - embb::base::Thread::SetThreadsMaxCount(255); - - std::cout << "Linearizability experiment on LockFreeMPMCQueue" << std::endl; - embb_experiment_queue>(true); - - std::cout << "Linearizability experiment on LockFreeStack" << std::endl; - embb_experiment_stack>(true); - return 0; -} - diff --git a/linearizability_tester/main.cc b/linearizability_tester/main.cc new file mode 100644 index 0000000..43990fe --- /dev/null +++ b/linearizability_tester/main.cc @@ -0,0 +1,192 @@ +#include +#include + +#include +#include +#include + +template +static void embb_worker_stack( + const WorkerConfiguration& worker_configuration, + ConcurrentLog>& concurrent_log, + S& concurrent_stack) +{ + 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 + bool ret; + + char value; + unsigned percentage; + EntryPtr> call_entry_ptr; + for (unsigned number_of_ops{ 0U }; + number_of_ops < worker_configuration.number_of_ops; + ++number_of_ops) + { + value = value_dist(rd); + percentage = percentage_dist(rd); + if (percentage < 30) + { + call_entry_ptr = concurrent_log.push_back(state::Stack::make_try_push_call(value)); + ret = concurrent_stack.TryPush(value); + concurrent_log.push_back(call_entry_ptr, state::Stack::make_try_push_ret(ret)); + } + else + { + call_entry_ptr = concurrent_log.push_back(state::Stack::make_try_pop_call()); + ret = concurrent_stack.TryPop(value); + concurrent_log.push_back(call_entry_ptr, state::Stack::make_try_pop_ret(ret, value)); + } + } +} + +template +static void embb_worker_queue( + const WorkerConfiguration& worker_configuration, + ConcurrentLog>& concurrent_log, + S& concurrent_queue) +{ + 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 + bool ret; + + char value; + unsigned percentage; + EntryPtr> call_entry_ptr; + for (unsigned number_of_ops{ 0U }; + number_of_ops < worker_configuration.number_of_ops; + ++number_of_ops) + { + value = value_dist(rd); + percentage = percentage_dist(rd); + if (percentage < 20) + { + call_entry_ptr = concurrent_log.push_back(state::Queue::make_try_enqueue_call(value)); + ret = concurrent_queue.TryEnqueue(value); + concurrent_log.push_back(call_entry_ptr, state::Queue::make_try_enqueue_ret(ret)); + } + else + { + call_entry_ptr = concurrent_log.push_back(state::Queue::make_try_dequeue_call()); + ret = concurrent_queue.TryDequeue(value); + concurrent_log.push_back(call_entry_ptr, state::Queue::make_try_dequeue_ret(ret, value)); + } + } +} + +template +static void embb_experiment_stack(bool is_linearizable) +{ + constexpr std::chrono::hours max_duration{ 1 }; + constexpr std::size_t N = 560000U; + constexpr unsigned number_of_threads = 4U; + constexpr WorkerConfiguration worker_configuration = { '\24', 70000U }; + constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops; + + Result> result; + ConcurrentLog> concurrent_log{ 2U * log_size }; + S concurrent_stack(N); + + if (!is_linearizable) + { + bool ok = concurrent_stack.TryPush(5); + assert(ok); + } + + // create history + start_threads(number_of_threads, embb_worker_stack, std::cref(worker_configuration), + std::ref(concurrent_log), std::ref(concurrent_stack)); + + const std::size_t number_of_entries{ concurrent_log.number_of_entries() }; + const LogInfo> log_info{ concurrent_log.info() }; + + auto start = std::chrono::system_clock::now(); + auto end = std::chrono::system_clock::now(); + std::chrono::seconds seconds; + + start = std::chrono::system_clock::now(); + { + Log> log_copy{ log_info }; + assert(log_copy.number_of_entries() == number_of_entries); + + LinearizabilityTester, Option::LRU_CACHE> tester{ log_copy.info(), max_duration }; + tester.check(result); + assert(result.is_timeout() || result.is_linearizable() == is_linearizable); + } + end = std::chrono::system_clock::now(); + seconds = std::chrono::duration_cast(end - start); + std::cout << "History length: " << number_of_entries + << ", elapsed time: " + << seconds.count() << " s " << std::endl; +} + +template +static void embb_experiment_queue(bool is_linearizable) +{ + constexpr std::chrono::hours max_duration{ 1 }; + constexpr std::size_t N = 560000U; + constexpr unsigned number_of_threads = 4U; + constexpr WorkerConfiguration worker_configuration = { '\24', 70000U }; + constexpr unsigned log_size = number_of_threads * worker_configuration.number_of_ops; + + + Result> result; + ConcurrentLog> concurrent_log{ 2U * log_size }; + S concurrent_queue(N); + + if (!is_linearizable) + { + bool ok = concurrent_queue.TryEnqueue(5); + assert(ok); + } + + // create history + start_threads(number_of_threads, embb_worker_queue, std::cref(worker_configuration), + std::ref(concurrent_log), std::ref(concurrent_queue)); + const std::size_t number_of_entries{ concurrent_log.number_of_entries() }; + const LogInfo> 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(); + std::chrono::seconds seconds; + + start = std::chrono::system_clock::now(); + { + Log> log_copy{ log_info }; + assert(log_copy.number_of_entries() == number_of_entries); + LinearizabilityTester, Option::LRU_CACHE> tester{ log_copy.info(), max_duration }; + tester.check(result); + assert(result.is_timeout() || result.is_linearizable() == is_linearizable); + } + end = std::chrono::system_clock::now(); + seconds = std::chrono::duration_cast(end - start); + std::cout << "History length: " << number_of_entries + << ", elapsed time: " + << seconds.count() << " s " << std::endl; +} + + +int main() +{ + + // Test functions and structures in linearizability_tester.h + run_tests(); + + embb::base::Thread::SetThreadsMaxCount(255); + + std::cout << "Linearizability test on LockFreeMPMCQueue" << std::endl; + embb_experiment_queue>(true); + + std::cout << "Linearizability test on LockFreeStack" << std::endl; + embb_experiment_stack>(true); + return 0; +} + diff --git a/linearizability_tester/src/linearizability_tester.h b/linearizability_tester/src/linearizability_tester.h index de3bd4d..e8a2eae 100755 --- a/linearizability_tester/src/linearizability_tester.h +++ b/linearizability_tester/src/linearizability_tester.h @@ -10,6 +10,9 @@ // // 3) Unit tests and experiments with TBB, EMBB, and etcd. +#ifndef __LINEARIZABILITY_TESTER +#define __LINEARIZABILITY_TESTER + #include #include #include @@ -73,6 +76,8 @@ std::unique_ptr make_unique(Args&& ...args) using std::make_unique; #endif + + /// Linearizability tester namespace lt { @@ -2945,2031 +2950,7 @@ namespace lt } } -/************* Unit tests && experiments *************/ - -using namespace lt; - -static void test_lru_cache() -{ - LruCache 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 read_call_op_ptr; - - OpPtr read_0_ret_op_ptr, read_0_pending_op_ptr; - OpPtr read_1_ret_op_ptr; - OpPtr read_2_ret_op_ptr; - - OpPtr write_1_call_op_ptr, write_1_ret_op_ptr, write_1_pending_op_ptr; - OpPtr cas_2_succeeded_call_op_ptr, cas_2_succeeded_ret_op_ptr, cas_2_pending_op_ptr; - OpPtr 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& read_call_op = *read_call_op_ptr; - - Op& read_0_ret_op = *read_0_ret_op_ptr; - Op& read_0_pending_op = *read_0_pending_op_ptr; - Op& read_1_ret_op = *read_1_ret_op_ptr; - Op& read_2_ret_op = *read_2_ret_op_ptr; - - Op& write_1_call_op = *write_1_call_op_ptr; - Op& write_1_ret_op = *write_1_ret_op_ptr; - Op& write_1_pending_op = *write_1_pending_op_ptr; - - Op& cas_2_succeeded_call_op = *cas_2_succeeded_call_op_ptr; - Op& cas_2_succeeded_ret_op = *cas_2_succeeded_ret_op_ptr; - Op& cas_2_pending_op = *cas_2_pending_op_ptr; - - Op& cas_2_failed_call_op = *cas_2_failed_call_op_ptr; - Op& 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 ret, call; - call.set_op(state::Set::make_contains_call('\1')); - ret.set_op(state::Set::make_ret(true)); - call.set_match(&ret); - - EntryPtr A{ &call }, B{ &call }, C{ &call }; - - Stack 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(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 empty_op_ptr; - OpPtr contains_op_ptr; - OpPtr insert_op_ptr; - OpPtr erase_op_ptr; - - OpPtr true_ret_op_ptr{ state::Set::make_ret(true) }; - OpPtr false_ret_op_ptr{ state::Set::make_ret(false) }; - - const Op& true_ret_op = *true_ret_op_ptr; - const Op& 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& empty_op = *empty_op_ptr; - Op& contains_op = *contains_op_ptr; - Op& insert_op = *insert_op_ptr; - Op& 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 stack; - state::Stack new_stack; - state::Stack 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 queue; - - state::Queue new_queue; - state::Queue 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 stack, new_stack; - - OpPtr> try_push_1_op_ptr, try_push_2_op_ptr; - OpPtr> try_pop_op_ptr; - - OpPtr> true_try_push_ret_op_ptr{ state::Stack::make_try_push_ret(true) }; - OpPtr> false_try_push_ret_op_ptr{ state::Stack::make_try_push_ret(false) }; - - const Op>& true_try_push_ret_op = *true_try_push_ret_op_ptr; - const Op>& false_try_push_ret_op = *false_try_push_ret_op_ptr; - - OpPtr> true_1_try_pop_ret_op_ptr{ state::Stack::make_try_pop_ret(true, '\1') }; - OpPtr> true_2_try_pop_ret_op_ptr{ state::Stack::make_try_pop_ret(true, '\2') }; - OpPtr> false_try_pop_ret_op_ptr{ state::Stack::make_try_pop_ret(false, '\0') }; - - const Op>& true_1_try_pop_ret_op = *true_1_try_pop_ret_op_ptr; - const Op>& true_2_try_pop_ret_op = *true_2_try_pop_ret_op_ptr; - const Op>& false_try_pop_ret_op = *false_try_pop_ret_op_ptr; - - try_pop_op_ptr = state::Stack::make_try_pop_call(); - Op>& 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::make_try_push_call('\2'); - Op>& 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::make_try_push_call('\1'); - Op>& 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 queue, new_queue; - - OpPtr> try_enqueue_1_op_ptr, try_enqueue_2_op_ptr; - OpPtr> try_dequeue_op_ptr; - - OpPtr> true_try_enqueue_ret_op_ptr{ state::Queue::make_try_enqueue_ret(true) }; - OpPtr> false_try_enqueue_ret_op_ptr{ state::Queue::make_try_enqueue_ret(false) }; - - const Op>& true_try_enqueue_ret_op = *true_try_enqueue_ret_op_ptr; - const Op>& false_try_enqueue_ret_op = *false_try_enqueue_ret_op_ptr; - - OpPtr> true_1_try_dequeue_ret_op_ptr{ state::Queue::make_try_dequeue_ret(true, '\1') }; - OpPtr> true_2_try_dequeue_ret_op_ptr{ state::Queue::make_try_dequeue_ret(true, '\2') }; - OpPtr> false_try_dequeue_ret_op_ptr{ state::Queue::make_try_dequeue_ret(false, '\0') }; - - const Op>& true_1_try_dequeue_ret_op = *true_1_try_dequeue_ret_op_ptr; - const Op>& true_2_try_dequeue_ret_op = *true_2_try_dequeue_ret_op_ptr; - const Op>& false_try_dequeue_ret_op = *false_try_dequeue_ret_op_ptr; - - try_dequeue_op_ptr = state::Queue::make_try_dequeue_call(); - Op>& 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::make_try_enqueue_call('\2'); - Op>& 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::make_try_enqueue_call('\1'); - Op>& 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 log_info; - LinearizabilityTester 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 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 log_info{ &contains_call, number_of_entries }; - LinearizabilityTester t{ log_info }; - assert(t.check()); -} - -static void test_raw_single_contains_is_not_linearizable() -{ - Entry 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 log_info{ &contains_call, number_of_entries }; - LinearizabilityTester t{ log_info }; - assert(!t.check()); -} - -static void test_single_contains(bool ret) -{ - Log log{ 4U }; - EntryPtr 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 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; +#endif - Log log{ 4U }; - EntryPtr 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 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 log{ 4U }; - EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; - EntryPtr 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 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 log{ 4U }; - EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; - EntryPtr 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 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 log{ 4U }; - EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; - EntryPtr 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 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 log{ 4U }; - EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; - EntryPtr 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 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 log{ 4U }; - EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; - EntryPtr 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 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 log{ 4U }; - EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; - EntryPtr 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 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 insert_call_0_entry_ptr, insert_ret_0_entry_ptr; - EntryPtr insert_call_1_entry_ptr, insert_ret_1_entry_ptr; - - Log 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 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 insert_call_0_entry_ptr, insert_ret_0_entry_ptr; - EntryPtr insert_call_1_entry_ptr, insert_ret_1_entry_ptr; - - Log 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 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 log{ 8U }; - EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; - EntryPtr insert_0_call_entry_ptr, insert_0_ret_entry_ptr; - EntryPtr 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 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 log{ 6U }; - - EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; - EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; - EntryPtr 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 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 log{ 6U }; - - EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; - EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; - EntryPtr 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 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 log{ 6U }; - - EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; - EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; - EntryPtr 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 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 log{ 10U }; - - EntryPtr erase_x_call_entry_ptr, erase_x_ret_entry_ptr; - EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; - EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; - EntryPtr insert_y_call_entry_ptr, insert_y_ret_entry_ptr; - EntryPtr 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 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 log{ 12U }; - - EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; - EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; - EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; - EntryPtr call_x3_entry_ptr, ret_x3_entry_ptr; - EntryPtr call_x4_entry_ptr, ret_x4_entry_ptr; - EntryPtr 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 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 log{ 14U }; - - EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; - EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; - EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; - EntryPtr call_x3_entry_ptr, ret_x3_entry_ptr; - EntryPtr call_x4_entry_ptr, ret_x4_entry_ptr; - EntryPtr call_x5_entry_ptr, ret_x5_entry_ptr; - - EntryPtr 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 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 log{ 6U }; - - EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; - EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; - EntryPtr 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 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 log{ 8U }; - - EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; - EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; - EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; - EntryPtr 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 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 log{ 8U }; - - EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; - EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; - EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; - EntryPtr 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 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 log{ 8U }; - - EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; - EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; - EntryPtr 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 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 log{ 8U }; - - EntryPtr call_insert_entry_ptr, ret_insert_entry_ptr; - EntryPtr call_contains_entry_ptr, ret_contains_entry_ptr; - EntryPtr 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 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 log{ 8U }; - - EntryPtr call_contains_0_entry_ptr, ret_contains_0_entry_ptr; - EntryPtr call_contains_1_entry_ptr, ret_contains_1_entry_ptr; - EntryPtr call_insert_entry_ptr, ret_insert_entry_ptr; - EntryPtr 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 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 log{ 8U }; - - EntryPtr call_contains_0_entry_ptr, ret_contains_0_entry_ptr; - EntryPtr call_contains_1_entry_ptr, ret_contains_1_entry_ptr; - EntryPtr call_insert_entry_ptr, ret_insert_entry_ptr; - EntryPtr 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 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> log{ 6U }; - EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; - EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; - EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; - - try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); - try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); - try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); - try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::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> 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> log{ 6U }; - EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; - EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; - EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; - - try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); - try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); - try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); - try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::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> 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> log{ 8U }; - EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; - EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; - EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; - - try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); - try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); - try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); - try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::make_try_pop_ret(true, x)); - try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::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> 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> log{ 12U }; - EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; - EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; - EntryPtr> try_push_z_call_entry_ptr, try_push_z_ret_entry_ptr; - EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; - EntryPtr> try_pop_y_call_entry_ptr, try_pop_y_ret_entry_ptr; - EntryPtr> try_pop_z_call_entry_ptr, try_pop_z_ret_entry_ptr; - - try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); - try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); - try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_pop_y_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); - try_push_z_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(z)); - try_pop_y_ret_entry_ptr = log.add_ret(try_pop_y_call_entry_ptr, state::Stack::make_try_pop_ret(true, y)); - try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); - try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::make_try_pop_ret(true, x)); - try_pop_z_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); - try_push_z_ret_entry_ptr = log.add_ret(try_push_z_call_entry_ptr, state::Stack::make_try_push_ret(true)); - try_pop_z_ret_entry_ptr = log.add_ret(try_pop_z_call_entry_ptr, state::Stack::make_try_pop_ret(true, z)); - - LinearizabilityTester> 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 log{ 10U }; - - EntryPtr erase_x_call_entry_ptr, erase_x_ret_entry_ptr; - EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; - EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; - EntryPtr insert_y_call_entry_ptr, insert_y_ret_entry_ptr; - EntryPtr 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 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 tester_0{ slicer.sublog_info(x) }; - assert(tester_0.check()); - - LinearizabilityTester 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 log{ 6U }; - EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; - EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; - EntryPtr 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 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 tester_0{ slicer.sublog_info(x) }; - assert(!tester_0.check()); - - LinearizabilityTester tester_1{ slicer.sublog_info(y) }; - assert(tester_1.check()); -} - -static void debug() -{ - constexpr char x = '\1'; - - Log log{ 2U }; - - EntryPtr 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 t{ log.info() }; - Result 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 log{ 6U }; - - EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; - EntryPtr 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 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 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& 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 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 -void start_threads(unsigned number_of_threads, F&& f, Args&&... args) -{ - std::vector threads(number_of_threads); - - for (Thread& thread : threads) - thread = Thread(std::forward(f), std::forward(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 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 tester{ concurrent_log.info() }; - - assert(!tester.check()); -} diff --git a/linearizability_tester/src/tests.h b/linearizability_tester/src/tests.h new file mode 100755 index 0000000..99123d1 --- /dev/null +++ b/linearizability_tester/src/tests.h @@ -0,0 +1,2103 @@ +#include + +using namespace lt; + +static void test_lru_cache() +{ + LruCache 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 read_call_op_ptr; + + OpPtr read_0_ret_op_ptr, read_0_pending_op_ptr; + OpPtr read_1_ret_op_ptr; + OpPtr read_2_ret_op_ptr; + + OpPtr write_1_call_op_ptr, write_1_ret_op_ptr, write_1_pending_op_ptr; + OpPtr cas_2_succeeded_call_op_ptr, cas_2_succeeded_ret_op_ptr, cas_2_pending_op_ptr; + OpPtr 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& read_call_op = *read_call_op_ptr; + + Op& read_0_ret_op = *read_0_ret_op_ptr; + Op& read_0_pending_op = *read_0_pending_op_ptr; + Op& read_1_ret_op = *read_1_ret_op_ptr; + Op& read_2_ret_op = *read_2_ret_op_ptr; + + Op& write_1_call_op = *write_1_call_op_ptr; + Op& write_1_ret_op = *write_1_ret_op_ptr; + Op& write_1_pending_op = *write_1_pending_op_ptr; + + Op& cas_2_succeeded_call_op = *cas_2_succeeded_call_op_ptr; + Op& cas_2_succeeded_ret_op = *cas_2_succeeded_ret_op_ptr; + Op& cas_2_pending_op = *cas_2_pending_op_ptr; + + Op& cas_2_failed_call_op = *cas_2_failed_call_op_ptr; + Op& 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 ret, call; + call.set_op(state::Set::make_contains_call('\1')); + ret.set_op(state::Set::make_ret(true)); + call.set_match(&ret); + + EntryPtr A{ &call }, B{ &call }, C{ &call }; + + Stack 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(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 empty_op_ptr; + OpPtr contains_op_ptr; + OpPtr insert_op_ptr; + OpPtr erase_op_ptr; + + OpPtr true_ret_op_ptr{ state::Set::make_ret(true) }; + OpPtr false_ret_op_ptr{ state::Set::make_ret(false) }; + + const Op& true_ret_op = *true_ret_op_ptr; + const Op& 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& empty_op = *empty_op_ptr; + Op& contains_op = *contains_op_ptr; + Op& insert_op = *insert_op_ptr; + Op& 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 stack; + state::Stack new_stack; + state::Stack 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 queue; + + state::Queue new_queue; + state::Queue 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 stack, new_stack; + + OpPtr> try_push_1_op_ptr, try_push_2_op_ptr; + OpPtr> try_pop_op_ptr; + + OpPtr> true_try_push_ret_op_ptr{ state::Stack::make_try_push_ret(true) }; + OpPtr> false_try_push_ret_op_ptr{ state::Stack::make_try_push_ret(false) }; + + const Op>& true_try_push_ret_op = *true_try_push_ret_op_ptr; + const Op>& false_try_push_ret_op = *false_try_push_ret_op_ptr; + + OpPtr> true_1_try_pop_ret_op_ptr{ state::Stack::make_try_pop_ret(true, '\1') }; + OpPtr> true_2_try_pop_ret_op_ptr{ state::Stack::make_try_pop_ret(true, '\2') }; + OpPtr> false_try_pop_ret_op_ptr{ state::Stack::make_try_pop_ret(false, '\0') }; + + const Op>& true_1_try_pop_ret_op = *true_1_try_pop_ret_op_ptr; + const Op>& true_2_try_pop_ret_op = *true_2_try_pop_ret_op_ptr; + const Op>& false_try_pop_ret_op = *false_try_pop_ret_op_ptr; + + try_pop_op_ptr = state::Stack::make_try_pop_call(); + Op>& 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::make_try_push_call('\2'); + Op>& 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::make_try_push_call('\1'); + Op>& 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 queue, new_queue; + + OpPtr> try_enqueue_1_op_ptr, try_enqueue_2_op_ptr; + OpPtr> try_dequeue_op_ptr; + + OpPtr> true_try_enqueue_ret_op_ptr{ state::Queue::make_try_enqueue_ret(true) }; + OpPtr> false_try_enqueue_ret_op_ptr{ state::Queue::make_try_enqueue_ret(false) }; + + const Op>& true_try_enqueue_ret_op = *true_try_enqueue_ret_op_ptr; + const Op>& false_try_enqueue_ret_op = *false_try_enqueue_ret_op_ptr; + + OpPtr> true_1_try_dequeue_ret_op_ptr{ state::Queue::make_try_dequeue_ret(true, '\1') }; + OpPtr> true_2_try_dequeue_ret_op_ptr{ state::Queue::make_try_dequeue_ret(true, '\2') }; + OpPtr> false_try_dequeue_ret_op_ptr{ state::Queue::make_try_dequeue_ret(false, '\0') }; + + const Op>& true_1_try_dequeue_ret_op = *true_1_try_dequeue_ret_op_ptr; + const Op>& true_2_try_dequeue_ret_op = *true_2_try_dequeue_ret_op_ptr; + const Op>& false_try_dequeue_ret_op = *false_try_dequeue_ret_op_ptr; + + try_dequeue_op_ptr = state::Queue::make_try_dequeue_call(); + Op>& 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::make_try_enqueue_call('\2'); + Op>& 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::make_try_enqueue_call('\1'); + Op>& 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 log_info; + LinearizabilityTester 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 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 log_info{ &contains_call, number_of_entries }; + LinearizabilityTester t{ log_info }; + assert(t.check()); +} + +static void test_raw_single_contains_is_not_linearizable() +{ + Entry 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 log_info{ &contains_call, number_of_entries }; + LinearizabilityTester t{ log_info }; + assert(!t.check()); +} + +static void test_single_contains(bool ret) +{ + Log log{ 4U }; + EntryPtr 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 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 log{ 4U }; + EntryPtr 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 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 log{ 4U }; + EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; + EntryPtr 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 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 log{ 4U }; + EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; + EntryPtr 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 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 log{ 4U }; + EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; + EntryPtr 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 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 log{ 4U }; + EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; + EntryPtr 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 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 log{ 4U }; + EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; + EntryPtr 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 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 log{ 4U }; + EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; + EntryPtr 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 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 insert_call_0_entry_ptr, insert_ret_0_entry_ptr; + EntryPtr insert_call_1_entry_ptr, insert_ret_1_entry_ptr; + + Log 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 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 insert_call_0_entry_ptr, insert_ret_0_entry_ptr; + EntryPtr insert_call_1_entry_ptr, insert_ret_1_entry_ptr; + + Log 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 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 log{ 8U }; + EntryPtr contains_call_entry_ptr, contains_ret_entry_ptr; + EntryPtr insert_0_call_entry_ptr, insert_0_ret_entry_ptr; + EntryPtr 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 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 log{ 6U }; + + EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; + EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; + EntryPtr 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 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 log{ 6U }; + + EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; + EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; + EntryPtr 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 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 log{ 6U }; + + EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; + EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; + EntryPtr 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 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 log{ 10U }; + + EntryPtr erase_x_call_entry_ptr, erase_x_ret_entry_ptr; + EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; + EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; + EntryPtr insert_y_call_entry_ptr, insert_y_ret_entry_ptr; + EntryPtr 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 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 log{ 12U }; + + EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; + EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; + EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; + EntryPtr call_x3_entry_ptr, ret_x3_entry_ptr; + EntryPtr call_x4_entry_ptr, ret_x4_entry_ptr; + EntryPtr 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 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 log{ 14U }; + + EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; + EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; + EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; + EntryPtr call_x3_entry_ptr, ret_x3_entry_ptr; + EntryPtr call_x4_entry_ptr, ret_x4_entry_ptr; + EntryPtr call_x5_entry_ptr, ret_x5_entry_ptr; + + EntryPtr 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 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 log{ 6U }; + + EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; + EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; + EntryPtr 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 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 log{ 8U }; + + EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; + EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; + EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; + EntryPtr 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 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 log{ 8U }; + + EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; + EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; + EntryPtr call_x2_entry_ptr, ret_x2_entry_ptr; + EntryPtr 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 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 log{ 8U }; + + EntryPtr call_x0_entry_ptr, ret_x0_entry_ptr; + EntryPtr call_x1_entry_ptr, ret_x1_entry_ptr; + EntryPtr 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 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 log{ 8U }; + + EntryPtr call_insert_entry_ptr, ret_insert_entry_ptr; + EntryPtr call_contains_entry_ptr, ret_contains_entry_ptr; + EntryPtr 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 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 log{ 8U }; + + EntryPtr call_contains_0_entry_ptr, ret_contains_0_entry_ptr; + EntryPtr call_contains_1_entry_ptr, ret_contains_1_entry_ptr; + EntryPtr call_insert_entry_ptr, ret_insert_entry_ptr; + EntryPtr 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 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 log{ 8U }; + + EntryPtr call_contains_0_entry_ptr, ret_contains_0_entry_ptr; + EntryPtr call_contains_1_entry_ptr, ret_contains_1_entry_ptr; + EntryPtr call_insert_entry_ptr, ret_insert_entry_ptr; + EntryPtr 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 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> log{ 6U }; + EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; + EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; + EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; + + try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); + try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); + try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); + try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::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> 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> log{ 6U }; + EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; + EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; + EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; + + try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); + try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); + try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); + try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::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> 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> log{ 8U }; + EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; + EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; + EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; + + try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); + try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); + try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); + try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::make_try_pop_ret(true, x)); + try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::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> 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> log{ 12U }; + EntryPtr> try_push_x_call_entry_ptr, try_push_x_ret_entry_ptr; + EntryPtr> try_push_y_call_entry_ptr, try_push_y_ret_entry_ptr; + EntryPtr> try_push_z_call_entry_ptr, try_push_z_ret_entry_ptr; + EntryPtr> try_pop_x_call_entry_ptr, try_pop_x_ret_entry_ptr; + EntryPtr> try_pop_y_call_entry_ptr, try_pop_y_ret_entry_ptr; + EntryPtr> try_pop_z_call_entry_ptr, try_pop_z_ret_entry_ptr; + + try_push_x_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(x)); + try_push_y_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(y)); + try_push_x_ret_entry_ptr = log.add_ret(try_push_x_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_push_y_ret_entry_ptr = log.add_ret(try_push_y_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_pop_y_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); + try_push_z_call_entry_ptr = log.add_call(state::Stack::make_try_push_call(z)); + try_pop_y_ret_entry_ptr = log.add_ret(try_pop_y_call_entry_ptr, state::Stack::make_try_pop_ret(true, y)); + try_pop_x_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); + try_pop_x_ret_entry_ptr = log.add_ret(try_pop_x_call_entry_ptr, state::Stack::make_try_pop_ret(true, x)); + try_pop_z_call_entry_ptr = log.add_call(state::Stack::make_try_pop_call()); + try_push_z_ret_entry_ptr = log.add_ret(try_push_z_call_entry_ptr, state::Stack::make_try_push_ret(true)); + try_pop_z_ret_entry_ptr = log.add_ret(try_pop_z_call_entry_ptr, state::Stack::make_try_pop_ret(true, z)); + + LinearizabilityTester> 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 log{ 10U }; + + EntryPtr erase_x_call_entry_ptr, erase_x_ret_entry_ptr; + EntryPtr insert_x_call_entry_ptr, insert_x_ret_entry_ptr; + EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; + EntryPtr insert_y_call_entry_ptr, insert_y_ret_entry_ptr; + EntryPtr 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 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 tester_0{ slicer.sublog_info(x) }; + assert(tester_0.check()); + + LinearizabilityTester 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 log{ 6U }; + EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; + EntryPtr contains_y_call_entry_ptr, contains_y_ret_entry_ptr; + EntryPtr 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 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 tester_0{ slicer.sublog_info(x) }; + assert(!tester_0.check()); + + LinearizabilityTester tester_1{ slicer.sublog_info(y) }; + assert(tester_1.check()); +} + +static void debug() +{ + constexpr char x = '\1'; + + Log log{ 2U }; + + EntryPtr 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 t{ log.info() }; + Result 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 log{ 6U }; + + EntryPtr contains_x_call_entry_ptr, contains_x_ret_entry_ptr; + EntryPtr 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 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 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& 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 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 +void start_threads(unsigned number_of_threads, F&& f, Args&&... args) +{ + std::vector threads(number_of_threads); + + for (Thread& thread : threads) + thread = Thread(std::forward(f), std::forward(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 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 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 -- libgit2 0.26.0