diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/README.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/README.rst Thu May 05 13:07:16 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 +`_ framework [1]_. + +The McVerSi guest workload can be found in ``_. + +Usage +===== + +The library is header-only. + +API documentation can be found `here +`_. + +The provided ``_ 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 `_ and + `guest_workload `_. + +References +========== + +.. [1] Marco Elver and Vijay Nagarajan. `McVerSi: A Test Generation Framework + for Fast Memory Consistency Verification in Simulation + `_. In IEEE + International Symposium on High Performance Computer Architecture + (HPCA). Barcelona, Spain, March 2016. diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/SConscript --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/SConscript Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,6 @@ +# -*- mode:python -*- + +Import('main') +main.Prepend(CPPPATH=Dir('./include')) + +# vim: set ft=python : diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/apidoc/mainpage.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/apidoc/mainpage.md Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,4 @@ +mc2lib {#mainpage} +====== + +This is the API documentation for [mc2lib](https://github.com/melver/mc2lib). diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/contrib/mcversi/README.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/contrib/mcversi/README.rst Thu May 05 13:07:16 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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,399 @@ +/* + * 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 copyright holders 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. + * + * Authors: Marco Elver + */ + +#ifndef _GNU_SOURCE +# define _GNU_SOURCE +#endif + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#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 " + " [ []]\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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,1 @@ +m5_host_support.h \ No newline at end of file diff -r 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,226 @@ +/* + * Copyright (c) 2014-2015 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 copyright holders 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. + * + * Authors: Marco Elver + */ + +#ifndef HOST_SUPPORT_H_ +#define HOST_SUPPORT_H_ + +#include +#include +#include +#include +#include +#include + +#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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,6 @@ +#!/bin/sh +# +# 8KB configuration with virtual address synonyms (2 virtual addresses per 1 +# physical). + +/mcversi/guest_workload $(nproc) 10 0x1000000 0x09140010 0x100000000 1 diff -r 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,22 @@ +#!/bin/sh +# +# 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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 +#include +#include +#include +#include +#include + +#include "../memconsistency/cats.hpp" +#include "compiler.hpp" + +namespace mc2lib { + +namespace codegen { + +// Workaround for Wtype-limits warning. +template +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] + * Bogdan F. Romanescu, Alvin R. Lebeck, Daniel J. Sorin, "Specifying and + * dynamically verifying address translation-aware memory consistency", + * 2010. + */ +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(1) + << (sizeof(types::Poi) * 8 - 1); + static constexpr types::Poi kMaxOther = + std::numeric_limits::max() - (kMaxOpEvents - 1); + + static constexpr types::WriteID kInitWrite = + std::numeric_limits::min(); + static constexpr types::WriteID kMinWrite = kInitWrite + 1; + + static constexpr types::WriteID kMaxWrite = + (lt__(std::numeric_limits::max(), kMinOther) + ? std::numeric_limits::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 + EventPtrs 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 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 + EventPtrs 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(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 + EventPtrs 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(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 + EventPtrs GetWrite(const EventPtrs &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 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 + 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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,520 @@ +/* + * 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 +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#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 +using EventPtrs = + std::array; + +template +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 Op { + public: + typedef EvtStateT EvtState; + + // Types + typedef std::shared_ptr Ptr; + typedef std::vector Thread; + typedef typename Thread::const_iterator ThreadIt; + typedef std::unordered_map Threads; + typedef std::vector> ThreadItStack; + + // Read-only thread types: new Ops can access previous Ops. + typedef std::vector 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 Callback; + typedef std::vector CallbackStack; + + template + friend Threads ExtractThreads(T *container) { + Threads result; + std::unordered_set 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. + * + * @return Last event in program-order generated by this operation. + */ + 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 MemOp : public Op { + public: + explicit MemOp(types::Pid pid) : Op(pid) {} + + virtual types::Addr addr() const = 0; +}; + +template +class NullOp : public Op { + public: + explicit NullOp(types::Pid pid) : Op(pid) {} + + bool EnableEmit(EvtState *evts) override { return false; } + + void InsertPo(typename Op::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 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 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 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(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(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(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) { + 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> + InstPtr_Op; + + std::unique_ptr 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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 +#include + +#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(code); +#define ASM_LEN (static_cast(cnext__ - static_cast(code))) +#define ASM_AT (start + ASM_LEN) + +#define ASM16(v) \ + do { \ + assert(ASM_LEN + 2 <= len); \ + *reinterpret_cast(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 Operation; +typedef MemOp MemOperation; +typedef NullOp NullOperation; + +class Return : public Operation { + public: + explicit Return(types::Pid pid = -1) : Operation(pid) {} + + Operation::Ptr Clone() const override { + return std::make_shared(*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(*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(*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(*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(evts->arch()); + if (arch != nullptr) { + do { + auto potential_dp_read = dynamic_cast(*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(*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(*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(*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(after); + if (potential_write != nullptr) { + auto arch = dynamic_cast(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 + Operation::Ptr operator()(URNG &urng, AddrFilterFunc addr_filter_func, + std::size_t max_fails = 0) const { + // Choice distribution + std::uniform_int_distribution dist_choice(0, 1000 - 1); + + // Pid distribution + std::uniform_int_distribution 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(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 dist_addr( + chunk_min_addr, chunk_max_addr - EvtStateCats::kMaxOpSize); + + // Sequence distribution + std::uniform_int_distribution dist_sequence(1, max_sequence_); + + // Register distribution + std::uniform_int_distribution 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(dist_reg(urng)); + }; + + if (choice < 320) { // 32% + return std::make_shared(addr(), reg(), pid); + } else if (choice < 560) { // 24% + return std::make_shared(addr(), reg(), reg(), pid); + } else if (choice < 980) { // 42% + return std::make_shared(addr(), pid); + } else if (choice < 990) { // 1% + return std::make_shared(pid); + } else if (choice < 1000) { // 1% + return std::make_shared(sequence(), pid); + } + + // should never get here + assert(false); + return nullptr; + } + + template + 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 + 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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 +#include +#include + +#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 Operation; +typedef MemOp MemOperation; +typedef NullOp NullOperation; + +class Return : public Operation { + public: + explicit Return(types::Pid pid = -1) : Operation(pid) {} + + Operation::Ptr Clone() const override { + return std::make_shared(*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(*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(*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(*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(*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(*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(evts->arch()) != nullptr) { + // Implied fence before atomic + auto arch_tso = dynamic_cast(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(*from_) + << ">, but overwriting <" << static_cast(*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(evts->arch()) != nullptr) { + // Implied fence after atomic + auto arch_tso = dynamic_cast(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(*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(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(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 + 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 dist_choice(0, max_choice); + + // Pid distribution + std::uniform_int_distribution 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(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 dist_addr( + chunk_min_addr, chunk_max_addr - EvtStateCats::kMaxOpSize); + + // Sequence distribution + std::uniform_int_distribution 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(addr(), pid); + } else if (choice < 550) { // 5% + return std::make_shared(addr(), pid); + } else if (choice < 970) { // 42% + return std::make_shared(addr(), pid); + } else if (choice < 980) { // 1% + return std::make_shared(addr(), pid); + } else if (choice < 990) { // 1% + return std::make_shared(addr(), pid); + } else if (choice < 1000) { // 1% + return std::make_shared(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(min_a, max_a, pid); + } + } + + // should never get here + assert(false); + return nullptr; + } + + template + 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 + 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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 + +#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(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(code); + + assert(len >= length); + for (std::size_t i = 0; i < length; ++i) { + // ASM> nop ; + *cnext++ = 0x90; + } + + assert((cnext - static_cast(code)) == + static_cast(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(code); + std::size_t expected_len = 0; + + if (addr <= static_cast(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(cnext) = + static_cast(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(cnext) = + static_cast(addr); + cnext += sizeof(std::uint64_t); + } + + assert((cnext - static_cast(code)) == + static_cast(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(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(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(cnext) = + static_cast(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(cnext) = + static_cast(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(code)) == + static_cast(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(code); + std::size_t expected_len = 0; + + assert(write_id != 0); + + if (addr <= static_cast(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(cnext) = + static_cast(addr); + cnext += sizeof(std::uint32_t); + + *reinterpret_cast(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(cnext) = + static_cast(addr); + cnext += sizeof(std::uint64_t); + + // @a + *cnext++ = 0xc6; + *cnext++ = 0x00; + *reinterpret_cast(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(cnext) = + static_cast(addr); + cnext += sizeof(std::uint64_t); + + // @a + *cnext++ = 0xba; + *reinterpret_cast(cnext) = write_id; + cnext += sizeof(std::uint32_t); + + // @f + *cnext++ = 0x66; + *cnext++ = 0x89; + *cnext++ = 0x10; + break; + + default: + assert(false); + } + } + + assert((cnext - static_cast(code)) == + static_cast(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(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(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(cnext) = write_id; + cnext += sizeof(std::uint32_t); + break; + + default: + assert(false); + } + + if (addr <= static_cast(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(cnext) = + static_cast(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(cnext) = + static_cast(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(cnext) = + static_cast(addr); + cnext += sizeof(std::uint64_t); + + // @c + *cnext++ = 0x66; + *cnext++ = 0xf0; + *cnext++ = 0x87; + *cnext++ = 0x02; + break; + + default: + assert(false); + } + } + + assert((cnext - static_cast(code)) == + static_cast(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(code); + std::size_t expected_len = 0; + + if (addr <= static_cast(0xffffffff)) { + // ASM @0> clflush addr ; + expected_len = 8; + assert(len >= expected_len); + + // @0 + *cnext++ = 0x0f; + *cnext++ = 0xae; + *cnext++ = 0x3c; + *cnext++ = 0x25; + *reinterpret_cast(cnext) = + static_cast(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(cnext) = + static_cast(addr); + cnext += sizeof(std::uint64_t); + + // @a + *cnext++ = 0x0f; + *cnext++ = 0xae; + *cnext++ = 0x3a; + } + + assert((cnext - static_cast(code)) == + static_cast(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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 +#include +#include + +#include "../sets.hpp" +#include "../simplega.hpp" +#include "../types.hpp" + +namespace mc2lib { +namespace codegen { + +template +class RandInstTest + : public simplega::Genome { + public: + typedef typename OperationFactory::ResultType Operation; + typedef sets::Set>> 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 g) + : simplega::Genome(std::move(g)), + urng_(parent1.urng_), + factory_(parent1.factory_), + fitness_(0.0f) {} + + void Mutate(float rate) override { + std::uniform_int_distribution dist_idx( + 0, this->genome_.size() - 1); + std::unordered_set used; + std::size_t selection_count = static_cast( + static_cast(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 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/include/mc2lib/mcversi.hpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/include/mc2lib/mcversi.hpp Thu May 05 13:07:16 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 +#include +#include + +#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 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::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(test1.Get()[i].get()); + auto mem_op2 = dynamic_cast(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(mutations) / static_cast(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(op.get()); + if (mem_op != nullptr) { + ++mem_ops; + if (rit.fitaddrs().Contains(mem_op->addr())) { + ++fitaddr_ops; + } + } + } + + return static_cast(fitaddr_ops) / static_cast(mem_ops); + } +}; + +} // namespace mcversi +} // namespace mc2lib + +#endif /* MCVERSI_HPP_ */ + +/* vim: set ts=2 sts=2 sw=2 et : */ diff -r 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 + +#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] + * J. Alglave, L. Maranget, M. Tautschnig, "Herding cats: Modelling, + * Simulation, Testing, and Data Mining for Weak Memory", 2014. + * + * [2] + * J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. "Fences in weak + * memory models", 2012. +*/ +namespace cats { + +class ExecWitness { + public: + template + 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 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 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 MakeChecker(const Architecture* arch, + const ExecWitness* exec) const override { + return arch_->MakeChecker(arch, exec); + } + + std::unique_ptr 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 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 MakeChecker(const Architecture* arch, + const ExecWitness* exec) const override { + return std::unique_ptr(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 MakeChecker(const Architecture* arch, + const ExecWitness* exec) const override { + return std::unique_ptr(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 MakeChecker(const Architecture* arch, + const ExecWitness* exec) const override { + return std::unique_ptr(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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 +#include +#include +#include + +#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::result_type result_type; + result_type operator()(const Iiid& k) const { + return std::hash()(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(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> EventSet; +typedef sets::Relation> EventRel; +typedef sets::RelationSeq> 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 2dd0e6146cbc -r 5c3ff5b33877 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 Thu May 05 13:07:16 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 + +#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] + * J. Alglave, L. Maranget, S. Sarkar, and P. Sewell. "Fences in weak + * memory models", 2012. +*/ +namespace model12 { + +class ExecWitness { + public: + template + 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 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 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 MakeChecker(const Architecture* arch, + const ExecWitness* exec) const override { + return std::unique_ptr(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 MakeChecker(const Architecture* arch, + const ExecWitness* exec) const override { + return std::unique_ptr(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 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/include/mc2lib/sets.hpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/include/mc2lib/sets.hpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,1519 @@ +/* + * 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 +#include +#include +#include +#include +#include + +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 +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 +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 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_; } + + /** + * 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 + 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 +inline Set operator|(const Set& lhs, const Set& rhs) { + Set res = lhs; + return res |= rhs; +} + +template +inline Set operator|(Set&& lhs, const Set& rhs) { + lhs |= rhs; + return std::move(lhs); +} + +template +inline Set operator|(const Set& lhs, Set&& rhs) { + rhs |= lhs; + return std::move(rhs); +} + +template +inline Set operator|(Set&& lhs, Set&& rhs) { + lhs |= rhs; + return std::move(lhs); +} + +template +inline Set operator-(const Set& lhs, const Set& rhs) { + Set res = lhs; + return res -= rhs; +} + +template +inline Set operator-(Set&& lhs, const Set& rhs) { + lhs -= rhs; + return std::move(lhs); +} + +template +inline Set operator-(const Set& lhs, Set&& rhs) { + Set res = lhs; + return res -= rhs; +} + +template +inline Set operator-(Set&& lhs, Set&& rhs) { + lhs -= rhs; + return std::move(lhs); +} + +template +inline Set operator&(const Set& lhs, const Set& rhs) { + Set res; + + for (const auto& e : rhs.Get()) { + if (lhs.Contains(e)) { + res.Insert(e); + } + } + + return res; +} + +template +inline Set operator&(Set&& lhs, const Set& rhs) { + lhs &= rhs; + return std::move(lhs); +} + +template +inline Set operator&(const Set& lhs, Set&& rhs) { + rhs &= lhs; + return std::move(rhs); +} + +template +inline Set operator&(Set&& lhs, Set&& rhs) { + lhs &= rhs; + return std::move(lhs); +} + +template +class Relation { + public: + typedef typename Ts::Element Element; + + typedef typename Ts::template MapContainer> Container; + + typedef std::pair Tuple; + + typedef std::vector 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& e2s) { + if (e2s.Empty()) return; + rel_[e1] |= e2s; + } + + void Insert(const Element& e1, Set&& 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& 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 + 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 + 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_; + } + + /** + * 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 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 Reachable(const Element& e) const { + Set 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& 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& 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& 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& on) const { + return WeakPartialOrder(on) && TotalOn(on); + } + + bool StrictPartialOrder(const Set& 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& 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 On() const { + Set res; + for (const auto& tuples : rel_) { + res.Insert(tuples.first); + res |= tuples.second; + } + return res; + } + + Set 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 res; + for (const auto& tuples : rel_) { + res.Insert(tuples.first); + } + + return res; + } + + Set Range() const { + if (all_props(kReflexiveClosure)) { + // See above. + return On(); + } + + Set 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 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& 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& 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 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* 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* 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* visited_; + FlagSet* visiting_; + bool is_tran_cl_; + SearchMode mode_; + }; + + protected: + Properties props_; + Container rel_; +}; + +template +inline Relation operator*(const Set& lhs, const Set& rhs) { + Relation res; + + for (const auto& e1 : lhs.Get()) { + for (const auto& e2 : rhs.Get()) { + res.Insert(e1, e2); + } + } + + return res; +} + +template +inline Relation operator|(const Relation& lhs, + const Relation& rhs) { + Relation res = lhs; + return res |= rhs; +} + +template +inline Relation operator|(Relation&& lhs, const Relation& rhs) { + lhs |= rhs; + return std::move(lhs); +} + +template +inline Relation operator|(const Relation& lhs, Relation&& rhs) { + rhs |= lhs; + return std::move(rhs); +} + +template +inline Relation operator|(Relation&& lhs, Relation&& rhs) { + lhs |= rhs; + return std::move(lhs); +} + +template +inline Relation operator-(const Relation& lhs, + const Relation& rhs) { + Relation res = lhs; + return res -= rhs; +} + +template +inline Relation operator-(Relation&& lhs, const Relation& rhs) { + lhs -= rhs; + return std::move(lhs); +} + +template +inline Relation operator-(const Relation& lhs, Relation&& rhs) { + Relation res = lhs; + return res -= rhs; +} + +template +inline Relation operator-(Relation&& lhs, Relation&& rhs) { + lhs -= rhs; + return std::move(lhs); +} + +template +inline Relation operator&(const Relation& lhs, + const Relation& rhs) { + Relation res; + + const auto lhs_domain = lhs.Domain(); + for (const auto& e : lhs_domain.Get()) { + Set intersect = lhs.Reachable(e) & rhs.Reachable(e); + // insert checks if empty or not + res.Insert(e, std::move(intersect)); + } + + return res; +} + +template +inline Relation operator&(Relation&& lhs, const Relation& rhs) { + lhs &= rhs; + return std::move(lhs); +} + +template +inline Relation operator&(const Relation& lhs, Relation&& rhs) { + rhs &= lhs; + return std::move(rhs); +} + +template +inline Relation operator&(Relation&& lhs, Relation&& rhs) { + lhs &= rhs; + return std::move(lhs); +} + +/** + * Relation operator base class. + * No derived class shall define a destructor! + */ +template +class RelationOp { + public: + RelationOp() {} + + explicit RelationOp(std::vector> 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 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 EvalClear() { + if (rels_.empty()) { + // Already cleared + return Relation(); + } + + EvalInplace(); + assert(rels_.size() == 1); + + Relation result = std::move(rels_.back()); + rels_.clear(); + return result; // NRVO + } + + protected: + void Add(const Relation& er) { rels_.push_back(er); } + + void Add(Relation&& er) { rels_.push_back(std::move(er)); } + + void Add(const std::vector>& rels) { + rels_.reserve(rels_.size() + rels.size()); + rels_.insert(rels_.end(), rels.begin(), rels.end()); + } + + protected: + std::vector> rels_; +}; + +/** + * Operator ";". + */ +template +class RelationSeq : public RelationOp { + public: + typedef typename Ts::Element Element; + + RelationSeq() {} + + explicit RelationSeq(std::vector> v) + : RelationOp(std::move(v)) {} + + RelationSeq& operator+=(const Relation& rhs) { + this->Add(rhs); + return *this; + } + + RelationSeq& operator+=(Relation&& rhs) { + this->Add(std::move(rhs)); + return *this; + } + + RelationSeq& operator+=(const RelationSeq& rhs) { + this->Add(rhs.rels_); + return *this; + } + + RelationOp& 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 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 Eval() const override { + Relation er; + + if (this->rels_.empty()) { + return Relation(); + } 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::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 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::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 +inline RelationSeq operator+(const RelationSeq& lhs, + const Relation& rhs) { + RelationSeq res = lhs; + return res += rhs; +} + +template +inline RelationSeq operator+(RelationSeq&& lhs, + const Relation& rhs) { + lhs += rhs; + return std::move(lhs); +} + +template +inline RelationSeq operator+(const RelationSeq& lhs, + Relation&& rhs) { + RelationSeq res = lhs; + return res += std::move(rhs); +} + +template +inline RelationSeq operator+(RelationSeq&& lhs, Relation&& rhs) { + lhs += std::move(rhs); + return std::move(lhs); +} + +template +inline RelationSeq operator+(const RelationSeq& lhs, + const RelationSeq& rhs) { + RelationSeq res = lhs; + return res += rhs; +} + +template +inline RelationSeq operator+(RelationSeq&& lhs, + const RelationSeq& rhs) { + lhs += rhs; + return std::move(lhs); +} + +template +inline RelationSeq operator+(const RelationSeq& lhs, + RelationSeq&& rhs) { + RelationSeq res = lhs; + return res += rhs; +} + +template +inline RelationSeq operator+(RelationSeq&& lhs, RelationSeq&& 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 +struct Types { + typedef E Element; + + typedef std::unordered_set SetContainer; + + template + using MapContainer = std::unordered_map; +}; + +} // namespace sets +} // namespace mc2lib + +#endif /* MC2LIB_SETS_HPP_ */ + +/* vim: set ts=2 sts=2 sw=2 et : */ diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/include/mc2lib/simplega.hpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/include/mc2lib/simplega.hpp Thu May 05 13:07:16 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 +#include +#include +#include +#include +#include +#include +#include +#include +#include + +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 +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 dist1(0, mate1.Get().size() - 1); + std::uniform_int_distribution 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 Genome { + public: + typedef std::vector 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 GenePool { + public: + /** + * Using a list for the population pool, as this permits O(1) removal of + * elements. + */ + typedef std::list Population; + typedef std::vector 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(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 + Selection SelectDist(URNG& urng, DIST& dist, std::size_t count) { + assert(population_.size() >= count); + + std::unordered_set 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 + Selection SelectRoulette(URNG& urng, std::size_t count) { + std::discrete_distribution 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 + Selection SelectUniform(URNG& urng, std::size_t count) { + std::uniform_int_distribution 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 + 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 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/include/mc2lib/types.hpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/include/mc2lib/types.hpp Thu May 05 13:07:16 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 + +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 +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::Addr Addr; + +/** + * @brief Processor/thread ID type. + */ +typedef typename Types::Pid Pid; + +/** + * @brief Program order index type. + */ +typedef typename Types::Poi Poi; + +/** + * @brief Instruction pointer type. + */ +typedef typename Types::InstPtr InstPtr; + +/** + * @brief Write ID type. + */ +typedef typename Types::WriteID WriteID; + +} // namespace types +} // namespace mc2lib + +#endif /* MC2LIB_TYPES_HPP_ */ + +/* vim: set ts=2 sts=2 sw=2 et : */ diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/src/test_codegen_armv7.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_codegen_armv7.cpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,180 @@ +#include "mc2lib/codegen/ops/armv7.hpp" +#include "mc2lib/codegen/rit.hpp" +#include "mc2lib/memconsistency/cats.hpp" + +#include + +using namespace mc2lib; +using namespace mc2lib::codegen; +using namespace mc2lib::memconsistency; + +TEST(CodeGen, ARMv7_Short) { + std::default_random_engine urng(42); + + cats::ExecWitness ew; + cats::Arch_ARMv7 arch; + + armv7::RandomFactory factory(0, 1, 0xccc0, 0xccca); + RandInstTest rit( + urng, &factory, 200); + + auto threads = [&rit]() { + auto result = rit.threads(); + EXPECT_EQ(result.size(), 2); + EXPECT_EQ(threads_size(result), rit.Get().size()); + return result; + }; + + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch)), threads()); + + constexpr std::size_t MAX_CODE_SIZE = 4096 / sizeof(std::uint16_t); + std::uint16_t code[MAX_CODE_SIZE]; + + std::size_t emit_len = compiler.Emit(0, 0xffff, code, sizeof(code)); + ASSERT_NE(emit_len, 0); + emit_len = compiler.Emit(1, 0, code, sizeof(code)); + ASSERT_NE(emit_len, 0); + +#ifdef OUTPUT_BIN_TO_TMP + std::fill(code + (emit_len / sizeof(std::uint16_t)), code + MAX_CODE_SIZE, + 0xbf00); + auto f = fopen("/tmp/mc2lib-armv7-test.bin", "wb"); + fwrite(code, sizeof(code), 1, f); + fclose(f); +#endif +} + +// Should be able to handle exhausting write-ids gracefully. +TEST(CodeGen, ARMv7_Exhaust) { + std::default_random_engine urng(42); + + cats::ExecWitness ew; + cats::Arch_ARMv7 arch; + + armv7::RandomFactory factory(0, 1, 0xbeef, 0xfeed); + RandInstTest rit( + urng, &factory, 1234); + + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch)), + rit.threads()); + + constexpr std::size_t MAX_CODE_SIZE = 4096 * 2; + char code[MAX_CODE_SIZE]; + + ASSERT_NE(0, compiler.Emit(0, 0, code, sizeof(code))); + ASSERT_NE(0, compiler.Emit(1, MAX_CODE_SIZE << 1, code, sizeof(code))); +} + +TEST(CodeGen, ARMv7_SC_PER_LOCATION) { + std::vector threads = { + // p0 + std::make_shared(0xf0, 0), // @0x0a + std::make_shared(0xf0, armv7::Backend::r1, 0), // @0x14 + std::make_shared(0xf0, armv7::Backend::r2, 0), // @0x1e + std::make_shared(0xf1, armv7::Backend::r3, 0), // @0x28 + std::make_shared(0xf1, armv7::Backend::r4, 0), // @0x32 + + // p1 + std::make_shared(0xf1, 1), + }; + + cats::ExecWitness ew; + cats::Arch_ARMv7 arch; + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch)), + ExtractThreads(&threads)); + + char code[128]; + + ASSERT_NE(0, compiler.Emit(0, 0, code, sizeof(code))); + ASSERT_NE(0, compiler.Emit(1, 0xffff, code, sizeof(code))); + + auto checker = arch.MakeChecker(&arch, &ew); + ew.po.set_props(mc::EventRel::kTransitiveClosure); + ew.co.set_props(mc::EventRel::kTransitiveClosure); + + types::WriteID wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0x0a, 0, 0xf0, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0x14, 0, 0xf0, &wid, 1)); + ASSERT_FALSE(checker->sc_per_location()); + + // Check update works. + wid = 1; + ASSERT_TRUE(compiler.UpdateObs(0x14, 0, 0xf0, &wid, 1)); + ASSERT_TRUE(checker->sc_per_location()); + + // Read-from external + wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0xffff + 0x0a, 0, 0xf1, &wid, 1)); + wid = 2; + ASSERT_TRUE(compiler.UpdateObs(0x28, 0, 0xf1, &wid, 1)); + wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0x32, 0, 0xf1, &wid, 1)); + ASSERT_FALSE(checker->sc_per_location()); + + // update + wid = 2; + ASSERT_TRUE(compiler.UpdateObs(0x32, 0, 0xf1, &wid, 1)); + ASSERT_TRUE(checker->sc_per_location()); + + ASSERT_TRUE(checker->no_thin_air()); + ASSERT_TRUE(checker->observation()); + ASSERT_TRUE(checker->propagation()); +} + +TEST(CodeGen, ARMv7_OBSERVATION) { + std::vector threads = { + // p0 + std::make_shared(0xf0, armv7::Backend::r1, 0), // @0x08 + std::make_shared(0xf1, armv7::Backend::r3, 0), // @0x12 + std::make_shared(0xf1, armv7::Backend::r2, + armv7::Backend::r1, 0), // @0x1e + + // p1 + std::make_shared(1), // check boundary condition + std::make_shared(0xf1, 1), // 0x0e + std::make_shared(1, 1), // + std::make_shared(1), // + std::make_shared(1, 1), // + std::make_shared(0xfa, 1), // 0x20 + std::make_shared(0xf0, 1), // 0x2c + std::make_shared(1), // check boundary condition + }; + + cats::ExecWitness ew; + cats::Arch_ARMv7 arch; + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch)), + ExtractThreads(&threads)); + + char code[128]; + + ASSERT_NE(0, compiler.Emit(0, 0, code, sizeof(code))); + ASSERT_NE(0, compiler.Emit(1, 0xffff, code, sizeof(code))); + + auto checker = arch.MakeChecker(&arch, &ew); + ew.po.set_props(mc::EventRel::kTransitiveClosure); + ew.co.set_props(mc::EventRel::kTransitiveClosure); + + types::WriteID wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0xffff + 0x0e, 0, 0xf1, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0xffff + 0x22, 0, 0xfa, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0xffff + 0x2e, 0, 0xf0, &wid, 1)); + + wid = 3; + ASSERT_TRUE(compiler.UpdateObs(0x08, 0, 0xf0, &wid, 1)); + wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0x12, 0, 0xf1, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0x1e, 0, 0xf1, &wid, 1)); + ASSERT_FALSE(checker->observation()); + + wid = 1; + ASSERT_TRUE(compiler.UpdateObs(0x1e, 0, 0xf1, &wid, 1)); + ASSERT_TRUE(checker->observation()); + + ASSERT_TRUE(checker->no_thin_air()); + ASSERT_TRUE(checker->sc_per_location()); + ASSERT_TRUE(checker->propagation()); +} diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/src/test_codegen_x86_64.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_codegen_x86_64.cpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,194 @@ +#include "mc2lib/codegen/ops/x86_64.hpp" +#include "mc2lib/codegen/rit.hpp" +#include "mc2lib/memconsistency/cats.hpp" + +#include + +using namespace mc2lib; +using namespace mc2lib::codegen; +using namespace mc2lib::memconsistency; + +TEST(CodeGen, X86_64) { + std::default_random_engine urng(1238); + + cats::ExecWitness ew; + cats::Arch_TSO arch; + + strong::RandomFactory factory(0, 1, 0xccc0, 0xccca); + RandInstTest rit( + urng, &factory, 150); + + auto threads = [&rit]() { + auto result = rit.threads(); + EXPECT_EQ(result.size(), 2); + EXPECT_EQ(threads_size(result), rit.Get().size()); + return result; + }; + + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch)), threads()); + + char code[1024]; + + std::size_t emit_len = compiler.Emit(0, 0xffff, code, sizeof(code)); + ASSERT_NE(emit_len, 0); + ASSERT_TRUE(compiler.IpToOp(0xffff - 1) == nullptr); + ASSERT_TRUE(compiler.IpToOp(0xffff + emit_len) == nullptr); + ASSERT_TRUE(compiler.IpToOp(0x1234) == nullptr); + ASSERT_TRUE(compiler.IpToOp(0xffff) != nullptr); + ASSERT_TRUE(compiler.IpToOp(0xffff + emit_len - 1) != nullptr); + + emit_len = compiler.Emit(1, 0, code, sizeof(code)); + ASSERT_NE(emit_len, 0); + +#ifdef OUTPUT_BIN_TO_TMP + memset(code + emit_len, 0x90, sizeof(code) - emit_len); + auto f = fopen("/tmp/mc2lib-test1.bin", "wb"); + fwrite(code, sizeof(code), 1, f); + fclose(f); +#endif +} + +TEST(CodeGen, X86_64_SC_PER_LOCATION) { + std::vector threads = { + // p0 + std::make_shared(0xf0, 0), // @0x0 + std::make_shared(0xf0, 0), // @0x8 + std::make_shared(0xf1, 0), // 0x17 + + // p1 + std::make_shared(0xf1, 1), // 0x0 + }; + + cats::ExecWitness ew; + cats::Arch_TSO arch; + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch)), + ExtractThreads(&threads)); + + char code[128]; + + ASSERT_NE(0, compiler.Emit(0, 0, code, sizeof(code))); + ASSERT_NE(0, compiler.Emit(1, 0xffff, code, sizeof(code))); + + auto checker = arch.MakeChecker(&arch, &ew); + ew.po.set_props(mc::EventRel::kTransitiveClosure); + ew.co.set_props(mc::EventRel::kTransitiveClosure); + + types::WriteID wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0x0, 0, 0xf0, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0x8, 0, 0xf0, &wid, 1)); + ASSERT_FALSE(checker->sc_per_location()); + + wid = 0x1; // check replacement/update works + ASSERT_TRUE(compiler.UpdateObs(0x8, 0, 0xf0, &wid, 1)); + ASSERT_TRUE(checker->sc_per_location()); + + // Check atomic works + wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0xffff + 0x0, 0, 0xf1, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0x17, 0, 0xf1, &wid, 1)); + + try { + wid = 3; + compiler.UpdateObs(0x17, 1, 0xf1, &wid, 1); + FAIL(); + } catch (const Error& e) { + ASSERT_NE(std::string(e.what()).find("NOT ATOMIC"), std::string::npos); + } + + wid = 3; // restart atomic + ASSERT_TRUE(compiler.UpdateObs(0x17, 0, 0xf1, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0x17, 1, 0xf1, &wid, 1)); + + ASSERT_TRUE(checker->sc_per_location()); + ASSERT_TRUE(checker->no_thin_air()); + ASSERT_TRUE(checker->observation()); + ASSERT_TRUE(checker->propagation()); +} + +TEST(CodeGen, X86_64_VA_Synonyms) { + std::vector threads = { + // p0 + std::make_shared(0x1ff, 0), // @0x0 + std::make_shared(0x2ff, 0), // @0x8 + + // p1 + std::make_shared(0x3ff, 1), // 0x0 + std::make_shared(0x3fe, 1), // 0x8 + }; + + cats::ExecWitness ew; + cats::Arch_TSO arch; + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch)), + ExtractThreads(&threads)); + compiler.evts()->set_addr_mask(0xff); + + char code[128]; + + ASSERT_NE(0, compiler.Emit(0, 0, code, sizeof(code))); + ASSERT_NE(0, compiler.Emit(1, 0xffff, code, sizeof(code))); + + auto checker = arch.MakeChecker(&arch, &ew); + ew.po.set_props(mc::EventRel::kTransitiveClosure); + ew.co.set_props(mc::EventRel::kTransitiveClosure); + + types::WriteID wid = 0; + ASSERT_TRUE(compiler.UpdateObs(0x0, 0, 0x1ff, &wid, 1)); + ASSERT_TRUE(compiler.UpdateObs(0xffff + 0x8, 0, 0x3fe, &wid, 1)); + wid = 1; + ASSERT_TRUE(compiler.UpdateObs(0xffff + 0x0, 0, 0x3ff, &wid, 1)); + wid = 2; + ASSERT_TRUE(compiler.UpdateObs(0x8, 0, 0x2ff, &wid, 1)); + + ASSERT_NO_THROW(checker->wf()); + ASSERT_TRUE(checker->sc_per_location()); + ASSERT_TRUE(checker->no_thin_air()); + ASSERT_TRUE(checker->observation()); + ASSERT_TRUE(checker->propagation()); +} + +#if defined(__linux__) && defined(__x86_64__) +#include +TEST(CodeGen, X86_64_ExecLinux) { + cats::ExecWitness ew; + cats::Arch_TSO arch; + + Compiler compiler( + std::unique_ptr(new EvtStateCats(&ew, &arch))); + + unsigned char test_mem[] = {0x03, 0x14, 0x25, 0x36, 0x47, 0x58, 0x69, 0x7a, + 0x8b, 0x9c, 0xad, 0xbe, 0xcf, 0xd0, 0xe1, 0xf2}; + + strong::Operation::Ptr ops[] = { + std::make_shared( + reinterpret_cast(&test_mem[0xf])), + std::make_shared()}; + + const std::size_t MAX_CODE_SIZE = 4096; + char* code = reinterpret_cast(mmap(NULL, MAX_CODE_SIZE, + PROT_READ | PROT_WRITE | PROT_EXEC, + MAP_ANONYMOUS | MAP_PRIVATE, 0, 0)); + memset(code, 0x90, MAX_CODE_SIZE); + + std::size_t emit_len = 0; + for (auto& op : ops) { + emit_len += compiler.Emit(emit_len, op.get(), code + emit_len, + MAX_CODE_SIZE - emit_len, nullptr, nullptr); + } + + unsigned char (*func)() = reinterpret_cast(code); + unsigned result = func(); + + ASSERT_EQ(result, test_mem[0xf]); + +#ifdef OUTPUT_BIN_TO_TMP + auto f = fopen("/tmp/mc2lib-test2.bin", "wb"); + fwrite(code, MAX_CODE_SIZE, 1, f); + fclose(f); +#endif + + munmap(code, MAX_CODE_SIZE); +} +#endif diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/src/test_main.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_main.cpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,6 @@ +#include + +int main(int argc, char **argv) { + ::testing::InitGoogleTest(&argc, argv); + return RUN_ALL_TESTS(); +} diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/src/test_mcversi.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_mcversi.cpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,34 @@ +#include "mc2lib/codegen/ops/strong.hpp" +#include "mc2lib/codegen/rit.hpp" +#include "mc2lib/mcversi.hpp" + +#include + +using namespace mc2lib; + +// This can only check syntax and type correctness: most literals are +// arbitrary. +TEST(McVerSi, CrossoverMutate) { + std::default_random_engine urng; + codegen::strong::RandomFactory factory(0, 2, 0, 10); + + typedef codegen::RandInstTest RandInstTest; + + simplega::GenePool::Population initial_population; + + for (size_t i = 0; i < 10; ++i) { + initial_population.emplace_back(urng, &factory, 20); + } + + simplega::GenePool pool(initial_population, 0.1f); + + auto selection = pool.SelectUniform(urng, 3); + + // Same values as in McVerSi paper. + mcversi::CrossoverMutate + crossover_mutate(0.2, 0.05); + + pool.Step(urng, crossover_mutate, selection, selection.size()); +} diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/src/test_memconsistency.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_memconsistency.cpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,111 @@ +#include "mc2lib/memconsistency/cats.hpp" +#include "mc2lib/memconsistency/model12.hpp" + +#include + +#include + +using namespace mc2lib::memconsistency; + +TEST(MemConsistency, Model12Empty) { + model12::ExecWitness ew; + model12::Arch_SC sc; + auto c = sc.MakeChecker(&sc, &ew); + + ASSERT_NO_THROW(c->wf()); + ASSERT_TRUE(c->uniproc()); + ASSERT_TRUE(c->thin()); + ASSERT_TRUE(c->check_exec()); + ASSERT_NO_THROW(c->valid_exec()); +} + +TEST(MemConsistency, CatsEmpty) { + cats::ExecWitness ew; + cats::Arch_SC sc; + auto c = sc.MakeChecker(&sc, &ew); + + ASSERT_NO_THROW(c->wf()); + ASSERT_TRUE(c->sc_per_location()); + ASSERT_TRUE(c->no_thin_air()); + ASSERT_TRUE(c->observation()); + ASSERT_TRUE(c->propagation()); + ASSERT_NO_THROW(c->valid_exec()); +} + +TEST(MemConsistency, Model12DekkerValidSC) { + model12::ExecWitness ew; + model12::Arch_SC sc; + auto c = sc.MakeChecker(&sc, &ew); + + Event Ix = Event(Event::kWrite, 10, Iiid(-1, 0)); + Event Iy = Event(Event::kWrite, 20, Iiid(-1, 1)); + + Event Wx0 = Event(Event::kWrite, 10, Iiid(0, 12)); + Event Wy1 = Event(Event::kWrite, 20, Iiid(1, 33)); + Event Ry0 = Event(Event::kRead, 20, Iiid(0, 55)); + Event Rx1 = Event(Event::kRead, 10, Iiid(1, 22)); + + ew.events |= EventSet({Ix, Iy, Wx0, Wy1, Ry0, Rx1}); + + ew.po.Insert(Wx0, Ry0); + ew.po.Insert(Wy1, Rx1); + + ew.ws.Insert(Ix, Wx0); + ew.ws.Insert(Iy, Wy1); + + ew.rf.Insert(Wx0, Rx1); + ew.rf.Insert(Wy1, Ry0); + + ASSERT_NO_THROW(c->wf()); + ASSERT_TRUE(c->uniproc()); + ASSERT_TRUE(c->thin()); + ASSERT_TRUE(c->check_exec()); + ASSERT_NO_THROW(c->valid_exec()); +} + +TEST(MemConsistency, CatsDekkerInvalidSCValidTSO) { + cats::ExecWitness ew; + cats::Arch_SC sc; + cats::Arch_TSO tso; + auto c_sc = sc.MakeChecker(&sc, &ew); + auto c_tso = tso.MakeChecker(&tso, &ew); + + Event Ix = Event(Event::kWrite, 10, Iiid(-1, 0)); + Event Iy = Event(Event::kWrite, 20, Iiid(-1, 1)); + + Event Wx0 = Event(Event::kWrite, 10, Iiid(0, 12)); + Event Wy1 = Event(Event::kWrite, 20, Iiid(1, 33)); + Event Ry0 = Event(Event::kRead, 20, Iiid(0, 55)); + Event Rx1 = Event(Event::kRead, 10, Iiid(1, 22)); + + ew.events |= EventSet({Ix, Iy, Wx0, Wy1, Ry0, Rx1}); + + ew.po.Insert(Wx0, Ry0); + ew.po.Insert(Wy1, Rx1); + + ew.co.Insert(Ix, Wx0); + ew.co.Insert(Iy, Wy1); + + ew.rf.Insert(Ix, Rx1); + ew.rf.Insert(Iy, Ry0); + + ASSERT_NO_THROW(c_sc->wf()); + ASSERT_TRUE(c_sc->sc_per_location()); + ASSERT_TRUE(c_sc->no_thin_air()); + ASSERT_TRUE(c_sc->observation()); + ASSERT_FALSE(c_sc->propagation()); + + try { + c_sc->valid_exec(); + FAIL(); + } catch (const Error& e) { + ASSERT_EQ(std::string("PROPAGATION"), e.what()); + } + + ASSERT_NO_THROW(c_tso->wf()); + ASSERT_TRUE(c_tso->sc_per_location()); + ASSERT_TRUE(c_tso->no_thin_air()); + ASSERT_TRUE(c_tso->observation()); + ASSERT_TRUE(c_tso->propagation()); + ASSERT_NO_THROW(c_tso->valid_exec()); +} diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/src/test_sets.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_sets.cpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,371 @@ +#include "mc2lib/memconsistency/eventsets.hpp" +#include "mc2lib/sets.hpp" + +#include + +using namespace mc2lib; +using namespace mc2lib::memconsistency; + +static Event base_event; +static Event ResetEvt() { + base_event.iiid.poi = 0; + return base_event; +} +static Event NextEvt() { + ++base_event.iiid; + return base_event; +} + +TEST(Sets, SimpleSet) { + EventSet s = EventSet({NextEvt(), NextEvt(), NextEvt()}); + ASSERT_EQ((s * s).size(), 9); + ASSERT_FALSE(s.Subset(s)); + ASSERT_TRUE(s.SubsetEq(s)); + ASSERT_TRUE(s == (s * s).Range()); + ASSERT_TRUE((s | s) == s); +} + +TEST(Sets, CycleDetectionUnionNo) { + Event e1 = ResetEvt(); + Event e2, e3; + + EventRel er1; + er1.Insert(e3 = e1, e2 = NextEvt()); + er1.Insert(e2, e1 = NextEvt()); + er1.Insert(e3, e1); + + ASSERT_FALSE(er1.props()); + ASSERT_TRUE(er1.Acyclic()); + ASSERT_FALSE(er1.props()); + + EventRel er2; + er2.Insert(e1, e2 = NextEvt()); + er2.Insert(e1, e2 = NextEvt()); + er2.Insert(e1, e2 = NextEvt()); + + ASSERT_TRUE(er1.Transitive()); + ASSERT_TRUE(er2.Transitive()); + ASSERT_TRUE((er1 | er2).Acyclic()); + er1 |= er2; + ASSERT_EQ(er1.size(), 6); + + er2.set_props(EventRel::kTransitiveClosure); + ASSERT_TRUE((EventRel() | er2).Acyclic()); +} + +TEST(Sets, CycleDetectionYes) { + Event e1 = ResetEvt(); + Event e2; + Event e3; + + EventRel er; + er.Insert(e1, e2 = NextEvt()); + er.Insert(e3 = e2, e1 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + + EventRel er_; + er_.Insert(e1, e2 = NextEvt()); + er_.Insert(e2, e3); + er_.Insert(e2, NextEvt()); + er_.Insert(e2, NextEvt()); + er_.Insert(e2, NextEvt()); + er_.Insert(e2, NextEvt()); + er |= er_; + + ASSERT_FALSE(er.Acyclic()); + + er.set_props(EventRel::kReflexiveTransitiveClosure); + ASSERT_EQ(er.size(), 43); +} + +TEST(Sets, CycleDetectionYes2) { + Event e1 = ResetEvt(); + Event e2; + Event e3; + + EventRel er; + er.Insert(e1, e2 = NextEvt()); + er.Insert(e3 = e2, e1 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e2, e1 = NextEvt()); + er.Insert(e1, e3); + + for (int i = 0; i < 30; ++i) { + // Catch out buggy cycle detection implementations, where they do not + // consider a visisted node after being visited once before. + // + // As unordered maps are used as backing store, by adding more edges + // that do not contribute to the cycle, we are likely to traverse these + // first. + er.Insert(NextEvt(), e3); + } + + EventRel::Path p; + ASSERT_FALSE(er.Acyclic(&p)); + ASSERT_TRUE(p[1] == p.back()); + ASSERT_EQ(p.size(), 6); + + p.clear(); + er.set_props(EventRel::kTransitiveClosure); + ASSERT_TRUE(er.R(e3, e1, &p)); + ASSERT_TRUE(p.front() == e3); + ASSERT_TRUE(p.back() == e1); + ASSERT_EQ(p.size(), 4); +} + +TEST(Sets, EventRelDiff) { + Event e1 = ResetEvt(); + Event e2; + + EventRel er; + er.Insert(e1, e2 = NextEvt()); + er.Insert(e2, e1 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + + EventRel d; + d.Insert(e1, e2); + d.Insert(e1, NextEvt()); + er -= d; + ASSERT_EQ(er.size(), 4); + + d.set_props(EventRel::kReflexiveTransitiveClosure); + auto evald = d.Eval(); + ASSERT_TRUE(d == evald); + ASSERT_TRUE(d.Raw() != evald.Raw()); + ASSERT_EQ(d.size(), 5); +} + +TEST(Sets, EventRelDiffProps) { + Event e1 = ResetEvt(); + Event e2, start; + + EventRel er; + er.Insert(start = e1, e2 = NextEvt()); + er.Insert(e2, e1 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + + EventRel d; + d.Insert(start, e2); + d.Insert(e2, e2); + d.Insert(e2, start); + er.add_props(EventRel::kTransitiveClosure); + d -= er; + ASSERT_EQ(d.size(), 2); + + er.add_props(EventRel::kReflexiveClosure); + d -= er; + ASSERT_EQ(d.size(), 1); +} + +TEST(Sets, EventRelIntersect) { + Event e1 = ResetEvt(); + Event e2; + + EventRel er; + er.Insert(e1, e2 = NextEvt()); + er.Insert(e2, e1 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e1); + + EventRel d; + d.Insert(e1, e2); + d.Insert(e1, NextEvt()); + d.Insert(e1, NextEvt()); + ASSERT_EQ((d & er).size(), 1); + + d.set_props(EventRel::kReflexiveClosure); + d &= er; + ASSERT_FALSE(d.props()); + ASSERT_EQ(d.size(), 2); + + ASSERT_TRUE(d.Domain().Subset(er.Domain())); +} + +TEST(Sets, EventRelInverse) { + Event e1 = ResetEvt(); + Event e2; + + EventRel er; + er.Insert(e1, e2 = NextEvt()); + er.Insert(e2, e1 = NextEvt()); + er.Insert(e2, e1 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + + EventRel inv = er.Inverse(); + ASSERT_TRUE(er.Domain() == inv.Range()); + ASSERT_TRUE(er.Range() == inv.Domain()); + ASSERT_EQ(er.size(), inv.size()); + + er.for_each([&inv](const Event& e1, const Event& e2) { + ASSERT_TRUE(inv.R(e2, e1)); + ASSERT_FALSE(inv.R(e1, e2)); + }); + + er.set_props(EventRel::kReflexiveTransitiveClosure); + inv = er.Inverse(); + ASSERT_TRUE(er.Domain() == inv.Range()); + ASSERT_TRUE(er.Range() == inv.Domain()); + ASSERT_EQ(er.size(), inv.size()); +} + +TEST(Sets, EventRelSeqR) { + Event e1 = ResetEvt(); + Event e2; + Event start, end; + + EventRelSeq ers; + EventRel er; + er.Insert(start = e1, e2 = NextEvt()); + ers += er; + + er = EventRel(); + er.Insert(e2, e1 = NextEvt()); + ers += EventRel(er); + + er = EventRel(); + er.Insert(e1, end = e2 = NextEvt()); + er.Insert(e2, e1 = NextEvt()); + er.add_props(EventRel::kTransitiveClosure); + ers += er; + + // First unevald + ASSERT_TRUE(ers.R(start, end)); + ASSERT_TRUE(ers.R(start, e1)); + ASSERT_TRUE(ers.Irreflexive()); + + const EventRel evald = ers.Eval(); + auto ers_copy = ers; + const EventRel evald_inplace = ers_copy.EvalClear(); + ASSERT_TRUE(evald == evald_inplace); + + ers.EvalInplace(); + // Should be same result after eval_inplace + ASSERT_TRUE(ers.R(start, end)); + ASSERT_TRUE(ers.R(start, e1)); + ASSERT_TRUE(ers.Irreflexive()); + + // Check evald + ASSERT_TRUE(evald.R(start, end)); + ASSERT_TRUE(evald.R(start, e1)); + ASSERT_TRUE(evald.Irreflexive()); +} + +TEST(Sets, EventRelSeqIrrefl1) { + Event e1 = ResetEvt(); + Event e2; + Event start, end; + + EventRelSeq ers; + EventRel er; + er.Insert(e1, NextEvt()); + er.Insert(e1, NextEvt()); + er.Insert(e1, NextEvt()); + er.Insert(start = e1, e2 = NextEvt()); + ers += er; + + er = EventRel(); + er.Insert(e2, e1 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.add_props(EventRel::kTransitiveClosure); + ers += er; + + er = EventRel(); + er.Insert(e2, start); + ers += er; + + ASSERT_FALSE(ers.Irreflexive()); + + const EventRel evald = ers.Eval(); + ASSERT_FALSE(evald.Irreflexive()); + + EventRel::Path p; + ers.Irreflexive(&p); + ASSERT_EQ(p.size(), 5); +} + +TEST(Sets, EventRelSeqIrrefl2) { + Event e1 = ResetEvt(); + Event e2; + Event start; + + EventRelSeq ers; + EventRel er; + er.Insert(start = e1, e2 = NextEvt()); + ers += er; + + er = EventRel(); + er.Insert(e2, start); + ers += er; + + er = EventRel(); + er.Insert(start, NextEvt()); + ASSERT_TRUE(er.Irreflexive()); + + er.add_props(EventRel::kReflexiveClosure); + ASSERT_FALSE(er.Irreflexive()); + ers += er; + + ASSERT_FALSE(ers.Irreflexive()); + + const EventRel evald = ers.Eval(); + ASSERT_FALSE(evald.Irreflexive()); +} + +TEST(Sets, EventRelReflexivePath) { + Event e1 = ResetEvt(); + Event e2; + + EventRelSeq ers; + + EventRel er; + er.Insert(e1, e2 = NextEvt()); + er.Insert(e1, e2 = NextEvt()); + er.set_props(EventRel::kReflexiveClosure); + ers += er; + + er = EventRel(); + er.Insert(e2, e1 = NextEvt()); + er.set_props(EventRel::kReflexiveClosure); + ers += er; + + EventRel::Path p; + ASSERT_FALSE(er.Irreflexive(&p)); + ASSERT_EQ(p.size(), 2); + ASSERT_TRUE(p[0] == p[1]); + + p.clear(); + ASSERT_FALSE(ers.Irreflexive(&p)); + ASSERT_EQ(p.size(), 3); + ASSERT_TRUE(p[0] == p[1]); + ASSERT_TRUE(p[1] == p[2]); +} + +TEST(Sets, EventRelSubset) { + Event e1 = ResetEvt(); + Event e2; + + EventRel er1; + er1.Insert(e1, e2 = NextEvt()); + er1.Insert(e2, e1 = NextEvt()); + er1.Insert(e2, e1 = NextEvt()); + er1.set_props(EventRel::kReflexiveTransitiveClosure); + + EventRel er2 = er1.Eval(); + ASSERT_TRUE(er2.SubsetEq(er1)); + ASSERT_TRUE(er1.SubsetEq(er2)); + ASSERT_FALSE(er2.Subset(er1)); + + er2.Insert(e1, e2 = NextEvt()); + er2.Insert(e1, e2 = NextEvt()); + + ASSERT_FALSE(er2.Subset(er1)); + ASSERT_TRUE(er1.Subset(er2)); +} diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/src/test_simplega.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_simplega.cpp Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,107 @@ +#include "mc2lib/simplega.hpp" + +#include + +#include + +using namespace mc2lib::simplega; + +class GenomeAdd : public Genome { + public: + static std::default_random_engine* urng; + + GenomeAdd() { + genome_.resize(5); + MutateImpl(1.0f); + } + + GenomeAdd(const GenomeAdd& parent1, const GenomeAdd& parent2, + const std::vector& g) + : Genome(g) {} + + void Mutate(float rate) override { MutateImpl(rate); }; + + float Fitness() const override { + float total = 0.0; + for (const auto& f : genome_) { + total += f; + } + + // restrict size + if (genome_.size() > 10) { + return 999.0f; + } + + // want to get sum closest to 24. + return (24 - total) * (24 - total); + } + + bool operator<(const Genome& rhs) const override { + return Fitness() < rhs.Fitness(); + } + + operator float() const override { return 1000.f - Fitness(); } + + private: + void MutateImpl(float rate) { + std::uniform_int_distribution dist_idx(0, genome_.size() - 1); + std::uniform_real_distribution dist_mut(-2.0f, 2.0f); + std::unordered_set used; + std::size_t selection_count = + static_cast(static_cast(genome_.size()) * rate); + + while (selection_count) { + auto idx = dist_idx(*urng); + if (used.find(idx) != used.end()) { + continue; + } + + genome_[idx] += dist_mut(*urng); + + used.insert(idx); + --selection_count; + } + } +}; + +// TODO(melver): Use proper test harness. +std::default_random_engine* GenomeAdd::urng = nullptr; + +TEST(SimpleGA, Add24) { + std::default_random_engine urng(1234); + GenomeAdd::urng = &urng; + + GenePool pool(25, // population_size + 0.3f); // mutation_rate + + std::size_t tournament_size = 10; + std::size_t tournament_winners = 5; + std::size_t elite = tournament_winners; + + for (int i = 0; i < 50; ++i) { + auto tournament_population = pool.SelectUniform(urng, tournament_size); + pool.SelectionSort(&tournament_population); + pool.Step(urng, + evolve::CutSpliceMutate::Population>, + tournament_population, tournament_winners, elite); + ASSERT_TRUE(pool.population_size() <= pool.target_population_size() + 1); + } + + // This mainly checks that the discrete_distribution implementation works + // as expected. + ASSERT_TRUE(GenePool(pool.SelectRoulette(urng, tournament_size)) + .AverageFitness() < + GenePool(pool.SelectUniform(urng, tournament_size)) + .AverageFitness()); + + ASSERT_TRUE(pool.BestFitness() < pool.WorstFitness()); + + auto gene = pool.SelectBest(); + float sum = 0.0f; + for (const auto& f : gene.Get()) { + sum += f; + } + + ASSERT_TRUE(sum >= 23.1f && sum <= 24.9); +} diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/.gitmodules --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/.gitmodules Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,3 @@ +[submodule "third_party/googletest"] + path = third_party/googletest + url = https://github.com/google/googletest.git diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/.travis.yml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/.travis.yml Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,42 @@ +# vim: set ts=2 sw=2 sts=2 et : + +language: cpp + +matrix: + include: + # Oldest supported GCC + - os: linux + addons: + apt: + sources: ubuntu-toolchain-r-test + packages: g++-4.7 + compiler: gcc-4.7 + env: CXX_=g++-4.7 + + # Latest GCC + - os: linux + addons: + apt: + sources: ubuntu-toolchain-r-test + packages: g++-5 + compiler: gcc-5 + env: CXX_=g++-5 + + # Latest Clang + - os: linux + addons: + apt: + sources: + - ubuntu-toolchain-r-test + - llvm-toolchain-precise-3.7 + packages: clang-3.7 + compiler: clang-3.7 + env: CXX_=clang++-3.7 + +script: + # Travis exports CXX after set via env. Fix. + - export CXX=$CXX_ + - $CXX --version + # Test library + - make clean check + - make clean check BUILDFLAGS='-O2 -DNDEBUG' diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/AUTHORS --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/AUTHORS Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,1 @@ +git shortlog -se diff -r 2dd0e6146cbc -r 5c3ff5b33877 ext/mc2lib/Doxyfile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/Doxyfile Thu May 05 13:07:16 2016 +0100 @@ -0,0 +1,2314 @@ +# Doxyfile 1.8.7 + +# This file describes the settings to be used by the documentation system +# doxygen (www.doxygen.org) for a project. +# +# All text after a double hash (##) is considered a comment and is placed in +# front of the TAG it is preceding. +# +# All text after a single hash (#) is considered a comment and will be ignored. +# The format is: +# TAG = value [value, ...] +# For lists, items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (\" \"). + +#--------------------------------------------------------------------------- +# Project related configuration options +#--------------------------------------------------------------------------- + +# This tag specifies the encoding used for all characters in the config file +# that follow. The default is UTF-8 which is also the encoding used for all text +# before the first occurrence of this tag. Doxygen uses libiconv (or the iconv +# built into libc) for the transcoding. See http://www.gnu.org/software/libiconv +# for the list of possible encodings. +# The default value is: UTF-8. + +DOXYFILE_ENCODING = UTF-8 + +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded by +# double-quotes, unless you are using Doxywizard) that should identify the +# project for which the documentation is generated. This name is used in the +# title of most generated pages and in a few other places. +# The default value is: My Project. + +PROJECT_NAME = "mc2lib" + +# The PROJECT_NUMBER tag can be used to enter a project or revision number. This +# could be handy for archiving the generated documentation or if some version +# control system is used. + +#PROJECT_NUMBER = 0.1 + +# Using the PROJECT_BRIEF tag one can provide an optional one line description +# for a project that appears at the top of each page and should give viewer a +# quick idea about the purpose of the project. Keep the description short. + +PROJECT_BRIEF = + +# With the PROJECT_LOGO tag one can specify an logo or icon that is included in +# the documentation. The maximum height of the logo should not exceed 55 pixels +# and the maximum width should not exceed 200 pixels. Doxygen will copy the logo +# to the output directory. + +PROJECT_LOGO = + +# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) path +# into which the generated documentation will be written. If a relative path is +# entered, it will be relative to the location where doxygen was started. If +# left blank the current directory will be used. + +OUTPUT_DIRECTORY = ./apidoc + +# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create 4096 sub- +# directories (in 2 levels) under the output directory of each output format and +# will distribute the generated files over these directories. Enabling this +# option can be useful when feeding doxygen a huge amount of source files, where +# putting all generated files in the same directory would otherwise causes +# performance problems for the file system. +# The default value is: NO. + +CREATE_SUBDIRS = NO + +# If the ALLOW_UNICODE_NAMES tag is set to YES, doxygen will allow non-ASCII +# characters to appear in the names of generated files. If set to NO, non-ASCII +# characters will be escaped, for example _xE3_x81_x84 will be used for Unicode +# U+3044. +# The default value is: NO. + +ALLOW_UNICODE_NAMES = NO + +# The OUTPUT_LANGUAGE tag is used to specify the language in which all +# documentation generated by doxygen is written. Doxygen will use this +# information to generate all constant output in the proper language. +# Possible values are: Afrikaans, Arabic, Armenian, Brazilian, Catalan, Chinese, +# Chinese-Traditional, Croatian, Czech, Danish, Dutch, English (United States), +# Esperanto, Farsi (Persian), Finnish, French, German, Greek, Hungarian, +# Indonesian, Italian, Japanese, Japanese-en (Japanese with English messages), +# Korean, Korean-en (Korean with English messages), Latvian, Lithuanian, +# Macedonian, Norwegian, Persian (Farsi), Polish, Portuguese, Romanian, Russian, +# Serbian, Serbian-Cyrillic, Slovak, Slovene, Spanish, Swedish, Turkish, +# Ukrainian and Vietnamese. +# The default value is: English. + +OUTPUT_LANGUAGE = English + +# If the BRIEF_MEMBER_DESC tag is set to YES doxygen will include brief member +# descriptions after the members that are listed in the file and class +# documentation (similar to Javadoc). Set to NO to disable this. +# The default value is: YES. + +BRIEF_MEMBER_DESC = YES + +# If the REPEAT_BRIEF tag is set to YES doxygen will prepend the brief +# description of a member or function before the detailed description +# +# Note: If both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the +# brief descriptions will be completely suppressed. +# The default value is: YES. + +REPEAT_BRIEF = YES + +# This tag implements a quasi-intelligent brief description abbreviator that is +# used to form the text in various listings. Each string in this list, if found +# as the leading text of the brief description, will be stripped from the text +# and the result, after processing the whole list, is used as the annotated +# text. Otherwise, the brief description is used as-is. If left blank, the +# following values are used ($name is automatically replaced with the name of +# the entity):The $name class, The $name widget, The $name file, is, provides, +# specifies, contains, represents, a, an and the. + +ABBREVIATE_BRIEF = + +# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then +# doxygen will generate a detailed section even if there is only a brief +# description. +# The default value is: NO. + +ALWAYS_DETAILED_SEC = NO + +# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all +# inherited members of a class in the documentation of that class as if those +# members were ordinary class members. Constructors, destructors and assignment +# operators of the base classes will not be shown. +# The default value is: NO. + +INLINE_INHERITED_MEMB = NO + +# If the FULL_PATH_NAMES tag is set to YES doxygen will prepend the full path +# before files name in the file list and in the header files. If set to NO the +# shortest path that makes the file name unique will be used +# The default value is: YES. + +FULL_PATH_NAMES = YES + +# The STRIP_FROM_PATH tag can be used to strip a user-defined part of the path. +# Stripping is only done if one of the specified strings matches the left-hand +# part of the path. The tag can be used to show relative paths in the file list. +# If left blank the directory from which doxygen is run is used as the path to +# strip. +# +# Note that you can specify absolute paths here, but also relative paths, which +# will be relative from the directory where doxygen is started. +# This tag requires that the tag FULL_PATH_NAMES is set to YES. + +STRIP_FROM_PATH = + +# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of the +# path mentioned in the documentation of a class, which tells the reader which +# header file to include in order to use a class. If left blank only the name of +# the header file containing the class definition is used. Otherwise one should +# specify the list of include paths that are normally passed to the compiler +# using the -I flag. + +STRIP_FROM_INC_PATH = + +# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter (but +# less readable) file names. This can be useful is your file systems doesn't +# support long names like on DOS, Mac, or CD-ROM. +# The default value is: NO. + +SHORT_NAMES = NO + +# If the JAVADOC_AUTOBRIEF tag is set to YES then doxygen will interpret the +# first line (until the first dot) of a Javadoc-style comment as the brief +# description. If set to NO, the Javadoc-style will behave just like regular Qt- +# style comments (thus requiring an explicit @brief command for a brief +# description.) +# The default value is: NO. + +JAVADOC_AUTOBRIEF = NO + +# If the QT_AUTOBRIEF tag is set to YES then doxygen will interpret the first +# line (until the first dot) of a Qt-style comment as the brief description. If +# set to NO, the Qt-style will behave just like regular Qt-style comments (thus +# requiring an explicit \brief command for a brief description.) +# The default value is: NO. + +QT_AUTOBRIEF = NO + +# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make doxygen treat a +# multi-line C++ special comment block (i.e. a block of //! or /// comments) as +# a brief description. This used to be the default behavior. The new default is +# to treat a multi-line C++ comment block as a detailed description. Set this +# tag to YES if you prefer the old behavior instead. +# +# Note that setting this tag to YES also means that rational rose comments are +# not recognized any more. +# The default value is: NO. + +MULTILINE_CPP_IS_BRIEF = NO + +# If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the +# documentation from any documented member that it re-implements. +# The default value is: YES. + +INHERIT_DOCS = YES + +# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce a +# new page for each member. If set to NO, the documentation of a member will be +# part of the file/class/namespace that contains it. +# The default value is: NO. + +SEPARATE_MEMBER_PAGES = NO + +# The TAB_SIZE tag can be used to set the number of spaces in a tab. Doxygen +# uses this value to replace tabs by spaces in code fragments. +# Minimum value: 1, maximum value: 16, default value: 4. + +TAB_SIZE = 4 + +# This tag can be used to specify a number of aliases that act as commands in +# the documentation. An alias has the form: +# name=value +# For example adding +# "sideeffect=@par Side Effects:\n" +# will allow you to put the command \sideeffect (or @sideeffect) in the +# documentation, which will result in a user-defined paragraph with heading +# "Side Effects:". You can put \n's in the value part of an alias to insert +# newlines. + +ALIASES = + +# This tag can be used to specify a number of word-keyword mappings (TCL only). +# A mapping has the form "name=value". For example adding "class=itcl::class" +# will allow you to use the command class in the itcl::class meaning. + +TCL_SUBST = + +# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources +# only. Doxygen will then generate output that is more tailored for C. For +# instance, some of the names that are used will be different. The list of all +# members will be omitted, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_FOR_C = NO + +# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java or +# Python sources only. Doxygen will then generate output that is more tailored +# for that language. For instance, namespaces will be presented as packages, +# qualified scopes will look different, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_JAVA = NO + +# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran +# sources. Doxygen will then generate output that is tailored for Fortran. +# The default value is: NO. + +OPTIMIZE_FOR_FORTRAN = NO + +# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL +# sources. Doxygen will then generate output that is tailored for VHDL. +# The default value is: NO. + +OPTIMIZE_OUTPUT_VHDL = NO + +# Doxygen selects the parser to use depending on the extension of the files it +# parses. With this tag you can assign which parser to use for a given +# extension. Doxygen has a built-in mapping, but you can override or extend it +# using this tag. The format is ext=language, where ext is a file extension, and +# language is one of the parsers supported by doxygen: IDL, Java, Javascript, +# C#, C, C++, D, PHP, Objective-C, Python, Fortran (fixed format Fortran: +# FortranFixed, free formatted Fortran: FortranFree, unknown formatted Fortran: +# Fortran. In the later case the parser tries to guess whether the code is fixed +# or free formatted code, this is the default for Fortran type files), VHDL. For +# instance to make doxygen treat .inc files as Fortran files (default is PHP), +# and .f files as C (default is Fortran), use: inc=Fortran f=C. +# +# Note For files without extension you can use no_extension as a placeholder. +# +# Note that for custom extensions you also need to set FILE_PATTERNS otherwise +# the files are not read by doxygen. + +EXTENSION_MAPPING = + +# If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments +# according to the Markdown format, which allows for more readable +# documentation. See http://daringfireball.net/projects/markdown/ for details. +# The output of markdown processing is further processed by doxygen, so you can +# mix doxygen, HTML, and XML commands with Markdown formatting. Disable only in +# case of backward compatibilities issues. +# The default value is: YES. + +MARKDOWN_SUPPORT = YES + +# When enabled doxygen tries to link words that correspond to documented +# classes, or namespaces to their corresponding documentation. Such a link can +# be prevented in individual cases by by putting a % sign in front of the word +# or globally by setting AUTOLINK_SUPPORT to NO. +# The default value is: YES. + +AUTOLINK_SUPPORT = YES + +# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want +# to include (a tag file for) the STL sources as input, then you should set this +# tag to YES in order to let doxygen match functions declarations and +# definitions whose arguments contain STL classes (e.g. func(std::string); +# versus func(std::string) {}). This also make the inheritance and collaboration +# diagrams that involve STL classes more complete and accurate. +# The default value is: NO. + +BUILTIN_STL_SUPPORT = NO + +# If you use Microsoft's C++/CLI language, you should set this option to YES to +# enable parsing support. +# The default value is: NO. + +CPP_CLI_SUPPORT = NO + +# Set the SIP_SUPPORT tag to YES if your project consists of sip (see: +# http://www.riverbankcomputing.co.uk/software/sip/intro) sources only. Doxygen +# will parse them like normal C++ but will assume all classes use public instead +# of private inheritance when no explicit protection keyword is present. +# The default value is: NO. + +SIP_SUPPORT = NO + +# For Microsoft's IDL there are propget and propput attributes to indicate +# getter and setter methods for a property. Setting this option to YES will make +# doxygen to replace the get and set methods by a property in the documentation. +# This will only work if the methods are indeed getting or setting a simple +# type. If this is not the case, or you want to show the methods anyway, you +# should set this option to NO. +# The default value is: YES. + +IDL_PROPERTY_SUPPORT = YES + +# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC +# tag is set to YES, then doxygen will reuse the documentation of the first +# member in the group (if any) for the other members of the group. By default +# all members of a group must be documented explicitly. +# The default value is: NO. + +DISTRIBUTE_GROUP_DOC = NO + +# Set the SUBGROUPING tag to YES to allow class member groups of the same type +# (for instance a group of public functions) to be put as a subgroup of that +# type (e.g. under the Public Functions section). Set it to NO to prevent +# subgrouping. Alternatively, this can be done per class using the +# \nosubgrouping command. +# The default value is: YES. + +SUBGROUPING = YES + +# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and unions +# are shown inside the group in which they are included (e.g. using \ingroup) +# instead of on a separate page (for HTML and Man pages) or section (for LaTeX +# and RTF). +# +# Note that this feature does not work in combination with +# SEPARATE_MEMBER_PAGES. +# The default value is: NO. + +INLINE_GROUPED_CLASSES = NO + +# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and unions +# with only public data fields or simple typedef fields will be shown inline in +# the documentation of the scope in which they are defined (i.e. file, +# namespace, or group documentation), provided this scope is documented. If set +# to NO, structs, classes, and unions are shown on a separate page (for HTML and +# Man pages) or section (for LaTeX and RTF). +# The default value is: NO. + +INLINE_SIMPLE_STRUCTS = NO + +# When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or +# enum is documented as struct, union, or enum with the name of the typedef. So +# typedef struct TypeS {} TypeT, will appear in the documentation as a struct +# with name TypeT. When disabled the typedef will appear as a member of a file, +# namespace, or class. And the struct will be named TypeS. This can typically be +# useful for C code in case the coding convention dictates that all compound +# types are typedef'ed and only the typedef is referenced, never the tag name. +# The default value is: NO. + +TYPEDEF_HIDES_STRUCT = NO + +# The size of the symbol lookup cache can be set using LOOKUP_CACHE_SIZE. This +# cache is used to resolve symbols given their name and scope. Since this can be +# an expensive process and often the same symbol appears multiple times in the +# code, doxygen keeps a cache of pre-resolved symbols. If the cache is too small +# doxygen will become slower. If the cache is too large, memory is wasted. The +# cache size is given by this formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range +# is 0..9, the default is 0, corresponding to a cache size of 2^16=65536 +# symbols. At the end of a run doxygen will report the cache usage and suggest +# the optimal cache size from a speed point of view. +# Minimum value: 0, maximum value: 9, default value: 0. + +LOOKUP_CACHE_SIZE = 0 + +#--------------------------------------------------------------------------- +# Build related configuration options +#--------------------------------------------------------------------------- + +# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in +# documentation are documented, even if no documentation was available. Private +# class members and static file members will be hidden unless the +# EXTRACT_PRIVATE respectively EXTRACT_STATIC tags are set to YES. +# Note: This will also disable the warnings about undocumented members that are +# normally produced when WARNINGS is set to YES. +# The default value is: NO. + +EXTRACT_ALL = YES + +# If the EXTRACT_PRIVATE tag is set to YES all private members of a class will +# be included in the documentation. +# The default value is: NO. + +EXTRACT_PRIVATE = YES + +# If the EXTRACT_PACKAGE tag is set to YES all members with package or internal +# scope will be included in the documentation. +# The default value is: NO. + +EXTRACT_PACKAGE = YES + +# If the EXTRACT_STATIC tag is set to YES all static members of a file will be +# included in the documentation. +# The default value is: NO. + +EXTRACT_STATIC = YES + +# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs) defined +# locally in source files will be included in the documentation. If set to NO +# only classes defined in header files are included. Does not have any effect +# for Java sources. +# The default value is: YES. + +EXTRACT_LOCAL_CLASSES = YES + +# This flag is only useful for Objective-C code. When set to YES local methods, +# which are defined in the implementation section but not in the interface are +# included in the documentation. If set to NO only methods in the interface are +# included. +# The default value is: NO. + +EXTRACT_LOCAL_METHODS = NO + +# If this flag is set to YES, the members of anonymous namespaces will be +# extracted and appear in the documentation as a namespace called +# 'anonymous_namespace{file}', where file will be replaced with the base name of +# the file that contains the anonymous namespace. By default anonymous namespace +# are hidden. +# The default value is: NO. + +EXTRACT_ANON_NSPACES = YES + +# If the HIDE_UNDOC_MEMBERS tag is set to YES, doxygen will hide all +# undocumented members inside documented classes or files. If set to NO these +# members will be included in the various overviews, but no documentation +# section is generated. This option has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_MEMBERS = NO + +# If the HIDE_UNDOC_CLASSES tag is set to YES, doxygen will hide all +# undocumented classes that are normally visible in the class hierarchy. If set +# to NO these classes will be included in the various overviews. This option has +# no effect if EXTRACT_ALL is enabled. +# The default value is: NO. + +HIDE_UNDOC_CLASSES = NO + +# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, doxygen will hide all friend +# (class|struct|union) declarations. If set to NO these declarations will be +# included in the documentation. +# The default value is: NO. + +HIDE_FRIEND_COMPOUNDS = NO + +# If the HIDE_IN_BODY_DOCS tag is set to YES, doxygen will hide any +# documentation blocks found inside the body of a function. If set to NO these +# blocks will be appended to the function's detailed documentation block. +# The default value is: NO. + +HIDE_IN_BODY_DOCS = NO + +# The INTERNAL_DOCS tag determines if documentation that is typed after a +# \internal command is included. If the tag is set to NO then the documentation +# will be excluded. Set it to YES to include the internal documentation. +# The default value is: NO. + +INTERNAL_DOCS = NO + +# If the CASE_SENSE_NAMES tag is set to NO then doxygen will only generate file +# names in lower-case letters. If set to YES upper-case letters are also +# allowed. This is useful if you have classes or files whose names only differ +# in case and if your file system supports case sensitive file names. Windows +# and Mac users are advised to set this option to NO. +# The default value is: system dependent. + +CASE_SENSE_NAMES = YES + +# If the HIDE_SCOPE_NAMES tag is set to NO then doxygen will show members with +# their full class and namespace scopes in the documentation. If set to YES the +# scope will be hidden. +# The default value is: NO. + +HIDE_SCOPE_NAMES = NO + +# If the SHOW_INCLUDE_FILES tag is set to YES then doxygen will put a list of +# the files that are included by a file in the documentation of that file. +# The default value is: YES. + +SHOW_INCLUDE_FILES = YES + +# If the SHOW_GROUPED_MEMB_INC tag is set to YES then Doxygen will add for each +# grouped member an include statement to the documentation, telling the reader +# which file to include in order to use the member. +# The default value is: NO. + +SHOW_GROUPED_MEMB_INC = NO + +# If the FORCE_LOCAL_INCLUDES tag is set to YES then doxygen will list include +# files with double quotes in the documentation rather than with sharp brackets. +# The default value is: NO. + +FORCE_LOCAL_INCLUDES = NO + +# If the INLINE_INFO tag is set to YES then a tag [inline] is inserted in the +# documentation for inline members. +# The default value is: YES. + +INLINE_INFO = YES + +# If the SORT_MEMBER_DOCS tag is set to YES then doxygen will sort the +# (detailed) documentation of file and class members alphabetically by member +# name. If set to NO the members will appear in declaration order. +# The default value is: YES. + +SORT_MEMBER_DOCS = YES + +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the brief +# descriptions of file, namespace and class members alphabetically by member +# name. If set to NO the members will appear in declaration order. Note that +# this will also influence the order of the classes in the class list. +# The default value is: NO. + +SORT_BRIEF_DOCS = NO + +# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the +# (brief and detailed) documentation of class members so that constructors and +# destructors are listed first. If set to NO the constructors will appear in the +# respective orders defined by SORT_BRIEF_DOCS and SORT_MEMBER_DOCS. +# Note: If SORT_BRIEF_DOCS is set to NO this option is ignored for sorting brief +# member documentation. +# Note: If SORT_MEMBER_DOCS is set to NO this option is ignored for sorting +# detailed member documentation. +# The default value is: NO. + +SORT_MEMBERS_CTORS_1ST = NO + +# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the hierarchy +# of group names into alphabetical order. If set to NO the group names will +# appear in their defined order. +# The default value is: NO. + +SORT_GROUP_NAMES = NO + +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be sorted by +# fully-qualified names, including namespaces. If set to NO, the class list will +# be sorted only by class name, not including the namespace part. +# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. +# Note: This option applies only to the class list, not to the alphabetical +# list. +# The default value is: NO. + +SORT_BY_SCOPE_NAME = NO + +# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to do proper +# type resolution of all parameters of a function it will reject a match between +# the prototype and the implementation of a member function even if there is +# only one candidate or it is obvious which candidate to choose by doing a +# simple string match. By disabling STRICT_PROTO_MATCHING doxygen will still +# accept a match between prototype and implementation in such cases. +# The default value is: NO. + +STRICT_PROTO_MATCHING = NO + +# The GENERATE_TODOLIST tag can be used to enable ( YES) or disable ( NO) the +# todo list. This list is created by putting \todo commands in the +# documentation. +# The default value is: YES. + +GENERATE_TODOLIST = YES + +# The GENERATE_TESTLIST tag can be used to enable ( YES) or disable ( NO) the +# test list. This list is created by putting \test commands in the +# documentation. +# The default value is: YES. + +GENERATE_TESTLIST = YES + +# The GENERATE_BUGLIST tag can be used to enable ( YES) or disable ( NO) the bug +# list. This list is created by putting \bug commands in the documentation. +# The default value is: YES. + +GENERATE_BUGLIST = YES + +# The GENERATE_DEPRECATEDLIST tag can be used to enable ( YES) or disable ( NO) +# the deprecated list. This list is created by putting \deprecated commands in +# the documentation. +# The default value is: YES. + +GENERATE_DEPRECATEDLIST= YES + +# The ENABLED_SECTIONS tag can be used to enable conditional documentation +# sections, marked by \if ... \endif and \cond +# ... \endcond blocks. + +ENABLED_SECTIONS = + +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines that the +# initial value of a variable or macro / define can have for it to appear in the +# documentation. If the initializer consists of more lines than specified here +# it will be hidden. Use a value of 0 to hide initializers completely. The +# appearance of the value of individual variables and macros / defines can be +# controlled using \showinitializer or \hideinitializer command in the +# documentation regardless of this setting. +# Minimum value: 0, maximum value: 10000, default value: 30. + +MAX_INITIALIZER_LINES = 30 + +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated at +# the bottom of the documentation of classes and structs. If set to YES the list +# will mention the files that were used to generate the documentation. +# The default value is: YES. + +SHOW_USED_FILES = YES + +# Set the SHOW_FILES tag to NO to disable the generation of the Files page. This +# will remove the Files entry from the Quick Index and from the Folder Tree View +# (if specified). +# The default value is: YES. + +SHOW_FILES = YES + +# Set the SHOW_NAMESPACES tag to NO to disable the generation of the Namespaces +# page. This will remove the Namespaces entry from the Quick Index and from the +# Folder Tree View (if specified). +# The default value is: YES. + +SHOW_NAMESPACES = YES + +# The FILE_VERSION_FILTER tag can be used to specify a program or script that +# doxygen should invoke to get the current version for each file (typically from +# the version control system). Doxygen will invoke the program by executing (via +# popen()) the command command input-file, where command is the value of the +# FILE_VERSION_FILTER tag, and input-file is the name of an input file provided +# by doxygen. Whatever the program writes to standard output is used as the file +# version. For an example see the documentation. + +FILE_VERSION_FILTER = + +# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed +# by doxygen. The layout file controls the global structure of the generated +# output files in an output format independent way. To create the layout file +# that represents doxygen's defaults, run doxygen with the -l option. You can +# optionally specify a file name after the option, if omitted DoxygenLayout.xml +# will be used as the name of the layout file. +# +# Note that if you run doxygen from a directory containing a file called +# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE +# tag is left empty. + +LAYOUT_FILE = + +# The CITE_BIB_FILES tag can be used to specify one or more bib files containing +# the reference definitions. This must be a list of .bib files. The .bib +# extension is automatically appended if omitted. This requires the bibtex tool +# to be installed. See also http://en.wikipedia.org/wiki/BibTeX for more info. +# For LaTeX the style of the bibliography can be controlled using +# LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the +# search path. Do not use file names with spaces, bibtex cannot handle them. See +# also \cite for info how to create references. + +CITE_BIB_FILES = + +#--------------------------------------------------------------------------- +# Configuration options related to warning and progress messages +#--------------------------------------------------------------------------- + +# The QUIET tag can be used to turn on/off the messages that are generated to +# standard output by doxygen. If QUIET is set to YES this implies that the +# messages are off. +# The default value is: NO. + +QUIET = NO + +# The WARNINGS tag can be used to turn on/off the warning messages that are +# generated to standard error ( stderr) by doxygen. If WARNINGS is set to YES +# this implies that the warnings are on. +# +# Tip: Turn warnings on while writing the documentation. +# The default value is: YES. + +WARNINGS = YES + +# If the WARN_IF_UNDOCUMENTED tag is set to YES, then doxygen will generate +# warnings for undocumented members. If EXTRACT_ALL is set to YES then this flag +# will automatically be disabled. +# The default value is: YES. + +WARN_IF_UNDOCUMENTED = YES + +# If the WARN_IF_DOC_ERROR tag is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as not documenting some parameters +# in a documented function, or documenting parameters that don't exist or using +# markup commands wrongly. +# The default value is: YES. + +WARN_IF_DOC_ERROR = YES + +# This WARN_NO_PARAMDOC option can be enabled to get warnings for functions that +# are documented, but have no documentation for their parameters or return +# value. If set to NO doxygen will only warn about wrong or incomplete parameter +# documentation, but not about the absence of documentation. +# The default value is: NO. + +WARN_NO_PARAMDOC = NO + +# The WARN_FORMAT tag determines the format of the warning messages that doxygen +# can produce. The string should contain the $file, $line, and $text tags, which +# will be replaced by the file and line number from which the warning originated +# and the warning text. Optionally the format may contain $version, which will +# be replaced by the version of the file (if it could be obtained via +# FILE_VERSION_FILTER) +# The default value is: $file:$line: $text. + +WARN_FORMAT = "$file:$line: $text" + +# The WARN_LOGFILE tag can be used to specify a file to which warning and error +# messages should be written. If left blank the output is written to standard +# error (stderr). + +WARN_LOGFILE = + +#--------------------------------------------------------------------------- +# Configuration options related to the input files +#--------------------------------------------------------------------------- + +# The INPUT tag is used to specify the files and/or directories that contain +# documented source files. You may enter file names like myfile.cpp or +# directories like /usr/src/myproject. Separate the files or directories with +# spaces. +# Note: If this tag is empty the current directory is searched. + +INPUT = ./include + +# Main Page +INPUT += apidoc/mainpage.md +USE_MDFILE_AS_MAINPAGE = apidoc/mainpage.md + +# This tag can be used to specify the character encoding of the source files +# that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses +# libiconv (or the iconv built into libc) for the transcoding. See the libiconv +# documentation (see: http://www.gnu.org/software/libiconv) for the list of +# possible encodings. +# The default value is: UTF-8. + +INPUT_ENCODING = UTF-8 + +# If the value of the INPUT tag contains directories, you can use the +# FILE_PATTERNS tag to specify one or more wildcard patterns (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank the +# following patterns are tested:*.c, *.cc, *.cxx, *.cpp, *.c++, *.java, *.ii, +# *.ixx, *.ipp, *.i++, *.inl, *.idl, *.ddl, *.odl, *.h, *.hh, *.hxx, *.hpp, +# *.h++, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, *.inc, *.m, *.markdown, +# *.md, *.mm, *.dox, *.py, *.f90, *.f, *.for, *.tcl, *.vhd, *.vhdl, *.ucf, +# *.qsf, *.as and *.js. + +FILE_PATTERNS = + +# The RECURSIVE tag can be used to specify whether or not subdirectories should +# be searched for input files as well. +# The default value is: NO. + +RECURSIVE = YES + +# The EXCLUDE tag can be used to specify files and/or directories that should be +# excluded from the INPUT source files. This way you can easily exclude a +# subdirectory from a directory tree whose root is specified with the INPUT tag. +# +# Note that relative paths are relative to the directory from which doxygen is +# run. + +EXCLUDE = + +# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or +# directories that are symbolic links (a Unix file system feature) are excluded +# from the input. +# The default value is: NO. + +EXCLUDE_SYMLINKS = NO + +# If the value of the INPUT tag contains directories, you can use the +# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude +# certain files from those directories. +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories for example use the pattern */test/* + +EXCLUDE_PATTERNS = + +# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names +# (namespaces, classes, functions, etc.) that should be excluded from the +# output. The symbol name can be a fully qualified name, a word, or if the +# wildcard * is used, a substring. Examples: ANamespace, AClass, +# AClass::ANamespace, ANamespace::*Test +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories use the pattern */test/* + +EXCLUDE_SYMBOLS = + +# The EXAMPLE_PATH tag can be used to specify one or more files or directories +# that contain example code fragments that are included (see the \include +# command). + +EXAMPLE_PATH = + +# If the value of the EXAMPLE_PATH tag contains directories, you can use the +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank all +# files are included. + +EXAMPLE_PATTERNS = + +# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be +# searched for input files to be used with the \include or \dontinclude commands +# irrespective of the value of the RECURSIVE tag. +# The default value is: NO. + +EXAMPLE_RECURSIVE = NO + +# The IMAGE_PATH tag can be used to specify one or more files or directories +# that contain images that are to be included in the documentation (see the +# \image command). + +IMAGE_PATH = + +# The INPUT_FILTER tag can be used to specify a program that doxygen should +# invoke to filter for each input file. Doxygen will invoke the filter program +# by executing (via popen()) the command: +# +# +# +# where is the value of the INPUT_FILTER tag, and is the +# name of an input file. Doxygen will then use the output that the filter +# program writes to standard output. If FILTER_PATTERNS is specified, this tag +# will be ignored. +# +# Note that the filter must not add or remove lines; it is applied before the +# code is scanned, but not when the output code is generated. If lines are added +# or removed, the anchors will not be placed correctly. + +INPUT_FILTER = + +# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern +# basis. Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. The filters are a list of the form: pattern=filter +# (like *.cpp=my_cpp_filter). See INPUT_FILTER for further information on how +# filters are used. If the FILTER_PATTERNS tag is empty or if none of the +# patterns match the file name, INPUT_FILTER is applied. + +FILTER_PATTERNS = + +# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using +# INPUT_FILTER ) will also be used to filter the input files that are used for +# producing the source files to browse (i.e. when SOURCE_BROWSER is set to YES). +# The default value is: NO. + +FILTER_SOURCE_FILES = NO + +# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file +# pattern. A pattern will override the setting for FILTER_PATTERN (if any) and +# it is also possible to disable source filtering for a specific pattern using +# *.ext= (so without naming a filter). +# This tag requires that the tag FILTER_SOURCE_FILES is set to YES. + +FILTER_SOURCE_PATTERNS = + +# If the USE_MDFILE_AS_MAINPAGE tag refers to the name of a markdown file that +# is part of the input, its contents will be placed on the main page +# (index.html). This can be useful if you have a project on for instance GitHub +# and want to reuse the introduction page also for the doxygen output. + +USE_MDFILE_AS_MAINPAGE = + +#--------------------------------------------------------------------------- +# Configuration options related to source browsing +#--------------------------------------------------------------------------- + +# If the SOURCE_BROWSER tag is set to YES then a list of source files will be +# generated. Documented entities will be cross-referenced with these sources. +# +# Note: To get rid of all source code in the generated output, make sure that +# also VERBATIM_HEADERS is set to NO. +# The default value is: NO. + +SOURCE_BROWSER = NO + +# Setting the INLINE_SOURCES tag to YES will include the body of functions, +# classes and enums directly into the documentation. +# The default value is: NO. + +INLINE_SOURCES = NO + +# Setting the STRIP_CODE_COMMENTS tag to YES will instruct doxygen to hide any +# special comment blocks from generated source code fragments. Normal C, C++ and +# Fortran comments will always remain visible. +# The default value is: YES. + +STRIP_CODE_COMMENTS = YES + +# If the REFERENCED_BY_RELATION tag is set to YES then for each documented +# function all documented functions referencing it will be listed. +# The default value is: NO. + +REFERENCED_BY_RELATION = NO + +# If the REFERENCES_RELATION tag is set to YES then for each documented function +# all documented entities called/used by that function will be listed. +# The default value is: NO. + +REFERENCES_RELATION = NO + +# If the REFERENCES_LINK_SOURCE tag is set to YES and SOURCE_BROWSER tag is set +# to YES, then the hyperlinks from functions in REFERENCES_RELATION and +# REFERENCED_BY_RELATION lists will link to the source code. Otherwise they will +# link to the documentation. +# The default value is: YES. + +REFERENCES_LINK_SOURCE = YES + +# If SOURCE_TOOLTIPS is enabled (the default) then hovering a hyperlink in the +# source code will show a tooltip with additional information such as prototype, +# brief description and links to the definition and documentation. Since this +# will make the HTML file larger and loading of large files a bit slower, you +# can opt to disable this feature. +# The default value is: YES. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +SOURCE_TOOLTIPS = YES + +# If the USE_HTAGS tag is set to YES then the references to source code will +# point to the HTML generated by the htags(1) tool instead of doxygen built-in +# source browser. The htags tool is part of GNU's global source tagging system +# (see http://www.gnu.org/software/global/global.html). You will need version +# 4.8.6 or higher. +# +# To use it do the following: +# - Install the latest version of global +# - Enable SOURCE_BROWSER and USE_HTAGS in the config file +# - Make sure the INPUT points to the root of the source tree +# - Run doxygen as normal +# +# Doxygen will invoke htags (and that will in turn invoke gtags), so these +# tools must be available from the command line (i.e. in the search path). +# +# The result: instead of the source browser generated by doxygen, the links to +# source code will now point to the output of htags. +# The default value is: NO. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +USE_HTAGS = NO + +# If the VERBATIM_HEADERS tag is set the YES then doxygen will generate a +# verbatim copy of the header file for each class for which an include is +# specified. Set to NO to disable this. +# See also: Section \class. +# The default value is: YES. + +VERBATIM_HEADERS = YES + +#--------------------------------------------------------------------------- +# Configuration options related to the alphabetical class index +#--------------------------------------------------------------------------- + +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index of all +# compounds will be generated. Enable this if the project contains a lot of +# classes, structs, unions or interfaces. +# The default value is: YES. + +ALPHABETICAL_INDEX = YES + +# The COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns in +# which the alphabetical index list will be split. +# Minimum value: 1, maximum value: 20, default value: 5. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. + +COLS_IN_ALPHA_INDEX = 5 + +# In case all classes in a project start with a common prefix, all classes will +# be put under the same header in the alphabetical index. The IGNORE_PREFIX tag +# can be used to specify a prefix (or a list of prefixes) that should be ignored +# while generating the index headers. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. + +IGNORE_PREFIX = + +#--------------------------------------------------------------------------- +# Configuration options related to the HTML output +#--------------------------------------------------------------------------- + +# If the GENERATE_HTML tag is set to YES doxygen will generate HTML output +# The default value is: YES. + +GENERATE_HTML = YES + +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. If a +# relative path is entered the value of OUTPUT_DIRECTORY will be put in front of +# it. +# The default directory is: html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_OUTPUT = html + +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for each +# generated HTML page (for example: .htm, .php, .asp). +# The default value is: .html. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FILE_EXTENSION = .html + +# The HTML_HEADER tag can be used to specify a user-defined HTML header file for +# each generated HTML page. If the tag is left blank doxygen will generate a +# standard header. +# +# To get valid HTML the header file that includes any scripts and style sheets +# that doxygen needs, which is dependent on the configuration options used (e.g. +# the setting GENERATE_TREEVIEW). It is highly recommended to start with a +# default header using +# doxygen -w html new_header.html new_footer.html new_stylesheet.css +# YourConfigFile +# and then modify the file new_header.html. See also section "Doxygen usage" +# for information on how to generate the default header that doxygen normally +# uses. +# Note: The header is subject to change so you typically have to regenerate the +# default header when upgrading to a newer version of doxygen. For a description +# of the possible markers and block names see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a user-defined HTML footer for each +# generated HTML page. If the tag is left blank doxygen will generate a standard +# footer. See HTML_HEADER for more information on how to generate a default +# footer and what special commands can be used inside the footer. See also +# section "Doxygen usage" for information on how to generate the default footer +# that doxygen normally uses. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading style +# sheet that is used by each HTML page. It can be used to fine-tune the look of +# the HTML output. If left blank doxygen will generate a default style sheet. +# See also section "Doxygen usage" for information on how to generate the style +# sheet that doxygen normally uses. +# Note: It is recommended to use HTML_EXTRA_STYLESHEET instead of this tag, as +# it is more robust and this tag (HTML_STYLESHEET) will in the future become +# obsolete. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_STYLESHEET = + +# The HTML_EXTRA_STYLESHEET tag can be used to specify an additional user- +# defined cascading style sheet that is included after the standard style sheets +# created by doxygen. Using this option one can overrule certain style aspects. +# This is preferred over using HTML_STYLESHEET since it does not replace the +# standard style sheet and is therefor more robust against future updates. +# Doxygen will copy the style sheet file to the output directory. For an example +# see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_STYLESHEET = + +# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or +# other source files which should be copied to the HTML output directory. Note +# that these files will be copied to the base HTML output directory. Use the +# $relpath^ marker in the HTML_HEADER and/or HTML_FOOTER files to load these +# files. In the HTML_STYLESHEET file, use the file name only. Also note that the +# files will be copied as-is; there are no commands or markers available. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_FILES = + +# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. Doxygen +# will adjust the colors in the stylesheet and background images according to +# this color. Hue is specified as an angle on a colorwheel, see +# http://en.wikipedia.org/wiki/Hue for more information. For instance the value +# 0 represents red, 60 is yellow, 120 is green, 180 is cyan, 240 is blue, 300 +# purple, and 360 is red again. +# Minimum value: 0, maximum value: 359, default value: 220. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_HUE = 220 + +# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of the colors +# in the HTML output. For a value of 0 the output will use grayscales only. A +# value of 255 will produce the most vivid colors. +# Minimum value: 0, maximum value: 255, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_SAT = 100 + +# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to the +# luminance component of the colors in the HTML output. Values below 100 +# gradually make the output lighter, whereas values above 100 make the output +# darker. The value divided by 100 is the actual gamma applied, so 80 represents +# a gamma of 0.8, The value 220 represents a gamma of 2.2, and 100 does not +# change the gamma. +# Minimum value: 40, maximum value: 240, default value: 80. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_GAMMA = 80 + +# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML +# page will contain the date and time when the page was generated. Setting this +# to NO can help when comparing the output of multiple runs. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_TIMESTAMP = YES + +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the +# page has loaded. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_DYNAMIC_SECTIONS = NO + +# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of entries +# shown in the various tree structured indices initially; the user can expand +# and collapse entries dynamically later on. Doxygen will expand the tree to +# such a level that at most the specified number of entries are visible (unless +# a fully collapsed tree already exceeds this amount). So setting the number of +# entries 1 will produce a full collapsed tree by default. 0 is a special value +# representing an infinite number of entries and will result in a full expanded +# tree by default. +# Minimum value: 0, maximum value: 9999, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_INDEX_NUM_ENTRIES = 100 + +# If the GENERATE_DOCSET tag is set to YES, additional index files will be +# generated that can be used as input for Apple's Xcode 3 integrated development +# environment (see: http://developer.apple.com/tools/xcode/), introduced with +# OSX 10.5 (Leopard). To create a documentation set, doxygen will generate a +# Makefile in the HTML output directory. Running make will produce the docset in +# that directory and running make install will install the docset in +# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find it at +# startup. See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html +# for more information. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_DOCSET = NO + +# This tag determines the name of the docset feed. A documentation feed provides +# an umbrella under which multiple documentation sets from a single provider +# (such as a company or product suite) can be grouped. +# The default value is: Doxygen generated docs. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_FEEDNAME = "Doxygen generated docs" + +# This tag specifies a string that should uniquely identify the documentation +# set bundle. This should be a reverse domain-name style string, e.g. +# com.mycompany.MyDocSet. Doxygen will append .docset to the name. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_BUNDLE_ID = org.doxygen.Project + +# The DOCSET_PUBLISHER_ID tag specifies a string that should uniquely identify +# the documentation publisher. This should be a reverse domain-name style +# string, e.g. com.mycompany.MyDocSet.documentation. +# The default value is: org.doxygen.Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_ID = org.doxygen.Publisher + +# The DOCSET_PUBLISHER_NAME tag identifies the documentation publisher. +# The default value is: Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. + +DOCSET_PUBLISHER_NAME = Publisher + +# If the GENERATE_HTMLHELP tag is set to YES then doxygen generates three +# additional HTML index files: index.hhp, index.hhc, and index.hhk. The +# index.hhp is a project file that can be read by Microsoft's HTML Help Workshop +# (see: http://www.microsoft.com/en-us/download/details.aspx?id=21138) on +# Windows. +# +# The HTML Help Workshop contains a compiler that can convert all HTML output +# generated by doxygen into a single compiled HTML file (.chm). Compiled HTML +# files are now used as the Windows 98 help format, and will replace the old +# Windows help format (.hlp) on all Windows platforms in the future. Compressed +# HTML files also contain an index, a table of contents, and you can search for +# words in the documentation. The HTML workshop also contains a viewer for +# compressed HTML files. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_HTMLHELP = NO + +# The CHM_FILE tag can be used to specify the file name of the resulting .chm +# file. You can add a path in front of the file if the result should not be +# written to the html output directory. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_FILE = + +# The HHC_LOCATION tag can be used to specify the location (absolute path +# including file name) of the HTML help compiler ( hhc.exe). If non-empty +# doxygen will try to run the HTML help compiler on the generated index.hhp. +# The file has to be specified with full path. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +HHC_LOCATION = + +# The GENERATE_CHI flag controls if a separate .chi index file is generated ( +# YES) or that it should be included in the master .chm file ( NO). +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +GENERATE_CHI = NO + +# The CHM_INDEX_ENCODING is used to encode HtmlHelp index ( hhk), content ( hhc) +# and project file content. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +CHM_INDEX_ENCODING = + +# The BINARY_TOC flag controls whether a binary table of contents is generated ( +# YES) or a normal table of contents ( NO) in the .chm file. Furthermore it +# enables the Previous and Next buttons. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +BINARY_TOC = NO + +# The TOC_EXPAND flag can be set to YES to add extra items for group members to +# the table of contents of the HTML help documentation and to the tree view. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. + +TOC_EXPAND = NO + +# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and +# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated that +# can be used as input for Qt's qhelpgenerator to generate a Qt Compressed Help +# (.qch) of the generated HTML documentation. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_QHP = NO + +# If the QHG_LOCATION tag is specified, the QCH_FILE tag can be used to specify +# the file name of the resulting .qch file. The path specified is relative to +# the HTML output folder. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QCH_FILE = + +# The QHP_NAMESPACE tag specifies the namespace to use when generating Qt Help +# Project output. For more information please see Qt Help Project / Namespace +# (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#namespace). +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_NAMESPACE = org.doxygen.Project + +# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating Qt +# Help Project output. For more information please see Qt Help Project / Virtual +# Folders (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#virtual- +# folders). +# The default value is: doc. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_VIRTUAL_FOLDER = doc + +# If the QHP_CUST_FILTER_NAME tag is set, it specifies the name of a custom +# filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_NAME = + +# The QHP_CUST_FILTER_ATTRS tag specifies the list of the attributes of the +# custom filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_CUST_FILTER_ATTRS = + +# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this +# project's filter section matches. Qt Help Project / Filter Attributes (see: +# http://qt-project.org/doc/qt-4.8/qthelpproject.html#filter-attributes). +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHP_SECT_FILTER_ATTRS = + +# The QHG_LOCATION tag can be used to specify the location of Qt's +# qhelpgenerator. If non-empty doxygen will try to run qhelpgenerator on the +# generated .qhp file. +# This tag requires that the tag GENERATE_QHP is set to YES. + +QHG_LOCATION = + +# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files will be +# generated, together with the HTML files, they form an Eclipse help plugin. To +# install this plugin and make it available under the help contents menu in +# Eclipse, the contents of the directory containing the HTML and XML files needs +# to be copied into the plugins directory of eclipse. The name of the directory +# within the plugins directory should be the same as the ECLIPSE_DOC_ID value. +# After copying Eclipse needs to be restarted before the help appears. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_ECLIPSEHELP = NO + +# A unique identifier for the Eclipse help plugin. When installing the plugin +# the directory name containing the HTML and XML files should also have this +# name. Each documentation set should have its own identifier. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_ECLIPSEHELP is set to YES. + +ECLIPSE_DOC_ID = org.doxygen.Project + +# If you want full control over the layout of the generated HTML pages it might +# be necessary to disable the index and replace it with your own. The +# DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) at top +# of each HTML page. A value of NO enables the index and the value YES disables +# it. Since the tabs in the index contain the same information as the navigation +# tree, you can set this option to YES if you also set GENERATE_TREEVIEW to YES. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +DISABLE_INDEX = NO + +# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index +# structure should be generated to display hierarchical information. If the tag +# value is set to YES, a side panel will be generated containing a tree-like +# index structure (just like the one that is generated for HTML Help). For this +# to work a browser that supports JavaScript, DHTML, CSS and frames is required +# (i.e. any modern browser). Windows users are probably better off using the +# HTML help feature. Via custom stylesheets (see HTML_EXTRA_STYLESHEET) one can +# further fine-tune the look of the index. As an example, the default style +# sheet generated by doxygen has an example that shows how to put an image at +# the root of the tree instead of the PROJECT_NAME. Since the tree basically has +# the same information as the tab index, you could consider setting +# DISABLE_INDEX to YES when enabling this option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +GENERATE_TREEVIEW = NO + +# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values that +# doxygen will group on one line in the generated HTML documentation. +# +# Note that a value of 0 will completely suppress the enum values from appearing +# in the overview section. +# Minimum value: 0, maximum value: 20, default value: 4. +# This tag requires that the tag GENERATE_HTML is set to YES. + +ENUM_VALUES_PER_LINE = 4 + +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be used +# to set the initial width (in pixels) of the frame in which the tree is shown. +# Minimum value: 0, maximum value: 1500, default value: 250. +# This tag requires that the tag GENERATE_HTML is set to YES. + +TREEVIEW_WIDTH = 250 + +# When the EXT_LINKS_IN_WINDOW option is set to YES doxygen will open links to +# external symbols imported via tag files in a separate window. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +EXT_LINKS_IN_WINDOW = NO + +# Use this tag to change the font size of LaTeX formulas included as images in +# the HTML documentation. When you change the font size after a successful +# doxygen run you need to manually remove any form_*.png images from the HTML +# output directory to force them to be regenerated. +# Minimum value: 8, maximum value: 50, default value: 10. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_FONTSIZE = 10 + +# Use the FORMULA_TRANPARENT tag to determine whether or not the images +# generated for formulas are transparent PNGs. Transparent PNGs are not +# supported properly for IE 6.0, but are supported on all modern browsers. +# +# Note that when changing this option you need to delete any form_*.png files in +# the HTML output directory before the changes have effect. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +FORMULA_TRANSPARENT = YES + +# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax (see +# http://www.mathjax.org) which uses client side Javascript for the rendering +# instead of using prerendered bitmaps. Use this if you do not have LaTeX +# installed or if you want to formulas look prettier in the HTML output. When +# enabled you may also need to install MathJax separately and configure the path +# to it using the MATHJAX_RELPATH option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +USE_MATHJAX = NO + +# When MathJax is enabled you can set the default output format to be used for +# the MathJax output. See the MathJax site (see: +# http://docs.mathjax.org/en/latest/output.html) for more details. +# Possible values are: HTML-CSS (which is slower, but has the best +# compatibility), NativeMML (i.e. MathML) and SVG. +# The default value is: HTML-CSS. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_FORMAT = HTML-CSS + +# When MathJax is enabled you need to specify the location relative to the HTML +# output directory using the MATHJAX_RELPATH option. The destination directory +# should contain the MathJax.js script. For instance, if the mathjax directory +# is located at the same level as the HTML output directory, then +# MATHJAX_RELPATH should be ../mathjax. The default value points to the MathJax +# Content Delivery Network so you can quickly see the result without installing +# MathJax. However, it is strongly recommended to install a local copy of +# MathJax from http://www.mathjax.org before deployment. +# The default value is: http://cdn.mathjax.org/mathjax/latest. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_RELPATH = http://cdn.mathjax.org/mathjax/latest + +# The MATHJAX_EXTENSIONS tag can be used to specify one or more MathJax +# extension names that should be enabled during MathJax rendering. For example +# MATHJAX_EXTENSIONS = TeX/AMSmath TeX/AMSsymbols +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_EXTENSIONS = + +# The MATHJAX_CODEFILE tag can be used to specify a file with javascript pieces +# of code that will be used on startup of the MathJax code. See the MathJax site +# (see: http://docs.mathjax.org/en/latest/output.html) for more details. For an +# example see the documentation. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_CODEFILE = + +# When the SEARCHENGINE tag is enabled doxygen will generate a search box for +# the HTML output. The underlying search engine uses javascript and DHTML and +# should work on any modern browser. Note that when using HTML help +# (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET) +# there is already a search function so this one should typically be disabled. +# For large projects the javascript based search engine can be slow, then +# enabling SERVER_BASED_SEARCH may provide a better solution. It is possible to +# search using the keyboard; to jump to the search box use + S +# (what the is depends on the OS and browser, but it is typically +# , /