From 14fb38c0da024bfc3510ae891ca147aee478187a Mon Sep 17 00:00:00 2001 From: Roman Manevich Date: Tue, 13 Apr 2021 06:12:38 -0700 Subject: [PATCH] Experiments with KLEE/fuzzing to catch linearizability bugs in simple data structures Reviewed By: jberdine Differential Revision: D27477093 fbshipit-source-id: 72a1e88ee --- .../test/linearizability-experiments/Makefile | 77 +++++ .../linearizability-experiments/ref_queue.c | 50 ++++ .../linearizability-experiments/ref_queue.h | 29 ++ .../linearizability-experiments/ref_stack.c | 33 +++ .../linearizability-experiments/ref_stack.h | 23 ++ .../linearizability-experiments/scheduler.c | 61 ++++ .../linearizability-experiments/scheduler.h | 32 ++ .../test_folly_ProducerConsumerQueue.c | 250 ++++++++++++++++ .../linearizability-experiments/test_mains.h | 137 +++++++++ .../test_ms_queue.c | 276 ++++++++++++++++++ .../test_treiber_stack.c | 214 ++++++++++++++ .../treiber_stack.c | 63 ++++ .../treiber_stack.h | 38 +++ 13 files changed, 1283 insertions(+) create mode 100644 sledge/test/linearizability-experiments/Makefile create mode 100644 sledge/test/linearizability-experiments/ref_queue.c create mode 100644 sledge/test/linearizability-experiments/ref_queue.h create mode 100644 sledge/test/linearizability-experiments/ref_stack.c create mode 100644 sledge/test/linearizability-experiments/ref_stack.h create mode 100644 sledge/test/linearizability-experiments/scheduler.c create mode 100644 sledge/test/linearizability-experiments/scheduler.h create mode 100644 sledge/test/linearizability-experiments/test_folly_ProducerConsumerQueue.c create mode 100644 sledge/test/linearizability-experiments/test_mains.h create mode 100644 sledge/test/linearizability-experiments/test_ms_queue.c create mode 100644 sledge/test/linearizability-experiments/test_treiber_stack.c create mode 100644 sledge/test/linearizability-experiments/treiber_stack.c create mode 100644 sledge/test/linearizability-experiments/treiber_stack.h diff --git a/sledge/test/linearizability-experiments/Makefile b/sledge/test/linearizability-experiments/Makefile new file mode 100644 index 000000000..306273cfe --- /dev/null +++ b/sledge/test/linearizability-experiments/Makefile @@ -0,0 +1,77 @@ +# Copyright (c) Facebook, Inc. and its affiliates. +# +# This source code is licensed under the MIT license found in the +# LICENSE file in the root directory of this source tree. + +CLANG_BUILD_FLAGS=-stdlib=libc++ -g -o1 -fsanitize=fuzzer,address,signed-integer-overflow +FUZZ_BUILD_FLAGS=${CLANG_BUILD_FLAGS} -DFUZZ +KLEE_RUN_FLAGS=--use-query-log=all:kquery --use-query-log=solver:kquery --optimize --search=dfs -use-independent-solver=0 -use-cex-cache=0 --write-no-tests -use-forked-solver=0 --rewrite-equalities=0 + +default: klee_treiber + +######################################## +## KLEE + +klee_clean: + rm -rf *.bc *.mbc klee-out-* klee-last + +klee_build: + clang -DKLEE -I$$HOME/klee/include/klee -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone *.c + llvm-link scheduler.bc ref_stack.bc treiber_stack.bc test_treiber_stack.bc -o klee_treiber_stack.mbc + llvm-link scheduler.bc ref_queue.bc test_folly_ProducerConsumerQueue.bc -o klee_folly_ProducerConsumerQueue.mbc + llvm-link scheduler.bc ref_queue.bc test_ms_queue.bc -o klee_ms_queue.mbc + +klee_treiber: clean klee_build + time klee ${KLEE_RUN_FLAGS} klee_treiber_stack.mbc + +klee_folly_ProducerConsumerQueue: clean klee_build + time klee ${KLEE_RUN_FLAGS} klee_folly_ProducerConsumerQueue.mbc + +klee_ms_queue: clean klee_build + time klee ${KLEE_RUN_FLAGS} klee_ms_queue.mbc + +######################################## +## libfuzz fuzzing + +fuzz_clean: + rm -rf crash-* fuzzer_* *.dSYM fuzz_treiber fuzz_folly_ProducerConsumerQueue fuzz_ms_queue + +fuzz_build: + clang $(FUZZ_BUILD_FLAGS) scheduler.c ref_stack.c treiber_stack.c test_treiber_stack.c -o fuzz_treiber + clang $(FUZZ_BUILD_FLAGS) scheduler.c ref_queue.c test_folly_ProducerConsumerQueue.c -o fuzz_folly_ProducerConsumerQueue + clang $(FUZZ_BUILD_FLAGS) scheduler.c ref_queue.c test_ms_queue.c -o fuzz_ms_queue + +fuzz_treiber: fuzz_clean fuzz_build + time ./fuzz_treiber + +fuzz_folly_ProducerConsumerQueue: fuzz_clean fuzz_build + time ./fuzz_folly_ProducerConsumerQueue + +fuzz_ms_queue: fuzz_clean fuzz_build + time ./fuzz_ms_queue + +######################################## +## Completely randomized fuzzer + +rand_clean: + rm -rf crash-* fuzzer_* rand_treiber rand_folly_ProducerConsumerQueue rand_ms_queue + +rand_build: + clang ${CLANG_BUILD_FLAGS} -DRAND_FUZZ scheduler.c ref_stack.c treiber_stack.c test_treiber_stack.c -o rand_treiber + clang ${CLANG_BUILD_FLAGS} -DRAND_FUZZ scheduler.c ref_queue.c test_folly_ProducerConsumerQueue.c -o rand_folly_ProducerConsumerQueue + clang ${CLANG_BUILD_FLAGS} -DRAND_FUZZ scheduler.c ref_queue.c test_ms_queue.c -o rand_ms_queue + +rand_treiber: rand_clean rand_build + time ./rand_treiber + +rand_folly_ProducerConsumerQueue: rand_clean rand_build + time ./rand_folly_ProducerConsumerQueue + +rand_ms_queue: rand_clean rand_build + time ./rand_ms_queue + +######################################## +## Common stuff + +clean: klee_clean fuzz_clean rand_clean + diff --git a/sledge/test/linearizability-experiments/ref_queue.c b/sledge/test/linearizability-experiments/ref_queue.c new file mode 100644 index 000000000..25baf357f --- /dev/null +++ b/sledge/test/linearizability-experiments/ref_queue.c @@ -0,0 +1,50 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include "ref_queue.h" +#include +#include + +ref_queue* new_ref_queue(int depth) { + ref_queue* result = malloc(sizeof(ref_queue)); + result->data = malloc(sizeof(data_type) * depth); + result->depth = depth; + result->size = 0; + result->start = 0; + result->end = 0; + return result; +} + +bool ref_enqueue(ref_queue* q, data_type v) { + if (q->size == q->depth) { + return false; + } + ++q->size; + q->data[q->end] = v; + ++q->end; + if (q->end == q->depth) { + q->end = 0; + } + // printf("ref_enqueue: %d\n", v); + return true; +} + +data_type ref_dequeue(ref_queue* q) { + if (q->size == 0) { + return EMPTY; + } + data_type result = q->data[q->start]; + ++q->start; + if (q->start == q->depth) { + q->start = 0; + } + --q->size; + // printf("ref_dequeue: %d\n", result); + return result; +} + +void print_ref_queue(ref_queue* q) {} diff --git a/sledge/test/linearizability-experiments/ref_queue.h b/sledge/test/linearizability-experiments/ref_queue.h new file mode 100644 index 000000000..ed481de74 --- /dev/null +++ b/sledge/test/linearizability-experiments/ref_queue.h @@ -0,0 +1,29 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#ifndef REF_QUEUE +#define REF_QUEUE + +#include + +typedef int data_type; +#define EMPTY -1 + +typedef struct { + data_type* data; + int depth; + int size; + int start; + int end; +} ref_queue; + +ref_queue* new_ref_queue(int depth); +bool ref_enqueue(ref_queue* q, data_type v); +data_type ref_dequeue(ref_queue* q); +void print_ref_queue(ref_queue* q); + +#endif diff --git a/sledge/test/linearizability-experiments/ref_stack.c b/sledge/test/linearizability-experiments/ref_stack.c new file mode 100644 index 000000000..ec282095f --- /dev/null +++ b/sledge/test/linearizability-experiments/ref_stack.c @@ -0,0 +1,33 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include "ref_stack.h" +#include +#include + +ref_stack* new_ref_stack(int max_size) { + ref_stack* result = malloc(sizeof(ref_stack)); + result->data = malloc(sizeof(data_type) * max_size); + result->max_size = max_size; + result->size = 0; + return result; +} + +void ref_stack_push(ref_stack* s, data_type v) { + assert(s != NULL); + assert(s->size < s->max_size); + s->data[s->size] = v; + ++s->size; +} + +data_type ref_stack_pop(ref_stack* s) { + assert(s != NULL); + assert(s->size > 0); + --s->size; + data_type result = s->data[s->size]; + return result; +} diff --git a/sledge/test/linearizability-experiments/ref_stack.h b/sledge/test/linearizability-experiments/ref_stack.h new file mode 100644 index 000000000..37fcb6930 --- /dev/null +++ b/sledge/test/linearizability-experiments/ref_stack.h @@ -0,0 +1,23 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#ifndef REF_STACK +#define REF_STACK + +typedef int data_type; + +typedef struct { + data_type* data; + int size; + int max_size; +} ref_stack; + +ref_stack* new_ref_stack(int max_size); +void ref_stack_push(ref_stack* s, data_type v); +data_type ref_stack_pop(ref_stack* s); + +#endif diff --git a/sledge/test/linearizability-experiments/scheduler.c b/sledge/test/linearizability-experiments/scheduler.c new file mode 100644 index 000000000..c86c2fbf6 --- /dev/null +++ b/sledge/test/linearizability-experiments/scheduler.c @@ -0,0 +1,61 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include "scheduler.h" +#include +#include +#include + +base_frame* make_frame(void* derived_frame, int derived_frame_type) { + base_frame* frame = malloc(sizeof(base_frame)); + init_frame(frame, derived_frame, derived_frame_type); + return frame; +} + +void init_frame(base_frame* frame, void* derived_frame, + int derived_frame_type) { + frame->pc = 0; + frame->derived_frame = derived_frame; + frame->derived_frame_type = derived_frame_type; +} + +int execute_schedule(uint8_t* schedule, size_t schedule_len, base_frame* frames, + int num_frames, int max_context_switches) { + int num_context_switches = 0; + int num_done = 0; + uint8_t previous_op = schedule[0]; + uint8_t current_op = previous_op; + assert(schedule != NULL); + bool frame_done = false; /* Tracks whether the last step ended a frame. */ + for (size_t schedule_idx = 0; + schedule_idx < schedule_len && num_done < num_frames; ++schedule_idx) { + current_op = schedule[schedule_idx]; + if (current_op != previous_op && !frame_done) { + ++num_context_switches; + if (num_context_switches > max_context_switches) { + return num_context_switches; + } + } + previous_op = current_op; + + base_frame* frame = &frames[current_op]; + if (frame->pc == PC_DONE) { + continue; + } else { + frame_done = false; + int next_pc = step(frame); + frame->pc = next_pc; + if (next_pc == PC_DONE) { + frame_done = true; + ++num_done; + } else if (next_pc == PC_ABORT) { + break; + } + } + } + return num_context_switches; +} diff --git a/sledge/test/linearizability-experiments/scheduler.h b/sledge/test/linearizability-experiments/scheduler.h new file mode 100644 index 000000000..1051c71f3 --- /dev/null +++ b/sledge/test/linearizability-experiments/scheduler.h @@ -0,0 +1,32 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#ifndef SCHEDULER_H +#define SCHEDULER_H + +#include + +typedef struct { + int pc; + int derived_frame_type; + void* derived_frame; +} base_frame; + +#define PC_DONE -1 +#define PC_ABORT -2 + +/** Steps the thread with the current frame and tests for correctness. + */ +extern int step(base_frame* frame); + +base_frame* make_frame(void* derived_frame, int derived_frame_type); +void init_frame(base_frame* frame, void* derived_frame, int derived_frame_type); +uint8_t* make_symbolic_schedule(int schedule_len, int max_id); +int execute_schedule(uint8_t* schedule, size_t schedule_len, base_frame* frames, + int num_frames, int max_context_switches); + +#endif diff --git a/sledge/test/linearizability-experiments/test_folly_ProducerConsumerQueue.c b/sledge/test/linearizability-experiments/test_folly_ProducerConsumerQueue.c new file mode 100644 index 000000000..4b0319604 --- /dev/null +++ b/sledge/test/linearizability-experiments/test_folly_ProducerConsumerQueue.c @@ -0,0 +1,250 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +// Testing ProducerConsumerQueue from +// https://github.com/facebook/folly/blob/master/folly/ProducerConsumerQueue.h + +#include +#include +#include + +#include "ref_queue.h" +#include "scheduler.h" + +#define NUM_THREADS 2 +#define CONTEXT_SWITCHES_BOUND 2 +#define SCHEDULE_POINTS 8 +#include "test_mains.h" + +// size must be >= 2. +#define QUEUE_DEPTH 2 + +#define READ_BUG false +#define SIZE_BUG true + +typedef enum { CONSUMER, PRODUCER } frame_type; + +typedef struct { + int size; + int readIndex; + int writeIndex; + data_type* records; +} queue; + +typedef struct { + queue* q; + ref_queue* ref; + data_type v; + int currentWrite; + int nextRecord; +} producer_frame; + +typedef struct { + queue* q; + ref_queue* ref; + int currentRead; + int currentWrite; // For the bug + int nextRecord; + data_type result; +} consumer_frame; + +void init_queue(queue* q, size_t size) { + q->size = size; + q->readIndex = 0; + q->writeIndex = 0; + q->records = malloc(sizeof(data_type) * size); +} + +consumer_frame* make_consumer_frame(queue* q, ref_queue* ref) { + consumer_frame* frame = malloc(sizeof(consumer_frame)); + frame->q = q; + frame->ref = ref; + return frame; +} + +producer_frame* make_producer_frame(queue* q, ref_queue* ref) { + producer_frame* frame = malloc(sizeof(producer_frame)); + frame->q = q; + frame->ref = ref; + return frame; +} + +data_type val = 0; + +// write +int step_producer(producer_frame* frame, int pc) { + queue* q = frame->q; + switch (pc) { + case 0: + frame->v = val; + val++; + frame->currentWrite = q->writeIndex; + frame->nextRecord = frame->currentWrite + 1; + if (frame->nextRecord == q->size) { + frame->nextRecord = 0; + } + pc = 1; + break; + + case 1: + if (frame->nextRecord != q->readIndex) { + pc = 2; + } else { + bool queue_result = false; + bool ref_result = ref_enqueue(frame->ref, frame->v); + if (ref_result != queue_result) { + printf("ref_result: %d, queue_result: %d\n", ref_result, queue_result); + } + assert(ref_result == queue_result); + pc = 0; + } + break; + + case 2: + q->records[frame->currentWrite] = frame->v; + pc = 3; + break; + + case 3: + q->writeIndex = frame->nextRecord; + bool queue_result = true; + // printf("test enqueue: %d\n", frame->v); + bool ref_result = ref_enqueue(frame->ref, frame->v); + assert(ref_result == queue_result); + pc = 0; + break; + + default: + assert(false); + } + return pc; +} + +// read +int step_consumer(consumer_frame* frame, int pc) { + queue* q = frame->q; + switch (pc) { + case 0: + frame->currentRead = q->readIndex; + pc = 1; + break; + + case 1: + if (frame->currentRead == q->writeIndex) { + // queue is empty + data_type ref_result = ref_dequeue(frame->ref); + assert(ref_result == EMPTY); + pc = 0; + break; + } + frame->nextRecord = frame->currentRead + 1; + if (frame->nextRecord == q->size) { + frame->nextRecord = 0; + } + pc = 2; + break; + + case 2: + frame->result = q->records[frame->currentRead]; + pc = 3; + break; + + case 3: + q->readIndex = frame->nextRecord; + data_type ref_result = ref_dequeue(frame->ref); + assert(ref_result == frame->result); + pc = 0; + break; + + default: + assert(false); + } + return pc; +} + +int step_consumer_bug(consumer_frame* frame, int pc) { + queue* q = frame->q; + switch (pc) { + case 0: + frame->currentWrite = q->writeIndex; + pc = 1; + break; + + case 1: + frame->currentRead = q->readIndex; + if (frame->currentRead == frame->currentWrite) { + // queue is empty + data_type ref_result = ref_dequeue(frame->ref); + assert(ref_result == EMPTY); + pc = 0; + break; + } + frame->nextRecord = frame->currentRead + 1; + if (frame->nextRecord == q->size) { + frame->nextRecord = 0; + } + pc = 2; + break; + + case 2: + frame->result = q->records[frame->currentRead]; + pc = 3; + break; + + case 3: + q->readIndex = frame->nextRecord; + data_type ref_result = ref_dequeue(frame->ref); + assert(ref_result == frame->result); + pc = 0; + break; + + default: + assert(false); + } + return pc; +} + +// Runs the operation associated with the given frame until reaching the next +// block. That is, the next statement accessing shared memory. +int step(base_frame* frame) { + assert(frame != NULL); + if (frame->derived_frame_type == CONSUMER) { + consumer_frame* derived_frame = (consumer_frame*)frame->derived_frame; + assert(derived_frame != NULL); + if (READ_BUG) { + return step_consumer_bug(derived_frame, frame->pc); + } else { + return step_consumer(derived_frame, frame->pc); + } + } else if (frame->derived_frame_type == PRODUCER) { + producer_frame* derived_frame = (producer_frame*)frame->derived_frame; + assert(derived_frame != NULL); + return step_producer(derived_frame, frame->pc); + } else { + assert(false); + } +} + +int test_with_schedule(uint8_t* schedule, size_t len) { + queue test_queue; + + init_queue(&test_queue, QUEUE_DEPTH); + // From the folly documentation: + // "Also, note that the number of usable slots in the queue at any + // given time is actually (size-1)..." + ref_queue* ref; + if (SIZE_BUG) { + ref = new_ref_queue(QUEUE_DEPTH); + } else { + ref = new_ref_queue(QUEUE_DEPTH - 1); + } + base_frame frames[2]; + init_frame(&frames[0], make_consumer_frame(&test_queue, ref), CONSUMER); + init_frame(&frames[1], make_producer_frame(&test_queue, ref), PRODUCER); + execute_schedule(schedule, len, frames, NUM_THREADS, CONTEXT_SWITCHES_BOUND); + return 0; +} diff --git a/sledge/test/linearizability-experiments/test_mains.h b/sledge/test/linearizability-experiments/test_mains.h new file mode 100644 index 000000000..a0b450fe4 --- /dev/null +++ b/sledge/test/linearizability-experiments/test_mains.h @@ -0,0 +1,137 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +// This file serves as a kind of template, used to separate the code needed +// to run the various testing tools (Klee, libfuzz, random fuzzer) +// from the code defining the blocks of the code under test. +// To use this file: +// 1) Include it, +// 2) Define the following values: NUM_THREADS, SCHEDULE_POINTS, and +// CONTEXT_SWITCHES_BOUND. +// 3) Define a function int test_with_schedule(uint8_t* +// schedule, size_t len), which should create 'NUM_THREADS' base_frames and call +// execute_schedule( +// schedule, +// len, +// frames, // 'NUM_THREADS' base_frames. +// NUM_THREADS, +// CONTEXT_SWITCHES_BOUND +// ); + +int test_with_schedule(uint8_t* schedule, size_t len); + +#ifdef KLEE +#include + +uint8_t* make_symbolic_schedule(int schedule_len, int max_id) { + uint8_t* schedule = malloc(sizeof(int) * schedule_len); + klee_make_symbolic(schedule, sizeof(int) * schedule_len, "schedule"); + for (int schedule_idx = 0; schedule_idx < schedule_len; ++schedule_idx) { + uint8_t current_id = schedule[schedule_idx]; + klee_assume(current_id < max_id); + } + return schedule; +} + +// Klee entry point. +int main(void) { + // print_test(); + // return 0; + uint8_t* schedule = make_symbolic_schedule(SCHEDULE_POINTS, NUM_THREADS); + test_with_schedule(schedule, SCHEDULE_POINTS); + return 0; +} +#endif + +#ifdef RAND_FUZZ +static int fuzz_counter = 0; +int main(void) { + uint8_t schedule[SCHEDULE_POINTS]; + while (true) { + for (int idx = 0; idx < SCHEDULE_POINTS; ++idx) { + schedule[idx] = rand() % NUM_THREADS; + } + printf("schedule %d: ", fuzz_counter); + ++fuzz_counter; + for (int idx = 0; idx < SCHEDULE_POINTS; ++idx) { + printf("%hhu ", schedule[idx]); + } + printf("\n"); + test_with_schedule(schedule, SCHEDULE_POINTS); + } + return 0; +} +#endif // RAND_FUZZ + +#ifdef ENUM_FUZZ +static int fuzz_counter = 0; +int main(void) { + uint8_t schedule[SCHEDULE_POINTS]; + for (int idx = 0; idx < SCHEDULE_POINTS; ++idx) { + schedule[idx] = 0; + } + while (true) { + bool all_max = true; + for (int idx = 0; idx < SCHEDULE_POINTS; ++idx) { + if (schedule[idx] != NUM_THREADS - 1) { + all_max = false; + break; + } + } + if (all_max) { + return 0; + } + printf("schedule %d: ", fuzz_counter); + ++fuzz_counter; + for (int idx = 0; idx < SCHEDULE_POINTS; ++idx) { + printf("%hhu ", schedule[idx]); + } + printf("\n"); + test_with_schedule(schedule, SCHEDULE_POINTS); + for (int idx = 0; idx < SCHEDULE_POINTS; ++idx) { + if (schedule[idx] < NUM_THREADS - 1) { + ++schedule[idx]; + break; + } else { + for (int idx2 = idx; idx2 < SCHEDULE_POINTS; ++idx2) { + if (schedule[idx2] == NUM_THREADS - 1) { + schedule[idx2] = 0; + } else { + ++schedule[idx2]; + break; + } + } + break; + } + } + } + return 0; +} +#endif // ENUM_FUZZ + +#ifdef FUZZ +static int fuzz_counter = 0; +int LLVMFuzzerTestOneInput(uint8_t* schedule, size_t size) { + if (size > SCHEDULE_POINTS) { + return 0; + } + for (int idx = 0; idx < size; ++idx) { + if (schedule[idx] >= NUM_THREADS) { + return 0; + } + } + printf("fuzz schedule: %d\n", fuzz_counter); + ++fuzz_counter; + // printf("schedule size: %zu\n", size); + // for (int idx = 0; idx < size; ++idx) { + // printf("%hhu ", schedule[idx]); + // } + // printf("\n"); + test_with_schedule(schedule, size); + return 0; // Non-zero return values are reserved for future use. +} +#endif // FUZZ diff --git a/sledge/test/linearizability-experiments/test_ms_queue.c b/sledge/test/linearizability-experiments/test_ms_queue.c new file mode 100644 index 000000000..3e8198041 --- /dev/null +++ b/sledge/test/linearizability-experiments/test_ms_queue.c @@ -0,0 +1,276 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +// Testing the non-blocking queue described in +// "Simple, Fast, and Practical Non-Blocking and Blocking +// Concurrent Queue Algorithms" +// (https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf) + +#include +#include +#include +#include +#include + +#include "ref_queue.h" +#include "scheduler.h" + +#define NUM_THREADS 2 +#define CONTEXT_SWITCHES_BOUND 1 +#define SCHEDULE_POINTS 13 +#include "test_mains.h" + +typedef int data_type; +#define EMPTY -1 + +typedef struct node_t { + data_type d; + struct node_t* n; +} node; + +typedef struct queue_t { + node* head; + node* tail; +} queue; + +typedef enum { ENQUEUE, DEQUEUE } frame_type; + +typedef struct { + queue* q; + ref_queue* ref; + data_type v; + node* new_node; + node* tail; + node* next; +} enqueue_frame; + +typedef struct { + queue* q; + ref_queue* ref; + data_type result; + node* head; + node* tail; + node* next; +} dequeue_frame; + +void init_queue(queue* q) { + node* dummy = malloc(sizeof(node)); + dummy->n = NULL; + q->head = dummy; + q->tail = dummy; +} + +dequeue_frame* make_dequeue_frame(queue* q, ref_queue* ref) { + dequeue_frame* frame = malloc(sizeof(dequeue_frame)); + frame->q = q; + frame->ref = ref; + return frame; +} + +enqueue_frame* make_enqueue_frame(queue* q, ref_queue* ref, data_type v) { + enqueue_frame* frame = malloc(sizeof(enqueue_frame)); + frame->q = q; + frame->ref = ref; + frame->v = v; + return frame; +} + +int step_enqueue(enqueue_frame* frame, int pc) { + queue* q = frame->q; + bool cas_result; + switch (pc) { + case 0: + case 1: + frame->new_node = malloc(sizeof(node)); + frame->new_node->d = frame->v; + frame->new_node->n = NULL; + pc = 4; + break; + + case 4: + case 5: + frame->tail = q->tail; + pc = 6; + break; + + case 6: + frame->next = frame->tail->n; + pc = 7; + break; + + case 7: + if (frame->tail == q->tail) { + pc = 8; + } else { + pc = 4; + } + break; + + case 8: + if (frame->next == NULL) { + pc = 9; + } else { + pc = 13; + } + break; + + case 9: + if (frame->tail->n == frame->next) { // Fake CAS + frame->tail->n = frame->new_node; + cas_result = true; + } else { + cas_result = false; + } + if (cas_result) { + bool ref_result = ref_enqueue(frame->ref, frame->v); + assert(ref_result); + pc = 17; + } else { + pc = 4; + } + break; + + case 13: + if (q->tail == frame->tail) { // Fake CAS + q->tail = frame->next; + } + pc = 4; + break; + + case 17: + if (q->tail == frame->tail) { // Fake CAS + q->tail = frame->new_node; + } + pc = PC_DONE; + break; + + default: + assert(false); + } + return pc; +} + +int step_dequeue(dequeue_frame* frame, int pc) { + queue* q = frame->q; + bool cas_result; + switch (pc) { + case 0: + case 1: + case 2: + frame->head = q->head; + pc = 3; + break; + + case 3: + frame->tail = q->tail; + pc = 4; + break; + + case 4: + frame->next = frame->head->n; + pc = 5; + break; + + case 5: + if (frame->head == q->head) { + pc = 6; + } else { + pc = 2; + } + break; + + case 6: + if (frame->head == frame->tail) { + pc = 7; + } else { + pc = 13; + } + break; + + case 7: + if (frame->next == NULL) { + bool dequeue_result = false; + data_type ref_result = ref_dequeue(frame->ref); + if (ref_result != EMPTY) { + printf("dequeue_result: %d, ref_result: %d\n", dequeue_result, + ref_result); + } + assert(ref_result == EMPTY); + pc = PC_DONE; + } else { + pc = 10; + } + break; + + case 10: + if (q->tail == frame->tail) { // Fake CAS. + q->tail = frame->next; + } + pc = 2; + break; + + case 13: + if (q->head == frame->head) { + q->head = frame->next; + cas_result = true; + } else { + cas_result = false; + } + if (cas_result) { + data_type result = frame->next->d; + data_type ref_result = ref_dequeue(frame->ref); + assert(result == ref_result); + pc = PC_DONE; + } else { + pc = 2; + } + break; + + default: + assert(false); + } + return pc; +} + +// Runs the operation associated with the given frame until reaching the next +// block. That is, the next statement accessing shared memory. +int step(base_frame* frame) { + assert(frame != NULL); + if (frame->derived_frame_type == DEQUEUE) { + dequeue_frame* derived_frame = (dequeue_frame*)frame->derived_frame; + assert(derived_frame != NULL); + return step_dequeue(derived_frame, frame->pc); + } else if (frame->derived_frame_type == ENQUEUE) { + enqueue_frame* derived_frame = (enqueue_frame*)frame->derived_frame; + assert(derived_frame != NULL); + return step_enqueue(derived_frame, frame->pc); + } else { + assert(false); + } +} + +int test_with_schedule(uint8_t* schedule, size_t len) { + queue test_queue; + init_queue(&test_queue); + ref_queue* ref = new_ref_queue(len); + base_frame frames[NUM_THREADS]; + for (int frame_idx = 0; frame_idx < NUM_THREADS; ++frame_idx) { + int derived_frame_type = (frame_idx % 2 == 0) ? ENQUEUE : DEQUEUE; + void* derived_frame = NULL; + if (derived_frame_type == DEQUEUE) { + // printf("idx: %d is dequeue\n", frame_idx); + derived_frame = make_dequeue_frame(&test_queue, ref); + } else { + // printf("idx: %d is enqueue\n", frame_idx); + int data_to_push = frame_idx + 1; + derived_frame = make_enqueue_frame(&test_queue, ref, data_to_push); + } + init_frame(&frames[frame_idx], derived_frame, derived_frame_type); + } + execute_schedule(schedule, len, frames, NUM_THREADS, CONTEXT_SWITCHES_BOUND); + return 0; +} diff --git a/sledge/test/linearizability-experiments/test_treiber_stack.c b/sledge/test/linearizability-experiments/test_treiber_stack.c new file mode 100644 index 000000000..dea60d200 --- /dev/null +++ b/sledge/test/linearizability-experiments/test_treiber_stack.c @@ -0,0 +1,214 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include +#include +#include + +#include "ref_stack.h" +#include "scheduler.h" +#include "treiber_stack.h" + +#define NUM_THREADS 3 +#define CONTEXT_SWITCHES_BOUND 1 +#define SCHEDULE_POINTS NUM_THREADS * 3 +#include "test_mains.h" + +#define REF_STACK_DEPTH SCHEDULE_POINTS +#define PUSH_NON_ATOMIC_COMPARE_BUG false +#define POP_NON_ATOMIC_COMPARE_BUG true + +typedef enum { PUSH, POP } frame_type; + +typedef struct { + stack* s; + ref_stack* ref; + data_type v; + node* x; + node* t; +} push_frame; + +typedef struct { + stack* s; + ref_stack* ref; + node* t; + node* tn; + data_type r; +} pop_frame; + +push_frame* make_push_frame(stack* s, ref_stack* ref, data_type v) { + push_frame* frame = malloc(sizeof(push_frame)); + frame->s = s; + frame->ref = ref; + frame->v = v; + return frame; +} + +pop_frame* make_pop_frame(stack* s, ref_stack* ref) { + pop_frame* frame = malloc(sizeof(pop_frame)); + frame->s = s; + frame->ref = ref; + return frame; +} + +int step_push(push_frame* frame, int pc) { + stack* s = frame->s; + switch (pc) { + case 0: + /* We filter this out, since this is the reference's precondition. */ + if (frame->ref->size == frame->ref->max_size) { + return PC_ABORT; + } + frame->x = malloc(sizeof(node)); + frame->x->d = frame->v; + frame->t = NULL; + pc = 1; + break; + + case 1: + frame->t = atomic_load(&s->top); + frame->x->n = frame->t; + pc = 2; + break; + + case 2: + if (PUSH_NON_ATOMIC_COMPARE_BUG) { + s->top = frame->x; + pc = PC_DONE; + ref_stack_push(frame->ref, frame->v); + } else { // Correct implementation. + if (!atomic_compare_exchange_weak(&s->top, &frame->t, frame->x)) { + pc = 1; + } else { + pc = PC_DONE; + ref_stack_push(frame->ref, frame->v); + } + } + int size = unsafe_size(s); + int ref_size = frame->ref->size; + // assert(size == ref_size); + break; + default: + assert(false); + } + return pc; +} + +int step_pop(pop_frame* frame, int pc) { + stack* s = frame->s; + switch (pc) { + case 0: + /* We filter this out, since this is the reference's precondition. */ + if (frame->ref->size == 0) { + return PC_ABORT; + } + frame->t = s->top; + if (frame->t == NULL) { + data_type ref_result = ref_stack_pop(frame->ref); + assert(ref_result == EMPTY); + pc = PC_DONE; + } else { + pc = 1; + } + break; + + case 1: + frame->tn = frame->t->n; + pc = 2; + break; + + case 2: + if (POP_NON_ATOMIC_COMPARE_BUG) { + s->top = frame->tn; + data_type r = frame->t->d; + data_type ref_result = ref_stack_pop(frame->ref); + assert(r == ref_result); + pc = PC_DONE; + } else { // Correct implementation + if (!atomic_compare_exchange_weak(&s->top, &frame->t, frame->tn)) { + pc = 0; + } else { + data_type r = frame->t->d; + data_type ref_result = ref_stack_pop(frame->ref); + assert(r == ref_result); + // free(frame->t); // Should we test for ABA? + pc = PC_DONE; + } + } + int size = unsafe_size(s); + int ref_size = frame->ref->size; + // assert(size == ref_size); + break; + default: + assert(false); + } + return pc; +} + +// Runs the operation associated with the given frame until reaching the next +// block. That is, the next statement accessing shared memory. +int step(base_frame* frame) { + assert(frame != NULL); + if (frame->derived_frame_type == POP) { + pop_frame* derived_frame = (pop_frame*)frame->derived_frame; + assert(derived_frame != NULL); + return step_pop(derived_frame, frame->pc); + } else { + push_frame* derived_frame = (push_frame*)frame->derived_frame; + if (derived_frame == NULL) { + } + assert(derived_frame != NULL); + return step_push(derived_frame, frame->pc); + } +} + +void print_test() { + stack test_stack; + init_stack(&test_stack); + print(&test_stack); + printf("\n"); + push(&test_stack, 1); + print(&test_stack); + printf("\n"); + push(&test_stack, 2); + print(&test_stack); + printf("\n"); + push(&test_stack, 3); + print(&test_stack); + printf("\n"); + assert(pop(&test_stack) == 3); + print(&test_stack); + printf("\n"); + assert(pop(&test_stack) == 2); + print(&test_stack); + printf("\n"); + assert(pop(&test_stack) == 1); + print(&test_stack); + printf("\n"); +} + +int test_with_schedule(uint8_t* schedule, size_t len) { + stack test_stack; + init_stack(&test_stack); + ref_stack* ref = new_ref_stack(len); + base_frame frames[NUM_THREADS]; + for (int frame_idx = 0; frame_idx < NUM_THREADS; ++frame_idx) { + int derived_frame_type = (frame_idx % 2 == 0) ? PUSH : POP; + void* derived_frame = NULL; + if (derived_frame_type == POP) { + // printf("adding pop frame\n"); + derived_frame = make_pop_frame(&test_stack, ref); + } else { + // printf("adding push frame\n"); + int data_to_push = frame_idx; + derived_frame = make_push_frame(&test_stack, ref, data_to_push); + } + init_frame(&frames[frame_idx], derived_frame, derived_frame_type); + } + execute_schedule(schedule, len, frames, NUM_THREADS, CONTEXT_SWITCHES_BOUND); + return 0; +} diff --git a/sledge/test/linearizability-experiments/treiber_stack.c b/sledge/test/linearizability-experiments/treiber_stack.c new file mode 100644 index 000000000..4e583f4ac --- /dev/null +++ b/sledge/test/linearizability-experiments/treiber_stack.c @@ -0,0 +1,63 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include "treiber_stack.h" +#include +#include + +void init_stack(stack* s) { s->top = NULL; } + +void push(stack* s, data_type v) { + /*L0:*/ node* new_node = malloc(sizeof(node)); + node* top_snapshot = NULL; + new_node->d = v; + do { + /*L1:*/ top_snapshot = atomic_load(&s->top); + new_node->n = top_snapshot; + } + /*L2:*/ + while (!atomic_compare_exchange_weak(&s->top, &top_snapshot, new_node)); +} + +data_type pop(stack* s) { + node* top_snapshot = NULL; + node* tn = NULL; + do { + /*L0:*/ top_snapshot = s->top; + if (top_snapshot == NULL) { + return EMPTY; + } + /*L1:*/ tn = top_snapshot->n; + } + /*L2:*/ + while (!atomic_compare_exchange_weak(&s->top, &top_snapshot, tn)); + data_type r = top_snapshot->d; + return r; +} + +int unsafe_size(stack* s) { + int result = 0; + node* curr = s->top; + while (curr != NULL) { + ++result; + curr = curr->n; + } + return result; +} + +void print(stack* s) { + node* curr = s->top; + printf("["); + while (curr != NULL) { + printf("%d", curr->d); + if (curr->n != NULL) { + printf(" "); + } + curr = curr->n; + } + printf("]"); +} diff --git a/sledge/test/linearizability-experiments/treiber_stack.h b/sledge/test/linearizability-experiments/treiber_stack.h new file mode 100644 index 000000000..c970e0f97 --- /dev/null +++ b/sledge/test/linearizability-experiments/treiber_stack.h @@ -0,0 +1,38 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#ifndef TREIBER_STACK +#define TREIBER_STACK + +#include +#include + +/** + * Treiber, R.K.: Systems programming: Coping with parallelism. Technical Report + * RJ 5118, IBM Almaden Research Center (1986) + */ + +typedef int data_type; +#define EMPTY -1 + +typedef struct node_t { + data_type d; + struct node_t* n; +} node; + +typedef struct stack_t { + _Atomic(node*) top; +} stack; + +void init_stack(stack* s); +void push(stack* s, data_type v); +data_type pop(stack* s); + +int unsafe_size(stack* s); +void print(stack* s); + +#endif