#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(); }