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 <stdio.h>
+#include <stdlib.h>
+
+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 <stdbool.h>
+
+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 <assert.h>
+#include <stdlib.h>
+
+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 <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+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 <stdbool.h>
+
+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 <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+#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 <klee.h>
+
+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 <assert.h>
+#include <stdatomic.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+#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 <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+#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 <stdio.h>
+#include <stdlib.h>
+
+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 <stdatomic.h>
+#include <stdbool.h>
+
+/**
+ * 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