diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/LICENSE
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/LICENSE	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,30 @@
+Copyright (c) 2014-2016, Marco Elver
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+ * Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the
+   distribution.
+
+ * Neither the name of the software nor the names of its contributors
+   may be used to endorse or promote products derived from this
+   software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/README.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/README.rst	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,59 @@
+======
+mc2lib
+======
+
+.. image:: https://travis-ci.org/melver/mc2lib.svg?branch=master
+    :target: https://travis-ci.org/melver/mc2lib
+
+A memory consistency model checking library implemented in C++11. This library
+provides the building blocks for the `McVerSi
+<http://ac.marcoelver.com/research/mcversi>`_ framework [1]_.
+
+The McVerSi guest workload can be found in `<contrib/mcversi>`_.
+
+Usage
+=====
+
+The library is header-only.
+
+API documentation can be found `here
+<http://ac.marcoelver.com/ext/apidoc/mc2lib>`_.
+
+The provided `<Makefile>`_ is for unit testing and static analysis.
+
+Citation
+========
+
+If you use this library or the McVerSi framework in your work, we would
+appreciate if you cite the McVerSi paper:
+
+.. code-block::
+
+    @inproceedings{ElverN2016,
+      author    = {Marco Elver and Vijay Nagarajan},
+      title     = {{McVerSi}: {A} {T}est {G}eneration {F}ramework for {F}ast
+                   {M}emory {C}onsistency {V}erification in {S}imulation},
+      booktitle = {IEEE International Symposium on
+                   High Performance Computer Architecture (HPCA)},
+      month     = mar,
+      year      = {2016},
+      venue     = {Barcelona, Spain}
+    }
+
+Extensions
+==========
+
+Notable extensions that have been added after publication of the McVerSi paper:
+
+* Support for synonym sets of virtual addresses mapping to same physical
+  address -- see `EvtStateCats <include/mc2lib/codegen/cats.hpp>`_ and
+  `guest_workload <contrib/mcversi/guest_workload.c>`_.
+
+References
+==========
+
+.. [1] Marco Elver and Vijay Nagarajan. `McVerSi: A Test Generation Framework
+       for Fast Memory Consistency Verification in Simulation
+       <http://ac.marcoelver.com/res/hpca2016-mcversi.pdf>`_. In IEEE
+       International Symposium on High Performance Computer Architecture
+       (HPCA). Barcelona, Spain, March 2016.
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/SConscript
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/SConscript	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,6 @@
+# -*- mode:python -*-
+
+Import('main')
+main.Prepend(CPPPATH=Dir('./include'))
+
+# vim: set ft=python :
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/_UPSTREAM
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/_UPSTREAM	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,1 @@
+https://github.com/melver/mc2lib
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/contrib/mcversi/README.rst
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/contrib/mcversi/README.rst	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,5 @@
+McVerSi Guest Workload
+======================
+
+This is the guest workload as used in the McVerSi paper, with modification to
+enable support on more architectures.
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/contrib/mcversi/guest_workload.c
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/contrib/mcversi/guest_workload.c	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,402 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef _GNU_SOURCE
+#  define _GNU_SOURCE
+#endif
+
+#include <assert.h>
+#include <errno.h>
+#include <pthread.h>
+#include <stdbool.h>
+#include <stddef.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <sys/mman.h>
+#include <sys/shm.h>
+
+#include "host_support.h"
+
+#ifndef MAX_CODE_SIZE
+#  define MAX_CODE_SIZE (4096*16)
+#endif
+
+#ifndef MAX_THREADS
+#  define MAX_THREADS 64
+#endif
+
+static size_t num_threads = 0;
+
+static char *test_mem = NULL;
+static size_t test_mem_bytes = 0;
+static size_t test_mem_stride = 0;
+
+static pthread_barrier_t barrier;
+static pthread_t thread_main_id;
+
+static inline void
+reset_test_mem(void **used_addrs, size_t len)
+{
+#if !HOST_ZERO_TEST_MEM
+	if (used_addrs != NULL) {
+		// NULL marks end of list.
+		for (size_t i = 0; i < len && used_addrs[i]; ++i) {
+			// Mask stride due encoding (see mc2lib RandomFactory)
+			memset(used_addrs[i], 0, (test_mem_stride & 0xffff));
+		}
+	} else {
+		memset(test_mem, 0, test_mem_bytes);
+	}
+
+	full_memory_barrier();
+#endif
+
+	if (used_addrs != NULL) {
+		// NULL marks end of list.
+		for (size_t i = 0; i < len && used_addrs[i]; ++i) {
+			flush_cache_line(used_addrs[i]);
+		}
+	} else {
+#if defined(CACHELINE_SIZE) && CACHELINE_SIZE != 0
+		// Fallback
+		for (size_t i = 0; i < test_mem_bytes; i += CACHELINE_SIZE) {
+			flush_cache_line(&test_mem[i]);
+		}
+#endif
+	}
+
+	full_memory_barrier();
+}
+
+static inline void
+barrier_wait_pthread(void)
+{
+	int rc = pthread_barrier_wait(&barrier);
+	assert(rc == 0 || rc == PTHREAD_BARRIER_SERIAL_THREAD);
+}
+
+void*
+thread_func(void *arg)
+{
+	const size_t test_iterations = (size_t) arg;
+	const pthread_t thread_self = pthread_self();
+
+	void *code = mmap(NULL, MAX_CODE_SIZE,
+	                  PROT_READ | PROT_WRITE | PROT_EXEC,
+	                  MAP_ANONYMOUS | MAP_PRIVATE,
+	                  -1, 0);
+	assert(code != NULL);
+	memset(code, 0, MAX_CODE_SIZE);
+
+	void (*thread_test)() = GET_CALLABLE_THREAD(code);
+
+	void **used_addrs = NULL;
+#if MAX_USED_ADDRS_SIZE
+	if (thread_self == thread_main_id) {
+		used_addrs = (void**)malloc(MAX_USED_ADDRS_SIZE);
+		assert(used_addrs != NULL);
+		memset(used_addrs, 0, MAX_USED_ADDRS_SIZE);
+	}
+#endif
+
+	barrier_wait_pthread();
+
+	while (1) {
+		host_make_test_thread(code, MAX_CODE_SIZE);
+		full_memory_barrier();
+
+		for (size_t i = 0; i < test_iterations; ++i) {
+			barrier_wait_precise(num_threads);
+
+			full_memory_barrier();
+
+			thread_test();
+
+			full_memory_barrier();
+
+			barrier_wait_coarse(num_threads);
+
+			if (i + 1 < test_iterations
+			    && thread_self == thread_main_id) {
+				host_verify_reset_conflict(used_addrs,
+				                           MAX_USED_ADDRS_SIZE);
+				reset_test_mem(used_addrs, MAX_USED_ADDRS_SIZE);
+			}
+		}
+
+		if (thread_self == thread_main_id) {
+			host_verify_reset_all(used_addrs, MAX_USED_ADDRS_SIZE);
+			reset_test_mem(used_addrs, MAX_USED_ADDRS_SIZE);
+		}
+
+		barrier_wait_coarse(num_threads);
+	}
+
+#if MAX_USED_ADDRS_SIZE
+	if (thread_self == thread_main_id) {
+		free(used_addrs);
+	}
+#endif
+
+	munmap(code, MAX_CODE_SIZE);
+	return NULL;
+}
+
+static void
+setaffinity_thread(size_t pid, pthread_t thread)
+{
+	cpu_set_t cpuset;
+	CPU_ZERO(&cpuset);
+	CPU_SET(pid, &cpuset);
+	int rc = pthread_setaffinity_np(thread, sizeof(cpu_set_t), &cpuset);
+	assert(!rc);
+}
+
+static void
+setaffinity_attr(size_t pid, pthread_attr_t *attr)
+{
+	cpu_set_t cpuset;
+	CPU_ZERO(&cpuset);
+	CPU_SET(pid, &cpuset);
+	int rc = pthread_attr_setaffinity_np(attr, sizeof(cpu_set_t), &cpuset);
+	assert(!rc);
+}
+
+static void
+spawn_threads(size_t test_iterations)
+{
+	assert(MAX_THREADS <= CPU_SETSIZE);
+	assert(num_threads <= MAX_THREADS);
+	assert(num_threads > 0);
+
+	// Reuse main thread.
+	pthread_t thread_ids[MAX_THREADS - 1];
+	pthread_attr_t attr;
+
+	int rc = pthread_barrier_init(&barrier, NULL, num_threads);
+	assert(!rc);
+
+	thread_main_id = pthread_self();
+	setaffinity_thread(0, thread_main_id);
+
+	printf("Spawning threads ...\n");
+
+	for (size_t i = 0; i < num_threads - 1; ++i) {
+		rc = pthread_attr_init(&attr);
+		assert(!rc);
+
+		setaffinity_attr(i + 1, &attr);
+
+		pthread_attr_getinheritsched(&attr, &rc);
+		assert(rc == PTHREAD_INHERIT_SCHED);
+
+		rc = pthread_create(&thread_ids[i], &attr, thread_func,
+				    (void*) test_iterations);
+		assert(!rc);
+
+		rc = pthread_attr_destroy(&attr);
+		assert(!rc);
+	}
+
+	roi_begin();
+
+	printf("Running tests ...\n");
+	thread_func((void*) test_iterations);
+
+	for (size_t i = 0; i < num_threads - 1; ++i) {
+		pthread_join(thread_ids[i], NULL);
+	}
+
+	printf("All tests complete.\n");
+
+	roi_end();
+
+	pthread_barrier_destroy(&barrier);
+}
+
+static void
+setup_sched(void)
+{
+	const char *env_policy = getenv("MC2_SCHED_POLICY");
+	if (!env_policy) {
+		// Do nothing.
+		return;
+	}
+
+	// defaults
+	int policy = SCHED_FIFO;
+	struct sched_param sp = {
+		.sched_priority = sched_get_priority_max(policy) - 20
+	};
+
+	if (env_policy[0] != '\0') {
+		if (!strcmp(env_policy, "SCHED_RR")) {
+			policy = SCHED_RR;
+		} else if (!strcmp(env_policy, "SCHED_FIFO")) {
+			policy = SCHED_FIFO;
+		} else {
+			perror("Invalid MC2_SCHED_POLICY!");
+			exit(1);
+		}
+	}
+
+	const char *env_prio = getenv("MC2_SCHED_PRIO");
+	if (env_prio) {
+		sp.sched_priority = atoi(env_prio);
+		assert(sp.sched_priority != 0);
+	}
+
+	if (sched_setscheduler(0, policy, &sp) == -1) {
+		perror("sched_setscheduler failed!");
+		exit(1);
+	} else {
+		printf("Set RT scheduler: %d @ %d\n", policy,
+		       sp.sched_priority);
+	}
+}
+
+static void
+usage(const char *progname)
+{
+	printf("Usage: %s <num-threads> <test-iterations> <test-mem-bytes> "
+	       "<test-mem-stride> [<test-mem-addr> [<synonym-count>]]\n",
+	       progname);
+
+	exit(42);
+}
+
+int
+main(int argc, char *argv[])
+{
+	if (argc <= 4) usage(argv[0]);
+
+	host_init();
+	setup_sched();
+
+	// Get number of threads
+	num_threads = strtoull(argv[1], NULL, 0);
+	if (!num_threads) usage(argv[0]);
+	printf("Threads: %zu\n", num_threads);
+
+	// Get iterations per test
+	size_t test_iterations = strtoull(argv[2], NULL, 0);
+	if (!test_iterations) usage(argv[0]);
+	printf("Test iterations: %zu\n", test_iterations);
+
+	// Initialize test memory
+	test_mem_bytes = strtoull(argv[3], NULL, 0);
+	if (!test_mem_bytes) usage(argv[0]);
+
+	test_mem_stride = strtoull(argv[4], NULL, 0);
+	if (!test_mem_stride) usage(argv[0]);
+
+	assert(test_mem == NULL);
+	size_t synonym_count = 0;
+	if (argc > 5) {
+		// Optionally set test-memory base address.
+		test_mem = (char*)strtoull(argv[5], NULL, 0);
+
+		if (test_mem && argc > 6) {
+			synonym_count = strtoull(argv[6], NULL, 0);
+		}
+	}
+
+	int shm_id;
+	if (synonym_count) {
+		shm_id = shmget(IPC_PRIVATE, test_mem_bytes,
+				IPC_CREAT | IPC_EXCL | S_IRUSR | S_IWUSR);
+		assert(shm_id != -1);
+		test_mem = (char*)shmat(shm_id, test_mem, 0);
+
+		for (size_t i = 0; i < synonym_count; ++i) {
+			char* synonym_mem = (char*)shmat(shm_id,
+					test_mem + (test_mem_bytes * (i+1)), 0);
+			assert(synonym_mem != (char*)-1);
+			printf("Test memory synonym @ 0x%tx\n",
+			       (ptrdiff_t)synonym_mem);
+		}
+	} else if (test_mem) {
+		test_mem = (char*)mmap(test_mem, test_mem_bytes,
+				       PROT_READ | PROT_WRITE,
+				       MAP_ANONYMOUS | MAP_PRIVATE | MAP_FIXED,
+				       0, 0);
+		assert(test_mem != MAP_FAILED);
+	} else {
+		test_mem = (char*)malloc(test_mem_bytes);
+		assert(test_mem != NULL);
+	}
+
+	printf("Test memory: %zu bytes (stride=0x%zx) @ 0x%tx\n",
+	       test_mem_bytes, test_mem_stride, (ptrdiff_t)test_mem);
+
+	// Let host know of memory range
+#if HOST_ZERO_TEST_MEM
+	// Need to access memory once if host wants to access page-table
+	// entries.
+#  if defined(CACHELINE_SIZE) && CACHELINE_SIZE != 0
+	for (size_t i = 0; i < test_mem_bytes; i += CACHELINE_SIZE) {
+		test_mem[i] = 0x42;
+	}
+#  else
+	memset(test_mem, 0, test_mem_bytes);
+#  endif
+	full_memory_barrier();
+#endif
+
+	host_mark_test_mem_range(test_mem,
+			(test_mem + (test_mem_bytes * (synonym_count+1)) - 1),
+			test_mem_stride,
+			(synonym_count ? (void*)(test_mem_bytes - 1) : NULL));
+
+	reset_test_mem(NULL, 0);
+
+	spawn_threads(test_iterations);
+
+	// cleanup
+	if (synonym_count) {
+		shmdt(test_mem);
+		for (size_t i = 0; i < synonym_count; ++i) {
+			char* synonym_mem = test_mem + (test_mem_bytes * (i+1));
+			shmdt(synonym_mem);
+		}
+		shmctl(shm_id, IPC_RMID, 0);
+	} else if (argc > 5 && strtoull(argv[5], NULL, 0)) {
+		munmap(test_mem, test_mem_bytes);
+	} else {
+		free(test_mem);
+	}
+
+	return EXIT_SUCCESS;
+}
+
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/contrib/mcversi/host_support.h
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/contrib/mcversi/host_support.h	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,1 @@
+m5_host_support.h
\ No newline at end of file
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/contrib/mcversi/m5_host_support.h
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/contrib/mcversi/m5_host_support.h	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,229 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef HOST_SUPPORT_H_
+#define HOST_SUPPORT_H_
+
+#include <errno.h>
+#include <fcntl.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <sys/mman.h>
+#include <sys/stat.h>
+
+#include "m5op.h"
+
+#ifndef CACHELINE_SIZE
+#  define CACHELINE_SIZE 64
+#endif
+
+#ifndef HOST_ZERO_TEST_MEM
+// 0 -- Host does not zero test-memory.
+// 1 -- Host zeroes test-memory in *reset* and mark_test_mem_range functions.
+#  define HOST_ZERO_TEST_MEM 1
+#endif
+
+#ifndef MAX_USED_ADDRS_SIZE
+// >0 -- Host must provide used addresses with *reset* functions.
+#  define MAX_USED_ADDRS_SIZE (4096*8)
+#endif
+
+#ifndef BARRIER_USE_QUIESCE
+// This is a performance optimization and (with the evaluated version of Gem5
+// used for McVerSi) speeds up execution (when using barrier_wait_coarse)
+// significantly with larger number of processors.
+//
+// With latest Gem5 and current async barrier implementation, using quiesce
+// seems to cause lock up, regardless of ISA; disable by default.
+#  define BARRIER_USE_QUIESCE 0
+#endif
+
+#ifdef M5OP_ADDR
+void *m5_mem = NULL;
+#endif
+
+#if defined(__x86_64__)
+
+inline void
+full_memory_barrier(void)
+{
+	__asm__ __volatile__ (
+			"mfence\n\t"
+			"mov $0, %%eax\n\t"
+			"cpuid\n\t" ::: "memory", "cc",
+			"rax", "rbx", "rcx", "rdx");
+}
+
+inline void
+flush_cache_line(volatile void *addr)
+{
+	// Note that, not all protocols support this; in the McVerSi paper, we
+	// implemented support for clflush for the protocols we used.
+	__asm__ __volatile__ ("clflush (%0)" :: "r" (addr) : "memory");
+}
+
+inline uint64_t
+host_make_test_thread(void *code, uint64_t len)
+{
+	len = m5_make_test_thread(code, len);
+	for (int i = 0; i < 0x42; ++i) {
+		// It seems that Gem5's O3 CPU still prefetches instructions somehow;
+		// work-around by not giving it the chance to prefetch the previous
+		// test. My assumption is, that if we had actual self-modifying code
+		// (and not the host writing the instructions to memory), it should not
+		// have this problem.
+		full_memory_barrier();
+	}
+	return len;
+}
+
+#define GET_CALLABLE_THREAD(code) ((void (*)()) code)
+
+#elif defined(__arm__)
+
+inline void
+full_memory_barrier(void)
+{
+	__asm__ __volatile__ (
+			"dsb; isb" :::
+			"memory", "cc",
+			// Clobber registers used by test generator.
+			"r0", "r1", "r2", "r3", "r4", "r5", "r6", "r7");
+}
+
+inline void
+flush_cache_line(volatile void *addr)
+{
+	// TODO: Implement me!
+}
+
+inline uint64_t
+host_make_test_thread(void *code, uint64_t len)
+{
+	len = m5_make_test_thread(code, len);
+	__clear_cache(code, code + len);
+	return len;
+}
+
+// Thumb
+#define GET_CALLABLE_THREAD(code) ((void (*)()) ((ptrdiff_t)code | 1))
+
+#else
+#  error "Unsupported architecture!"
+#endif
+
+#define host_mark_test_mem_range m5_mark_test_mem_range
+
+inline void
+host_verify_reset_conflict(void **used_addrs, uint64_t len)
+{
+	while(!m5_verify_reset_conflict(used_addrs, len));
+}
+
+inline void
+host_verify_reset_all(void **used_addrs, uint64_t len)
+{
+	while(!m5_verify_reset_all(used_addrs, len));
+}
+
+inline void
+barrier_wait_precise(uint64_t nt)
+{
+	full_memory_barrier();
+
+#if BARRIER_USE_QUIESCE
+	while(m5_barrier_async(nt, 1));
+
+	full_memory_barrier();
+#endif
+
+	while(m5_barrier_async(nt, 0));
+
+	full_memory_barrier();
+}
+
+inline void
+barrier_wait_coarse(uint64_t nt)
+{
+#if BARRIER_USE_QUIESCE
+	full_memory_barrier();
+
+	while(m5_barrier_async(nt, 1));
+
+	full_memory_barrier();
+#else
+	barrier_wait_precise(nt);
+#endif
+}
+
+#ifdef M5OP_ADDR
+inline void
+map_m5_mem(void)
+{
+    int fd;
+
+    fd = open("/dev/mem", O_RDWR | O_SYNC);
+    if (fd == -1) {
+        perror("Cannot open /dev/mem");
+        exit(1);
+    }
+
+    m5_mem = mmap(NULL, 0x10000, PROT_READ | PROT_WRITE, MAP_SHARED, fd, M5OP_ADDR);
+    if (!m5_mem) {
+        perror("Cannot mmap /dev/mem");
+        exit(1);
+    }
+}
+#endif
+
+inline void
+host_init(void)
+{
+#ifdef M5OP_ADDR
+	map_m5_mem();
+#endif
+}
+
+inline void
+roi_begin(void)
+{
+	m5_dumpreset_stats(0, 0);
+}
+
+inline void
+roi_end(void)
+{
+	m5_fail(0, 42);
+}
+
+#endif /* HOST_SUPPORT_H_ */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/contrib/mcversi/run-10-8KB-1synonym.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/contrib/mcversi/run-10-8KB-1synonym.sh	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,9 @@
+#!/bin/sh
+#
+# This code is licensed under the BSD 3-Clause license. See the LICENSE file in
+# the project root for license terms.
+#
+# 8KB configuration with virtual address synonyms (2 virtual addresses per 1
+# physical).
+
+/mcversi/guest_workload $(nproc) 10 0x1000000 0x09140010 0x100000000 1
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/contrib/mcversi/run-10-8KB.sh
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/contrib/mcversi/run-10-8KB.sh	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,25 @@
+#!/bin/sh
+#
+# This code is licensed under the BSD 3-Clause license. See the LICENSE file in
+# the project root for license terms.
+#
+# 8KB configuration from McVerSi paper.
+
+# Optionally set this to one of:
+# - SCHED_RR
+# - SCHED_FIFO
+export MC2_SCHED_POLICY=
+
+# Run with as many threads as reported by nproc; 10 iterations per test;
+# allocate 15729152 bytes of memory, with
+#
+# - stride = (0x09140010 & ((1 << 16) - 1)) = 16 bytes;
+# - chunks of size (1 << ((0x09140010 & (0xff << 24)) >> 24)) = 512 bytes;
+# - and valid chunk base addresses offset by multiples of
+#   (1 << ((0x09140010 & (0xff << 16)) >> 16)) = 1048576 bytes from first base address.
+#
+# and first base address of memory is 0x100000000 (optionally set, but used
+# here to force 64bit address instructions by the code generator). This
+# effectively uses 8KB of memory distributed across 16MB.
+
+/mcversi/guest_workload $(nproc) 10 0xf00200 0x09140010 0x100000000
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/codegen/cats.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/codegen/cats.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,278 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_CODEGEN_CATS_HPP_
+#define MC2LIB_CODEGEN_CATS_HPP_
+
+#include <cassert>
+#include <cstddef>
+#include <limits>
+#include <sstream>
+#include <stdexcept>
+#include <unordered_map>
+
+#include "../memconsistency/cats.hpp"
+#include "compiler.hpp"
+
+namespace mc2lib {
+
+namespace codegen {
+
+// Workaround for Wtype-limits warning.
+template <class T1, class T2>
+constexpr bool lt__(T1 a, T2 b) {
+  return a < b;
+}
+
+/**
+ * @brief Interface to memconsistency::cats data structures.
+ *
+ * This class serves as a helper to interface with data structures in
+ * memconsistency::cats. Its primary function is the creation of new events by
+ * Operations.
+ *
+ * Furthermore, as this is the interface to the consistency model descriptions
+ * and checker, we can encode efficient support for virtual address synonyms
+ * here by transforming the address used to construct events (see
+ * EvtStateCats::set_addr_mask). As described in [1], if we are working at the
+ * virtual address level, we are checking VAMC (Virtual Address
+ * Memory Consistency). Here we only consider the problem of synonym sets of
+ * virtual addresses mapping to the same physical address, and add simple
+ * support for it.
+ *
+ * [1] <a href="http://dx.doi.org/10.1145/1736020.1736057">
+ *      Bogdan F. Romanescu, Alvin R. Lebeck, Daniel J. Sorin, "Specifying and
+ *      dynamically verifying address translation-aware memory consistency",
+ *      2010.</a>
+ */
+class EvtStateCats {
+ public:
+  // 1 Op can at most emit 2 write Events
+  static constexpr std::size_t kMaxOpSize = sizeof(types::WriteID) * 2;
+  static constexpr std::size_t kMaxOpEvents =
+      kMaxOpSize / sizeof(types::WriteID);
+
+  static constexpr types::Poi kMinOther = static_cast<types::Poi>(1)
+                                          << (sizeof(types::Poi) * 8 - 1);
+  static constexpr types::Poi kMaxOther =
+      std::numeric_limits<types::Poi>::max() - (kMaxOpEvents - 1);
+
+  static constexpr types::WriteID kInitWrite =
+      std::numeric_limits<types::WriteID>::min();
+  static constexpr types::WriteID kMinWrite = kInitWrite + 1;
+
+  static constexpr types::WriteID kMaxWrite =
+      (lt__(std::numeric_limits<types::WriteID>::max(), kMinOther)
+           ? std::numeric_limits<types::WriteID>::max()
+           : kMinOther - 1) -
+      (kMaxOpEvents - 1);
+
+  static_assert(kMinOther > kMaxWrite, "Invalid read/write ID limits!");
+
+  explicit EvtStateCats(mc::cats::ExecWitness *ew, mc::cats::Architecture *arch)
+      : ew_(ew), arch_(arch), addr_mask_(~0) {}
+
+  void Reset() {
+    last_write_id_ = kMinWrite - 1;
+    last_other_id = kMinOther - 1;
+
+    writes_.clear();
+    ew_->Clear();
+    arch_->Clear();
+  }
+
+  bool Exhausted() const {
+    return last_write_id_ >= kMaxWrite || last_other_id >= kMaxOther;
+  }
+
+  template <std::size_t max_size_bytes, class Func>
+  EventPtrs<max_size_bytes> MakeEvent(types::Pid pid, mc::Event::Type type,
+                                      std::size_t size, Func mkevt) {
+    static_assert(max_size_bytes <= kMaxOpSize, "Invalid size!");
+    static_assert(sizeof(types::WriteID) <= max_size_bytes, "Invalid size!");
+    static_assert(max_size_bytes % sizeof(types::WriteID) == 0,
+                  "Invalid size!");
+    assert(size <= max_size_bytes);
+    assert(sizeof(types::WriteID) <= size);
+    assert(size % sizeof(types::WriteID) == 0);
+
+    // Initialize to avoid uninitialized warning with some older compilers.
+    EventPtrs<max_size_bytes> result{{nullptr}};
+
+    for (std::size_t i = 0; i < size / sizeof(types::WriteID); ++i) {
+      result[i] = mkevt(i * sizeof(types::WriteID));
+    }
+
+    return result;
+  }
+
+  mc::Event MakeOther(types::Pid pid, mc::Event::Type type, types::Addr addr) {
+    assert(!Exhausted());
+    addr &= addr_mask_;
+    return mc::Event(type, addr, mc::Iiid(pid, ++last_other_id));
+  }
+
+  template <std::size_t max_size_bytes = sizeof(types::WriteID)>
+  EventPtrs<max_size_bytes> MakeRead(types::Pid pid, mc::Event::Type type,
+                                     types::Addr addr,
+                                     std::size_t size = max_size_bytes) {
+    assert(!Exhausted());
+    addr &= addr_mask_;
+    ++last_other_id;
+    return MakeEvent<max_size_bytes>(pid, type, size, [&](types::Addr offset) {
+      const mc::Event event =
+          mc::Event(type, addr + offset, mc::Iiid(pid, last_other_id));
+
+      return &ew_->events.Insert(event, true);
+    });
+  }
+
+  template <std::size_t max_size_bytes = sizeof(types::WriteID)>
+  EventPtrs<max_size_bytes> MakeWrite(types::Pid pid, mc::Event::Type type,
+                                      types::Addr addr, types::WriteID *data,
+                                      std::size_t size = max_size_bytes) {
+    assert(!Exhausted());
+    addr &= addr_mask_;
+    ++last_write_id_;
+    return MakeEvent<max_size_bytes>(pid, type, size, [&](types::Addr offset) {
+      const types::WriteID write_id = last_write_id_;
+
+      const mc::Event event =
+          mc::Event(type, addr + offset, mc::Iiid(pid, write_id));
+
+      *(data + offset) = write_id;
+      return (writes_[write_id] = &ew_->events.Insert(event, true));
+    });
+  }
+
+  template <std::size_t max_size_bytes = sizeof(types::WriteID)>
+  EventPtrs<max_size_bytes> GetWrite(const EventPtrs<max_size_bytes> &after,
+                                     types::Addr addr,
+                                     const types::WriteID *from_id,
+                                     std::size_t size = max_size_bytes) {
+    static_assert(max_size_bytes <= kMaxOpSize, "Invalid size!");
+    static_assert(sizeof(types::WriteID) <= max_size_bytes, "Invalid size!");
+    static_assert(max_size_bytes % sizeof(types::WriteID) == 0,
+                  "Invalid size!");
+    assert(size <= max_size_bytes);
+    assert(sizeof(types::WriteID) <= size);
+    assert(size % sizeof(types::WriteID) == 0);
+    addr &= addr_mask_;
+
+    EventPtrs<max_size_bytes> result;
+    result.fill(nullptr);  // init
+
+    for (std::size_t i = 0; i < size / sizeof(types::WriteID); ++i) {
+      WriteID_EventPtr::const_iterator write;
+
+      const bool valid = from_id[i] != kInitWrite &&
+                         (write = writes_.find(from_id[i])) != writes_.end() &&
+                         write->second->addr == addr &&
+                         write->second->iiid != after[i]->iiid;
+      if (valid) {
+        result[i] = write->second;
+      } else {
+        if (from_id[i] != kInitWrite) {
+          // While the checker works even if memory is not 0'ed out
+          // completely, as the chances of reading a write-id from a
+          // previous test that has already been used in this test is
+          // low and doesn't necessarily cause a false positive, it is
+          // recommended that memory is 0'ed out for every new test.
+          //
+          // This does also provides limited checking for single-copy
+          // atomicity violations where sizeof(WriteID) > 1.
+
+          std::ostringstream oss;
+          oss << __func__ << ": Invalid write!"
+              << " A=" << std::hex << addr << " S=" << size;
+
+          if (write != writes_.end()) {
+            oss << ((write->second->addr != addr) ? " (addr mismatch)" : "")
+                << ((write->second->iiid == after[i]->iiid) ? " (same iiid)"
+                                                            : "");
+          }
+
+          throw std::logic_error(oss.str());
+        }
+
+        auto initial = mc::Event(mc::Event::kWrite, addr, mc::Iiid(-1, addr));
+        result[i] = &ew_->events.Insert(initial);
+      }
+
+      addr += sizeof(types::WriteID);
+    }
+
+    return result;
+  }
+
+  mc::cats::ExecWitness *ew() { return ew_; }
+
+  const mc::cats::ExecWitness *ew() const { return ew_; }
+
+  mc::cats::Architecture *arch() { return arch_; }
+
+  const mc::cats::Architecture *arch() const { return arch_; }
+
+  /**
+   * When using virtual addresses, this can be used to mask test memory
+   * addresses, s.t. synonyms map to the same address used by the checker.
+   * Although we could modify the checker to permit sets of addresses, this
+   * would be much more expensive in terms of storage and hash-map lookup by
+   * the checker. Assumes that synonym range start addresses are multiples of
+   * 2**n (the size of memory).
+   */
+  void set_addr_mask(types::Addr val) { addr_mask_ = val; }
+
+  types::Addr addr_mask() const { return addr_mask_; }
+
+ private:
+  typedef std::unordered_map<types::WriteID, const mc::Event *>
+      WriteID_EventPtr;
+
+  mc::cats::ExecWitness *ew_;
+  mc::cats::Architecture *arch_;
+
+  WriteID_EventPtr writes_;
+
+  types::WriteID last_write_id_;
+  types::Poi last_other_id;
+
+  types::Addr addr_mask_;
+};
+
+}  // namespace codegen
+}  // namespace mc2lib
+
+#endif /* MC2LIB_CODEGEN_CATS_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/codegen/compiler.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/codegen/compiler.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,518 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_CODEGEN_COMPILER_HPP_
+#define MC2LIB_CODEGEN_COMPILER_HPP_
+
+#include <array>
+#include <cassert>
+#include <cstddef>
+#include <functional>
+#include <map>
+#include <memory>
+#include <stdexcept>
+#include <unordered_map>
+#include <unordered_set>
+#include <utility>
+#include <vector>
+
+#include "../memconsistency/eventsets.hpp"
+#include "../types.hpp"
+
+namespace mc2lib {
+
+/**
+ * @namespace mc2lib::codegen
+ * @brief Code generation for memory consistency verification.
+ */
+namespace codegen {
+
+namespace mc = memconsistency;
+
+template <std::size_t max_size_bytes>
+using EventPtrs =
+    std::array<const mc::Event *, max_size_bytes / sizeof(types::WriteID)>;
+
+template <class... Ts>
+inline auto MakeEventPtrs(const mc::Event *e1, Ts... en)
+    -> EventPtrs<(1 + sizeof...(Ts)) * sizeof(types::WriteID)> {
+  EventPtrs<(1 + sizeof...(Ts)) * sizeof(types::WriteID)> es{{e1, en...}};
+  return es;
+}
+
+/**
+ * Baseclass for Operation implementations.
+ */
+template <class Backend, class EvtStateT>
+class Op {
+ public:
+  typedef EvtStateT EvtState;
+
+  // Types
+  typedef std::shared_ptr<Op> Ptr;
+  typedef std::vector<Ptr> Thread;
+  typedef typename Thread::const_iterator ThreadIt;
+  typedef std::unordered_map<types::Pid, Thread> Threads;
+  typedef std::vector<std::pair<ThreadIt, ThreadIt>> ThreadItStack;
+
+  // Read-only thread types: new Ops can access previous Ops.
+  typedef std::vector<const Op *> ThreadConst;
+  typedef typename ThreadConst::const_iterator ThreadConstIt;
+
+  // Callback type: optionally, previous Ops get called back with new Ops.
+  // E.g. for lazily constructing control flow graph with random branches.
+  typedef std::function<std::size_t(Op *, types::InstPtr, Backend *, EvtState *,
+                                    void *, std::size_t)> Callback;
+  typedef std::vector<Callback> CallbackStack;
+
+  template <class T>
+  friend Threads ExtractThreads(T *container) {
+    Threads result;
+    std::unordered_set<Op *> used;
+
+    for (auto &op : (*container)) {
+      assert(op != nullptr);
+
+      if (used.insert(op.get()).second) {
+        // Using same instance of Op multiple times is not permitted.
+        op = op->Clone();
+      }
+
+      result[op->pid()].emplace_back(op);
+    }
+
+    return result;
+  }
+
+  friend std::size_t threads_size(const Threads &threads) {
+    std::size_t result = 0;
+
+    for (const auto &thread : threads) {
+      result += thread.second.size();
+    }
+
+    return result;
+  }
+
+ public:
+  explicit Op(types::Pid pid) : pid_(pid) {}
+
+  virtual ~Op() {}
+
+  virtual void AdvanceThread(ThreadItStack *it_stack) const {
+    ++(it_stack->back().first);
+  }
+
+  /**
+   * Clone the instance.
+   */
+  virtual Ptr Clone() const = 0;
+
+  /**
+   * Provide Reset, as emit functions may modify the state of an Op to store
+   * information to map instructions to events.
+   */
+  virtual void Reset() = 0;
+
+  /**
+   * Prepares the operation for emit; common emit code.
+   *
+   * @param[in,out] evts Pointer to EvtState instance of calling Compiler.
+   *
+   * @return true if can emit; false otherwise.
+   */
+  virtual bool EnableEmit(EvtState *evts) = 0;
+
+  /**
+   * Generate static program-order relation.
+   *
+   * @param before Pointer to last Op; nullptr if none exists.
+   * @param[in,out] evts Pointer to EvtState instance maintained by
+   *                     Compiler.
+   */
+  virtual void InsertPo(ThreadConstIt before, EvtState *evts) = 0;
+
+  /**
+   * Optionally register callback.
+   *
+   * @param[out] callback_stack Pointer to callback_stack with which to
+   *                            register the callback.
+   */
+  virtual void RegisterCallback(CallbackStack *callback_stack) {}
+
+  /**
+   * Emit machine code.
+   *
+   * @param start Instruction pointer to first instruction when executing.
+   * @param[in,out] backend Architecture backend.
+   * @param[in,out] evts Pointer to EvtState instance of calling Compiler.
+   * @param[out] code Pointer to memory to be copied into.
+   * @param len Maximum lenth of code.
+   *
+   * @return Size of emitted code.
+   */
+  virtual std::size_t Emit(types::InstPtr start, Backend *backend,
+                           EvtState *evts, void *code, std::size_t len) = 0;
+
+  /**
+   * Accessor for last event generated. Also used to insert additional
+   * ordering based on passed next_event (e.g. fences).
+   *
+   * @param next_event Event after last in program order; nullptr if none
+   *                   exists.
+   * @param[in,out] evts Pointer to EvtState instance maintained by
+   *                     Compiler.
+   *
+   * @return Last event in program-order; nullptr if none exists.
+   */
+  virtual const mc::Event *LastEvent(const mc::Event *next_event,
+                                     EvtState *evts) const = 0;
+
+  /**
+   * Accessor for first event generated.
+   *
+   * @param prev_event Event before first in program order; nullptr if none
+   *                   exists.
+   * @param[in,out] evts Pointer to EvtState instance maintained by
+   *                     Compiler.
+   *
+   * @return First event in program-order; nullptr if none exists.
+   */
+  virtual const mc::Event *FirstEvent(const mc::Event *prev_event,
+                                      EvtState *evts) const = 0;
+
+  /**
+   * Updates dynamic observation for instruction's memory operation.
+   *
+   * @param ip Instruction pointer of instruction for which a value was
+   *           observed.
+   * @param part Which part of an instruction; e.g., if an instruction
+   *             generates multiple memory events, part can be used to denote
+   *             which.
+   * @param addr Address for observed operation.
+   * @param from_id Pointer to observed memory (WriteIDs).
+   * @param size Total size of observed memory operations in from_id;
+   *             implementation should assert expected size.
+   * @param[in,out] evts Pointer to EvtState instance maintained by
+   *                     Compiler.
+   *
+   * @return Success or not.
+   */
+  virtual bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                         const types::WriteID *from_id, std::size_t size,
+                         EvtState *evts) = 0;
+
+  types::Pid pid() const { return pid_; }
+
+  void set_pid(types::Pid pid) { pid_ = pid; }
+
+ private:
+  types::Pid pid_;
+};
+
+template <class Backend, class EvtState>
+class MemOp : public Op<Backend, EvtState> {
+ public:
+  explicit MemOp(types::Pid pid) : Op<Backend, EvtState>(pid) {}
+
+  virtual types::Addr addr() const = 0;
+};
+
+template <class Backend, class EvtState>
+class NullOp : public Op<Backend, EvtState> {
+ public:
+  explicit NullOp(types::Pid pid) : Op<Backend, EvtState>(pid) {}
+
+  bool EnableEmit(EvtState *evts) override { return false; }
+
+  void InsertPo(typename Op<Backend, EvtState>::ThreadConstIt before,
+                EvtState *evts) override {
+    throw std::logic_error("Not supported!");
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtState *evts,
+                   void *code, std::size_t len) override {
+    throw std::logic_error("Not supported!");
+    return 0;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtState *evts) override {
+    throw std::logic_error("Not supported!");
+    return false;
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtState *evts) const override {
+    throw std::logic_error("Not supported!");
+    return nullptr;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtState *evts) const override {
+    throw std::logic_error("Not supported!");
+    return nullptr;
+  }
+};
+
+/**
+ * @brief Top level class used to manage code generation (compiler).
+ */
+template <class Operation, class Backend>
+class Compiler {
+ public:
+  typedef typename Operation::EvtState EvtState;
+  typedef typename Operation::Threads Threads;
+  typedef typename Operation::ThreadIt ThreadIt;
+  typedef typename Operation::ThreadItStack ThreadItStack;
+  typedef typename Operation::ThreadConst ThreadConst;
+  typedef typename Operation::Callback Callback;
+  typedef typename Operation::CallbackStack CallbackStack;
+
+  /**
+   * Implies a reset of state in evts.
+   *
+   * @param evts Pointer to instance of EvtState as required by Operation. The
+   *             choice of unique_ptr here is deliberate, in that the class
+   *             that Operation requires may be a virtual base class, and
+   *             Compiler takes ownership.
+   */
+  explicit Compiler(std::unique_ptr<EvtState> evts) : evts_(std::move(evts)) {
+    Reset();
+  }
+
+  /**
+   * Implies a reset of state in evts and threads (the Ops contained).
+   *
+   * @param evts Pointer to instance of EvtState as required by Operation. The
+   *             choice of unique_ptr here is deliberate, in that the class
+   *             that Operation requires may be a virtual base class.
+   *             Takes ownership.
+   * @param[in,out] threads Threads container. The Ops pointed to by Threads may
+   *                        be modified.
+   */
+  explicit Compiler(std::unique_ptr<EvtState> evts, Threads &&threads)
+      : evts_(std::move(evts)) {
+    Reset(std::move(threads));
+  }
+
+  void Reset() {
+    evts_->Reset();
+    backend_.Reset();
+    ip_to_op_.clear();
+  }
+
+  void Reset(Threads &&threads) {
+    threads_ = std::move(threads);
+
+    // Must ensure all Operation instances have been reset.
+    for (const auto &thread : threads_) {
+      for (const auto &op : thread.second) {
+        op->Reset();
+      }
+    }
+
+    Reset();
+  }
+
+  const Threads &threads() { return threads_; }
+
+  const EvtState *evts() const { return evts_.get(); }
+
+  EvtState *evts() { return evts_.get(); }
+
+  std::size_t Emit(types::InstPtr base, Operation *op, void *code,
+                   std::size_t len, ThreadConst *thread_const_ops,
+                   CallbackStack *callback_stack) {
+    // Prepare op for emit.
+    if (!op->EnableEmit(evts_.get())) {
+      return 0;
+    }
+
+    // Generate program-order.
+    if (thread_const_ops != nullptr) {
+      assert(!thread_const_ops->empty());
+      op->InsertPo(--thread_const_ops->end(), evts_.get());
+      thread_const_ops->push_back(op);
+    } else {
+      ThreadConst invalid{nullptr};
+      op->InsertPo(invalid.begin(), evts_.get());
+    }
+
+    std::size_t ctrl_len = 0;
+
+    if (callback_stack != nullptr) {
+      // Call all registered callbacks
+      for (auto &callback : (*callback_stack)) {
+        // Pass in current base, e.g. to allow late resolving of branch
+        // targets; allows inserting code for flow control.
+        const std::size_t s =
+            callback(op, base, &backend_, evts_.get(), code, len);
+
+        assert(s < len);
+        base += s;
+        code = static_cast<char *>(code) + s;
+        len -= s;
+        ctrl_len += s;
+      }
+
+      // Register callback
+      op->RegisterCallback(callback_stack);
+    }
+
+    // Must be called *after* InsertPo and callback!
+    const std::size_t op_len =
+        op->Emit(base, &backend_, evts_.get(), code, len);
+    assert(op_len != 0);
+
+    // Base IP must be unique!
+    assert(IpToOp(base) == nullptr);
+    // Insert IP to Operation mapping.
+    ip_to_op_[base] = std::make_pair(base + op_len, op);
+
+    return op_len + ctrl_len;
+  }
+
+  std::size_t Emit(types::Pid pid, types::InstPtr base, void *code,
+                   std::size_t len) {
+    auto thread = threads_.find(pid);
+
+    if (thread == threads_.end()) {
+      return 0;
+    }
+
+    std::size_t emit_len = 0;
+
+    // Maintain const sequence of *emitted* ops; nullptr denotes beginning
+    // of sequence (in absence of thread_const_ops.begin()).
+    //
+    // This will be a flattened sequence of ops (evaluated recursive ops).
+    ThreadConst thread_const_ops{nullptr};
+    thread_const_ops.reserve(thread->second.size() + 1);
+
+    // Callback function list
+    CallbackStack callback_stack;
+
+    // Enable recursive, nested sequences.
+    ThreadItStack it_stack;
+    it_stack.emplace_back(thread->second.begin(), thread->second.end());
+
+    while (!it_stack.empty()) {
+      auto &it = it_stack.back().first;
+      auto &end = it_stack.back().second;
+
+      if (it == end) {
+        it_stack.pop_back();
+        continue;
+      }
+
+      const auto &op = *it;
+
+      // Generate code and architecture-specific ordering relations.
+      const std::size_t op_len =
+          Emit(base + emit_len, op.get(), code, len - emit_len,
+               &thread_const_ops, &callback_stack);
+
+      emit_len += op_len;
+      assert(emit_len <= len);
+      code = static_cast<char *>(code) + op_len;
+
+      op->AdvanceThread(&it_stack);
+    }
+
+    // Notify ops of completion
+    for (auto &callback : callback_stack) {
+      const std::size_t s = callback(nullptr, base + emit_len, &backend_,
+                                     evts_.get(), code, len - emit_len);
+
+      emit_len += s;
+      assert(emit_len <= len);
+      code = static_cast<char *>(code) + s;
+    }
+
+    return emit_len;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size) {
+    auto op = IpToOp(ip);
+
+    if (op == nullptr) {
+      return false;
+    }
+
+    return op->UpdateObs(ip, part, addr, from_id, size, evts_.get());
+  }
+
+  Operation *IpToOp(types::InstPtr ip) const {
+    if (ip_to_op_.empty()) {
+      // Can be legally empty if no code has yet been emitted, i.e. right
+      // after host system startup. By not faulting here, the host can
+      // still use ip_to_op to check if an instruction needs to be
+      // treated specially: before any code has been emitted, no
+      // instructions will be treated specially.
+      return nullptr;
+    }
+
+    auto e = ip_to_op_.upper_bound(ip);
+    if (e != ip_to_op_.begin()) {
+      e--;
+    }
+
+    if (!(e->first <= ip && ip < e->second.first)) {
+      return nullptr;
+    }
+
+    return e->second.second;
+  }
+
+ private:
+  typedef std::map<types::InstPtr, std::pair<types::InstPtr, Operation *>>
+      InstPtr_Op;
+
+  std::unique_ptr<EvtState> evts_;
+  Backend backend_;
+  Threads threads_;
+
+  // Each processor executes unique code, hence IP must be unique. Only stores
+  // the start IP of Op's code.
+  InstPtr_Op ip_to_op_;
+};
+
+}  // namespace codegen
+}  // namespace mc2lib
+
+#endif /* MC2LIB_CODEGEN_COMPILER_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/codegen/ops/armv7.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/codegen/ops/armv7.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,779 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_CODEGEN_OPS_ARMv7_HPP_
+#define MC2LIB_CODEGEN_OPS_ARMv7_HPP_
+
+#include <algorithm>
+#include <random>
+
+#include "../cats.hpp"
+#include "../compiler.hpp"
+
+namespace mc2lib {
+namespace codegen {
+
+/**
+ * @namespace mc2lib::codegen::armv7
+ * @brief Implementations of Operations for ARMv7 (incomplete).
+ *
+ * The current operations do not exercise all aspects of the MCM.
+ */
+namespace armv7 {
+
+#define ASM_PRELUDE char *cnext__ = static_cast<char *>(code);
+#define ASM_LEN (static_cast<std::size_t>(cnext__ - static_cast<char *>(code)))
+#define ASM_AT (start + ASM_LEN)
+
+#define ASM16(v)                                       \
+  do {                                                 \
+    assert(ASM_LEN + 2 <= len);                        \
+    *reinterpret_cast<std::uint16_t *>(cnext__) = (v); \
+    cnext__ += 2;                                      \
+  } while (0)
+
+#define ASM_PROLOGUE return ASM_LEN;
+
+// Thumb
+class Backend {
+ public:
+  void Reset() {}
+
+  // Currently supports single byte operations only; to test for single-copy
+  // atomicity, implement multi-byte operations support.
+  static_assert(sizeof(types::WriteID) == 1, "Unsupported read/write size!");
+
+  enum Reg {
+    r0 = 0,
+    r1,
+    r2,
+    r3,
+    r4,
+
+    // reserved
+    r5__,
+    r6__,
+    r7__
+  };
+
+  std::size_t Return(void *code, std::size_t len) const {
+    ASM_PRELUDE;
+    ASM16(0x4770);  // bx lr
+    ASM_PROLOGUE;
+  }
+
+  std::size_t Delay(std::size_t length, void *code, std::size_t len) const {
+    ASM_PRELUDE;
+    for (std::size_t i = 0; i < length; ++i) {
+      ASM16(0xbf00);  // nop
+    }
+    ASM_PROLOGUE;
+  }
+
+  std::size_t DMB_ST(void *code, std::size_t len) const {
+    ASM_PRELUDE;
+    // dmb st
+    ASM16(0xf3bf);
+    ASM16(0x8f5e);
+    ASM_PROLOGUE;
+  }
+
+  std::size_t Read(types::Addr addr, Reg out, types::InstPtr start, void *code,
+                   std::size_t len, types::InstPtr *at) const {
+    ASM_PRELUDE;
+
+    Helper h(cnext__, code, len);
+    h.MovImm32(r6__, addr);
+
+    // ldrb out, [r6, #0]
+    *at = ASM_AT;
+    ASM16(0x7830 | out);
+
+    ASM_PROLOGUE;
+  }
+
+  std::size_t ReadAddrDp(types::Addr addr, Reg out, Reg dp,
+                         types::InstPtr start, void *code, std::size_t len,
+                         types::InstPtr *at) const {
+    ASM_PRELUDE;
+
+    Helper h(cnext__, code, len);
+    h.MovImm32(r6__, addr);
+
+    // eor dp, dp
+    ASM16(0x4040 | (dp << 3) | dp);
+
+    // ldrb out, [r6, dp]
+    *at = ASM_AT;
+    ASM16(0x5c30 | (dp << 6) | out);
+
+    ASM_PROLOGUE;
+  }
+
+  std::size_t Write(types::Addr addr, types::WriteID write_id,
+                    types::InstPtr start, void *code, std::size_t len,
+                    types::InstPtr *at) const {
+    ASM_PRELUDE;
+
+    Helper h(cnext__, code, len);
+    h.MovImm32(r6__, addr);
+
+    // movs r7, #write_id
+    ASM16(0x2700 | write_id);
+
+    // strb r7, [r6, #0]
+    *at = ASM_AT;
+    ASM16(0x7037);
+
+    ASM_PROLOGUE;
+  }
+
+ protected:
+  class Helper {
+   public:
+    Helper(char *&cnext, void *&code, std::size_t len)
+        : cnext__(cnext), code(code), len(len) {}
+
+    void MovImm32(Reg reg, std::uint32_t imm32) {
+      // movw reg, #(imm32 & 0xffff)
+      std::uint16_t imm32_w = imm32 & 0xffff;
+      ASM16(0xf240
+            // [10:10]
+            | ((imm32_w & 0x0800) >> 1)
+            // [3:0]
+            | ((imm32_w & 0xf000) >> 12));
+      ASM16(  // [14:12]
+          ((imm32_w & 0x0700) << 4)
+          // [11:8]
+          | (reg << 8)
+          // [7:0]
+          | (imm32_w & 0x00ff));
+
+      // movt reg, #((imm32 & 0xffff0000) >> 16)
+      std::uint16_t imm32_t = (imm32 & 0xffff0000) >> 16;
+      ASM16(0xf2c0
+            // [10:10]
+            | ((imm32_t & 0x0800) >> 1)
+            // [3:0]
+            | ((imm32_t & 0xf000) >> 12));
+      ASM16(  // [14:12]
+          ((imm32_t & 0x0700) << 4)
+          // [11:8]
+          | (reg << 8)
+          // [7:0]
+          | (imm32_t & 0x00ff));
+    }
+
+   protected:
+    char *&cnext__;
+    void *&code;
+    const std::size_t len;
+  };
+};
+
+#undef ASM_PRELUDE
+#undef ASM_LEN
+#undef ASM_AT
+#undef ASM16
+#undef ASM_PROLOGUE
+
+typedef Op<Backend, EvtStateCats> Operation;
+typedef MemOp<Backend, EvtStateCats> MemOperation;
+typedef NullOp<Backend, EvtStateCats> NullOperation;
+
+class Return : public Operation {
+ public:
+  explicit Return(types::Pid pid = -1) : Operation(pid) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Return>(*this);
+  }
+
+  void Reset() override {}
+
+  bool EnableEmit(EvtStateCats *evts) override { return true; }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {}
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Return(code, len);
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    return nullptr;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    return nullptr;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    return true;
+  }
+};
+
+class Delay : public Operation {
+ public:
+  explicit Delay(std::size_t length, types::Pid pid = -1)
+      : Operation(pid), length_(length), before_(nullptr) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Delay>(*this);
+  }
+
+  void Reset() override { before_ = nullptr; }
+
+  bool EnableEmit(EvtStateCats *evts) override { return true; }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    before_ = *before;
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Delay(length_, code, len);
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->LastEvent(next_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->FirstEvent(prev_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    assert(false);
+    return false;
+  }
+
+ protected:
+  std::size_t length_;
+  const Operation *before_;
+};
+
+class Read : public MemOperation {
+ public:
+  explicit Read(types::Addr addr, Backend::Reg out, types::Pid pid = -1)
+      : MemOperation(pid),
+        addr_(addr),
+        out_(out),
+        event_(nullptr),
+        from_(nullptr) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Read>(*this);
+  }
+
+  void Reset() override {
+    event_ = nullptr;
+    from_ = nullptr;
+  }
+
+  bool EnableEmit(EvtStateCats *evts) override { return !evts->Exhausted(); }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    event_ = evts->MakeRead(pid(), mc::Event::kRead, addr_)[0];
+
+    if (*before != nullptr) {
+      auto event_before = (*before)->LastEvent(event_, evts);
+      if (event_before != nullptr) {
+        evts->ew()->po.Insert(*event_before, *event_);
+      }
+    }
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Read(addr_, out(), start, code, len, &at_);
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    assert(event_ != nullptr);
+    assert(ip == at_);
+    assert(addr == addr_);
+    assert(size == sizeof(types::WriteID));
+
+    const mc::Event *from =
+        evts->GetWrite(MakeEventPtrs(event_), addr_, from_id)[0];
+
+    if (from_ != nullptr) {
+      // If from_ == from, we still need to continue to try to erase and
+      // insert, in case the from-relation has been cleared.
+
+      evts->ew()->rf.Erase(*from_, *event_);
+    }
+
+    from_ = from;
+    evts->ew()->rf.Insert(*from_, *event_, true);
+
+    return true;
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    return event_;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    return event_;
+  }
+
+  types::Addr addr() const override { return addr_; }
+
+  Backend::Reg out() const { return out_; }
+
+ protected:
+  types::Addr addr_;
+  Backend::Reg out_;
+  const mc::Event *event_;
+  const mc::Event *from_;
+  types::InstPtr at_;
+};
+
+class ReadAddrDp : public Read {
+ public:
+  explicit ReadAddrDp(types::Addr addr, Backend::Reg reg, Backend::Reg dp,
+                      types::Pid pid = -1)
+      : Read(addr, reg, pid), dp_(dp) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<ReadAddrDp>(*this);
+  }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    event_ = evts->MakeRead(pid(), mc::Event::kRead | mc::Event::kRegInAddr,
+                            addr_)[0];
+
+    if (*before != nullptr) {
+      auto event_before = (*before)->LastEvent(event_, evts);
+      if (event_before != nullptr) {
+        evts->ew()->po.Insert(*event_before, *event_);
+
+        // Find read dependency.
+        auto arch = dynamic_cast<mc::cats::Arch_ARMv7 *>(evts->arch());
+        if (arch != nullptr) {
+          do {
+            auto potential_dp_read = dynamic_cast<const Read *>(*before);
+            if (potential_dp_read != nullptr) {
+              if (potential_dp_read->out() == dp_) {
+                auto event_dp = potential_dp_read->LastEvent(event_, evts);
+                arch->dd_reg.Insert(*event_dp, *event_);
+                break;
+              }
+            }
+          } while (*(--before) != nullptr);
+        }
+      }
+    }
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->ReadAddrDp(addr_, out(), dp_, start, code, len, &at_);
+  }
+
+ protected:
+  Backend::Reg dp_;
+};
+
+class Write : public MemOperation {
+ public:
+  explicit Write(types::Addr addr, types::Pid pid = -1)
+      : MemOperation(pid), addr_(addr), write_id_(0) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Write>(*this);
+  }
+
+  void Reset() override {
+    event_ = nullptr;
+    from_ = nullptr;
+    write_id_ = 0;
+  }
+
+  bool EnableEmit(EvtStateCats *evts) override { return !evts->Exhausted(); }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    event_ = evts->MakeWrite(pid(), mc::Event::kWrite, addr_, &write_id_)[0];
+
+    if (*before != nullptr) {
+      auto event_before = (*before)->LastEvent(event_, evts);
+      if (event_before != nullptr) {
+        evts->ew()->po.Insert(*event_before, *event_);
+      }
+    }
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Write(addr_, write_id_, start, code, len, &at_);
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    assert(event_ != nullptr);
+    assert(ip == at_);
+    assert(addr == addr_);
+    assert(size == sizeof(types::WriteID));
+
+    const mc::Event *from =
+        evts->GetWrite(MakeEventPtrs(event_), addr_, from_id)[0];
+
+    if (from_ != nullptr) {
+      // If from_ == from, we still need to continue to try to erase and
+      // insert, in case the from-relation has been cleared.
+
+      evts->ew()->co.Erase(*from_, *event_);
+    }
+
+    from_ = from;
+    evts->ew()->co.Insert(*from_, *event_, true);
+
+    return true;
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    return event_;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    return event_;
+  }
+
+  types::Addr addr() const override { return addr_; }
+
+ protected:
+  types::Addr addr_;
+  types::WriteID write_id_;
+  const mc::Event *event_;
+  const mc::Event *from_;
+  types::InstPtr at_;
+};
+
+class DMB_ST : public Operation {
+ public:
+  explicit DMB_ST(types::Pid pid = -1)
+      : Operation(pid), before_(nullptr), first_write_before_(nullptr) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<DMB_ST>(*this);
+  }
+
+  void Reset() override {
+    before_ = nullptr;
+    first_write_before_ = nullptr;
+  }
+
+  bool EnableEmit(EvtStateCats *evts) override { return true; }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    before_ = *before;
+
+    while (*before != nullptr) {
+      auto potential_write = dynamic_cast<const Write *>(*before);
+      if (potential_write != nullptr) {
+        first_write_before_ = potential_write;
+        break;
+      }
+      --before;
+    }
+  }
+
+  void RegisterCallback(Operation::CallbackStack *callback_stack) override {
+    callback_stack->push_back([this](Operation *after, types::InstPtr start,
+                                     Backend *backend, EvtStateCats *evts,
+                                     void *code, std::size_t len) {
+      if (first_write_before_ != nullptr) {
+        auto potential_write = dynamic_cast<const Write *>(after);
+        if (potential_write != nullptr) {
+          auto arch = dynamic_cast<mc::cats::Arch_ARMv7 *>(evts->arch());
+          if (arch != nullptr) {
+            auto event_before = first_write_before_->LastEvent(nullptr, evts);
+            auto event_after = potential_write->FirstEvent(nullptr, evts);
+            assert(event_before != nullptr);
+            assert(event_after != nullptr);
+
+            arch->dmb_st.Insert(*event_before, *event_after);
+            // cats::ARMv7 takes care of transitivity.
+          }
+          first_write_before_ = nullptr;
+        }
+      }
+      return 0;
+    });
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->DMB_ST(code, len);
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->LastEvent(next_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->FirstEvent(prev_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    assert(false);
+    return false;
+  }
+
+ protected:
+  const Operation *before_;
+  const Operation *first_write_before_;
+};
+
+/**
+ * RandomFactory.
+ */
+struct RandomFactory {
+  typedef Operation ResultType;
+
+  explicit RandomFactory(types::Pid min_pid, types::Pid max_pid,
+                         types::Addr min_addr, types::Addr max_addr,
+                         std::size_t stride = sizeof(types::WriteID),
+                         std::size_t max_sequence = 50)
+      : min_pid_(min_pid),
+        max_pid_(max_pid),
+        min_addr_(min_addr),
+        max_addr_(max_addr),
+        stride_(stride),
+        max_sequence_(max_sequence) {
+    assert(this->stride() >= sizeof(types::WriteID));
+    assert(this->stride() % sizeof(types::WriteID) == 0);
+  }
+
+  void Reset(types::Pid min_pid, types::Pid max_pid, types::Addr min_addr,
+             types::Addr max_addr,
+             std::size_t stride = sizeof(types::WriteID)) {
+    min_pid_ = min_pid;
+    max_pid_ = max_pid;
+    min_addr_ = min_addr;
+    max_addr_ = max_addr;
+    stride_ = stride;
+  }
+
+  template <class URNG, class AddrFilterFunc>
+  Operation::Ptr operator()(URNG &urng, AddrFilterFunc addr_filter_func,
+                            std::size_t max_fails = 0) const {
+    // Choice distribution
+    std::uniform_int_distribution<std::size_t> dist_choice(0, 1000 - 1);
+
+    // Pid distribution
+    std::uniform_int_distribution<types::Pid> dist_pid(min_pid_, max_pid_);
+
+    // Addr distribution
+    auto chunk_min_addr = min_addr_;
+    auto chunk_max_addr = max_addr_;
+
+    if (ChunkSize() > 1 && HoleSize() > 1) {
+      std::size_t chunk_cnt =
+          for_each_AddrRange([](types::Addr a, types::Addr b) {});
+      std::size_t select_chunk =
+          std::uniform_int_distribution<std::size_t>(0, chunk_cnt - 1)(urng);
+
+      chunk_min_addr = min_addr_ + (select_chunk * HoleSize());
+      chunk_max_addr = chunk_min_addr + ChunkSize() - 1;
+
+      assert(chunk_min_addr >= min_addr_);
+      assert(chunk_max_addr <= max_addr_);
+    }
+
+    std::uniform_int_distribution<types::Addr> dist_addr(
+        chunk_min_addr, chunk_max_addr - EvtStateCats::kMaxOpSize);
+
+    // Sequence distribution
+    std::uniform_int_distribution<std::size_t> dist_sequence(1, max_sequence_);
+
+    // Register distribution
+    std::uniform_int_distribution<int> dist_reg(Backend::r0, Backend::r4);
+
+    // select op
+    const auto choice = dist_choice(urng);
+
+    // pid
+    const auto pid = dist_pid(urng);
+
+    // addr (lazy)
+    auto addr = [&]() {
+      types::Addr result = 0;
+
+      for (std::size_t tries = 0; tries < max_fails + 1; ++tries) {
+        result = dist_addr(urng);
+        result -= result % stride();
+        if (result < chunk_min_addr) result += stride();
+        assert(result >= chunk_min_addr);
+        assert(result <= chunk_max_addr - EvtStateCats::kMaxOpSize);
+
+        if (addr_filter_func(result)) {
+          return result;
+        }
+      }
+
+      return result;
+    };
+
+    // sequence (lazy)
+    auto sequence = [&dist_sequence, &urng]() { return dist_sequence(urng); };
+
+    // sequence (lazy)
+    auto reg = [&dist_reg, &urng]() {
+      return static_cast<Backend::Reg>(dist_reg(urng));
+    };
+
+    if (choice < 320) {  // 32%
+      return std::make_shared<Read>(addr(), reg(), pid);
+    } else if (choice < 560) {  // 24%
+      return std::make_shared<ReadAddrDp>(addr(), reg(), reg(), pid);
+    } else if (choice < 980) {  // 42%
+      return std::make_shared<Write>(addr(), pid);
+    } else if (choice < 990) {  // 1%
+      return std::make_shared<DMB_ST>(pid);
+    } else if (choice < 1000) {  // 1%
+      return std::make_shared<Delay>(sequence(), pid);
+    }
+
+    // should never get here
+    assert(false);
+    return nullptr;
+  }
+
+  template <class URNG>
+  Operation::Ptr operator()(URNG &urng) const {
+    return (*this)(urng, [](types::Addr addr) { return true; });
+  }
+
+  types::Pid min_pid() const { return min_pid_; }
+
+  types::Pid max_pid() const { return max_pid_; }
+
+  types::Addr min_addr() const { return min_addr_; }
+
+  types::Addr max_addr() const { return max_addr_; }
+
+  std::size_t stride() const { return stride_ & ((1ULL << 16) - 1); }
+
+  std::size_t ChunkSize() const {
+    return 1ULL << ((stride_ & (0xffULL << 24)) >> 24);
+  }
+
+  std::size_t HoleSize() const {
+    return 1ULL << ((stride_ & (0xffULL << 16)) >> 16);
+  }
+
+  template <class Func>
+  std::size_t for_each_AddrRange(Func func) const {
+    if (ChunkSize() > 1 && HoleSize() > 1) {
+      assert(HoleSize() >= ChunkSize());
+      assert(ChunkSize() <= (max_addr_ - min_addr_ + 1));
+
+      std::size_t chunk_cnt = 0;
+
+      for (;; ++chunk_cnt) {
+        types::Addr min = min_addr_ + (chunk_cnt * HoleSize());
+        types::Addr max = min + ChunkSize() - 1;
+        if (max > max_addr_) break;
+
+        func(min, max);
+      }
+
+      return chunk_cnt;
+    }
+
+    func(min_addr_, max_addr_);
+    return 1;
+  }
+
+  std::size_t max_sequence() const { return max_sequence_; }
+
+  void set_max_sequence(std::size_t val) { max_sequence_ = val; }
+
+ private:
+  types::Pid min_pid_;
+  types::Pid max_pid_;
+  types::Addr min_addr_;
+  types::Addr max_addr_;
+  std::size_t stride_;
+  std::size_t max_sequence_;
+};
+
+}  // namespace armv7
+}  // namespace codegen
+}  // namespace mc2lib
+
+#endif /* MC2LIB_CODEGEN_OPS_ARMv7_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/codegen/ops/strong.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/codegen/ops/strong.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,732 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_CODEGEN_OPS_STRONG_HPP_
+#define MC2LIB_CODEGEN_OPS_STRONG_HPP_
+
+#include <algorithm>
+#include <random>
+#include <sstream>
+
+#include "../cats.hpp"
+#include "../compiler.hpp"
+
+namespace mc2lib {
+namespace codegen {
+
+/**
+ * @namespace mc2lib::codegen::strong
+ * @brief Implementations of Operations for strong memory consistency models.
+ */
+namespace strong {
+
+struct Backend {
+  virtual ~Backend() {}
+
+  virtual void Reset() {}
+
+  virtual std::size_t Return(void *code, std::size_t len) const = 0;
+
+  virtual std::size_t Delay(std::size_t length, void *code,
+                            std::size_t len) const = 0;
+
+  virtual std::size_t Read(types::Addr addr, types::InstPtr start, void *code,
+                           std::size_t len, types::InstPtr *at) const = 0;
+
+  virtual std::size_t ReadAddrDp(types::Addr addr, types::InstPtr start,
+                                 void *code, std::size_t len,
+                                 types::InstPtr *at) const = 0;
+
+  virtual std::size_t Write(types::Addr addr, types::WriteID write_id,
+                            types::InstPtr start, void *code, std::size_t len,
+                            types::InstPtr *at) const = 0;
+
+  virtual std::size_t ReadModifyWrite(types::Addr addr, types::WriteID write_id,
+                                      types::InstPtr start, void *code,
+                                      std::size_t len,
+                                      types::InstPtr *at) const = 0;
+
+  virtual std::size_t CacheFlush(types::Addr addr, void *code,
+                                 std::size_t len) const = 0;
+};
+
+typedef Op<Backend, EvtStateCats> Operation;
+typedef MemOp<Backend, EvtStateCats> MemOperation;
+typedef NullOp<Backend, EvtStateCats> NullOperation;
+
+class Return : public Operation {
+ public:
+  explicit Return(types::Pid pid = -1) : Operation(pid) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Return>(*this);
+  }
+
+  void Reset() override {}
+
+  bool EnableEmit(EvtStateCats *evts) override { return true; }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {}
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Return(code, len);
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    return nullptr;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    return nullptr;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    return true;
+  }
+};
+
+class Delay : public Operation {
+ public:
+  explicit Delay(std::size_t length, types::Pid pid = -1)
+      : Operation(pid), length_(length), before_(nullptr) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Delay>(*this);
+  }
+
+  void Reset() override { before_ = nullptr; }
+
+  bool EnableEmit(EvtStateCats *evts) override { return true; }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    before_ = *before;
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Delay(length_, code, len);
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->LastEvent(next_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->FirstEvent(prev_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    assert(false);
+    return false;
+  }
+
+ protected:
+  std::size_t length_;
+  const Operation *before_;
+};
+
+class Read : public MemOperation {
+ public:
+  explicit Read(types::Addr addr, types::Pid pid = -1)
+      : MemOperation(pid), addr_(addr), event_(nullptr), from_(nullptr) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Read>(*this);
+  }
+
+  void Reset() override {
+    event_ = nullptr;
+    from_ = nullptr;
+  }
+
+  bool EnableEmit(EvtStateCats *evts) override { return !evts->Exhausted(); }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    event_ = evts->MakeRead(pid(), mc::Event::kRead, addr_)[0];
+
+    if (*before != nullptr) {
+      auto event_before = (*before)->LastEvent(event_, evts);
+      if (event_before != nullptr) {
+        evts->ew()->po.Insert(*event_before, *event_);
+      }
+    }
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Read(addr_, start, code, len, &at_);
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    assert(event_ != nullptr);
+    assert(ip == at_);
+    assert(addr == addr_);
+    assert(size == sizeof(types::WriteID));
+
+    const mc::Event *from =
+        evts->GetWrite(MakeEventPtrs(event_), addr_, from_id)[0];
+
+    if (from_ != nullptr) {
+      // If from_ == from, we still need to continue to try to erase and
+      // insert, in case the from-relation has been cleared.
+
+      EraseObsHelper(from_, event_, evts->ew());
+    }
+
+    from_ = from;
+    InsertObsHelper(from_, event_, evts->ew());
+
+    return true;
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    return event_;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    return event_;
+  }
+
+  types::Addr addr() const override { return addr_; }
+
+ protected:
+  virtual void InsertObsHelper(const mc::Event *e1, const mc::Event *e2,
+                               mc::cats::ExecWitness *ew) {
+    ew->rf.Insert(*e1, *e2, true);
+  }
+
+  virtual void EraseObsHelper(const mc::Event *e1, const mc::Event *e2,
+                              mc::cats::ExecWitness *ew) {
+    ew->rf.Erase(*e1, *e2);
+  }
+
+  types::Addr addr_;
+  const mc::Event *event_;
+  const mc::Event *from_;
+  types::InstPtr at_;
+};
+
+class ReadAddrDp : public Read {
+ public:
+  explicit ReadAddrDp(types::Addr addr, types::Pid pid = -1)
+      : Read(addr, pid) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<ReadAddrDp>(*this);
+  }
+
+  // TODO(melver): InsertPo: if we start supporting an Arch which does not
+  // order Read->Read, add a dependency-hb between this and the last Read --
+  // this assumes all Reads are reading into the same register, and this read
+  // computes the address with this one register.
+  // NOTE: before can be used to traverse operations backwards before "before".
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->ReadAddrDp(addr_, start, code, len, &at_);
+  }
+};
+
+class Write : public Read {
+ public:
+  explicit Write(types::Addr addr, types::Pid pid = -1)
+      : Read(addr, pid), write_id_(0) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<Write>(*this);
+  }
+
+  void Reset() override {
+    event_ = nullptr;
+    from_ = nullptr;
+    write_id_ = 0;
+  }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    event_ = evts->MakeWrite(pid(), mc::Event::kWrite, addr_, &write_id_)[0];
+
+    if (*before != nullptr) {
+      auto event_before = (*before)->LastEvent(event_, evts);
+      if (event_before != nullptr) {
+        evts->ew()->po.Insert(*event_before, *event_);
+      }
+    }
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->Write(addr_, write_id_, start, code, len, &at_);
+  }
+
+ protected:
+  void InsertObsHelper(const mc::Event *e1, const mc::Event *e2,
+                       mc::cats::ExecWitness *ew) override {
+    ew->co.Insert(*e1, *e2);
+  }
+
+  void EraseObsHelper(const mc::Event *e1, const mc::Event *e2,
+                      mc::cats::ExecWitness *ew) override {
+    ew->co.Erase(*e1, *e2);
+  }
+
+  types::WriteID write_id_;
+};
+
+class ReadModifyWrite : public MemOperation {
+ public:
+  explicit ReadModifyWrite(types::Addr addr, types::Pid pid = -1)
+      : MemOperation(pid), addr_(addr), last_part_(-1) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<ReadModifyWrite>(*this);
+  }
+
+  void Reset() override {
+    last_part_ = -1;
+    event_r_ = nullptr;
+    event_w_ = nullptr;
+    from_ = nullptr;
+    write_id_ = 0;
+  }
+
+  bool EnableEmit(EvtStateCats *evts) override { return !evts->Exhausted(); }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    event_r_ = evts->MakeRead(pid(), mc::Event::kRead, addr_)[0];
+    event_w_ = evts->MakeWrite(pid(), mc::Event::kWrite, addr_, &write_id_)[0];
+
+    if (*before != nullptr) {
+      auto event_before = (*before)->LastEvent(event_r_, evts);
+      if (event_before != nullptr) {
+        evts->ew()->po.Insert(*event_before, *event_r_);
+
+        if (dynamic_cast<mc::cats::Arch_TSO *>(evts->arch()) != nullptr) {
+          // Implied fence before atomic
+          auto arch_tso = dynamic_cast<mc::cats::Arch_TSO *>(evts->arch());
+          arch_tso->mfence.Insert(*event_before, *event_r_);
+        }
+      }
+    }
+
+    evts->ew()->po.Insert(*event_r_, *event_w_);
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->ReadModifyWrite(addr_, write_id_, start, code, len, &at_);
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    assert(event_r_ != nullptr);
+    assert(event_w_ != nullptr);
+    assert(ip == at_);
+    assert(addr == addr_);
+    assert(size == sizeof(types::WriteID));
+
+    // This also alerts us if the read would be seeing the write's data.
+    const mc::Event *from =
+        evts->GetWrite(MakeEventPtrs(event_w_), addr_, from_id)[0];
+
+    auto part_event = event_r_;
+    auto obs_rel = &evts->ew()->rf;
+
+    // TODO(melver): clean this up! Do we need ability to update squashed?
+
+    if (last_part_ == -1 || part <= last_part_) {
+      // First part: read
+
+      if (from_ != nullptr) {
+        // Restart
+        evts->ew()->rf.Erase(*from_, *event_r_);
+        evts->ew()->co.Erase(*from_, *event_w_);
+      }
+    } else {
+      // Second part: write
+      assert(part > last_part_);
+
+      // Check atomicity.
+      if (*from != *from_) {
+        std::ostringstream oss;
+        oss << "RMW NOT ATOMIC: expected <" << static_cast<std::string>(*from_)
+            << ">, but overwriting <" << static_cast<std::string>(*from)
+            << ">!";
+        throw mc::Error(oss.str());
+      }
+
+      part_event = event_w_;
+      obs_rel = &evts->ew()->co;
+    }
+
+    obs_rel->Insert(*from, *part_event, true);
+
+    from_ = from;
+    last_part_ = part;
+    return true;
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    if (dynamic_cast<mc::cats::Arch_TSO *>(evts->arch()) != nullptr) {
+      // Implied fence after atomic
+      auto arch_tso = dynamic_cast<mc::cats::Arch_TSO *>(evts->arch());
+      arch_tso->mfence.Insert(*event_w_, *next_event);
+    }
+
+    return event_w_;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    return event_r_;
+  }
+
+  types::Addr addr() const override { return addr_; }
+
+ protected:
+  types::Addr addr_;
+  int last_part_;
+  const mc::Event *event_r_;
+  const mc::Event *event_w_;
+  const mc::Event *from_;
+  types::WriteID write_id_;
+  types::InstPtr at_;
+};
+
+class CacheFlush : public MemOperation {
+ public:
+  explicit CacheFlush(types::Addr addr, types::Pid pid = -1)
+      : MemOperation(pid), addr_(addr), before_(nullptr) {}
+
+  Operation::Ptr Clone() const override {
+    return std::make_shared<CacheFlush>(*this);
+  }
+
+  void Reset() override { before_ = nullptr; }
+
+  bool EnableEmit(EvtStateCats *evts) override { return true; }
+
+  void InsertPo(Operation::ThreadConstIt before, EvtStateCats *evts) override {
+    before_ = *before;
+  }
+
+  std::size_t Emit(types::InstPtr start, Backend *backend, EvtStateCats *evts,
+                   void *code, std::size_t len) override {
+    return backend->CacheFlush(addr_, code, len);
+  }
+
+  const mc::Event *LastEvent(const mc::Event *next_event,
+                             EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->LastEvent(next_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  const mc::Event *FirstEvent(const mc::Event *prev_event,
+                              EvtStateCats *evts) const override {
+    // Forward
+    if (before_ != nullptr) {
+      return before_->FirstEvent(prev_event, evts);
+    }
+
+    return nullptr;
+  }
+
+  bool UpdateObs(types::InstPtr ip, int part, types::Addr addr,
+                 const types::WriteID *from_id, std::size_t size,
+                 EvtStateCats *evts) override {
+    return true;
+  }
+
+  types::Addr addr() const override { return addr_; }
+
+ protected:
+  types::Addr addr_;
+  const Operation *before_;
+};
+
+class ReadSequence : public NullOperation {
+ public:
+  explicit ReadSequence(types::Addr min_addr, types::Addr max_addr,
+                        types::Pid pid = -1)
+      : NullOperation(pid), min_addr_(min_addr), max_addr_(max_addr) {
+    while (min_addr <= max_addr) {
+      sequence_.emplace_back(std::make_shared<Read>(min_addr, pid));
+      min_addr += 64;
+    }
+  }
+
+  void AdvanceThread(Operation::ThreadItStack *it_stack) const override {
+    ++(it_stack->back().first);
+    it_stack->emplace_back(sequence_.begin(), sequence_.end());
+  }
+
+  Operation::Ptr Clone() const override {
+    // Don't just copy, need deep clone
+    return std::make_shared<ReadSequence>(min_addr_, max_addr_, pid());
+  }
+
+  void Reset() override {
+    for (const auto &op : sequence_) {
+      op->Reset();
+    }
+  }
+
+ protected:
+  types::Addr min_addr_;
+  types::Addr max_addr_;
+  Operation::Thread sequence_;
+};
+
+/**
+ * RandomFactory.
+ */
+struct RandomFactory {
+  typedef Operation ResultType;
+
+  explicit RandomFactory(types::Pid min_pid, types::Pid max_pid,
+                         types::Addr min_addr, types::Addr max_addr,
+                         std::size_t stride = sizeof(types::WriteID),
+                         std::size_t max_sequence = 50, bool extended = false)
+      : min_pid_(min_pid),
+        max_pid_(max_pid),
+        min_addr_(min_addr),
+        max_addr_(max_addr),
+        stride_(stride),
+        max_sequence_(max_sequence),
+        extended_(extended) {
+    assert(this->stride() >= sizeof(types::WriteID));
+    assert(this->stride() % sizeof(types::WriteID) == 0);
+  }
+
+  void Reset(types::Pid min_pid, types::Pid max_pid, types::Addr min_addr,
+             types::Addr max_addr,
+             std::size_t stride = sizeof(types::WriteID)) {
+    min_pid_ = min_pid;
+    max_pid_ = max_pid;
+    min_addr_ = min_addr;
+    max_addr_ = max_addr;
+    stride_ = stride;
+  }
+
+  template <class URNG, class AddrFilterFunc>
+  Operation::Ptr operator()(URNG &urng, AddrFilterFunc addr_filter_func,
+                            std::size_t max_fails = 0) const {
+    // Choice distribution
+    const std::size_t max_choice = (extended_ ? 1005 : 1000) - 1;
+    std::uniform_int_distribution<std::size_t> dist_choice(0, max_choice);
+
+    // Pid distribution
+    std::uniform_int_distribution<types::Pid> dist_pid(min_pid_, max_pid_);
+
+    // Addr distribution
+    auto chunk_min_addr = min_addr_;
+    auto chunk_max_addr = max_addr_;
+
+    if (ChunkSize() > 1 && HoleSize() > 1) {
+      std::size_t chunk_cnt =
+          for_each_AddrRange([](types::Addr a, types::Addr b) {});
+      std::size_t select_chunk =
+          std::uniform_int_distribution<std::size_t>(0, chunk_cnt - 1)(urng);
+
+      chunk_min_addr = min_addr_ + (select_chunk * HoleSize());
+      chunk_max_addr = chunk_min_addr + ChunkSize() - 1;
+
+      assert(chunk_min_addr >= min_addr_);
+      assert(chunk_max_addr <= max_addr_);
+    }
+
+    std::uniform_int_distribution<types::Addr> dist_addr(
+        chunk_min_addr, chunk_max_addr - EvtStateCats::kMaxOpSize);
+
+    // Sequence distribution
+    std::uniform_int_distribution<std::size_t> dist_sequence(1, max_sequence_);
+
+    // select op
+    const auto choice = dist_choice(urng);
+
+    // pid
+    const auto pid = dist_pid(urng);
+
+    // addr (lazy)
+    auto addr = [&]() {
+      types::Addr result = 0;
+
+      for (std::size_t tries = 0; tries < max_fails + 1; ++tries) {
+        result = dist_addr(urng);
+        result -= result % stride();
+        if (result < chunk_min_addr) result += stride();
+        assert(result >= chunk_min_addr);
+        assert(result <= chunk_max_addr - EvtStateCats::kMaxOpSize);
+
+        if (addr_filter_func(result)) {
+          return result;
+        }
+      }
+
+      return result;
+    };
+
+    // sequence (lazy)
+    auto sequence = [&dist_sequence, &urng]() { return dist_sequence(urng); };
+
+    if (choice < 500) {  // 50%
+      return std::make_shared<Read>(addr(), pid);
+    } else if (choice < 550) {  // 5%
+      return std::make_shared<ReadAddrDp>(addr(), pid);
+    } else if (choice < 970) {  // 42%
+      return std::make_shared<Write>(addr(), pid);
+    } else if (choice < 980) {  // 1%
+      return std::make_shared<ReadModifyWrite>(addr(), pid);
+    } else if (choice < 990) {  // 1%
+      return std::make_shared<CacheFlush>(addr(), pid);
+    } else if (choice < 1000) {  // 1%
+      return std::make_shared<Delay>(sequence(), pid);
+    } else if (extended_) {
+      // REAL_PERCENTAGE_OF_100 = PERC * (1000 / MAX_CHOICE)
+
+      if (choice < 1005) {  // 0.5%
+        auto min_a = addr();
+        // TODO(melver): do not hard-code stride
+        auto max_a = min_a + sequence() * 64;
+        if (max_a > max_addr()) {
+          max_a = max_addr();
+        }
+
+        return std::make_shared<ReadSequence>(min_a, max_a, pid);
+      }
+    }
+
+    // should never get here
+    assert(false);
+    return nullptr;
+  }
+
+  template <class URNG>
+  Operation::Ptr operator()(URNG &urng) const {
+    return (*this)(urng, [](types::Addr addr) { return true; });
+  }
+
+  types::Pid min_pid() const { return min_pid_; }
+
+  types::Pid max_pid() const { return max_pid_; }
+
+  types::Addr min_addr() const { return min_addr_; }
+
+  types::Addr max_addr() const { return max_addr_; }
+
+  std::size_t stride() const { return stride_ & ((1ULL << 16) - 1); }
+
+  std::size_t ChunkSize() const {
+    return 1ULL << ((stride_ & (0xffULL << 24)) >> 24);
+  }
+
+  std::size_t HoleSize() const {
+    return 1ULL << ((stride_ & (0xffULL << 16)) >> 16);
+  }
+
+  template <class Func>
+  std::size_t for_each_AddrRange(Func func) const {
+    if (ChunkSize() > 1 && HoleSize() > 1) {
+      assert(HoleSize() >= ChunkSize());
+      assert(ChunkSize() <= (max_addr_ - min_addr_ + 1));
+
+      std::size_t chunk_cnt = 0;
+
+      for (;; ++chunk_cnt) {
+        types::Addr min = min_addr_ + (chunk_cnt * HoleSize());
+        types::Addr max = min + ChunkSize() - 1;
+        if (max > max_addr_) break;
+
+        func(min, max);
+      }
+
+      return chunk_cnt;
+    }
+
+    func(min_addr_, max_addr_);
+    return 1;
+  }
+
+  std::size_t max_sequence() const { return max_sequence_; }
+
+  void set_max_sequence(std::size_t val) { max_sequence_ = val; }
+
+  bool extended() const { return extended_; }
+
+  void set_extended(bool val) { extended_ = val; }
+
+ private:
+  types::Pid min_pid_;
+  types::Pid max_pid_;
+  types::Addr min_addr_;
+  types::Addr max_addr_;
+  std::size_t stride_;
+  std::size_t max_sequence_;
+  bool extended_;
+};
+
+}  // namespace strong
+}  // namespace codegen
+}  // namespace mc2lib
+
+#endif /* MC2LIB_CODEGEN_OPS_STRONG_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/codegen/ops/x86_64.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/codegen/ops/x86_64.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,492 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_CODEGEN_OPS_X86_64_HPP_
+#define MC2LIB_CODEGEN_OPS_X86_64_HPP_
+
+#include <cstdint>
+
+#include "strong.hpp"
+
+namespace mc2lib {
+namespace codegen {
+namespace strong {
+
+struct Backend_X86_64 : Backend {
+  std::size_t Return(void *code, std::size_t len) const override;
+
+  std::size_t Delay(std::size_t length, void *code,
+                    std::size_t len) const override;
+
+  std::size_t Read(types::Addr addr, types::InstPtr start, void *code,
+                   std::size_t len, types::InstPtr *at) const override;
+
+  std::size_t ReadAddrDp(types::Addr addr, types::InstPtr start, void *code,
+                         std::size_t len, types::InstPtr *at) const override;
+
+  std::size_t Write(types::Addr addr, types::WriteID write_id,
+                    types::InstPtr start, void *code, std::size_t len,
+                    types::InstPtr *at) const override;
+
+  std::size_t ReadModifyWrite(types::Addr addr, types::WriteID write_id,
+                              types::InstPtr start, void *code, std::size_t len,
+                              types::InstPtr *at) const override;
+
+  std::size_t CacheFlush(types::Addr addr, void *code,
+                         std::size_t len) const override;
+};
+
+inline std::size_t Backend_X86_64::Return(void *code, std::size_t len) const {
+  assert(len >= 1);
+  // ASM> retq ;
+  *static_cast<char *>(code) = 0xc3;
+  return 1;
+}
+
+inline std::size_t Backend_X86_64::Delay(std::size_t length, void *code,
+                                         std::size_t len) const {
+  char *cnext = static_cast<char *>(code);
+
+  assert(len >= length);
+  for (std::size_t i = 0; i < length; ++i) {
+    // ASM> nop ;
+    *cnext++ = 0x90;
+  }
+
+  assert((cnext - static_cast<char *>(code)) ==
+         static_cast<std::ptrdiff_t>(length));
+  return length;
+}
+
+inline std::size_t Backend_X86_64::Read(types::Addr addr, types::InstPtr start,
+                                        void *code, std::size_t len,
+                                        types::InstPtr *at) const {
+  char *cnext = static_cast<char *>(code);
+  std::size_t expected_len = 0;
+
+  if (addr <= static_cast<types::Addr>(0xffffffff)) {
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @0> movzbl addr, %eax ;
+        expected_len = 8;
+        assert(len >= expected_len);
+        *at = start;
+
+        // @0
+        *cnext++ = 0x0f;
+        *cnext++ = 0xb6;
+        *cnext++ = 0x04;
+        *cnext++ = 0x25;
+        *reinterpret_cast<std::uint32_t *>(cnext) =
+            static_cast<std::uint32_t>(addr);
+        cnext += sizeof(std::uint32_t);
+        break;
+
+      default:
+        assert(false);
+    }
+  } else {
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @0> movabs addr, %al ;
+        expected_len = 9;
+        assert(len >= expected_len);
+        *at = start;
+
+        // @0
+        *cnext++ = 0xa0;
+        break;
+
+      case 2:
+        // ASM @0> movabs addr, %ax ;
+        expected_len = 10;
+        assert(len >= expected_len);
+        *at = start;
+
+        // @0
+        *cnext++ = 0x66;
+        *cnext++ = 0xa1;
+        break;
+
+      default:
+        assert(false);
+    }
+
+    *reinterpret_cast<std::uint64_t *>(cnext) =
+        static_cast<std::uint64_t>(addr);
+    cnext += sizeof(std::uint64_t);
+  }
+
+  assert((cnext - static_cast<char *>(code)) ==
+         static_cast<std::ptrdiff_t>(expected_len));
+  return expected_len;
+}
+
+inline std::size_t Backend_X86_64::ReadAddrDp(types::Addr addr,
+                                              types::InstPtr start, void *code,
+                                              std::size_t len,
+                                              types::InstPtr *at) const {
+  char *cnext = static_cast<char *>(code);
+  std::size_t expected_len = 0;
+
+  // ASM @0> xor %rax, %rax
+  expected_len = 3;
+  assert(len >= expected_len);
+
+  // @0
+  *cnext++ = 0x48;
+  *cnext++ = 0x31;
+  *cnext++ = 0xc0;
+
+  if (addr <= static_cast<types::Addr>(0xffffffff)) {
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @3> movzbl addr(%rax), %eax ;
+        expected_len = 10;
+        assert(len >= expected_len);
+        *at = start + 3;
+
+        // @3
+        *cnext++ = 0x0f;
+        *cnext++ = 0xb6;
+        *cnext++ = 0x80;
+        *reinterpret_cast<std::uint32_t *>(cnext) =
+            static_cast<std::uint32_t>(addr);
+        cnext += sizeof(std::uint32_t);
+        break;
+
+      default:
+        assert(false);
+    }
+  } else {
+    // ASM @03> movabs addr, %rdx ;
+    //     @0d> add %rdx, %rax ;
+    expected_len = 19;
+    assert(len >= expected_len);
+    *at = start + 0x10;
+
+    // @03
+    *cnext++ = 0x48;
+    *cnext++ = 0xba;
+    *reinterpret_cast<std::uint64_t *>(cnext) =
+        static_cast<std::uint64_t>(addr);
+    cnext += sizeof(std::uint64_t);
+
+    // @0d
+    *cnext++ = 0x48;
+    *cnext++ = 0x01;
+    *cnext++ = 0xd0;
+
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @10> movzbl (%rax), %eax ;
+        // @10
+        *cnext++ = 0x0f;
+        *cnext++ = 0xb6;
+        *cnext++ = 0x00;
+        break;
+
+      case 2:
+        // ASM @10> movzwl (%rax), %eax ;
+        // @10
+        *cnext++ = 0x0f;
+        *cnext++ = 0xb7;
+        *cnext++ = 0x00;
+        break;
+
+      default:
+        assert(false);
+    }
+  }
+
+  assert((cnext - static_cast<char *>(code)) ==
+         static_cast<std::ptrdiff_t>(expected_len));
+  return expected_len;
+}
+
+inline std::size_t Backend_X86_64::Write(types::Addr addr,
+                                         types::WriteID write_id,
+                                         types::InstPtr start, void *code,
+                                         std::size_t len,
+                                         types::InstPtr *at) const {
+  char *cnext = static_cast<char *>(code);
+  std::size_t expected_len = 0;
+
+  assert(write_id != 0);
+
+  if (addr <= static_cast<types::Addr>(0xffffffff)) {
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @0> movb write_id, addr ;
+        expected_len = 8;
+        assert(len >= expected_len);
+        *at = start;
+
+        // @0
+        *cnext++ = 0xc6;
+        *cnext++ = 0x04;
+        *cnext++ = 0x25;
+
+        *reinterpret_cast<std::uint32_t *>(cnext) =
+            static_cast<std::uint32_t>(addr);
+        cnext += sizeof(std::uint32_t);
+
+        *reinterpret_cast<types::WriteID *>(cnext) = write_id;
+        cnext += sizeof(types::WriteID);
+        break;
+
+      default:
+        assert(false);
+    }
+  } else {
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @0> movabs addr, %rax    ;
+        //     @a> movb write_id, (%rax) ;
+        expected_len = 13;
+        assert(len >= expected_len);
+        *at = start + 0xa;
+
+        // @0
+        *cnext++ = 0x48;
+        *cnext++ = 0xb8;
+        *reinterpret_cast<std::uint64_t *>(cnext) =
+            static_cast<std::uint64_t>(addr);
+        cnext += sizeof(std::uint64_t);
+
+        // @a
+        *cnext++ = 0xc6;
+        *cnext++ = 0x00;
+        *reinterpret_cast<types::WriteID *>(cnext) = write_id;
+        cnext += sizeof(types::WriteID);
+        break;
+
+      case 2:
+        // ASM @0> movabs addr, %rax ;
+        //     @a> mov write_id, %edx ;
+        //     @f> mov %dx, (%rax) ;
+        expected_len = 18;
+        assert(len >= expected_len);
+        *at = start + 0xf;
+
+        // @0
+        *cnext++ = 0x48;
+        *cnext++ = 0xb8;
+        *reinterpret_cast<std::uint64_t *>(cnext) =
+            static_cast<std::uint64_t>(addr);
+        cnext += sizeof(std::uint64_t);
+
+        // @a
+        *cnext++ = 0xba;
+        *reinterpret_cast<std::uint32_t *>(cnext) = write_id;
+        cnext += sizeof(std::uint32_t);
+
+        // @f
+        *cnext++ = 0x66;
+        *cnext++ = 0x89;
+        *cnext++ = 0x10;
+        break;
+
+      default:
+        assert(false);
+    }
+  }
+
+  assert((cnext - static_cast<char *>(code)) ==
+         static_cast<std::ptrdiff_t>(expected_len));
+  return expected_len;
+}
+
+inline std::size_t Backend_X86_64::ReadModifyWrite(types::Addr addr,
+                                                   types::WriteID write_id,
+                                                   types::InstPtr start,
+                                                   void *code, std::size_t len,
+                                                   types::InstPtr *at) const {
+  char *cnext = static_cast<char *>(code);
+  std::size_t expected_len = 0;
+
+  assert(write_id != 0);
+
+  switch (sizeof(types::WriteID)) {
+    case 1:
+      // ASM @0> mov write_id, %al
+      expected_len = 2;
+      assert(len >= expected_len);
+
+      // @0
+      *cnext++ = 0xb0;
+      *reinterpret_cast<types::WriteID *>(cnext) = write_id;
+      cnext += sizeof(types::WriteID);
+      break;
+
+    case 2:
+      // ASM @0> mov write_id, %eax
+      expected_len = 5;
+      assert(len >= expected_len);
+
+      // @0
+      *cnext++ = 0xb8;
+      *reinterpret_cast<std::uint32_t *>(cnext) = write_id;
+      cnext += sizeof(std::uint32_t);
+      break;
+
+    default:
+      assert(false);
+  }
+
+  if (addr <= static_cast<types::Addr>(0xffffffff)) {
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @2> mov addr, %edx
+        //     @7> lock xchg %al, (%rdx)
+        expected_len = 10;
+        assert(len >= expected_len);
+        *at = start + 0x7;
+
+        // @2
+        *cnext++ = 0xba;
+        *reinterpret_cast<std::uint32_t *>(cnext) =
+            static_cast<std::uint32_t>(addr);
+        cnext += sizeof(std::uint32_t);
+
+        // @7
+        *cnext++ = 0xf0;
+        *cnext++ = 0x86;
+        *cnext++ = 0x02;
+        break;
+
+      default:
+        assert(false);
+    }
+  } else {
+    switch (sizeof(types::WriteID)) {
+      case 1:
+        // ASM @2> movabs addr, %rdx ;
+        //     @c> lock xchg %al, (%rdx) ;
+        expected_len = 15;
+        assert(len >= expected_len);
+        *at = start + 0xc;
+
+        // @2
+        *cnext++ = 0x48;
+        *cnext++ = 0xba;
+        *reinterpret_cast<std::uint64_t *>(cnext) =
+            static_cast<std::uint64_t>(addr);
+        cnext += sizeof(std::uint64_t);
+
+        // @c
+        *cnext++ = 0xf0;
+        *cnext++ = 0x86;
+        *cnext++ = 0x02;
+        break;
+
+      case 2:
+        // ASM @5> movabs addr, %rdx ;
+        //     @f> lock xchg %ax, (%rdx) ;
+        expected_len = 19;
+        assert(len >= expected_len);
+        *at = start + 0xf;
+
+        // @2
+        *cnext++ = 0x48;
+        *cnext++ = 0xba;
+        *reinterpret_cast<std::uint64_t *>(cnext) =
+            static_cast<std::uint64_t>(addr);
+        cnext += sizeof(std::uint64_t);
+
+        // @c
+        *cnext++ = 0x66;
+        *cnext++ = 0xf0;
+        *cnext++ = 0x87;
+        *cnext++ = 0x02;
+        break;
+
+      default:
+        assert(false);
+    }
+  }
+
+  assert((cnext - static_cast<char *>(code)) ==
+         static_cast<std::ptrdiff_t>(expected_len));
+  return expected_len;
+}
+
+inline std::size_t Backend_X86_64::CacheFlush(types::Addr addr, void *code,
+                                              std::size_t len) const {
+  char *cnext = static_cast<char *>(code);
+  std::size_t expected_len = 0;
+
+  if (addr <= static_cast<types::Addr>(0xffffffff)) {
+    // ASM @0> clflush addr ;
+    expected_len = 8;
+    assert(len >= expected_len);
+
+    // @0
+    *cnext++ = 0x0f;
+    *cnext++ = 0xae;
+    *cnext++ = 0x3c;
+    *cnext++ = 0x25;
+    *reinterpret_cast<std::uint32_t *>(cnext) =
+        static_cast<std::uint32_t>(addr);
+    cnext += sizeof(std::uint32_t);
+  } else {
+    // ASM @0> mov addr, %rdx ;
+    //     @a> clflush (%rdx) ;
+    expected_len = 13;
+    assert(len >= expected_len);
+
+    // @0
+    *cnext++ = 0x48;
+    *cnext++ = 0xba;
+    *reinterpret_cast<std::uint64_t *>(cnext) =
+        static_cast<std::uint64_t>(addr);
+    cnext += sizeof(std::uint64_t);
+
+    // @a
+    *cnext++ = 0x0f;
+    *cnext++ = 0xae;
+    *cnext++ = 0x3a;
+  }
+
+  assert((cnext - static_cast<char *>(code)) ==
+         static_cast<std::ptrdiff_t>(expected_len));
+  return expected_len;
+}
+
+}  // namespace strong
+}  // namespace codegen
+}  // namespace mc2lib
+
+#endif /* MC2LIB_CODEGEN_OPS_X86_64_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/codegen/rit.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/codegen/rit.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,127 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_CODEGEN_RIT_HPP_
+#define MC2LIB_CODEGEN_RIT_HPP_
+
+#include <functional>
+#include <random>
+#include <vector>
+
+#include "../sets.hpp"
+#include "../simplega.hpp"
+#include "../types.hpp"
+
+namespace mc2lib {
+namespace codegen {
+
+template <class URNG, class OperationFactory>
+class RandInstTest
+    : public simplega::Genome<typename OperationFactory::ResultType::Ptr> {
+ public:
+  typedef typename OperationFactory::ResultType Operation;
+  typedef sets::Set<sets::Types<types::Addr, std::hash<types::Addr>>> AddrSet;
+
+  explicit RandInstTest(URNG& urng, const OperationFactory* factory,
+                        std::size_t len)
+      : urng_(urng), factory_(factory), fitness_(0.0f) {
+    this->genome_.resize(len);
+
+    for (auto& op_ptr : this->genome_) {
+      op_ptr = (*factory)(urng);
+    }
+  }
+
+  explicit RandInstTest(const RandInstTest& parent1,
+                        const RandInstTest& parent2,
+                        std::vector<typename Operation::Ptr> g)
+      : simplega::Genome<typename Operation::Ptr>(std::move(g)),
+        urng_(parent1.urng_),
+        factory_(parent1.factory_),
+        fitness_(0.0f) {}
+
+  void Mutate(float rate) override {
+    std::uniform_int_distribution<std::size_t> dist_idx(
+        0, this->genome_.size() - 1);
+    std::unordered_set<std::size_t> used;
+    std::size_t selection_count = static_cast<std::size_t>(
+        static_cast<float>(this->genome_.size()) * rate);
+
+    while (selection_count) {
+      auto idx = dist_idx(urng_);
+      if (used.find(idx) != used.end()) {
+        continue;
+      }
+
+      this->genome_[idx] = MakeRandom();
+
+      used.insert(idx);
+      --selection_count;
+    }
+  }
+
+  float Fitness() const override { return fitness_; }
+
+  void set_fitness(float fitness) { fitness_ = fitness; }
+
+  const AddrSet& fitaddrs() const { return fitaddrs_; }
+
+  AddrSet* fitaddrsptr() { return &fitaddrs_; }
+
+  typename Operation::Ptr MakeRandom() const { return (*factory_)(urng_); }
+
+  typename Operation::Ptr MakeRandom(const AddrSet& subset_addrs,
+                                     std::size_t max_tries = 1000) const {
+    return (*factory_)(urng_, [&subset_addrs](types::Addr addr) {
+      return subset_addrs.Contains(addr);
+    }, max_tries);
+  }
+
+  typename Operation::Threads threads() {
+    return ExtractThreads(this->GetPtr());
+  }
+
+ private:
+  URNG& urng_;
+  const OperationFactory* factory_;
+
+  float fitness_;
+  AddrSet fitaddrs_;
+};
+
+}  // namespace codegen
+}  // namespace mc2lib
+
+#endif /* MC2LIB_CODEGEN_RIT_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/mcversi.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/mcversi.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,185 @@
+/*
+ * Copyright (c) 2015-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_MCVERSI_HPP_
+#define MC2LIB_MCVERSI_HPP_
+
+#include <cassert>
+#include <cstddef>
+#include <random>
+
+#include "simplega.hpp"
+
+namespace mc2lib {
+
+/**
+ * @namespace mc2lib::mcversi
+ * @brief Implementations of algorithms from McVerSi paper.
+ */
+namespace mcversi {
+
+/**
+ * Crossover and mutation (Algorithm 1) from McVerSi paper.
+ */
+template <class URNG, class RandInstTest, class MemOperation>
+class CrossoverMutate {
+ public:
+  explicit CrossoverMutate(double P_USEL, double P_BFA)
+      : P_USEL_(P_USEL), P_BFA_(P_BFA) {}
+
+  void operator()(
+      URNG& urng, const RandInstTest& test1, const RandInstTest& test2,
+      float mutation_rate,
+      typename simplega::GenePool<RandInstTest>::Population* container) {
+    assert(test1.Get().size() == test2.Get().size());
+
+    // Probability with which we unconditionally select a particular gene. We
+    // don't always just want to pick fitaddr operations, as surrounding
+    // operations may contribute to coverage or other timing effects.
+    std::bernoulli_distribution mem_unconditional_select(P_USEL_);
+
+    const double faf1 = FitaddrFraction(test1);
+    const double faf2 = FitaddrFraction(test2);
+
+    // Same rate as selecting a memory-operation.
+    std::bernoulli_distribution nonmem_select1(faf1 + P_USEL_ -
+                                               (faf1 * P_USEL_));
+    std::bernoulli_distribution nonmem_select2(faf2 + P_USEL_ -
+                                               (faf2 * P_USEL_));
+
+    // Tiebreaker: If both are valid, pick one consistently and do not break up
+    // a good genome's dominant genes as they may interact in an imporant way.
+    const bool prefer_test2 = std::bernoulli_distribution(0.5)(urng);
+
+    // In case both operations are invalid, probability with which we make a
+    // new operation with the address-set restricted to fitaddrs.
+    std::bernoulli_distribution new_from_fitaddrs(P_BFA_);
+    const auto all_fitaddrs = test1.fitaddrs() | test2.fitaddrs();
+
+    auto child = test1.Get();
+    std::size_t mutations = 0;
+
+    for (std::size_t i = 0; i < child.size(); ++i) {
+      bool select1 = false;
+      bool select2 = false;
+
+      auto mem_op1 = dynamic_cast<MemOperation*>(test1.Get()[i].get());
+      auto mem_op2 = dynamic_cast<MemOperation*>(test2.Get()[i].get());
+
+      // Decide validity of genes
+      if (mem_op1 != nullptr) {
+        select1 = test1.fitaddrs().Contains(mem_op1->addr()) ||
+                  mem_unconditional_select(urng);
+      } else {
+        select1 = nonmem_select1(urng);
+      }
+
+      if (mem_op2 != nullptr) {
+        select2 = test2.fitaddrs().Contains(mem_op2->addr()) ||
+                  mem_unconditional_select(urng);
+      } else {
+        select2 = nonmem_select2(urng);
+      }
+
+      // Pick gene
+      if (select1 && select2) {
+        if (prefer_test2) {
+          child[i] = test2.Get()[i];
+        }
+      } else if (!select1 && select2) {
+        child[i] = test2.Get()[i];
+      } else if (!select1 && !select2) {
+        ++mutations;
+
+        if (new_from_fitaddrs(urng)) {
+          // Make new random operation, but only select from set of
+          // fitaddrs.
+          child[i] = test1.MakeRandom(all_fitaddrs);
+        } else {
+          // By deciding to discard fit addresses, we control where the
+          // tests mutate, so that in the initial phases the good
+          // operations do not get mutated away.
+          //
+          child[i] = test1.MakeRandom();
+        }
+      } else {
+        assert(select1);
+        // child[i] is valid, don't do anything.
+      }
+    }
+
+    auto result = RandInstTest(test1, test2, child);
+
+    float cur_mutation =
+        static_cast<float>(mutations) / static_cast<float>(child.size());
+    if (cur_mutation < mutation_rate) {
+      // cur_mutation is the fraction of newly generated instructions, i.e.
+      // replaced non-dominant genes. We must mutate full mutation_rate
+      // again, as newly generated instructions are considered for mutation
+      // as well (redundant).
+      result.Mutate(mutation_rate);
+    } else {
+      // No mutation neccessary.
+    }
+
+    container->push_back(std::move(result));
+  }
+
+ private:
+  double P_USEL_;
+  double P_BFA_;
+
+  double FitaddrFraction(const RandInstTest& rit) {
+    std::size_t mem_ops = 0;
+    std::size_t fitaddr_ops = 0;
+
+    for (const auto& op : rit.Get()) {
+      auto mem_op = dynamic_cast<MemOperation*>(op.get());
+      if (mem_op != nullptr) {
+        ++mem_ops;
+        if (rit.fitaddrs().Contains(mem_op->addr())) {
+          ++fitaddr_ops;
+        }
+      }
+    }
+
+    return static_cast<double>(fitaddr_ops) / static_cast<double>(mem_ops);
+  }
+};
+
+}  // namespace mcversi
+}  // namespace mc2lib
+
+#endif /* MCVERSI_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/memconsistency/cats.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/memconsistency/cats.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,618 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_MEMCONSISTENCY_CATS_HPP_
+#define MC2LIB_MEMCONSISTENCY_CATS_HPP_
+
+#include <memory>
+
+#include "eventsets.hpp"
+
+namespace mc2lib {
+namespace memconsistency {
+
+/**
+ * @namespace mc2lib::memconsistency::cats
+ * @brief Memory consistency model framework based on "Herding cats".
+ *
+ * This memory consistency model framework is based upon [1], and [2].
+ *
+ * [1] <a href="http://dx.doi.org/10.1145/2627752">
+ *      J. Alglave, L. Maranget, M.  Tautschnig, "Herding cats: Modelling,
+ *      Simulation, Testing, and Data Mining for Weak Memory", 2014.</a>
+ *
+ * [2] <a href="http://dx.doi.org/10.1007/s10703-011-0135-z">
+ *      J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. "Fences in weak
+ *      memory models", 2012.</a>
+*/
+namespace cats {
+
+class ExecWitness {
+ public:
+  template <class FilterFunc>
+  EventRel fr(FilterFunc filter_func) const {
+    EventRel er;
+
+    // Use of Raw() is justified, as we do not expect (according to wf_rf), the
+    // rf-relation to have any additional properties.
+    for (const auto& rf_tuples : rf.Raw()) {
+      const auto co_reach = co.Reachable(rf_tuples.first);
+      for (const auto& co_w : co_reach.Get()) {
+        for (const auto& rf_r : rf_tuples.second.Get()) {
+          if (filter_func(std::make_pair(rf_tuples.first, rf_r),
+                          std::make_pair(rf_tuples.first, co_w))) {
+            er.Insert(rf_r, co_w);
+          }
+        }
+      }
+    }
+
+    return er;
+  }
+
+  EventRel fr() const {
+    return fr([](const EventRel::Tuple& t1, const EventRel::Tuple& t2) {
+      return true;
+    });
+  }
+
+  EventRel fri() const {
+    return fr([](const EventRel::Tuple& t1, const EventRel::Tuple& t2) {
+      return t1.second.iiid.pid == t2.second.iiid.pid;
+    });
+  }
+
+  EventRel fre() const {
+    return fr([](const EventRel::Tuple& t1, const EventRel::Tuple& t2) {
+      return t1.second.iiid.pid != t2.second.iiid.pid;
+    });
+  }
+
+  EventRel rfi() const {
+    return rf.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid == e2.iiid.pid;
+    });
+  }
+
+  EventRel rfe() const {
+    return rf.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid != e2.iiid.pid;
+    });
+  }
+
+  EventRel coi() const {
+    return co.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid == e2.iiid.pid;
+    });
+  }
+
+  EventRel coe() const {
+    return co.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid != e2.iiid.pid;
+    });
+  }
+
+  EventRel com() const { return rf | co | fr(); }
+
+  EventRel po_loc() const {
+    return po.Filter(
+        [](const Event& e1, const Event& e2) { return e1.addr == e2.addr; });
+  }
+
+  void Clear() {
+    events.Clear();
+    po.Clear();
+    co.Clear();
+    rf.Clear();
+  }
+
+ public:
+  EventSet events;
+  EventRel po;
+  EventRel co;
+  EventRel rf;
+};
+
+class Checker;
+
+class Architecture {
+ public:
+  Architecture() : proxy_(this) {}
+
+  virtual ~Architecture() { assert(proxy_ == this); }
+
+  virtual void Clear() {}
+
+  /**
+   * Creates a checker compatible with this Architecture.
+   */
+  virtual std::unique_ptr<Checker> MakeChecker(
+      const Architecture* arch, const ExecWitness* exec) const = 0;
+
+  virtual EventRel ppo(const ExecWitness& ew) const = 0;
+  virtual EventRel fences(const ExecWitness& ew) const = 0;
+  virtual EventRel prop(const ExecWitness& ew) const = 0;
+
+  virtual EventRel hb(const ExecWitness& ew) const {
+    return ew.rfe() | proxy_->ppo(ew) | proxy_->fences(ew);
+  }
+
+  /**
+   * Should return the mask of all types that are classed as read.
+   */
+  virtual Event::Type EventTypeRead() const = 0;
+
+  /**
+   * Should return the mask of all types that are classed as write.
+   */
+  virtual Event::Type EventTypeWrite() const = 0;
+
+  void set_proxy(const Architecture* proxy) {
+    assert(proxy != nullptr);
+    proxy_ = proxy;
+  }
+
+ protected:
+  const Architecture* proxy_;
+};
+
+template <class ConcreteArch>
+class ArchProxy : public Architecture {
+ public:
+  explicit ArchProxy(ConcreteArch* arch)
+      : arch_(arch),
+        memoized_ppo_(false),
+        memoized_fences_(false),
+        memoized_prop_(false),
+        memoized_hb_(false) {
+    arch_->set_proxy(this);
+  }
+
+  ~ArchProxy() override { arch_->set_proxy(arch_); }
+
+  void Clear() override {
+    arch_->Clear();
+    memoized_ppo_ = false;
+    memoized_fences_ = false;
+    memoized_prop_ = false;
+    memoized_hb_ = false;
+  }
+
+  std::unique_ptr<Checker> MakeChecker(const Architecture* arch,
+                                       const ExecWitness* exec) const override {
+    return arch_->MakeChecker(arch, exec);
+  }
+
+  std::unique_ptr<Checker> MakeChecker(const ExecWitness* exec) const {
+    return MakeChecker(this, exec);
+  }
+
+  void Memoize(const ExecWitness& ew) {
+    // fences and ppo are likely used by hb and prop
+    fences_ = arch_->fences(ew);
+    memoized_fences_ = true;
+
+    ppo_ = arch_->ppo(ew);
+    memoized_ppo_ = true;
+
+    hb_ = arch_->hb(ew);
+    memoized_hb_ = true;
+
+    prop_ = arch_->prop(ew);
+    memoized_prop_ = true;
+  }
+
+  EventRel ppo(const ExecWitness& ew) const override {
+    return memoized_ppo_ ? ppo_ : arch_->ppo(ew);
+  }
+
+  EventRel fences(const ExecWitness& ew) const override {
+    return memoized_fences_ ? fences_ : arch_->fences(ew);
+  }
+
+  EventRel prop(const ExecWitness& ew) const override {
+    return memoized_prop_ ? prop_ : arch_->prop(ew);
+  }
+
+  EventRel hb(const ExecWitness& ew) const override {
+    return memoized_hb_ ? hb_ : arch_->hb(ew);
+  }
+
+  Event::Type EventTypeRead() const override { return arch_->EventTypeRead(); }
+
+  Event::Type EventTypeWrite() const override {
+    return arch_->EventTypeWrite();
+  }
+
+ protected:
+  ConcreteArch* arch_;
+
+  bool memoized_ppo_;
+  bool memoized_fences_;
+  bool memoized_prop_;
+  bool memoized_hb_;
+
+  EventRel ppo_;
+  EventRel fences_;
+  EventRel prop_;
+  EventRel hb_;
+};
+
+class Checker {
+ public:
+  Checker(const Architecture* arch, const ExecWitness* exec)
+      : arch_(arch), exec_(exec) {}
+
+  virtual ~Checker() {}
+
+  virtual void wf_rf() const {
+    EventSet reads;
+
+    for (const auto& tuples : exec_->rf.Raw()) {
+      if (!tuples.first.AnyType(arch_->EventTypeWrite())) {
+        throw Error("WF_RF_NOT_FROM_WRITE");
+      }
+
+      for (const auto& e : tuples.second.Get()) {
+        if (!e.AnyType(arch_->EventTypeRead()) || tuples.first.addr != e.addr) {
+          throw Error("WF_RF_NOT_SAME_LOC");
+        }
+
+        // For every read, there exists only 1 source!
+        if (reads.Contains(e)) {
+          throw Error("WF_RF_MULTI_SOURCE");
+        }
+        reads.Insert(e);
+      }
+    }
+  }
+
+  virtual void wf_co() const {
+    std::unordered_set<types::Addr> addrs;
+
+    // Assert writes ordered captured in ws are to the same location.
+    for (const auto& tuples : exec_->co.Raw()) {
+      addrs.insert(tuples.first.addr);
+
+      for (const auto& e : tuples.second.Get()) {
+        if (tuples.first.addr != e.addr) {
+          throw Error("WF_CO_NOT_SAME_LOC");
+        }
+      }
+    }
+
+    auto writes = exec_->events.Filter(
+        [&](const Event& e) { return e.AnyType(arch_->EventTypeWrite()); });
+    if (!exec_->co.StrictPartialOrder(writes)) {
+      throw Error("WF_CO_NOT_STRICT_PARTIAL_ORDER");
+    }
+
+    for (const auto& addr : addrs) {
+      auto same_addr_writes =
+          writes.Filter([&](const Event& e) { return e.addr == addr; });
+      if (!exec_->co.ConnexOn(same_addr_writes)) {
+        throw Error("WF_CO_NOT_CONNEX");
+      }
+    }
+  }
+
+  virtual void wf() const {
+    wf_rf();
+    wf_co();
+  }
+
+  virtual bool sc_per_location(EventRel::Path* cyclic = nullptr) const {
+    return (exec_->com() | exec_->po_loc()).Acyclic(cyclic);
+  }
+
+  virtual bool no_thin_air(EventRel::Path* cyclic = nullptr) const {
+    return arch_->hb(*exec_).Acyclic(cyclic);
+  }
+
+  virtual bool observation(EventRel::Path* cyclic = nullptr) const {
+    const EventRel prop = arch_->prop(*exec_);
+    const EventRel hbstar =
+        arch_->hb(*exec_).set_props(EventRel::kReflexiveTransitiveClosure);
+
+    // Not eval'ing hbstar causes performance to degrade substantially, as
+    // EventRelSeq recomputes reachability from nodes from prop to hbstar
+    // several times!
+    bool r = EventRelSeq({exec_->fre(), prop, hbstar.Eval()}).Irreflexive();
+
+    if (!r && cyclic != nullptr) {
+      // However, here we want hbstar unevald, as otherwise the graph is
+      // too collapsed.
+      EventRelSeq({exec_->fre(), prop, hbstar}).Irreflexive(cyclic);
+    }
+
+    return r;
+  }
+
+  virtual bool propagation(EventRel::Path* cyclic = nullptr) const {
+    return (exec_->co | arch_->prop(*exec_)).Acyclic(cyclic);
+  }
+
+  virtual void valid_exec(EventRel::Path* cyclic = nullptr) const {
+    wf();
+
+    if (!sc_per_location(cyclic)) {
+      throw Error("SC_PER_LOCATION");
+    }
+
+    if (!no_thin_air(cyclic)) {
+      throw Error("NO_THIN_AIR");
+    }
+
+    if (!observation(cyclic)) {
+      throw Error("OBSERVATION");
+    }
+
+    if (!propagation(cyclic)) {
+      throw Error("PROPAGATION");
+    }
+  }
+
+ protected:
+  const Architecture* arch_;
+  const ExecWitness* exec_;
+};
+
+/*
+=============================
+Some common memory models.
+=============================
+*/
+
+class Arch_SC : public Architecture {
+ public:
+  std::unique_ptr<Checker> MakeChecker(const Architecture* arch,
+                                       const ExecWitness* exec) const override {
+    return std::unique_ptr<Checker>(new Checker(arch, exec));
+  }
+
+  EventRel ppo(const ExecWitness& ew) const override {
+    assert(ew.po.Transitive());
+    return ew.po.Eval();
+  }
+
+  EventRel fences(const ExecWitness& ew) const override { return EventRel(); }
+
+  EventRel prop(const ExecWitness& ew) const override {
+    return proxy_->ppo(ew) | proxy_->fences(ew) | ew.rf | ew.fr();
+  }
+
+  Event::Type EventTypeRead() const override { return Event::kRead; }
+
+  Event::Type EventTypeWrite() const override { return Event::kWrite; }
+};
+
+class Arch_TSO : public Architecture {
+ public:
+  void Clear() override { mfence.Clear(); }
+
+  std::unique_ptr<Checker> MakeChecker(const Architecture* arch,
+                                       const ExecWitness* exec) const override {
+    return std::unique_ptr<Checker>(new Checker(arch, exec));
+  }
+
+  EventRel ppo(const ExecWitness& ew) const override {
+    assert(ew.po.Transitive());
+    return ew.po.Filter([](const Event& e1, const Event& e2) {
+      return !e1.AllType(Event::kWrite) || !e2.AllType(Event::kRead);
+    });
+  }
+
+  EventRel fences(const ExecWitness& ew) const override {
+    if (mfence.empty()) {
+      return mfence;
+    }
+
+    // Filter postar by only those events which are possibly relevent.
+    const auto postar =
+        ew.po.Filter([&](const Event& e1, const Event& e2) {
+               // Only include those where first event is write or second
+               // is a read, all other are included in po regardless.
+               return e1.AllType(Event::kWrite) || e2.AllType(Event::kRead);
+             })
+            .set_props(EventRel::kReflexiveClosure);
+
+    return EventRelSeq({postar, mfence, postar}).EvalClear();
+  }
+
+  EventRel prop(const ExecWitness& ew) const override {
+    return proxy_->ppo(ew) | proxy_->fences(ew) | ew.rfe() | ew.fr();
+  }
+
+  Event::Type EventTypeRead() const override { return Event::kRead; }
+
+  Event::Type EventTypeWrite() const override { return Event::kWrite; }
+
+ public:
+  EventRel mfence;
+};
+
+/**
+ * ARMv7 as defined in [1]
+ */
+class Arch_ARMv7 : public Architecture {
+ public:
+  Arch_ARMv7() { dd_reg.set_props(EventRel::kTransitiveClosure); }
+
+  void Clear() override {
+    dd_reg.Clear();
+    dsb.Clear();
+    dmb.Clear();
+    dsb_st.Clear();
+    dmb_st.Clear();
+    isb.Clear();
+  }
+
+  std::unique_ptr<Checker> MakeChecker(const Architecture* arch,
+                                       const ExecWitness* exec) const override {
+    return std::unique_ptr<Checker>(new Checker(arch, exec));
+  }
+
+  EventRel ppo(const ExecWitness& ew) const override {
+    assert(ew.po.Transitive());
+    assert(dd_reg.SubsetEq(ew.po));
+
+    // 1. Obtain dependencies
+    //
+    EventRel addr, data, ctrl_part;
+    dd_reg.for_each(
+        [&addr, &data, &ctrl_part, this](const Event& e1, const Event& e2) {
+          if (!e1.AnyType(EventTypeRead())) {
+            return;
+          }
+
+          if (e2.AnyType(Event::kMemoryOperation)) {
+            if (e2.AllType(Event::kRegInAddr)) {
+              addr.Insert(e1, e2);
+            }
+
+            if (e2.AllType(Event::kRegInData)) {
+              data.Insert(e1, e2);
+            }
+          }
+
+          if (e2.AllType(Event::kBranch)) {
+            ctrl_part.Insert(e1, e2);
+          }
+        });
+
+    EventRel ctrl = EventRelSeq({ctrl_part, ew.po}).EvalClear();
+    EventRel ctrl_cfence = EventRelSeq({ctrl_part, isb}).EvalClear();
+
+    // 2. Compute helper relations
+    //
+    const auto po_loc = ew.po_loc();
+    const auto rfe = ew.rfe();
+    EventRel dd = addr | data;
+    EventRel rdw = po_loc & EventRelSeq({ew.fre(), rfe}).EvalClear();
+    EventRel detour = po_loc & EventRelSeq({ew.coe(), rfe}).EvalClear();
+    EventRel addrpo = EventRelSeq({addr, ew.po}).EvalClear();
+
+    // 3. Compute ppo
+    //
+    // Init
+    EventRel ci = ctrl_cfence | detour;
+    EventRel ii = dd | ew.rfi() | rdw;
+    EventRel cc = dd | ctrl | addrpo | po_loc;
+    EventRel ic;
+
+    std::size_t total_size = ci.size() + ii.size() + cc.size() + ic.size();
+    std::size_t prev_total_size;
+
+    // Fix-point computation
+    do {
+      prev_total_size = total_size;
+
+      ci |=
+          EventRelSeq({ci, ii}).EvalClear() | EventRelSeq({cc, ci}).EvalClear();
+
+      ii |= ci | EventRelSeq({ic, ci}).EvalClear() |
+            EventRelSeq({ii, ii}).EvalClear();
+
+      cc |= ci | EventRelSeq({ci, ic}).EvalClear() |
+            EventRelSeq({cc, cc}).EvalClear();
+
+      ic |= ii | cc | EventRelSeq({ic, cc}).EvalClear() |
+            EventRelSeq({ii, ic}).EvalClear();
+
+      total_size = ci.size() + ii.size() + cc.size() + ic.size();
+      assert(prev_total_size <= total_size);
+    } while (total_size != prev_total_size);
+
+    EventRel result = ic.Filter([this](const Event& e1, const Event& e2) {
+      return e1.AnyType(EventTypeRead()) && e2.AnyType(EventTypeWrite());
+    });
+    result |= ii.Filter([this](const Event& e1, const Event& e2) {
+      return e1.AnyType(EventTypeRead()) && e2.AnyType(EventTypeRead());
+    });
+
+    return result;
+  }
+
+  // Ensure fences is transitive
+  EventRel fences(const ExecWitness& ew) const override {
+    const auto postar = ew.po.Eval().set_props(EventRel::kReflexiveClosure);
+    const auto postar_WW = postar.Filter([&](const Event& e1, const Event& e2) {
+      return e1.AllType(Event::kWrite) && e2.AllType(Event::kWrite);
+    });
+
+    auto ff = EventRelSeq({postar, (dmb | dsb), postar}).EvalClear();
+    ff |= EventRelSeq({postar_WW, (dmb_st | dsb_st), postar_WW}).EvalClear();
+    return ff;
+  }
+
+  EventRel prop(const ExecWitness& ew) const override {
+    EventRel hbstar = proxy_->hb(ew)
+                          .set_props(EventRel::kReflexiveTransitiveClosure)
+                          .EvalInplace();
+    EventRel A_cumul = EventRelSeq({ew.rfe(), proxy_->fences(ew)}).EvalClear();
+    EventRel propbase =
+        EventRelSeq({(proxy_->fences(ew) | A_cumul), hbstar}).EvalClear();
+
+    EventRel comstar = ew.com().set_props(EventRel::kReflexiveClosure);
+
+    EventRel result = propbase.Filter([this](const Event& e1, const Event& e2) {
+      return e1.AnyType(EventTypeWrite()) && e2.AnyType(EventTypeWrite());
+    });
+
+    propbase.set_props(EventRel::kReflexiveTransitiveClosure).EvalInplace();
+    result |=
+        EventRelSeq({comstar, propbase /*star*/, proxy_->fences(ew), hbstar})
+            .EvalClear();
+    return result;
+  }
+
+  Event::Type EventTypeRead() const override { return Event::kRead; }
+
+  Event::Type EventTypeWrite() const override { return Event::kWrite; }
+
+ public:
+  EventRel dd_reg;
+  EventRel dsb;
+  EventRel dmb;
+  EventRel dsb_st;
+  EventRel dmb_st;
+  EventRel isb;
+};
+
+}  // namespace cats
+}  // namespace memconsistency
+}  // namespace mc2lib
+
+#endif /* MEMCONSISTENCY_CATS_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/memconsistency/eventsets.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/memconsistency/eventsets.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,244 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_MEMCONSISTENCY_EVENTSETS_HPP_
+#define MC2LIB_MEMCONSISTENCY_EVENTSETS_HPP_
+
+#include <iomanip>
+#include <sstream>
+#include <stdexcept>
+#include <string>
+
+#include "../sets.hpp"
+#include "../types.hpp"
+
+namespace mc2lib {
+
+/**
+ * @namespace mc2lib::memconsistency
+ * @brief Various formal models for expressing memory consistency semantics.
+ */
+namespace memconsistency {
+
+class Iiid {
+ public:
+  struct Hash {
+    typedef std::hash<types::Poi>::result_type result_type;
+    result_type operator()(const Iiid& k) const {
+      return std::hash<types::Poi>()(k.poi);
+    }
+  };
+
+  Iiid() : pid(0), poi(0) {}
+
+  Iiid(types::Pid pid_, types::Poi poi_) : pid(pid_), poi(poi_) {}
+
+  operator std::string() const {
+    std::ostringstream oss;
+    oss << "P" << std::setfill('0') << std::setw(2) << pid << ": "
+        << std::setfill('0') << std::setw(sizeof(types::Poi) * 2) << std::hex
+        << poi;
+    return oss.str();
+  }
+
+  bool operator==(const Iiid& rhs) const {
+    return pid == rhs.pid && poi == rhs.poi;
+  }
+
+  bool operator!=(const Iiid& rhs) const {
+    return pid != rhs.pid || poi != rhs.poi;
+  }
+
+  bool operator<(const Iiid& rhs) const {
+    return pid < rhs.pid || (pid == rhs.pid && poi < rhs.poi);
+  }
+
+  Iiid& operator++() {
+    ++poi;
+    return *this;
+  }
+
+  Iiid Next() const { return Iiid(pid, poi + 1); }
+
+  Iiid Prev() const {
+    assert(poi > 0);
+    return Iiid(pid, poi - 1);
+  }
+
+ public:
+  types::Pid pid;
+  types::Poi poi;
+};
+
+class Event {
+ public:
+  struct Hash {
+    Iiid::Hash::result_type operator()(const Event& k) const {
+      return Iiid::Hash()(k.iiid);
+    }
+  };
+
+  typedef std::uint32_t Type;
+
+  // TYPE DEFINITIONS {{{
+
+  static constexpr Type kNone = 0x00000000;
+
+  // Memory operations
+  static constexpr Type kRead = 0x00000001;
+  static constexpr Type kWrite = 0x00000002;
+  static constexpr Type kAcquire = 0x00000004;
+  static constexpr Type kRelease = 0x00000008;
+  static constexpr Type kMemoryOperation = kRead | kWrite | kAcquire | kRelease;
+
+  // Auxiliary attributes
+  static constexpr Type kRegInAddr = 0x00000010;
+  static constexpr Type kRegInData = 0x00000020;
+  static constexpr Type kRegOut = 0x00000040;
+  static constexpr Type kBranch = 0x00000080;
+
+  // User declared attributes
+  static constexpr Type kNext = 0x00000100;
+
+  // }}}
+
+  Event() : addr(0), type(kNone) {}
+
+  Event(Type type_, types::Addr addr_, const Iiid& iiid_)
+      : addr(addr_), type(type_), iiid(iiid_) {}
+
+  operator std::string() const {
+    std::ostringstream oss;
+    oss << "[" << static_cast<std::string>(iiid) << "] ";
+
+    std::ostringstream memtype;
+
+    if (type == kNone) {
+      memtype << "None";
+    } else {
+      bool found_type = false;
+
+      if (AllType(kRead)) {
+        memtype << "Read";
+        found_type = true;
+      }
+
+      if (AllType(kWrite)) {
+        memtype << (found_type ? "|" : "") << "Write";
+        found_type = true;
+      }
+
+      if (AllType(kAcquire)) {
+        memtype << (found_type ? "|" : "") << "Acquire";
+        found_type = true;
+      }
+
+      if (AllType(kRelease)) {
+        memtype << (found_type ? "|" : "") << "Release";
+        found_type = true;
+      }
+
+      if (AllType(kRegInAddr)) {
+        memtype << (found_type ? "|" : "") << "RegInAddr";
+        found_type = true;
+      }
+
+      if (AllType(kRegInData)) {
+        memtype << (found_type ? "|" : "") << "RegInData";
+        found_type = true;
+      }
+
+      if (AllType(kRegOut)) {
+        memtype << (found_type ? "|" : "") << "RegOut";
+        found_type = true;
+      }
+
+      if (AllType(kBranch)) {
+        memtype << (found_type ? "|" : "") << "Branch";
+        // found_type = true;
+      }
+    }
+
+    oss << std::setfill(' ') << std::setw(8) << memtype.str() << " @ "
+        << std::hex << addr;
+    return oss.str();
+  }
+
+  bool operator==(const Event& rhs) const {
+    return type == rhs.type && addr == rhs.addr && iiid == rhs.iiid;
+  }
+
+  bool operator!=(const Event& rhs) const {
+    return type != rhs.type || addr != rhs.addr || iiid != rhs.iiid;
+  }
+
+  // This function in no way says anything about event ordering. Used for
+  // ordered map.
+  bool operator<(const Event& rhs) const { return iiid < rhs.iiid; }
+
+  bool AllType(Type type_mask) const {
+    return sets::AllBitmask(type, type_mask);
+  }
+
+  bool AnyType(Type type_mask) const {
+    return sets::AnyBitmask(type, type_mask);
+  }
+
+ public:
+  types::Addr addr;
+  Type type;
+  Iiid iiid;
+};
+
+typedef sets::Set<sets::Types<Event>> EventSet;
+typedef sets::Relation<sets::Types<Event>> EventRel;
+typedef sets::RelationSeq<sets::Types<Event>> EventRelSeq;
+
+class Error : public std::logic_error {
+ public:
+#if 0
+  // constructor inheritance not supported by gcc 4.7
+  using std::logic_error::logic_error;
+#else
+  explicit Error(const std::string& what_arg) : std::logic_error(what_arg) {}
+
+  explicit Error(const char* what_arg) : std::logic_error(what_arg) {}
+#endif
+};
+
+}  // namespace memconsistency
+}  // namespace mc2lib
+
+#endif /* MEMCONSISTENCY_EVENTSETS_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/memconsistency/model12.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/memconsistency/model12.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,347 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_MEMCONSISTENCY_MODEL12_HPP_
+#define MC2LIB_MEMCONSISTENCY_MODEL12_HPP_
+
+#include <memory>
+
+#include "eventsets.hpp"
+
+namespace mc2lib {
+namespace memconsistency {
+
+/**
+ * @namespace mc2lib::memconsistency::model12
+ * @brief Memory consistency model framework based on 2012 FMSD paper.
+ *
+ * This memory consistency model framework is based upon [1].
+ *
+ * [1] <a href="http://dx.doi.org/10.1007/s10703-011-0135-z">
+ *      J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. "Fences in weak
+ *      memory models", 2012.</a>
+*/
+namespace model12 {
+
+class ExecWitness {
+ public:
+  template <class FilterFunc>
+  EventRel fr(FilterFunc filter_func) const {
+    EventRel er;
+
+    for (const auto& rf_tuples : rf.Raw()) {
+      const auto ws_reach = ws.Reachable(rf_tuples.first);
+      for (const auto& ws_w : ws_reach.Get()) {
+        for (const auto& rf_r : rf_tuples.second.Get()) {
+          if (filter_func(std::make_pair(rf_tuples.first, rf_r),
+                          std::make_pair(rf_tuples.first, ws_w))) {
+            er.Insert(rf_r, ws_w);
+          }
+        }
+      }
+    }
+
+    return er;
+  }
+
+  EventRel fr() const {
+    return fr([](const EventRel::Tuple& t1, const EventRel::Tuple& t2) {
+      return true;
+    });
+  }
+
+  EventRel fri() const {
+    return fr([](const EventRel::Tuple& t1, const EventRel::Tuple& t2) {
+      return t1.second.iiid.pid == t2.second.iiid.pid;
+    });
+  }
+
+  EventRel fre() const {
+    return fr([](const EventRel::Tuple& t1, const EventRel::Tuple& t2) {
+      return t1.second.iiid.pid != t2.second.iiid.pid;
+    });
+  }
+
+  EventRel rfi() const {
+    return rf.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid == e2.iiid.pid;
+    });
+  }
+
+  EventRel rfe() const {
+    return rf.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid != e2.iiid.pid;
+    });
+  }
+
+  EventRel wsi() const {
+    return ws.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid == e2.iiid.pid;
+    });
+  }
+
+  EventRel wse() const {
+    return ws.Filter([](const Event& e1, const Event& e2) {
+      return e1.iiid.pid != e2.iiid.pid;
+    });
+  }
+
+  EventRel com() const { return rf | ws | fr(); }
+
+  EventRel po_loc() const {
+    return po.Filter(
+        [](const Event& e1, const Event& e2) { return e1.addr == e2.addr; });
+  }
+
+  void Clear() {
+    events.Clear();
+    po.Clear();
+    dp.Clear();
+    rf.Clear();
+    ws.Clear();
+  }
+
+ public:
+  EventSet events;
+  EventRel po;
+  EventRel dp;
+  EventRel rf;
+  EventRel ws;
+};
+
+class Checker;
+
+class Architecture {
+ public:
+  virtual ~Architecture() {}
+
+  virtual void Clear() {}
+
+  /**
+   * Creates a checker compatible with this Architecture.
+   */
+  virtual std::unique_ptr<Checker> MakeChecker(
+      const Architecture* arch, const ExecWitness* exec) const = 0;
+
+  virtual EventRel ppo(const ExecWitness& ew) const = 0;
+  virtual EventRel grf(const ExecWitness& ew) const = 0;
+  virtual EventRel ab(const ExecWitness& ew) const = 0;
+
+  virtual EventRel ghb(const ExecWitness& ew) const {
+    return ew.ws | ew.fr() | ppo(ew) | grf(ew) | ab(ew);
+  }
+
+  /**
+   * Should return the mask of all types that are classed as read.
+   */
+  virtual Event::Type EventTypeRead() const = 0;
+
+  /**
+   * Should return the mask of all types that are classed as write.
+   */
+  virtual Event::Type EventTypeWrite() const = 0;
+};
+
+class Checker {
+ public:
+  Checker(const Architecture* arch, const ExecWitness* exec)
+      : arch_(arch), exec_(exec) {}
+
+  virtual ~Checker() {}
+
+  virtual void wf_rf() const {
+    EventSet reads;
+
+    for (const auto& tuples : exec_->rf.Raw()) {
+      if (!tuples.first.AnyType(arch_->EventTypeWrite())) {
+        throw Error("WF_RF_NOT_FROM_WRITE");
+      }
+
+      for (const auto& e : tuples.second.Get()) {
+        if (!e.AnyType(arch_->EventTypeRead()) || tuples.first.addr != e.addr) {
+          throw Error("WF_RF_NOT_SAME_LOC");
+        }
+
+        // For every read, there exists only 1 source!
+        if (reads.Contains(e)) {
+          throw Error("WF_RF_MULTI_SOURCE");
+        }
+        reads.Insert(e);
+      }
+    }
+  }
+
+  virtual void wf_ws() const {
+    std::unordered_set<types::Addr> addrs;
+
+    // Assert writes ordered captured in ws are to the same location.
+    for (const auto& tuples : exec_->ws.Raw()) {
+      addrs.insert(tuples.first.addr);
+
+      for (const auto& e : tuples.second.Get()) {
+        if (tuples.first.addr != e.addr) {
+          throw Error("WF_WS_NOT_SAME_LOC");
+        }
+      }
+    }
+
+    auto writes = exec_->events.Filter(
+        [&](const Event& e) { return e.AnyType(arch_->EventTypeWrite()); });
+    if (!exec_->ws.StrictPartialOrder(writes)) {
+      throw Error("WF_WS_NOT_STRICT_PARTIAL_ORDER");
+    }
+
+    for (const auto& addr : addrs) {
+      auto same_addr_writes =
+          writes.Filter([&](const Event& e) { return e.addr == addr; });
+      if (!exec_->ws.ConnexOn(same_addr_writes)) {
+        throw Error("WF_WS_NOT_CONNEX");
+      }
+    }
+  }
+
+  virtual void wf() const {
+    wf_rf();
+    wf_ws();
+  }
+
+  virtual bool uniproc(EventRel::Path* cyclic = nullptr) const {
+    return (exec_->com() | exec_->po_loc()).Acyclic(cyclic);
+  }
+
+  virtual bool thin(EventRel::Path* cyclic = nullptr) const {
+    return (exec_->rf | exec_->dp).Acyclic(cyclic);
+  }
+
+  virtual bool check_exec(EventRel::Path* cyclic = nullptr) const {
+    return arch_->ghb(*exec_).Acyclic(cyclic);
+  }
+
+  virtual void valid_exec(EventRel::Path* cyclic = nullptr) const {
+    wf();
+
+    if (!uniproc(cyclic)) {
+      throw Error("UNIPROC");
+    }
+
+    if (!thin(cyclic)) {
+      throw Error("THIN");
+    }
+
+    if (!check_exec(cyclic)) {
+      throw Error("CHECK_EXEC");
+    }
+  }
+
+ protected:
+  const Architecture* arch_;
+  const ExecWitness* exec_;
+};
+
+/*
+=============================
+Some common memory models.
+=============================
+*/
+
+class Arch_SC : public Architecture {
+ public:
+  std::unique_ptr<Checker> MakeChecker(const Architecture* arch,
+                                       const ExecWitness* exec) const override {
+    return std::unique_ptr<Checker>(new Checker(arch, exec));
+  }
+
+  EventRel ppo(const ExecWitness& ew) const override {
+    assert(ew.po.Transitive());
+    return ew.po.Eval();
+  }
+
+  EventRel grf(const ExecWitness& ew) const override { return ew.rf; }
+
+  EventRel ab(const ExecWitness& ew) const override { return EventRel(); }
+
+  Event::Type EventTypeRead() const override { return Event::kRead; }
+
+  Event::Type EventTypeWrite() const override { return Event::kWrite; }
+};
+
+class Arch_TSO : public Architecture {
+ public:
+  void Clear() override { mfence.Clear(); }
+
+  std::unique_ptr<Checker> MakeChecker(const Architecture* arch,
+                                       const ExecWitness* exec) const override {
+    return std::unique_ptr<Checker>(new Checker(arch, exec));
+  }
+
+  EventRel ppo(const ExecWitness& ew) const override {
+    assert(ew.po.Transitive());
+    return ew.po.Filter([](const Event& e1, const Event& e2) {
+      return !e1.AllType(Event::kWrite) || !e2.AllType(Event::kRead);
+    });
+  }
+
+  EventRel grf(const ExecWitness& ew) const override { return ew.rfe(); }
+
+  EventRel ab(const ExecWitness& ew) const override {
+    if (mfence.empty()) {
+      return mfence;
+    }
+
+    // Filter postar by only those events which are possibly relevent.
+    const auto postar =
+        ew.po.Filter([&](const Event& e1, const Event& e2) {
+               // Only include those where first event is write or second
+               // is a read, all other are included in po regardless.
+               return e1.AllType(Event::kWrite) || e2.AllType(Event::kRead);
+             })
+            .set_props(EventRel::kReflexiveClosure);
+
+    return EventRelSeq({postar, mfence, postar}).EvalClear();
+  }
+
+  Event::Type EventTypeRead() const override { return Event::kRead; }
+
+  Event::Type EventTypeWrite() const override { return Event::kWrite; }
+
+ public:
+  EventRel mfence;
+};
+
+}  // namespace model12
+}  // namespace memconsistency
+}  // namespace mc2lib
+
+#endif /* MEMCONSISTENCY_MODEL12_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/sets.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/sets.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,1523 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_SETS_HPP_
+#define MC2LIB_SETS_HPP_
+
+#include <cassert>
+#include <cstddef>
+#include <unordered_map>
+#include <unordered_set>
+#include <utility>
+#include <vector>
+
+namespace mc2lib {
+
+/**
+ * @namespace mc2lib::sets
+ * @brief Sets and maps exposed in a restricted set of set theory.
+ */
+namespace sets {
+
+/**
+ * Checks that a bit mask has all given bits set.
+ *
+ * @param mask Bit mask to check.
+ * @param all Bit mask to check against.
+ * @return True if all bits in all are also set in mask, false otherwise.
+ */
+template <class T>
+inline bool AllBitmask(T mask, T all) {
+  assert(all != 0);
+  return (mask & all) == all;
+}
+
+/**
+ * Checks that a bit mask has any of given bits set.
+ *
+ * @param mask Bit mask to check.
+ * @param any Bit mask to check against.
+ * @return True if at least any one of the bits in any is set in mask.
+ */
+template <class T>
+inline bool AnyBitmask(T mask, T any) {
+  assert(any != 0);
+  return (mask & any) != 0;
+}
+
+/**
+ * @brief Abstracts over container library's set implementation.
+ *
+ * Provides additional functions and operators not provided in the standard
+ * library.
+ */
+template <class Ts>
+class Set {
+ public:
+  typedef typename Ts::Element Element;
+  typedef typename Ts::SetContainer Container;
+
+  Set() {}
+
+  explicit Set(Container s) : set_(std::move(s)) {}
+
+  /**
+   * Provide access to underlying container.
+   *
+   * @return Reference to underlying container.
+   */
+  const Container& Get() const { return set_; }
+
+  bool operator==(const Set& rhs) const { return set_ == rhs.set_; }
+
+  bool operator!=(const Set& rhs) const { return set_ != rhs.set_; }
+
+  /**
+   * Insert element.
+   *
+   * @param e Element to be inserted.
+   * @param assert_unique Assert that element does not exist in container.
+   * @return Reference to inserted Element.
+   */
+  const Element& Insert(const Element& e, bool assert_unique = false) {
+    auto result = set_.insert(e);
+    assert(!assert_unique || result.second);
+    return *result.first;
+  }
+
+  /**
+   * Insert element.
+   *
+   * @param e Element to be inserted.
+   * @param assert_unique Assert that element does not exist in container.
+   * @return Reference to inserted Element.
+   */
+  const Element& Insert(Element&& e, bool assert_unique = false) {
+    auto result = set_.emplace(std::move(e));
+    assert(!assert_unique || result.second);
+    return *result.first;
+  }
+
+  /**
+   * Erase element.
+   *
+   * @param e Element to be erased.
+   * @param assert_exists Assert that element exists.
+   */
+  bool Erase(const Element& e, bool assert_exists = false) {
+    auto result = set_.erase(e);
+    assert(!assert_exists || result != 0);
+    return result != 0;
+  }
+
+  template <class FilterFunc>
+  Set Filter(FilterFunc filterFunc) const {
+    Set res;
+
+    for (const auto& e : set_) {
+      if (filterFunc(e)) {
+        res.Insert(e);
+      }
+    }
+
+    return res;
+  }
+
+  void Clear() { set_.clear(); }
+
+  bool Contains(const Element& e) const { return set_.find(e) != set_.end(); }
+
+  /**
+   * Set union.
+   */
+  Set& operator|=(const Set& rhs) {
+    if (this != &rhs) {
+      set_.insert(rhs.set_.begin(), rhs.set_.end());
+    }
+
+    return *this;
+  }
+
+  Set& operator|=(Set&& rhs) {
+    if (empty()) {
+      set_ = std::move(rhs.set_);
+    } else {
+      set_.insert(rhs.set_.begin(), rhs.set_.end());
+    }
+
+    return *this;
+  }
+
+  /**
+   * Set difference.
+   */
+  Set& operator-=(const Set& rhs) {
+    if (this == &rhs) {
+      Clear();
+    } else {
+      // Cannot use set_.erase with iterator, as rhs may contain elements
+      // that do not exist in this set. In such a case, the erase
+      // implementation of current GCC segfaults.
+      for (const auto& e : rhs.Get()) {
+        Erase(e);
+      }
+    }
+
+    return *this;
+  }
+
+  /**
+   * Set intersection
+   */
+  Set& operator&=(const Set& rhs) {
+    if (this != &rhs) {
+      for (auto it = set_.begin(); it != set_.end();) {
+        if (!rhs.Contains(*it)) {
+          it = set_.erase(it);
+          continue;
+        }
+
+        it++;
+      }
+    }
+
+    return *this;
+  }
+
+  std::size_t size() const { return set_.size(); }
+
+  bool empty() const { return set_.empty(); }
+
+  bool SubsetEq(const Set& s) const {
+    if (size() > s.size()) return false;
+
+    for (const auto& e : set_) {
+      if (!s.Contains(e)) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+
+  bool Subset(const Set& s) const { return size() < s.size() && SubsetEq(s); }
+
+ protected:
+  Container set_;
+};
+
+template <class Ts>
+inline Set<Ts> operator|(const Set<Ts>& lhs, const Set<Ts>& rhs) {
+  Set<Ts> res = lhs;
+  return res |= rhs;
+}
+
+template <class Ts>
+inline Set<Ts> operator|(Set<Ts>&& lhs, const Set<Ts>& rhs) {
+  lhs |= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Set<Ts> operator|(const Set<Ts>& lhs, Set<Ts>&& rhs) {
+  rhs |= lhs;
+  return std::move(rhs);
+}
+
+template <class Ts>
+inline Set<Ts> operator|(Set<Ts>&& lhs, Set<Ts>&& rhs) {
+  lhs |= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Set<Ts> operator-(const Set<Ts>& lhs, const Set<Ts>& rhs) {
+  Set<Ts> res = lhs;
+  return res -= rhs;
+}
+
+template <class Ts>
+inline Set<Ts> operator-(Set<Ts>&& lhs, const Set<Ts>& rhs) {
+  lhs -= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Set<Ts> operator-(const Set<Ts>& lhs, Set<Ts>&& rhs) {
+  Set<Ts> res = lhs;
+  return res -= rhs;
+}
+
+template <class Ts>
+inline Set<Ts> operator-(Set<Ts>&& lhs, Set<Ts>&& rhs) {
+  lhs -= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Set<Ts> operator&(const Set<Ts>& lhs, const Set<Ts>& rhs) {
+  Set<Ts> res;
+
+  for (const auto& e : rhs.Get()) {
+    if (lhs.Contains(e)) {
+      res.Insert(e);
+    }
+  }
+
+  return res;
+}
+
+template <class Ts>
+inline Set<Ts> operator&(Set<Ts>&& lhs, const Set<Ts>& rhs) {
+  lhs &= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Set<Ts> operator&(const Set<Ts>& lhs, Set<Ts>&& rhs) {
+  rhs &= lhs;
+  return std::move(rhs);
+}
+
+template <class Ts>
+inline Set<Ts> operator&(Set<Ts>&& lhs, Set<Ts>&& rhs) {
+  lhs &= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+class Relation {
+ public:
+  typedef typename Ts::Element Element;
+
+  typedef typename Ts::template MapContainer<Set<Ts>> Container;
+
+  typedef std::pair<Element, Element> Tuple;
+
+  typedef std::vector<Element> Path;
+
+  /**
+   * Lazy operators as properties.
+   *
+   * All in-place operators (e.g. |=) evaluate the current relation in place
+   * and clear properties.
+   */
+  typedef unsigned Properties;
+
+  // Properties {{{
+
+  static constexpr Properties kNone = 0x0;
+  static constexpr Properties kTransitiveClosure = 0x1;
+  static constexpr Properties kReflexiveClosure = 0x2;
+  static constexpr Properties kReflexiveTransitiveClosure =
+      kTransitiveClosure | kReflexiveClosure;
+
+  // }}}
+
+  Relation() : props_(kNone) {}
+
+  explicit Relation(Container r) : props_(kNone), rel_(std::move(r)) {}
+
+  /**
+   * Avoid accessing rel_ directly! Uses of Raw() should be justified.
+   */
+  const Container& Raw() const { return rel_; }
+
+  Properties props() const { return props_; }
+
+  Relation& set_props(Properties props) {
+    props_ = props;
+    return *this;
+  }
+
+  Relation& add_props(Properties props) {
+    props_ |= props;
+    return *this;
+  }
+
+  Relation& unset_props(Properties props) {
+    props_ &= ~props;
+    return *this;
+  }
+
+  bool all_props(Properties all) const { return AllBitmask(props_, all); }
+
+  bool any_props(Properties any) const { return AnyBitmask(props_, any); }
+
+  Properties clear_props() {
+    const auto props = props_;
+    props_ = kNone;
+    return props;
+  }
+
+  void Insert(const Element& e1, const Element& e2,
+              bool assert_unique = false) {
+    rel_[e1].Insert(e2, assert_unique);
+  }
+
+  void Insert(const Element& e1, Element&& e2, bool assert_unique = false) {
+    rel_[e1].Insert(std::move(e2), assert_unique);
+  }
+
+  void Insert(const Element& e1, const Set<Ts>& e2s) {
+    if (e2s.empty()) return;
+    rel_[e1] |= e2s;
+  }
+
+  void Insert(const Element& e1, Set<Ts>&& e2s) {
+    if (e2s.empty()) return;
+    rel_[e1] |= std::move(e2s);
+  }
+
+  bool Erase(const Element& e1, const Element& e2, bool assert_exists = false) {
+    // May not work as expect if kReflexiveClosure is set.
+    if (Contains__(e1)) {
+      bool result = rel_[e1].Erase(e2, assert_exists);
+
+      if (rel_[e1].empty()) {
+        rel_.erase(e1);
+      }
+
+      return result;
+    }
+
+    return false;
+  }
+
+  void Erase(const Element& e1, const Set<Ts>& e2s) {
+    if (Contains__(e1)) {
+      rel_[e1] -= e2s;
+
+      if (rel_[e1].empty()) {
+        rel_.erase(e1);
+      }
+    }
+  }
+
+  /**
+   * Total size of the relation (i.e. number of tuples or edges); uses
+   * properties.
+   *
+   * @return Total number of tuples (or edges).
+   */
+  std::size_t size() const {
+    std::size_t total = 0;
+
+    if (props()) {
+      const auto dom = Domain();
+      for (const auto& e : dom.Get()) {
+        total += Reachable(e).size();
+      }
+    } else {
+      for (const auto& tuples : rel_) {
+        total += tuples.second.size();
+      }
+    }
+
+    return total;
+  }
+
+  /**
+   * Iterates over each tuple in the relation (uses properties).
+   *
+   * @param func A function taking two parameters of type Element.
+   */
+  template <class Func>
+  Func for_each(Func func) const {
+    const auto dom = Domain();
+
+    for (const auto& e1 : dom.Get()) {
+      const auto reach = Reachable(e1);
+      for (const auto& e2 : reach.Get()) {
+        func(e1, e2);
+      }
+    }
+
+    return std::move(func);
+  }
+
+  /**
+   * Evaluated view of the relation, with properties evaluated.
+   *
+   * @return Evaluated Relation.
+   */
+  Relation Eval() const {
+    if (props() == kNone) {
+      return *this;
+    }
+
+    Relation result;
+
+    for_each([&result](const Element& e1, const Element& e2) {
+      result.Insert(e1, e2);
+    });
+
+    return result;
+  }
+
+  /**
+   * Evaluate all properties in-place.
+   *
+   * @return Reference to this object.
+   */
+  Relation& EvalInplace() {
+    if (props() == kNone) {
+      return *this;
+    }
+
+    Relation result;
+
+    for_each([&result](const Element& e1, const Element& e2) {
+      result.Insert(e1, e2);
+    });
+
+    clear_props();
+    rel_ = std::move(result.rel_);
+    return *this;
+  }
+
+  template <class FilterFunc>
+  Relation Filter(FilterFunc filterFunc) const {
+    Relation result;
+
+    for_each([&filterFunc, &result](const Element& e1, const Element& e2) {
+      if (filterFunc(e1, e2)) {
+        result.Insert(e1, e2);
+      }
+    });
+
+    return result;
+  }
+
+  /**
+   * @return R^-1 = {(y,x) | (x,y)  R}
+   */
+  Relation Inverse() const {
+    Relation result;
+
+    for_each([&result](const Element& e1, const Element& e2) {
+      result.Insert(e2, e1);
+    });
+
+    return result;
+  }
+
+  /**
+   * Relation union.
+   */
+  Relation& operator|=(const Relation& rhs) {
+    EvalInplace();
+
+    if (rhs.props()) {
+      const auto rhs_domain = rhs.Domain();
+      for (const auto& e : rhs_domain.Get()) {
+        rel_[e] |= rhs.Reachable(e);
+      }
+    } else {
+      for (const auto& tuples : rhs.Raw()) {
+        rel_[tuples.first] |= tuples.second;
+      }
+    }
+
+    return *this;
+  }
+
+  /**
+   * Relation difference.
+   */
+  Relation& operator-=(const Relation& rhs) {
+    EvalInplace();
+
+    if (rhs.props()) {
+      const auto rhs_domain = rhs.Domain();
+      for (const auto& e : rhs_domain.Get()) {
+        Erase(e, rhs.Reachable(e));
+      }
+    } else {
+      for (const auto& tuples : rhs.Raw()) {
+        Erase(tuples.first, tuples.second);
+      }
+    }
+
+    return *this;
+  }
+
+  /**
+   * Relation intersection
+   */
+  Relation& operator&=(const Relation& rhs) {
+    EvalInplace();
+
+    for (auto it = rel_.begin(); it != rel_.end();) {
+      it->second &= rhs.Reachable(it->first);
+
+      if (it->second.empty()) {
+        it = rel_.erase(it);
+        continue;
+      }
+
+      it++;
+    }
+
+    return *this;
+  }
+
+  void Clear() { rel_.clear(); }
+
+  bool empty() const {
+    // Upon erasure, we ensure that an element is not related to an empty
+    // set, i.e. in that case it is deleted.
+    return rel_.empty();
+  }
+
+  bool operator==(const Relation& rhs) const {
+    return (props() ? Eval() : *this).rel_ ==
+           (rhs.props() ? rhs.Eval() : rhs).rel_;
+  }
+
+  bool operator!=(const Relation& rhs) const { return !((*this) == rhs); }
+
+  /**
+   * Check if (e1, e2) is in the relation. This effectively does a search if
+   * there is an edge from e1 to e2.
+   *
+   * @param e1 first element.
+   * @param e2 second element
+   * @param path Optional; return path from e1 to e2.
+   * @return true if (e1, e2) is in the relation.
+   */
+  bool R(const Element& e1, const Element& e2, Path* path = nullptr) const {
+    if (e1 == e2 && all_props(kReflexiveClosure)) {
+      if (InOn(e1)) {
+        if (path != nullptr) {
+          path->push_back(e1);
+          path->push_back(e1);
+        }
+
+        return true;
+      }
+    }
+
+    Set<Ts> visited;
+
+    if (path != nullptr) {
+      FlagSet visiting;
+
+      bool result = R_search(e1, &e2, &visited, &visiting);
+      if (result) {
+        GetPath(path, &e1, &e2, &visiting);
+      }
+
+      return result;
+    }
+
+    return R_search(e1, &e2, &visited);
+  }
+
+  /**
+   * Returns all rechable elements from a start element without the start
+   * itself, but includes start if start can reach itself (e.g. through
+   * cycle).
+   *
+   * @param e Start element.
+   * @return Set of reachable elements.
+   */
+  Set<Ts> Reachable(const Element& e) const {
+    Set<Ts> visited;
+
+    if (all_props(kReflexiveClosure) && InOn(e)) {
+      visited.Insert(e);
+    }
+
+    if (!all_props(kTransitiveClosure)) {
+      const auto tuples = rel_.find(e);
+      if (tuples != rel_.end()) {
+        visited |= tuples->second;
+      }
+
+      return visited;
+    }
+
+    if (!R_search(e, &e, &visited, nullptr, kNone,
+                  SearchMode::kRelatedVisitAll)) {
+      if (!all_props(kReflexiveClosure)) {
+        visited.Erase(e);
+      }
+    }
+
+    return visited;
+  }
+
+  bool Irreflexive(Path* cyclic = nullptr) const {
+    return Irreflexive(kNone, cyclic);
+  }
+
+  bool Acyclic(Path* cyclic = nullptr) const {
+    return Irreflexive(kTransitiveClosure, cyclic);
+  }
+
+  /**
+   * xy  yz  xz
+   */
+  bool Transitive() const {
+    if (all_props(kTransitiveClosure)) {
+      return true;
+    }
+
+    for (const auto& tuples1 : rel_) {
+      for (const auto& e1 : tuples1.second.Get()) {
+        const auto tuples2 = rel_.find(e1);
+        if (tuples2 != rel_.end()) {
+          for (const auto& e2 : tuples2->second.Get()) {
+            if (!R(tuples1.first, e2)) {
+              return false;
+            }
+          }
+        }
+      }
+    }
+
+    return true;
+  }
+
+  /**
+   * (x,y)  onon, xy  yx
+   */
+  bool TotalOn(const Set<Ts>& on) const {
+    for (const auto& e1 : on.Get()) {
+      for (const auto& e2 : on.Get()) {
+        if (!R(e1, e2) && !R(e2, e1)) {
+          return false;
+        }
+      }
+    }
+
+    return true;
+  }
+
+  /**
+   * (x,y)  onon, xy  yx  x=y
+   */
+  bool ConnexOn(const Set<Ts>& on) const {
+    for (const auto& e1 : on.Get()) {
+      for (const auto& e2 : on.Get()) {
+        if (e1 != e2 && !R(e1, e2) && !R(e2, e1)) {
+          return false;
+        }
+      }
+    }
+
+    return true;
+  }
+
+  bool WeakPartialOrder(const Set<Ts>& on) const {
+    // (domain  range) in on
+    for (const auto& tuples : rel_) {
+      if (!on.Contains(tuples.first) && !tuples.second.SubsetEq(on)) {
+        return false;
+      }
+    }
+
+    return Transitive() && !Irreflexive();
+  }
+
+  bool WeakTotalOrder(const Set<Ts>& on) const {
+    return WeakPartialOrder(on) && TotalOn(on);
+  }
+
+  bool StrictPartialOrder(const Set<Ts>& on) const {
+    // (domain  range) in on
+    for (const auto& tuples : rel_) {
+      if (!on.Contains(tuples.first) && !tuples.second.SubsetEq(on)) {
+        return false;
+      }
+    }
+
+    return Transitive() && Irreflexive();
+  }
+
+  bool StrictTotalOrder(const Set<Ts>& on) const {
+    return StrictPartialOrder(on) && ConnexOn(on);
+  }
+
+  bool InOn(const Element& e) const {
+    if (Contains__(e)) {
+      return true;
+    } else {
+      for (const auto& tuples : rel_) {
+        if (tuples.second.Contains(e)) {
+          return true;
+        }
+      }
+    }
+
+    return false;
+  }
+
+  bool InDomain(const Element& e) const {
+    if (all_props(kReflexiveClosure)) {
+      return InOn(e);
+    }
+
+    return Contains__(e);
+  }
+
+  bool InRange(const Element& e) const {
+    if (all_props(kReflexiveClosure)) {
+      return InOn(e);
+    }
+
+    for (const auto& tuples : rel_) {
+      if (Reachable(tuples.first).Contains(e)) {
+        return true;
+      }
+    }
+
+    return false;
+  }
+
+  Set<Ts> On() const {
+    Set<Ts> res;
+    for (const auto& tuples : rel_) {
+      res.Insert(tuples.first);
+      res |= tuples.second;
+    }
+    return res;
+  }
+
+  Set<Ts> Domain() const {
+    if (all_props(kReflexiveClosure)) {
+      // By the fact that the reflexive closure is
+      // R  {(x,x). x  S}, where S is the set the relation is on, and
+      // thus S contains both the range and domain, constructing the
+      // above will yield domain = range = S under the reflexive closure.
+      return On();
+    }
+
+    Set<Ts> res;
+    for (const auto& tuples : rel_) {
+      res.Insert(tuples.first);
+    }
+
+    return res;
+  }
+
+  Set<Ts> Range() const {
+    if (all_props(kReflexiveClosure)) {
+      // See above.
+      return On();
+    }
+
+    Set<Ts> res;
+    for (const auto& tuples : rel_) {
+      res |= Reachable(tuples.first);
+    }
+
+    return res;
+  }
+
+  bool SubsetEq(const Relation& rhs) const {
+    const Relation diff = (*this - rhs);
+    return diff.empty();
+  }
+
+  bool Subset(const Relation& rhs) const {
+    return size() < rhs.size() && SubsetEq(rhs);
+  }
+
+ protected:
+  typedef typename Ts::template MapContainer<bool> FlagSet;
+
+  /**
+   * Search mode.
+   */
+  enum class SearchMode {
+    /**
+     * Check if two elements are related.
+     */
+    kRelated,
+
+    /**
+     * Check if two elements are related, but visit all elements.
+     */
+    kRelatedVisitAll,
+
+    /**
+     * Only find a cycle from a given element (node).
+     */
+    kFindCycle
+  };
+
+  /**
+   * @return true if e in rel_.
+   */
+  bool Contains__(const Element& e) const { return rel_.find(e) != rel_.end(); }
+
+  /**
+   * Get path from start to end.
+   */
+  void GetPath(Path* out, const Element* start, const Element* end,
+               FlagSet* visiting,
+               SearchMode mode = SearchMode::kRelated) const {
+    assert(out != nullptr && start != nullptr && visiting != nullptr);
+
+    out->push_back(*start);
+    (*visiting)[*start] = false;
+
+    while (start != nullptr) {
+      const Set<Ts>& next = rel_.find(*start)->second;
+      start = nullptr;
+
+      for (const auto& e : next.Get()) {
+        const auto se = visiting->find(e);
+        if (se != visiting->end() && se->second) {
+          out->push_back(e);
+          se->second = false;
+          start = &e;
+          break;
+        }
+      }
+    }
+
+    const Set<Ts>& next = rel_.find(out->back())->second;
+    if (mode == SearchMode::kFindCycle) {
+      assert(end == nullptr);
+
+      for (const auto& e : *out) {
+        if (next.Contains(e)) {
+          // Final edge
+          out->push_back(e);
+          break;
+        }
+      }
+    } else {
+      assert(end != nullptr);
+
+      // This function should only be called if search established there
+      // is a path between start->end.
+      assert(next.Contains(*end));
+
+      out->push_back(*end);
+    }
+  }
+
+  /**
+   * Check that relation is irreflexive.
+   *
+   * @param local_props Call specific properties.
+   * @param cyclic Optional parameter, in which the cycle is returned, if
+   *               result is false.
+   * @return true if irreflexive, false otherwise.
+   */
+  bool Irreflexive(Properties local_props, Path* cyclic) const {
+    local_props |= props_;
+
+    if (AllBitmask(local_props, kReflexiveClosure) && !empty()) {
+      if (cyclic != nullptr) {
+        // Pick arbitrary.
+        cyclic->push_back(rel_.begin()->first);
+        cyclic->push_back(rel_.begin()->first);
+      }
+
+      return false;
+    }
+
+    Set<Ts> visited;
+    FlagSet visiting;
+
+    for (const auto& tuples : rel_) {
+      if (R_search(tuples.first, nullptr, &visited, &visiting, local_props,
+                   SearchMode::kFindCycle)) {
+        if (cyclic != nullptr) {
+          GetPath(cyclic, &tuples.first, nullptr, &visiting,
+                  SearchMode::kFindCycle);
+        }
+
+        return false;
+      }
+    }
+
+    return true;
+  }
+
+  /**
+   * Check if two elements are related, i.e. there exists an edge or path from
+   * e1 to e2. This is implemented as a directed graph search.
+   *
+   * @param e1 First element.
+   * @param e2 Second element.
+   * @param visited Visited element (node) set.
+   * @param visiting Currently visiting elements (nodes).
+   * @param local_props Call specific properties.
+   * @param mode Search mode.
+   *
+   * @return true if there exists an edge or path, false otherwise.
+   */
+  bool R_search(const Element& e1, const Element* e2, Set<Ts>* visited,
+                FlagSet* visiting = nullptr, Properties local_props = kNone,
+                SearchMode mode = SearchMode::kRelated) const {
+    // We always require visited to be set.
+    assert(visited != nullptr);
+
+    // Merge call-specific props with global props.
+    local_props |= props_;
+
+    const bool is_tran_cl = AllBitmask(local_props, kTransitiveClosure);
+
+    R_impl search(this, visited, visiting, is_tran_cl, mode);
+
+    if (e2 == nullptr) {
+      // For the purpose of cycle detection, we are looking for e1->*e1.
+      // In addition, if the transitive property is set, we require that
+      // visiting is provided, as we cannot make assumptions on if visited
+      // is reset before every call -- and for performance reasons, this
+      // usage is discouraged.
+
+      assert(mode == SearchMode::kFindCycle);
+
+      e2 = &e1;
+
+      if (is_tran_cl) {
+        assert(visiting != nullptr);
+        return search.DfsRecFindCycle(e1);
+      }
+    } else {
+      assert(mode != SearchMode::kFindCycle);
+    }
+
+    return search.DfsRec(e1, *e2);
+  }
+
+  /**
+   * Helper class to check if two elements are related.
+   */
+  class R_impl {
+   public:
+    R_impl(const Relation* src, Set<Ts>* visited, FlagSet* visiting,
+           bool is_tran_cl, SearchMode mode)
+        : src_(src),
+          visited_(visited),
+          visiting_(visiting),
+          is_tran_cl_(is_tran_cl),
+          mode_(mode) {}
+
+    /**
+     * Recursive DFS implementation, searching if there exists a path from e1
+     * to e2.
+     */
+    bool DfsRec(const Element& e1, const Element& e2) const {
+      const auto tuples = src_->Raw().find(e1);
+
+      if (tuples == src_->Raw().end()) {
+        return false;
+      }
+
+      if (visiting_ != nullptr) {
+        (*visiting_)[e1] = true;
+      }
+
+      bool result = false;
+      visited_->Insert(e1);
+
+      for (const auto& e : tuples->second.Get()) {
+        if (e == e2) {
+          if (mode_ == SearchMode::kRelatedVisitAll) {
+            result = true;
+          } else {
+            return true;
+          }
+        }
+
+        if (is_tran_cl_) {
+          if (!visited_->Contains(e)) {
+            if (DfsRec(e, e2)) {
+              if (mode_ == SearchMode::kRelatedVisitAll) {
+                result = true;
+              } else {
+                return true;
+              }
+            }
+
+            // There might not be an edge e -> e2, but we must update
+            // the visited set regardless -- this is only relevant, as
+            // the caller might expect the complete set of visited
+            // nodes if mode == RelatedVisitAll.
+            visited_->Insert(e);
+          } else {
+            // assert(mode_ != SearchMode::kFindCycle);
+          }
+        }
+      }
+
+      if (visiting_ != nullptr) {
+        (*visiting_)[e1] = false;
+      }
+
+      return result;
+    }
+
+    /**
+     * DFS optimized to just find a cycle; elides some branches that are not
+     * needed compared to DfsRec.
+     */
+    bool DfsRecFindCycle(const Element& start) const {
+      // assert(is_tran_cl_);
+      // assert(mode_ == SearchMode::kFindCycle);
+      // assert(visiting_ != nullptr);
+
+      const auto tuples = src_->Raw().find(start);
+
+      if (tuples == src_->Raw().end()) {
+        return false;
+      }
+
+      (*visiting_)[start] = true;
+      visited_->Insert(start);
+
+      for (const auto& e : tuples->second.Get()) {
+        if (!visited_->Contains(e)) {
+          if (DfsRecFindCycle(e)) {
+            return true;
+          }
+        } else {
+          const auto se = visiting_->find(e);
+          if (se != visiting_->end() && se->second) {
+            // Found a backedge --> cycle!
+            return true;
+          }
+        }
+      }
+
+      (*visiting_)[start] = false;
+      return false;
+    }
+
+   private:
+    const Relation* src_;
+    Set<Ts>* visited_;
+    FlagSet* visiting_;
+    bool is_tran_cl_;
+    SearchMode mode_;
+  };
+
+ protected:
+  Properties props_;
+  Container rel_;
+};
+
+template <class Ts>
+inline Relation<Ts> operator*(const Set<Ts>& lhs, const Set<Ts>& rhs) {
+  Relation<Ts> res;
+
+  for (const auto& e1 : lhs.Get()) {
+    for (const auto& e2 : rhs.Get()) {
+      res.Insert(e1, e2);
+    }
+  }
+
+  return res;
+}
+
+template <class Ts>
+inline Relation<Ts> operator|(const Relation<Ts>& lhs,
+                              const Relation<Ts>& rhs) {
+  Relation<Ts> res = lhs;
+  return res |= rhs;
+}
+
+template <class Ts>
+inline Relation<Ts> operator|(Relation<Ts>&& lhs, const Relation<Ts>& rhs) {
+  lhs |= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Relation<Ts> operator|(const Relation<Ts>& lhs, Relation<Ts>&& rhs) {
+  rhs |= lhs;
+  return std::move(rhs);
+}
+
+template <class Ts>
+inline Relation<Ts> operator|(Relation<Ts>&& lhs, Relation<Ts>&& rhs) {
+  lhs |= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Relation<Ts> operator-(const Relation<Ts>& lhs,
+                              const Relation<Ts>& rhs) {
+  Relation<Ts> res = lhs;
+  return res -= rhs;
+}
+
+template <class Ts>
+inline Relation<Ts> operator-(Relation<Ts>&& lhs, const Relation<Ts>& rhs) {
+  lhs -= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Relation<Ts> operator-(const Relation<Ts>& lhs, Relation<Ts>&& rhs) {
+  Relation<Ts> res = lhs;
+  return res -= rhs;
+}
+
+template <class Ts>
+inline Relation<Ts> operator-(Relation<Ts>&& lhs, Relation<Ts>&& rhs) {
+  lhs -= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Relation<Ts> operator&(const Relation<Ts>& lhs,
+                              const Relation<Ts>& rhs) {
+  Relation<Ts> res;
+
+  const auto lhs_domain = lhs.Domain();
+  for (const auto& e : lhs_domain.Get()) {
+    Set<Ts> intersect = lhs.Reachable(e) & rhs.Reachable(e);
+    // insert checks if empty or not
+    res.Insert(e, std::move(intersect));
+  }
+
+  return res;
+}
+
+template <class Ts>
+inline Relation<Ts> operator&(Relation<Ts>&& lhs, const Relation<Ts>& rhs) {
+  lhs &= rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline Relation<Ts> operator&(const Relation<Ts>& lhs, Relation<Ts>&& rhs) {
+  rhs &= lhs;
+  return std::move(rhs);
+}
+
+template <class Ts>
+inline Relation<Ts> operator&(Relation<Ts>&& lhs, Relation<Ts>&& rhs) {
+  lhs &= rhs;
+  return std::move(lhs);
+}
+
+/**
+ * Relation operator base class.
+ * No derived class shall define a destructor!
+ */
+template <class Ts>
+class RelationOp {
+ public:
+  RelationOp() {}
+
+  explicit RelationOp(std::vector<Relation<Ts>> rels)
+      : rels_(std::move(rels)) {}
+
+  /*//virtual ~RelationOp()
+   *
+   * No destructor, so compiler can implicitly create move constructor and
+   * assignment operators.
+  */
+
+  /**
+   * Evaluate in-place, where postcondition is rels_.size() <= 1. This avoids
+   * some of the copying overhead of Eval(), and can therefore be more
+   * efficient.
+   *
+   * @return Reference to this object.
+   */
+  virtual RelationOp& EvalInplace() = 0;
+
+  /**
+   * Evaluate operator, computing the result of the opertor.
+   *
+   * @return Relation representing view of operator.
+   */
+  virtual Relation<Ts> Eval() const = 0;
+
+  void Clear() { rels_.clear(); }
+
+  /**
+   * Evaluate operator in-place, and clearing it, returning the evaluated
+   * Relation. Optimized for move, and should be used where the operator is
+   * used as a temporary.
+   *
+   * @return Relation representing view of operator before call.
+   */
+  Relation<Ts> EvalClear() {
+    if (rels_.empty()) {
+      // Already cleared
+      return Relation<Ts>();
+    }
+
+    EvalInplace();
+    assert(rels_.size() == 1);
+
+    Relation<Ts> result = std::move(rels_.back());
+    rels_.clear();
+    return result;  // NRVO
+  }
+
+ protected:
+  void Add(const Relation<Ts>& er) { rels_.push_back(er); }
+
+  void Add(Relation<Ts>&& er) { rels_.push_back(std::move(er)); }
+
+  void Add(const std::vector<Relation<Ts>>& rels) {
+    rels_.reserve(rels_.size() + rels.size());
+    rels_.insert(rels_.end(), rels.begin(), rels.end());
+  }
+
+ protected:
+  std::vector<Relation<Ts>> rels_;
+};
+
+/**
+ * Operator ";".
+ */
+template <class Ts>
+class RelationSeq : public RelationOp<Ts> {
+ public:
+  typedef typename Ts::Element Element;
+
+  RelationSeq() {}
+
+  explicit RelationSeq(std::vector<Relation<Ts>> v)
+      : RelationOp<Ts>(std::move(v)) {}
+
+  RelationSeq& operator+=(const Relation<Ts>& rhs) {
+    this->Add(rhs);
+    return *this;
+  }
+
+  RelationSeq& operator+=(Relation<Ts>&& rhs) {
+    this->Add(std::move(rhs));
+    return *this;
+  }
+
+  RelationSeq& operator+=(const RelationSeq& rhs) {
+    this->Add(rhs.rels_);
+    return *this;
+  }
+
+  RelationOp<Ts>& EvalInplace() override {
+    while (this->rels_.size() > 1) {
+      std::size_t from_idx = this->rels_.size() - 2;
+      const auto& first = this->rels_[from_idx];
+      const auto& last = this->rels_.back();
+
+      Relation<Ts> er;
+
+      first.for_each([&er, &last](const Element& e1, const Element& e2) {
+        if (last.InDomain(e2)) {
+          er.Insert(e1, last.Reachable(e2));
+        }
+      });
+
+      this->rels_.erase(this->rels_.end() - 2, this->rels_.end());
+      this->rels_.push_back(std::move(er));
+    }
+
+    return *this;
+  }
+
+  Relation<Ts> Eval() const override {
+    Relation<Ts> er;
+
+    if (this->rels_.empty()) {
+      return Relation<Ts>();
+    } else if (this->rels_.size() == 1) {
+      return this->rels_.back();
+    }
+
+    const auto potential_domain = this->rels_.front().Domain();
+    const auto potential_range = this->rels_.back().Range();
+
+    for (const auto& e1 : potential_domain.Get()) {
+      for (const auto& e2 : potential_range.Get()) {
+        if (R(e1, e2)) {
+          er.Insert(e1, e2);
+        }
+      }
+    }
+
+    return er;
+  }
+
+  /**
+   * Check if (e1, e2) is in the relation. This effectively does a search if
+   * there is an edge from e1 to e2.
+   *
+   * @param e1 First element.
+   * @param e2 Second element.
+   * @param path Optional; return path from e1 to e2.
+   * @return true if related, false otherwise.
+   */
+  bool R(const Element& e1, const Element& e2,
+         typename Relation<Ts>::Path* path = nullptr,
+         std::size_t seq = 0) const {
+    if (this->rels_.empty()) {
+      return false;
+    }
+
+    assert(seq < this->rels_.size());
+
+    if (seq + 1 < this->rels_.size()) {
+      const auto& rel = this->rels_[seq];
+      std::size_t path_size = 0;
+
+      const Set<Ts> reach = rel.Reachable(e1);
+      for (const auto& e : reach.Get()) {
+        if (path != nullptr) {
+          path_size = path->size();
+          rel.R(e1, e, path);  // true
+          path->pop_back();    // remove e
+        }
+
+        if (R(e, e2, path, seq + 1)) {
+          return true;
+        }
+
+        if (path != nullptr) {
+          // e not connected to e2, remove all up to e1 (inclusive).
+          assert(path_size < path->size());
+          path->erase(path->begin() + path_size, path->end());
+        }
+      }
+
+      return false;
+    }
+
+    return this->rels_[seq].R(e1, e2, path);
+  }
+
+  /**
+   * Check if irreflexive.
+   *
+   * @param cyclic Optional parameter, in which the cycle is returned, if
+   *               result is false.
+   * @return true if irreflexive, false otherwise.
+   */
+  bool Irreflexive(typename Relation<Ts>::Path* cyclic = nullptr) const {
+    if (this->rels_.empty()) {
+      return true;
+    }
+
+    const auto domain = this->rels_.front().Domain();
+    for (const auto& e : domain.Get()) {
+      if (R(e, e, cyclic)) {
+        return false;
+      }
+    }
+
+    return true;
+  }
+};
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(const RelationSeq<Ts>& lhs,
+                                 const Relation<Ts>& rhs) {
+  RelationSeq<Ts> res = lhs;
+  return res += rhs;
+}
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(RelationSeq<Ts>&& lhs,
+                                 const Relation<Ts>& rhs) {
+  lhs += rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(const RelationSeq<Ts>& lhs,
+                                 Relation<Ts>&& rhs) {
+  RelationSeq<Ts> res = lhs;
+  return res += std::move(rhs);
+}
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(RelationSeq<Ts>&& lhs, Relation<Ts>&& rhs) {
+  lhs += std::move(rhs);
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(const RelationSeq<Ts>& lhs,
+                                 const RelationSeq<Ts>& rhs) {
+  RelationSeq<Ts> res = lhs;
+  return res += rhs;
+}
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(RelationSeq<Ts>&& lhs,
+                                 const RelationSeq<Ts>& rhs) {
+  lhs += rhs;
+  return std::move(lhs);
+}
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(const RelationSeq<Ts>& lhs,
+                                 RelationSeq<Ts>&& rhs) {
+  RelationSeq<Ts> res = lhs;
+  return res += rhs;
+}
+
+template <class Ts>
+inline RelationSeq<Ts> operator+(RelationSeq<Ts>&& lhs, RelationSeq<Ts>&& rhs) {
+  lhs += rhs;
+  return std::move(lhs);
+}
+
+/**
+ * @brief Helper class to instantiate types used by Set, Relation, etc.
+ *
+ * Set, Relation, etc. take a template parameter that provides Element, and
+ * SetContainer or MapContainer; this class can be used to instantiate a class
+ * to be passed as the template parameter to Set and Relation.
+ */
+template <class E, class Hash = typename E::Hash>
+struct Types {
+  typedef E Element;
+
+  typedef std::unordered_set<Element, Hash> SetContainer;
+
+  template <class T>
+  using MapContainer = std::unordered_map<Element, T, Hash>;
+};
+
+}  // namespace sets
+}  // namespace mc2lib
+
+#endif /* MC2LIB_SETS_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/simplega.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/simplega.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,466 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_SIMPLEGA_HPP_
+#define MC2LIB_SIMPLEGA_HPP_
+
+#include <algorithm>
+#include <cassert>
+#include <cstddef>
+#include <list>
+#include <random>
+#include <sstream>
+#include <string>
+#include <unordered_set>
+#include <utility>
+#include <vector>
+
+namespace mc2lib {
+
+/**
+ * @namespace mc2lib::simplega
+ * @brief Simple Genetic Algorithm library.
+ */
+namespace simplega {
+
+/**
+ * @namespace mc2lib::simplega::evolve
+ * @brief Example CrossoverMutateFunc implementations.
+ */
+namespace evolve {
+
+/**
+ * Cut & splice. If template parameter one_point is set, turns this into
+ * one-point crossover.
+ *
+ * Assumes that GenomeT implements Get() and uses a vector-like structure to
+ * represent the genome.
+ */
+template <class URNG, class GenomeT, class C, bool one_point = false,
+          bool theone = false>
+inline void CutSpliceMutate(URNG& urng, const GenomeT& mate1,
+                            const GenomeT& mate2, float mutation_rate,
+                            C* container) {
+  assert(!mate1.Get().empty());
+  assert(!mate2.Get().empty());
+
+  std::uniform_int_distribution<std::size_t> dist1(0, mate1.Get().size() - 1);
+  std::uniform_int_distribution<std::size_t> dist2(0, mate2.Get().size() - 1);
+
+  const std::size_t cut1 = dist1(urng);
+  const std::size_t cut2 = one_point ? cut1 : dist2(urng);
+
+  // a[0:cut_a] + b[cut_b:]
+  auto cut_and_splice = [](const GenomeT& a, const GenomeT& b,
+                           std::size_t cut_a, std::size_t cut_b) {
+    auto result = a.Get();
+    auto ita = result.begin();
+    std::advance(ita, cut_a);
+    result.erase(ita, result.end());
+    auto itb = b.Get().begin();
+    std::advance(itb, cut_b);
+    result.insert(result.end(), itb, b.Get().end());
+    return GenomeT(a, b, result);
+  };
+
+  // child1 = mate1[0:cut1] + mate2[cut2:]
+  GenomeT child1 = cut_and_splice(mate1, mate2, cut1, cut2);
+  if (child1.Get().size()) {
+    child1.Mutate(mutation_rate);
+    container->push_back(std::move(child1));
+  }
+
+  if (!theone) {
+    // child2 = mate2[0:cut2] + mate1[cut1:]
+    GenomeT child2 = cut_and_splice(mate2, mate1, cut2, cut1);
+    if (child2.Get().size()) {
+      child2.Mutate(mutation_rate);
+      container->push_back(std::move(child2));
+    }
+  }
+}
+
+}  // namespace evolve
+
+/**
+ * @brief Simple Genome interface.
+ *
+ * Use as a baseclass for genome implementations, but this is optional, as long
+ * as the interface is implemented (see GenePool).
+ *
+ * Note that this class is virtual, as it is possible that we could have a
+ * heterogeneous collection of genomes, all based off of the same baseclass,
+ * e.g., where a specialized crossover_mutate operator yields children of
+ * different classes.
+ *
+ * @tparam T The type of genes in this Genome.
+ */
+template <class T>
+class Genome {
+ public:
+  typedef std::vector<T> Container;
+
+  /**
+   * @brief Default constructor.
+   *
+   * Yields an empty genome.
+   */
+  Genome() {}
+
+  /**
+   * @brief Converting constructor.
+   *
+   * @param g A raw vector of type T genes forming this new Genome.
+   */
+  explicit Genome(Container g) : genome_(std::move(g)) {}
+
+  virtual ~Genome() {}
+
+  /**
+   * @brief Read-only genome accessor.
+   *
+   * @return Const reference to vector of genes.
+   */
+  const Container& Get() const { return genome_; }
+
+  /**
+   * @brief Modifiable genome accessor.
+   *
+   * @return Pointer to vector of genes.
+   */
+  Container* GetPtr() { return &genome_; }
+
+  /**
+   * @brief Less than comparison operator.
+   *
+   * Use to rank genomes from best fitness to worst fitness. Assumes higher
+   * fitness means better.
+   *
+   * @return True if this instance (lhs) is fitter than rhs, false otherwise.
+   */
+  virtual bool operator<(const Genome& rhs) const {
+    return Fitness() > rhs.Fitness();
+  }
+
+  /**
+   * @brief Mutate this Genome.
+   *
+   * @param rate Mutation rate.
+   */
+  virtual void Mutate(float rate) = 0;
+
+  /**
+   * @brief Fitness accessor.
+   *
+   * @return Current fitness.
+   */
+  virtual float Fitness() const = 0;
+
+  /**
+   * @brief Converting operator to float.
+   *
+   * As this is also used for the roulette selection, the assumption is that
+   * higher fitness means better.
+   */
+  virtual operator float() const { return Fitness(); }
+
+  /**
+   * @brief Converting operator to std::string.
+   */
+  virtual operator std::string() const {
+    std::ostringstream oss;
+    oss << "[";
+    bool first = true;
+    for (const auto& v : genome_) {
+      oss << (first ? "" : ", ") << v;
+      first = false;
+    }
+    oss << "]";
+    return oss.str();
+  }
+
+ protected:
+  /**
+   * @brief Raw genome of individual genes of T.
+   */
+  Container genome_;
+};
+
+/**
+ * @brief Helper to manages and evolve a populates.
+ *
+ * Helps manage and evolve a population, and provides various primitives for
+ * implementing selection operators.
+ */
+template <class GenomeT>
+class GenePool {
+ public:
+  /**
+   * Using a list for the population pool, as this permits O(1) removal of
+   * elements.
+   */
+  typedef std::list<GenomeT> Population;
+  typedef std::vector<GenomeT*> Selection;
+
+  explicit GenePool(std::size_t target_population_size = 80,
+                    float mutation_rate = 0.02f)
+      : target_population_size_(target_population_size),
+        mutation_rate_(mutation_rate),
+        steps_(0) {
+    // mutation rate is a percentage
+    if (mutation_rate_ > 1.0f) {
+      mutation_rate_ = 1.0f;
+    } else if (mutation_rate_ < 0.0f) {
+      mutation_rate_ = 0.0f;
+    }
+
+    // Initialize with defaults (e.g. random)
+    population_.resize(target_population_size_);
+  }
+
+  explicit GenePool(Population population, float mutation_rate = 0.02f)
+      : target_population_size_(population.size()),
+        mutation_rate_(mutation_rate),
+        steps_(0),
+        population_(std::move(population)) {}
+
+  explicit GenePool(Selection selection, float mutation_rate = 0.02f)
+      : target_population_size_(selection.size()),
+        mutation_rate_(mutation_rate),
+        steps_(0) {
+    for (const auto& gptr : selection) {
+      population_.push_back(*gptr);
+    }
+  }
+
+  operator std::string() const {
+    std::ostringstream oss;
+    oss << "{ ";
+
+    bool first = true;
+    for (const auto& genome : population_) {
+      oss << (first ? "" : ", ") << static_cast<std::string>(genome);
+      first = false;
+    }
+
+    oss << " }";
+    return oss.str();
+  }
+
+  const Population& Get() const { return population_; }
+
+  Population* GetPtr() { return &population_; }
+
+  float mutation_rate() const { return mutation_rate_; }
+
+  void set_mutation_rate(float mutation_rate) {
+    mutation_rate_ = mutation_rate;
+  }
+
+  std::size_t target_population_size() const { return target_population_size_; }
+
+  std::size_t population_size() const { return population_.size(); }
+
+  std::size_t steps() const { return steps_; }
+
+  float AverageFitness() const {
+    float result = 0.0f;
+    for (const auto& g : population_) {
+      result += g.Fitness();
+    }
+    return result / population_.size();
+  }
+
+  float WorstFitness() const {
+    return std::max_element(population_.begin(), population_.end())->Fitness();
+  }
+
+  float BestFitness() const {
+    return std::min_element(population_.begin(), population_.end())->Fitness();
+  }
+
+  /**
+   * Sorts (in-place) the population based on fitness.
+   */
+  void Sort() { population_.Sort(); }
+
+  const GenomeT& SelectBest() const {
+    return *std::min_element(population_.begin(), population_.end());
+  }
+
+  /**
+   * @return Entire population as Selection.
+   */
+  Selection SelectAll() {
+    Selection result;
+    result.reserve(population_.size());
+    for (GenomeT& g : population_) {
+      result.push_back(&g);
+    }
+    return result;
+  }
+
+  /**
+   * @return Random subset of population, using distribution dist to select.
+   */
+  template <class URNG, class DIST>
+  Selection SelectDist(URNG& urng, DIST& dist, std::size_t count) {
+    assert(population_.size() >= count);
+
+    std::unordered_set<std::size_t> used;
+    Selection result;
+    result.reserve(count);
+
+    while (result.size() < count) {
+      std::size_t idx = dist(urng);
+      if (used.find(idx) != used.end()) {
+        continue;
+      }
+
+      auto it = population_.begin();
+      std::advance(it, idx);
+      result.push_back(&(*it));
+      used.insert(idx);
+    }
+
+    return result;
+  }
+
+  /**
+   * @return Random subset of population, where a higher fitness means an
+   *         individual is more likely to be selected.
+   */
+  template <class URNG>
+  Selection SelectRoulette(URNG& urng, std::size_t count) {
+    std::discrete_distribution<std::size_t> dist(population_.begin(),
+                                                 population_.end());
+    return SelectDist(urng, dist, count);
+  }
+
+  /**
+   * @return Random subset of the population, where each individual has the
+   *         same probability of being selected.
+   */
+  template <class URNG>
+  Selection SelectUniform(URNG& urng, std::size_t count) {
+    std::uniform_int_distribution<std::size_t> dist(0, population_.size() - 1);
+    return SelectDist(urng, dist, count);
+  }
+
+  /**
+   * Sorts (in-place) a Selection based on fitness.
+   */
+  void SelectionSort(Selection* v) {
+    std::sort(v->begin(), v->end(), [](const GenomeT* lhs, const GenomeT* rhs) {
+      return (*lhs) < (*rhs);
+    });
+  }
+
+  /**
+   * Takes a selection and mates the initial selection[:mates] individuals.
+   *
+   * The elements in selection also determine which individuals are to be
+   * removed from the population; selection[keep:] are removed from population
+   * (can e.g. be used for elitism).
+   */
+  template <class URNG, class CrossoverMutateFunc>
+  void Step(URNG& urng, CrossoverMutateFunc crossover_mutate,
+            const Selection& selection, std::size_t mates, std::size_t keep = 0,
+            std::size_t mate1_stride = 1, std::size_t mate2_stride = 1) {
+    assert(selection.size() >= mates);
+    assert(selection.size() >= keep);
+
+    std::size_t replace = selection.size() - keep;
+    assert(replace > 0);
+
+    const std::size_t target_population_size =
+        target_population_size_ + replace;
+
+    // Add offspring
+    for (std::size_t i = 0; i < mates; i += mate1_stride) {
+      const auto mate1 = selection[i];
+
+      // j = i: avoid mating 2 individuals twice
+      for (std::size_t j = i + 1; j < mates; j += mate2_stride) {
+        const auto mate2 = selection[j];
+
+        crossover_mutate(urng, *mate1, *mate2, mutation_rate_, &population_);
+
+        if (population_.size() >= target_population_size) {
+          goto target_reached;
+        }
+      }
+    }
+  target_reached:
+
+    // Remove selection[keep:]
+    auto selection_start = selection.begin();
+    std::advance(selection_start, keep);
+
+    for (auto it = population_.begin();
+         it != population_.end() && replace > 0;) {
+      const GenomeT* val = &(*it);
+      auto match = std::find(selection_start, selection.end(), val);
+
+      if (match != selection.end()) {
+        if (match == selection_start) {
+          ++selection_start;
+        }
+
+        it = population_.erase(it);
+        --replace;
+      } else {
+        ++it;
+      }
+    }
+
+    assert(population_.size() >= target_population_size_);
+    // The population might be larger than the target, if crossover
+    // generates more than one offspring.
+
+    ++steps_;
+  }
+
+ protected:
+  std::size_t target_population_size_;
+  float mutation_rate_;
+  std::size_t steps_;
+  Population population_;
+};
+
+}  // namespace simplega
+}  // namespace mc2lib
+
+#endif /* SIMPLEGA_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 ext/mc2lib/include/mc2lib/types.hpp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ext/mc2lib/include/mc2lib/types.hpp	Sat Jun 04 16:25:49 2016 +0100
@@ -0,0 +1,93 @@
+/*
+ * Copyright (c) 2014-2016, Marco Elver
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *  * Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ *
+ *  * Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the
+ *    distribution.
+ *
+ *  * Neither the name of the software nor the names of its contributors
+ *    may be used to endorse or promote products derived from this
+ *    software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*/
+
+#ifndef MC2LIB_TYPES_HPP_
+#define MC2LIB_TYPES_HPP_
+
+#include <cstdint>
+
+namespace mc2lib {
+
+/**
+ * @namespace mc2lib::types
+ * @brief Common types.
+ */
+namespace types {
+
+/**
+ * @brief Template class of common types, permitting specialization.
+ *
+ * Can be specialized to declare custom types without overwriting types.hh;
+ * however, this appraoch depends on user specializing before including any
+ * mc2lib header file. Do *not* define more than 1 per project!
+ */
+template <bool use_specialized>
+struct Types {
+  typedef std::uint64_t Addr;
+  typedef std::uint16_t Pid;
+  typedef std::uint16_t Poi;
+  typedef Addr InstPtr;
+  typedef std::uint8_t WriteID;
+};
+
+/**
+ * @brief Address type.
+ */
+typedef typename Types<true>::Addr Addr;
+
+/**
+ * @brief Processor/thread ID type.
+ */
+typedef typename Types<true>::Pid Pid;
+
+/**
+ * @brief Program order index type.
+ */
+typedef typename Types<true>::Poi Poi;
+
+/**
+ * @brief Instruction pointer type.
+ */
+typedef typename Types<true>::InstPtr InstPtr;
+
+/**
+ * @brief Write ID type.
+ */
+typedef typename Types<true>::WriteID WriteID;
+
+}  // namespace types
+}  // namespace mc2lib
+
+#endif /* MC2LIB_TYPES_HPP_ */
+
+/* vim: set ts=2 sts=2 sw=2 et : */
diff -r e18a6c55bec0 -r 74e2d3943b89 SConstruct
--- a/SConstruct	Fri Jun 03 16:20:08 2016 -0400
+++ b/SConstruct	Sat Jun 04 16:25:49 2016 +0100
@@ -1321,6 +1321,10 @@
 main.SConscript('ext/nomali/SConscript',
                 variant_dir = joinpath(build_root, 'nomali'))
 
+# mc2lib build is shared across all configs in the build root.
+main.SConscript('ext/mc2lib/SConscript',
+                variant_dir = joinpath(build_root, 'mc2lib'))
+
 ###################################################
 #
 # This function is used to set up a directory with switching headers