diff -r bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/src/test_main.cpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/src/test_main.cpp Wed Apr 13 18:40:16 2016 +0100 @@ -0,0 +1,6 @@ +#include + +int main(int argc, char **argv) { + ::testing::InitGoogleTest(&argc, argv); + return RUN_ALL_TESTS(); +} diff -r bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/include/mc2lib/types.hpp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/include/mc2lib/types.hpp Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 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 Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/SConscript --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/SConscript Wed Apr 13 18:40:16 2016 +0100 @@ -0,0 +1,6 @@ +# -*- mode:python -*- + +Import('main') +main.Prepend(CPPPATH=Dir('./include')) + +# vim: set ft=python : diff -r bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/apidoc/mainpage.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/apidoc/mainpage.md Wed Apr 13 18:40:16 2016 +0100 @@ -0,0 +1,4 @@ +mc2lib {#mainpage} +====== + +This is the API documentation for [mc2lib](https://github.com/melver/mc2lib). diff -r bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/README.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/README.rst Wed Apr 13 18:40: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 bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/HACKING.rst --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/HACKING.rst Wed Apr 13 18:40:16 2016 +0100 @@ -0,0 +1,13 @@ +Guidelines +========== + +Following `C++ Core Guidelines `_ +where possible. + +Naming and formatting is according to the `Google C++ Style Guide +`_. Use ``make format``. + +New standards-compliant language features in C++11 are encouraged if they make +the code safer, more maintainable and/or easier to understand/use. The only +limiting factor is the oldest to be supported compiler versions (currently GCC +4.7, Clang 3.3). diff -r bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/AUTHORS --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/AUTHORS Wed Apr 13 18:40:16 2016 +0100 @@ -0,0 +1,1 @@ +git shortlog -se diff -r bb8e0e8819ec -r d4b894bba3c4 ext/mc2lib/Doxyfile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/ext/mc2lib/Doxyfile Wed Apr 13 18:40: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 +# , /