From c03f477e79e72e459fbb44e61a135ecd40cf2ce3 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 17:55:53 +0200 Subject: [PATCH 01/14] adding a tikz output to match the paper --- CMakeLists.txt | 1 + src/branching/eager/version_store.cc | 1 + src/gitmem.cc | 12 +- src/interpreter.cc | 19 +- src/interpreter.hh | 1 + src/tikz.cc | 460 +++++++++++++++++++++++++++ src/tikz.hh | 14 + 7 files changed, 502 insertions(+), 6 deletions(-) create mode 100644 src/tikz.cc create mode 100644 src/tikz.hh diff --git a/CMakeLists.txt b/CMakeLists.txt index 31e84b7..f7807de 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -49,6 +49,7 @@ add_executable(gitmem src/debugger.cc src/model_checker.cc src/graphviz.cc + src/tikz.cc ) add_executable(gitmem_trieste diff --git a/src/branching/eager/version_store.cc b/src/branching/eager/version_store.cc index 511bbda..c638461 100644 --- a/src/branching/eager/version_store.cc +++ b/src/branching/eager/version_store.cc @@ -2,6 +2,7 @@ #include "debug.hh" #include "thread_trace.hh" +#include #include namespace gitmem { diff --git a/src/gitmem.cc b/src/gitmem.cc index 0c7a025..654c81f 100644 --- a/src/gitmem.cc +++ b/src/gitmem.cc @@ -22,6 +22,12 @@ int main(int argc, char **argv) { std::filesystem::path output_path = ""; app.add_option("-o,--output", output_path, "Path to the output file."); + std::string output_format = "dot"; + app.add_option("--format", output_format, + "Output format for execution graph: dot (default) or tikz.") + ->check(CLI::IsMember({"dot", "tikz"})) + ->type_name("FORMAT"); + bool verbose = false; app.add_flag("-v,--verbose", verbose, "Enable verbose output from the interpreter."); @@ -103,8 +109,10 @@ int main(int argc, char **argv) { return 1; } - if (output_path.empty()) - output_path = input_path.stem().replace_extension(".dot"); + if (output_path.empty()) { + std::string ext = (output_format == "tikz") ? ".tex" : ".dot"; + output_path = input_path.stem().replace_extension(ext); + } gitmem::verbose::out << "Output will be written to " << output_path << std::endl; diff --git a/src/interpreter.cc b/src/interpreter.cc index c6582f6..c156719 100644 --- a/src/interpreter.cc +++ b/src/interpreter.cc @@ -655,6 +655,10 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { thread_tails[tid] = node; }; + // Track whether each thread's trace already included an EndEvent (e.g. for + // stuck threads that had on_end() called on them in Interpreter::run()). + std::vector thread_has_end(gctx.threads.size(), false); + // Process events from all threads for (ThreadID tid = 0; tid < gctx.threads.size(); ++tid) { auto& thread = gctx.threads[tid]; @@ -674,6 +678,7 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { auto node = std::make_shared(); link_in_program_order(tid, node); event_to_node[event] = node; + thread_has_end[tid] = true; }, [&](const WriteEvent& arg) { auto node = std::make_shared(arg.var, arg.value, tid); @@ -751,8 +756,9 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { }, event->data); } - // Add pending node if thread hasn't terminated - if (!thread.terminated) { + // Add pending node if thread hasn't terminated and didn't already receive + // an EndEvent (which run() adds for stuck threads via on_end()). + if (!thread.terminated && !thread_has_end[tid]) { if (thread.pc < thread.block->size()) { // Thread is stuck waiting at a specific statement trieste::Node stmt = thread.block->at(thread.pc); @@ -784,8 +790,13 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { void Interpreter::print_execution_graph(const std::filesystem::path& output_path) { auto exec_graph = build_execution_graph_from_traces(); - graph::GraphvizPrinter gv(output_path); - gv.visit(exec_graph.entry.get()); + if (output_path.extension() == ".tex") { + graph::TikzPrinter tikz; + tikz.print(exec_graph, output_path); + } else { + graph::GraphvizPrinter gv(output_path); + gv.visit(exec_graph.entry.get()); + } } int interpret(const Node ast, const std::filesystem::path &output_path, diff --git a/src/interpreter.hh b/src/interpreter.hh index 6927982..189fc62 100644 --- a/src/interpreter.hh +++ b/src/interpreter.hh @@ -3,6 +3,7 @@ #include "execution_state.hh" #include "graph.hh" #include "graphviz.hh" +#include "tikz.hh" #include "lang.hh" #include "progress_status.hh" #include diff --git a/src/tikz.cc b/src/tikz.cc new file mode 100644 index 0000000..b6fb60d --- /dev/null +++ b/src/tikz.cc @@ -0,0 +1,460 @@ +#include "tikz.hh" +#include "overloaded.hh" +#include +#include +#include +#include +#include + +namespace gitmem { +namespace graph { + +static std::string latex_escape(const std::string& s) { + std::string r; + r.reserve(s.size()); + for (char c : s) { + switch (c) { + case '_': r += "\\_"; break; + case '$': r += "\\$"; break; + case '&': r += "\\&"; break; + case '%': r += "\\%"; break; + case '#': r += "\\#"; break; + case '{': r += "\\{"; break; + case '}': r += "\\}"; break; + default: r += c; break; + } + } + return r; +} + +static std::string node_id(size_t tid, size_t idx) { + return "t" + std::to_string(tid) + "e" + std::to_string(idx); +} + +static std::string fmt(double v) { + char buf[32]; + std::snprintf(buf, sizeof(buf), "%.2f", v); + return buf; +} + +// Formatter macros from the paper (verbatim). Stored as a raw string so that +// LaTeX special characters (backslashes, #, etc.) are preserved. +static const char* FORMATTER = R"( +\newlength{\codeboxleftshift} +\newlength{\codeboxrightshift} +\setlength{\codeboxrightshift}{3pt} +\tikzset{ + common timeline styles/.style={ + >={Latex[scale=0.8]}, + every node/.style={font=\scriptsize\ttfamily}, + codebox/.style={rounded corners=1.5pt, inner sep=1pt}, + thread lane/.style={ultra thick, draw=threadtime, dashed}, + shared lane/.style={thread lane, draw=sharedmem}, + history link/.style={line width=0.8pt}, + link left/.style={history link, {Latex[round, scale=1.1]}-, draw=communicationblue}, + link right/.style={history link, -{Latex[round, scale=1.1]}, draw=communicationblue}, + link oneway/.style={history link, -{Latex[round, scale=1.1]}, draw=communicationblue}, + link both/.style={history link, + {Latex[round, scale=1.1]}-{Latex[round, scale=1.1]}, + draw=communicationblue}, + conflict/.style={line width=3pt, -{Latex[round,scale=0.8]}, draw=conflictred}, + stateupdate/.style={draw=threadtime, fill=threadtime!15, rounded corners=4pt, + inner sep=1.5pt, font=\scriptsize\ttfamily}, + sharedupdate/.style={draw=sharedmem!80!black, fill=sharedmem!30, rounded corners=4pt, + inner sep=1.5pt, font=\scriptsize\ttfamily}, + t1 code/.style={anchor=west, xshift=\the\codeboxleftshift, codebox}, + t2 code/.style={anchor=west, xshift=\the\codeboxrightshift, codebox}, + t1 state/.style={right, xshift=3pt, stateupdate}, + t2 state/.style={left, xshift=-3pt, stateupdate}, + g state right/.style={right, xshift=3pt, sharedupdate}, + g state left/.style={left, xshift=-3pt, sharedupdate}, + } +} +\newcommand{\TimelineColorSetup}{ + \definecolor{threadtime}{rgb}{0.5,0.5,0.5} + \definecolor{sharedmem}{rgb}{0.3,0.3,0.3} + \definecolor{communicationblue}{rgb}{0.2,0.4,1} + \definecolor{conflictred}{rgb}{1,0.2,0.2} +} +\newcommand{\DefineThreadEventMacros}{ + \newcommand{\ResolveThreadX}[1]{% + \def\tx{\onex}\ifnum\pdfstrcmp{##1}{t2}=0\def\tx{\twox}\fi} + \newcommand{\ThreadEvent}[4]{% + \ResolveThreadX{##1}% + \fill[fill=threadtime] (\tx,##2) circle (2pt) coordinate (##3) node[##1 code] {##4};} + \newcommand{\ThreadEventFrom}[5]{% + \fill[fill=threadtime] ($(##2)+(0,##3)$) circle (2pt) coordinate (##4) node[##1 code] {##5};} + \newcommand{\ThreadSyncEvent}[4]{% + \ResolveThreadX{##1}% + \fill (\tx,##2) circle (0pt) coordinate (##3) node[##1 code] {##4};} + \newcommand{\ThreadSyncEventFrom}[5]{% + \fill ($(##2)+(0,##3)$) circle (0pt) coordinate (##4) node[##1 code] {##5};} + \newcommand{\PullPush}[2]{ + \ifdoublearrows + \path let \p1 = ##1, \p2 = ##2 in \pgfextra{% + \ifdim\x1<\x2 + \draw[link oneway] ##2 to[looseness=.5, out=140, in=30] ##1; + \draw[link oneway] ##1 to[looseness=.5, out=320, in=210] ##2; + \else + \draw[link oneway] ##2 to[looseness=.5, out=40, in=150] ##1; + \draw[link oneway] ##1 to[looseness=.5, out=220, in=330] ##2; + \fi + }; + \else + \draw[link both] ##1 -- ##2; + \fi + } + \newcommand{\ConflictEvent}[2]{ + \node[regular polygon, regular polygon sides=8, + draw=black, fill=black, line width=2pt, + minimum size=20pt, inner sep=0pt] (##2) at (##1) {}; + \node[regular polygon, regular polygon sides=8, + draw=white, fill=conflictred, line width=0.9pt, + minimum size=14pt, inner sep=0pt, + font=\scriptsize\bfseries\sffamily, text=white] at (##1) {\textsc{fail}}; + } +} +\newcommand{\CodeWidthOf}[1]{\widthof{{\scriptsize\ttfamily\selectfont #1}}} +\newcommand{\SetLeftCodeShift}[1]{% + \settowidth{\codeboxleftshift}{#1}% + \setlength{\codeboxleftshift}{-\codeboxleftshift}% + \addtolength{\codeboxleftshift}{-3mm}% +} +\newcommand{\SetRightCodeShift}[1]{\setlength{\codeboxrightshift}{#1}} +)"; + +// ───────────────────────────────────────────────────────────────────────────── + +struct EventInfo { + const Node* node; + std::string name; + std::string label; + bool is_sync = false; + bool is_conflict = false; + bool is_pending = false; + double y = 0.0; + size_t tid = 0; +}; + +struct ConflictEdge { + const Node* src1; + const Node* src2; + const Node* ordered_after; // Unlock that links src1 to the conflict via shared lane + const Node* conflict_node; + std::string lock_var; // non-empty when routed through a lock lane +}; + +void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& path) { + const double Y_STEP = -0.8; + const double SPACING = 1.3; + const size_t n_threads = g.threads.size(); + + // ── Phase 1: collect events ─────────────────────────────────────────────── + std::vector> per_thread(n_threads); + std::unordered_map node_name; + std::unordered_map node_y; + std::vector lock_vars; + std::vector conflicts; + + auto add_lock_var = [&](const std::string& v) { + if (std::find(lock_vars.begin(), lock_vars.end(), v) == lock_vars.end()) + lock_vars.push_back(v); + }; + + for (size_t tid = 0; tid < n_threads; ++tid) { + double y = 0.0; + size_t idx = 0; + const Node* n = g.threads[tid].get(); + while (n) { + EventInfo ev; + ev.node = n; + ev.name = node_id(tid, idx++); + ev.y = y; + ev.tid = tid; + + if (auto* nd = dynamic_cast(n)) { + (void)nd; + ev.label = ""; + ev.is_sync = true; + } else if (auto* nd = dynamic_cast(n)) { + (void)nd; + ev.label = ""; + ev.is_sync = true; + } else if (auto* nd = dynamic_cast(n)) { + ev.label = latex_escape(nd->var) + " = " + std::to_string(nd->value); + } else if (auto* nd = dynamic_cast(n)) { + std::visit(overloaded{ + [&](const Read::SuccessfulRead& sr) { + ev.label = latex_escape(nd->var) + " = " + std::to_string(sr.value); + }, + [&](const Conflict&) { + ev.label = latex_escape(nd->var) + " = ?"; + ev.is_conflict = true; + } + }, nd->read_result); + } else if (auto* nd = dynamic_cast(n)) { + (void)nd; + ev.label = ""; + ev.is_sync = true; + } else if (auto* nd = dynamic_cast(n)) { + ev.label = ""; + ev.is_sync = true; + if (nd->conflict) { + ev.is_conflict = true; + conflicts.push_back({ + nd->conflict->sources.first.get(), + nd->conflict->sources.second.get(), + nd->joinee.get(), + n, "" + }); + } + } else if (auto* nd = dynamic_cast(n)) { + ev.label = "lock(" + latex_escape(nd->var) + ")"; + ev.is_sync = true; + add_lock_var(nd->var); + if (nd->conflict) { + ev.is_conflict = true; + conflicts.push_back({ + nd->conflict->sources.first.get(), + nd->conflict->sources.second.get(), + nd->ordered_after.get(), + n, nd->var + }); + } + } else if (auto* nd = dynamic_cast(n)) { + ev.label = "unlock(" + latex_escape(nd->var) + ")"; + ev.is_sync = true; + add_lock_var(nd->var); + } else if (auto* nd = dynamic_cast(n)) { + ev.label = "assert(" + latex_escape(nd->cond) + ")"; + if (!nd->passed) ev.is_conflict = true; + } else if (auto* nd = dynamic_cast(n)) { + ev.label = latex_escape(nd->statement); + ev.is_pending = true; + ev.is_sync = true; + } + + node_name[n] = ev.name; + node_y[n] = y; + per_thread[tid].push_back(std::move(ev)); + y += Y_STEP; + n = n->next.get(); + } + } + + // ── Phase 2: layout ─────────────────────────────────────────────────────── + const size_t n_locks = lock_vars.size(); + + auto thread_x = [&](size_t tid) -> double { + return tid == 0 ? 0.0 : SPACING * (n_locks + tid); + }; + auto lock_x = [&](size_t li) -> double { + return SPACING * (li + 1); + }; + + std::unordered_map lock_idx; + for (size_t i = 0; i < n_locks; ++i) + lock_idx[lock_vars[i]] = i; + + double lane_bottom = -0.5; + for (size_t tid = 0; tid < n_threads; ++tid) + if (!per_thread[tid].empty()) + lane_bottom = std::min(lane_bottom, per_thread[tid].back().y - 0.5); + + // ── Phase 3: emit ───────────────────────────────────────────────────────── + std::ofstream f(path); + + // Document preamble + f << "\\documentclass{standalone}\n" + << "\\usepackage{tikz}\n" + << "\\usepackage{calc}\n" + << "\\usetikzlibrary{automata,shapes,decorations,arrows,calc," + "arrows.meta,fit,positioning,quotes,tikzmark,shadows}\n" + << "\n" + << "\\newif\\ifdoublearrows\n" + << "\\doublearrowsfalse\n" + << FORMATTER + << "\n\\begin{document}\n" + << "\\begin{tikzpicture}[common timeline styles]\n" + << "\\TimelineColorSetup\n\n"; + + + // Named coordinates for each lock lane (used with |- notation) + for (size_t li = 0; li < n_locks; ++li) { + std::string suffix; + for (char c : lock_vars[li]) if (std::isalpha(c)) suffix += c; + if (suffix.empty()) suffix = "L" + std::to_string(li); + f << "\\coordinate (lane" << suffix << ") at (" << fmt(lock_x(li)) << ", 0);\n"; + } + f << "\n"; + + // Compute longest label for thread 0 and set left code shift + { + std::string longest; + for (auto& ev : per_thread[0]) + if (ev.label.size() > longest.size()) longest = ev.label; + if (!longest.empty()) + f << "\\SetLeftCodeShift{\\CodeWidthOf{" << longest << "}}\n"; + } + f << "\\DefineThreadEventMacros\n\n"; + + // Column headers + for (size_t tid = 0; tid < n_threads; ++tid) + f << "\\node at (" << fmt(thread_x(tid)) << ", 0.6) {T$_{" << tid << "}$};\n"; + for (size_t li = 0; li < n_locks; ++li) + f << "\\node at (" << fmt(lock_x(li)) << ", 0.6) {" + << latex_escape(lock_vars[li]) << "};\n"; + f << "\n"; + + // Helper: emit a single event node + auto emit_event = [&](const EventInfo& ev) { + double x = thread_x(ev.tid); + // Label anchor: thread 0 labels go LEFT (east anchor), others go RIGHT (west anchor) + const char* anchor = (ev.tid == 0) ? "anchor=east, xshift=-3pt" : "anchor=west, xshift=3pt"; + + if (ev.is_conflict) { + // Conflict event: emit a black outer octagon + red inner with "fail" text. + // Using a named \node (not a coordinate) so the name can be used with |-. + f << "\\node[regular polygon, regular polygon sides=8,\n" + << " draw=black, fill=black, line width=2pt,\n" + << " minimum size=20pt, inner sep=0pt] (" << ev.name << ")\n" + << " at (" << fmt(x) << ", " << fmt(ev.y) << ") {};\n" + << "\\node[regular polygon, regular polygon sides=8,\n" + << " draw=white, fill=conflictred, line width=0.9pt,\n" + << " minimum size=14pt, inner sep=0pt,\n" + << " font=\\scriptsize\\bfseries\\sffamily, text=white]\n" + << " at (" << fmt(x) << ", " << fmt(ev.y) << ") {\\textsc{fail}};\n"; + } else if (ev.is_pending) { + f << "\\fill[fill=threadtime!50] (" << fmt(x) << ", " << fmt(ev.y) << ")\n" + << " circle (1.5pt) coordinate (" << ev.name << ")\n" + << " node[" << anchor << ", codebox, opacity=0.6] {" + << ev.label << "};\n"; + } else if (ev.is_sync) { + // Sync event: invisible dot, label only + f << "\\fill (" << fmt(x) << ", " << fmt(ev.y) << ")\n" + << " circle (0pt) coordinate (" << ev.name << ")\n" + << " node[" << anchor << ", codebox] {" << ev.label << "};\n"; + } else { + // Regular event: visible gray dot + label + f << "\\fill[fill=threadtime] (" << fmt(x) << ", " << fmt(ev.y) << ")\n" + << " circle (2pt) coordinate (" << ev.name << ")\n" + << " node[" << anchor << ", codebox] {" << ev.label << "};\n"; + } + }; + + // Emit all events + for (size_t tid = 0; tid < n_threads; ++tid) { + f << "% Thread " << tid << "\n"; + for (auto& ev : per_thread[tid]) + emit_event(ev); + f << "\n"; + } + + // ── Lane lines ──────────────────────────────────────────────────────────── + f << "% Lane lines\n"; + for (size_t tid = 0; tid < n_threads; ++tid) { + double x = thread_x(tid); + auto& evs = per_thread[tid]; + if (evs.empty()) continue; + auto& last = evs.back(); + bool ends = dynamic_cast(last.node) != nullptr; + bool conflict_last = last.is_conflict; + + if (ends || conflict_last) { + f << "\\draw[thread lane, ->] (" << fmt(x) << ", 0.3) -- (" << last.name << ");\n"; + } else { + f << "\\draw[thread lane, ->] (" << fmt(x) << ", 0.3) -- (" + << fmt(x) << ", " << fmt(lane_bottom) << ");\n"; + } + } + for (size_t li = 0; li < n_locks; ++li) { + double lx = lock_x(li); + f << "\\draw[shared lane] (" << fmt(lx) << ", 0.3) -- (" + << fmt(lx) << ", " << fmt(lane_bottom) << ");\n"; + } + f << "\n"; + + // ── Sync connections ────────────────────────────────────────────────────── + f << "% Sync connections\n"; + for (size_t tid = 0; tid < n_threads; ++tid) { + for (auto& ev : per_thread[tid]) { + if (auto* nd = dynamic_cast(ev.node)) { + if (nd->spawned) { + auto it = node_name.find(nd->spawned.get()); + if (it != node_name.end()) + f << "\\draw[link oneway] (" << ev.name << ") -- (" << it->second << ");\n"; + } + } else if (auto* nd = dynamic_cast(ev.node)) { + if (nd->joinee) { + auto it = node_name.find(nd->joinee.get()); + if (it != node_name.end()) + f << "\\draw[link oneway] (" << it->second << ") -- (" << ev.name << ");\n"; + } + } else if (auto* nd = dynamic_cast(ev.node)) { + if (nd->ordered_after) { + // Pull from shared lane + std::string suffix; + for (char c : nd->var) if (std::isalpha(c)) suffix += c; + if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(nd->var)); + f << "\\draw[link oneway] (lane" << suffix << " |- " << ev.name + << ") -- (" << ev.name << ");\n"; + } + } else if (auto* nd = dynamic_cast(ev.node)) { + // Push to / pull from shared lane + std::string suffix; + for (char c : nd->var) if (std::isalpha(c)) suffix += c; + if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(nd->var)); + f << "\\PullPush{(" << ev.name << ")}{(lane" << suffix + << " |- " << ev.name << ")}\n"; + } + } + } + f << "\n"; + + // ── Conflict paths ──────────────────────────────────────────────────────── + if (!conflicts.empty()) { + f << "% Conflict paths\n" + << "\\begin{scope}[opacity=0.5]\n"; + for (auto& ce : conflicts) { + auto get_name = [&](const Node* n) -> std::optional { + if (!n) return std::nullopt; + auto it = node_name.find(n); + if (it == node_name.end()) return std::nullopt; + return it->second; + }; + + auto cn = get_name(ce.conflict_node); + if (!cn) continue; + + if (ce.src1 && !ce.lock_var.empty() && ce.ordered_after) { + // Route via shared lane: src1 → unlock → lane → conflict + auto s1 = get_name(ce.src1); + auto unl = get_name(ce.ordered_after); + std::string suffix; + for (char c : ce.lock_var) if (std::isalpha(c)) suffix += c; + if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(ce.lock_var)); + if (s1 && unl) + f << "\\draw[conflict] (" << *s1 << ") -- (" << *unl + << ") -- (lane" << suffix << " |- " << *unl + << ") -- (lane" << suffix << " |- " << *cn + << ") -- (" << *cn << ");\n"; + } else if (ce.src1) { + auto s1 = get_name(ce.src1); + if (s1) + f << "\\draw[conflict] (" << *s1 << ") to[bend right=30] (" << *cn << ");\n"; + } + + if (ce.src2) { + auto s2 = get_name(ce.src2); + if (s2) + f << "\\draw[conflict] (" << *s2 << ") -- (" << *cn << ");\n"; + } + } + f << "\\end{scope}\n\n"; + } + + f << "\\end{tikzpicture}\n\\end{document}\n"; +} + +} // namespace graph +} // namespace gitmem diff --git a/src/tikz.hh b/src/tikz.hh new file mode 100644 index 0000000..94703ab --- /dev/null +++ b/src/tikz.hh @@ -0,0 +1,14 @@ +#pragma once +#include "graph.hh" +#include +#include + +namespace gitmem { +namespace graph { + +struct TikzPrinter { + void print(const ExecutionGraph& g, const std::filesystem::path& path); +}; + +} // namespace graph +} // namespace gitmem From 31413b9e89c85fc84fce32837e3939ce7756d38d Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 21:29:35 +0200 Subject: [PATCH 02/14] better linear drawing --- src/conflict.hh | 19 +++++- src/interpreter.cc | 23 +++++-- src/interpreter.hh | 1 + src/linear/version_store.cc | 4 +- src/tikz.cc | 116 +++++++++++++++++++++++++----------- src/tikz.hh | 3 +- 6 files changed, 124 insertions(+), 42 deletions(-) diff --git a/src/conflict.hh b/src/conflict.hh index 70971d7..8c1aaff 100644 --- a/src/conflict.hh +++ b/src/conflict.hh @@ -1,11 +1,14 @@ #pragma once #include +#include #include #include namespace gitmem { +struct Event; // forward declaration — full definition in thread_trace.hh + struct FileLocation { std::string file; size_t line = 0; @@ -34,6 +37,9 @@ struct ConflictBase { virtual std::ostream &print(std::ostream &os) const = 0; virtual std::string object_name() const = 0; virtual std::pair source_locations() const = 0; + virtual std::pair, std::shared_ptr> source_events() const { + return {nullptr, nullptr}; + } friend std::ostream &operator<<(std::ostream &os, const ConflictBase &conflict) { return conflict.print(os); @@ -46,11 +52,16 @@ struct Conflict : ConflictBase { std::string var; std::pair version_a; std::pair version_b; + std::shared_ptr source_event_a; + std::shared_ptr source_event_b; Conflict(std::string var, std::pair version_a, - std::pair version_b) - : var(std::move(var)), version_a(std::move(version_a)), version_b(std::move(version_b)) {} + std::pair version_b, + std::shared_ptr source_event_a = nullptr, + std::shared_ptr source_event_b = nullptr) + : var(std::move(var)), version_a(std::move(version_a)), version_b(std::move(version_b)), + source_event_a(std::move(source_event_a)), source_event_b(std::move(source_event_b)) {} std::ostream &print(std::ostream &os) const override; @@ -62,6 +73,10 @@ struct Conflict : ConflictBase { return std::make_pair(version_a.second, version_b.second); } + std::pair, std::shared_ptr> source_events() const override { + return {source_event_a, source_event_b}; + } + bool operator==(const Conflict &other) const { // Ignore the FileLocation information for equality, as it is only for reporting purposes return var == other.var && version_a.first == other.version_a.first && version_b.first == other.version_b.first; diff --git a/src/interpreter.cc b/src/interpreter.cc index c156719..0535c2d 100644 --- a/src/interpreter.cc +++ b/src/interpreter.cc @@ -627,6 +627,9 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { // Track join nodes that need fixing up after all threads are processed std::vector> joins_to_fix; + // Track join conflict source fixups: (join node, conflict base carrying source events) + std::vector, std::shared_ptr>> join_conflict_fixups; + // Track read nodes that need their source fixed up std::vector, std::shared_ptr>> reads_to_fix; @@ -710,14 +713,15 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { event_to_node[event] = node; }, [&](const JoinEvent& arg) { - // Create join node - will fix up joinee pointer later + // Create join node - will fix up joinee pointer and conflict sources later std::optional conflict; if (arg.maybe_conflict) { - // Just mark as conflicting - version IDs don't map directly to nodes - conflict = graph::Conflict(""); // empty var name for joins + conflict = graph::Conflict(arg.maybe_conflict->object_name()); } auto node = std::make_shared(arg.joinee_tid, nullptr, conflict); joins_to_fix.push_back(node); + if (arg.maybe_conflict) + join_conflict_fixups.push_back({node, arg.maybe_conflict}); link_in_program_order(tid, node); event_to_node[event] = node; }, @@ -779,6 +783,16 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { const_cast&>(join_node->joinee) = thread_tails[joinee_tid]; } + // Fix up join conflict sources using the source events now that event_to_node is complete + for (auto& [join_node, cb] : join_conflict_fixups) { + auto [evt_a, evt_b] = cb->source_events(); + std::shared_ptr src_a, src_b; + if (evt_a && event_to_node.count(evt_a)) src_a = event_to_node.at(evt_a); + if (evt_b && event_to_node.count(evt_b)) src_b = event_to_node.at(evt_b); + if (src_a || src_b) + const_cast(*join_node->conflict).sources = {src_a, src_b}; + } + // Fix up read nodes to point to their source write events for (auto& [read_node, source_event] : reads_to_fix) { assert(event_to_node.contains(source_event) && "source missing in event_to_node map"); @@ -791,8 +805,9 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { void Interpreter::print_execution_graph(const std::filesystem::path& output_path) { auto exec_graph = build_execution_graph_from_traces(); if (output_path.extension() == ".tex") { + bool linear_mode = dynamic_cast(gctx.model.get()) != nullptr; graph::TikzPrinter tikz; - tikz.print(exec_graph, output_path); + tikz.print(exec_graph, output_path, linear_mode); } else { graph::GraphvizPrinter gv(output_path); gv.visit(exec_graph.entry.get()); diff --git a/src/interpreter.hh b/src/interpreter.hh index 189fc62..c6f4298 100644 --- a/src/interpreter.hh +++ b/src/interpreter.hh @@ -4,6 +4,7 @@ #include "graph.hh" #include "graphviz.hh" #include "tikz.hh" +#include "linear/memory_model.hh" #include "lang.hh" #include "progress_status.hh" #include diff --git a/src/linear/version_store.cc b/src/linear/version_store.cc index bce8a52..f825994 100644 --- a/src/linear/version_store.cc +++ b/src/linear/version_store.cc @@ -97,7 +97,9 @@ std::optional GlobalVersionStore::check_conflicts( return Conflict( obj, {current_timestamp, event_location(local_value)}, - {latest.timestamp(), event_location(latest.value())}); + {latest.timestamp(), event_location(latest.value())}, + local_value.source_event, + latest.value().source_event); } } return std::nullopt; diff --git a/src/tikz.cc b/src/tikz.cc index b6fb60d..faedb85 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -144,7 +144,8 @@ struct ConflictEdge { std::string lock_var; // non-empty when routed through a lock lane }; -void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& path) { +void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& path, + bool linear_mode) { const double Y_STEP = -0.8; const double SPACING = 1.3; const size_t n_threads = g.threads.size(); @@ -153,6 +154,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa std::vector> per_thread(n_threads); std::unordered_map node_name; std::unordered_map node_y; + std::unordered_map node_tid; std::vector lock_vars; std::vector conflicts; @@ -181,14 +183,14 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa ev.label = ""; ev.is_sync = true; } else if (auto* nd = dynamic_cast(n)) { - ev.label = latex_escape(nd->var) + " = " + std::to_string(nd->value); + ev.label = "W(" + latex_escape(nd->var) + ") = " + std::to_string(nd->value); } else if (auto* nd = dynamic_cast(n)) { std::visit(overloaded{ [&](const Read::SuccessfulRead& sr) { - ev.label = latex_escape(nd->var) + " = " + std::to_string(sr.value); + ev.label = "R(" + latex_escape(nd->var) + ") = " + std::to_string(sr.value); }, [&](const Conflict&) { - ev.label = latex_escape(nd->var) + " = ?"; + ev.label = "R(" + latex_escape(nd->var) + ") = ?"; ev.is_conflict = true; } }, nd->read_result); @@ -236,6 +238,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa node_name[n] = ev.name; node_y[n] = y; + node_tid[n] = tid; per_thread[tid].push_back(std::move(ev)); y += Y_STEP; n = n->next.get(); @@ -243,7 +246,10 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } // ── Phase 2: layout ─────────────────────────────────────────────────────── - const size_t n_locks = lock_vars.size(); + // In linear mode a single "g" lane represents the global sync object and + // replaces per-variable lock lanes in the diagram. + const bool has_g_lane = linear_mode; + const size_t n_locks = has_g_lane ? 0 : lock_vars.size(); auto thread_x = [&](size_t tid) -> double { return tid == 0 ? 0.0 : SPACING * (n_locks + tid); @@ -251,6 +257,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa auto lock_x = [&](size_t li) -> double { return SPACING * (li + 1); }; + const double g_x = SPACING * (n_locks + n_threads); std::unordered_map lock_idx; for (size_t i = 0; i < n_locks; ++i) @@ -272,7 +279,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa "arrows.meta,fit,positioning,quotes,tikzmark,shadows}\n" << "\n" << "\\newif\\ifdoublearrows\n" - << "\\doublearrowsfalse\n" + << "\\doublearrowstrue\n" << FORMATTER << "\n\\begin{document}\n" << "\\begin{tikzpicture}[common timeline styles]\n" @@ -304,6 +311,10 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa for (size_t li = 0; li < n_locks; ++li) f << "\\node at (" << fmt(lock_x(li)) << ", 0.6) {" << latex_escape(lock_vars[li]) << "};\n"; + if (has_g_lane) { + f << "\\coordinate (laneG) at (" << fmt(g_x) << ", 0);\n"; + f << "\\node at (" << fmt(g_x) << ", 0.6) {g};\n"; + } f << "\n"; // Helper: emit a single event node @@ -335,7 +346,6 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa << " circle (0pt) coordinate (" << ev.name << ")\n" << " node[" << anchor << ", codebox] {" << ev.label << "};\n"; } else { - // Regular event: visible gray dot + label f << "\\fill[fill=threadtime] (" << fmt(x) << ", " << fmt(ev.y) << ")\n" << " circle (2pt) coordinate (" << ev.name << ")\n" << " node[" << anchor << ", codebox] {" << ev.label << "};\n"; @@ -372,6 +382,9 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa f << "\\draw[shared lane] (" << fmt(lx) << ", 0.3) -- (" << fmt(lx) << ", " << fmt(lane_bottom) << ");\n"; } + if (has_g_lane) + f << "\\draw[shared lane] (" << fmt(g_x) << ", 0.3) -- (" + << fmt(g_x) << ", " << fmt(lane_bottom) << ");\n"; f << "\n"; // ── Sync connections ────────────────────────────────────────────────────── @@ -379,20 +392,21 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa for (size_t tid = 0; tid < n_threads; ++tid) { for (auto& ev : per_thread[tid]) { if (auto* nd = dynamic_cast(ev.node)) { - if (nd->spawned) { - auto it = node_name.find(nd->spawned.get()); - if (it != node_name.end()) - f << "\\draw[link oneway] (" << ev.name << ") -- (" << it->second << ");\n"; - } + (void)nd; + // g: spawn pulls + pushes + if (has_g_lane) + f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; } else if (auto* nd = dynamic_cast(ev.node)) { - if (nd->joinee) { - auto it = node_name.find(nd->joinee.get()); - if (it != node_name.end()) - f << "\\draw[link oneway] (" << it->second << ") -- (" << ev.name << ");\n"; - } + (void)nd; + // g: join pulls + if (has_g_lane) + f << "\\draw[link oneway] (laneG |- " << ev.name << ") -- (" << ev.name << ");\n"; } else if (auto* nd = dynamic_cast(ev.node)) { - if (nd->ordered_after) { - // Pull from shared lane + if (has_g_lane) { + // g: lock pulls + f << "\\draw[link oneway] (laneG |- " << ev.name << ") -- (" << ev.name << ");\n"; + } else if (nd->ordered_after) { + // Lock lane: pull from per-variable lane std::string suffix; for (char c : nd->var) if (std::isalpha(c)) suffix += c; if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(nd->var)); @@ -400,12 +414,25 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa << ") -- (" << ev.name << ");\n"; } } else if (auto* nd = dynamic_cast(ev.node)) { - // Push to / pull from shared lane - std::string suffix; - for (char c : nd->var) if (std::isalpha(c)) suffix += c; - if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(nd->var)); - f << "\\PullPush{(" << ev.name << ")}{(lane" << suffix - << " |- " << ev.name << ")}\n"; + if (has_g_lane) { + // g: unlock pulls + pushes + f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; + } else { + // Lock lane: PullPush to per-variable lane + std::string suffix; + for (char c : nd->var) if (std::isalpha(c)) suffix += c; + if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(nd->var)); + f << "\\PullPush{(" << ev.name << ")}{(lane" << suffix + << " |- " << ev.name << ")}\n"; + } + } else if (dynamic_cast(ev.node)) { + // g: start pulls + if (has_g_lane) + f << "\\draw[link oneway] (laneG |- " << ev.name << ") -- (" << ev.name << ");\n"; + } else if (dynamic_cast(ev.node)) { + // g: end pulls + pushes + if (has_g_lane) + f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; } } } @@ -438,16 +465,37 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa << ") -- (lane" << suffix << " |- " << *unl << ") -- (lane" << suffix << " |- " << *cn << ") -- (" << *cn << ");\n"; - } else if (ce.src1) { - auto s1 = get_name(ce.src1); - if (s1) - f << "\\draw[conflict] (" << *s1 << ") to[bend right=30] (" << *cn << ");\n"; - } + } else if (ce.src1 || ce.src2) { + // Emit one conflict path per source. + // Same-thread source → direct line along the thread lane. + // Cross-thread source → route through the source thread's last sync + // node (its End) then down the g lane to the conflict. + auto conflict_tid_it = node_tid.find(ce.conflict_node); + size_t conflict_tid = (conflict_tid_it != node_tid.end()) + ? conflict_tid_it->second : SIZE_MAX; + + auto emit_src = [&](const Node* src) { + auto s = get_name(src); + if (!s) return; + auto src_tid_it = node_tid.find(src); + size_t src_tid = (src_tid_it != node_tid.end()) + ? src_tid_it->second : SIZE_MAX; + + if (has_g_lane && src_tid != conflict_tid) { + // Cross-thread: src → End of src thread → g → conflict + const std::string& end_name = per_thread[src_tid].back().name; + f << "\\draw[conflict] (" << *s << ") -- (" << end_name + << ") -- (laneG |- " << end_name + << ") -- (laneG |- " << *cn + << ") -- (" << *cn << ");\n"; + } else { + // Same thread (or no g lane): direct line + f << "\\draw[conflict] (" << *s << ") -- (" << *cn << ");\n"; + } + }; - if (ce.src2) { - auto s2 = get_name(ce.src2); - if (s2) - f << "\\draw[conflict] (" << *s2 << ") -- (" << *cn << ");\n"; + if (ce.src1) emit_src(ce.src1); + if (ce.src2) emit_src(ce.src2); } } f << "\\end{scope}\n\n"; diff --git a/src/tikz.hh b/src/tikz.hh index 94703ab..c347566 100644 --- a/src/tikz.hh +++ b/src/tikz.hh @@ -7,7 +7,8 @@ namespace gitmem { namespace graph { struct TikzPrinter { - void print(const ExecutionGraph& g, const std::filesystem::path& path); + void print(const ExecutionGraph& g, const std::filesystem::path& path, + bool linear_mode = false); }; } // namespace graph From d2cd2c41f33c234199a9a5a725a6ad0dcf1f6b93 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 21:35:40 +0200 Subject: [PATCH 03/14] linear conflicts follow paths proprly and vars are subscripted --- src/tikz.cc | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/src/tikz.cc b/src/tikz.cc index faedb85..de9d79b 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -183,23 +183,23 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa ev.label = ""; ev.is_sync = true; } else if (auto* nd = dynamic_cast(n)) { - ev.label = "W(" + latex_escape(nd->var) + ") = " + std::to_string(nd->value); + ev.label = "W(" + latex_escape(nd->var) + "$_{" + std::to_string(tid) + "}$) = " + std::to_string(nd->value); } else if (auto* nd = dynamic_cast(n)) { std::visit(overloaded{ [&](const Read::SuccessfulRead& sr) { - ev.label = "R(" + latex_escape(nd->var) + ") = " + std::to_string(sr.value); + ev.label = "R(" + latex_escape(nd->var) + "$_{" + std::to_string(tid) + "}$) = " + std::to_string(sr.value); }, [&](const Conflict&) { - ev.label = "R(" + latex_escape(nd->var) + ") = ?"; + ev.label = "R(" + latex_escape(nd->var) + "$_{" + std::to_string(tid) + "}$) = ?"; ev.is_conflict = true; } }, nd->read_result); } else if (auto* nd = dynamic_cast(n)) { (void)nd; - ev.label = ""; + ev.label = "spawn"; ev.is_sync = true; } else if (auto* nd = dynamic_cast(n)) { - ev.label = ""; + ev.label = "join"; ev.is_sync = true; if (nd->conflict) { ev.is_conflict = true; @@ -370,10 +370,11 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa bool ends = dynamic_cast(last.node) != nullptr; bool conflict_last = last.is_conflict; + const std::string& start_name = evs.front().name; if (ends || conflict_last) { - f << "\\draw[thread lane, ->] (" << fmt(x) << ", 0.3) -- (" << last.name << ");\n"; + f << "\\draw[thread lane, ->] (" << start_name << ") -- (" << last.name << ");\n"; } else { - f << "\\draw[thread lane, ->] (" << fmt(x) << ", 0.3) -- (" + f << "\\draw[thread lane, ->] (" << start_name << ") -- (" << fmt(x) << ", " << fmt(lane_bottom) << ");\n"; } } @@ -482,10 +483,14 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa ? src_tid_it->second : SIZE_MAX; if (has_g_lane && src_tid != conflict_tid) { - // Cross-thread: src → End of src thread → g → conflict + // Cross-thread: src → End of src thread → (arc) → g → conflict const std::string& end_name = per_thread[src_tid].back().name; + // Match the PullPush push-arc direction (event left of g → out=320,in=210) + const char* push_arc = (thread_x(src_tid) < g_x) + ? "looseness=.5, out=320, in=210" + : "looseness=.5, out=220, in=330"; f << "\\draw[conflict] (" << *s << ") -- (" << end_name - << ") -- (laneG |- " << end_name + << ") to[" << push_arc << "] (laneG |- " << end_name << ") -- (laneG |- " << *cn << ") -- (" << *cn << ");\n"; } else { From a3a16967b8975c949030ae97b097138e0897abf1 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 23:34:01 +0200 Subject: [PATCH 04/14] stage changes are now communicated --- src/tikz.cc | 69 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 69 insertions(+) diff --git a/src/tikz.cc b/src/tikz.cc index de9d79b..4782143 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -2,6 +2,7 @@ #include "overloaded.hh" #include #include +#include #include #include #include @@ -268,6 +269,63 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa if (!per_thread[tid].empty()) lane_bottom = std::min(lane_bottom, per_thread[tid].back().y - 0.5); + // ── Phase 1b: sync state annotations (push/pull labels on g-lane arcs) ──── + // push_annotation: dark grey sharedupdate box — what the thread staged → g + // pull_annotation: light grey stateupdate box — what the thread receives ← g + std::unordered_map push_annotation; + std::unordered_map pull_annotation; + + if (has_g_lane) { + auto format_state = [&](size_t tid, + const std::map& state) -> std::string { + if (state.empty()) return ""; + std::string lbl = "$"; + bool first = true; + for (auto& [var, val] : state) { + if (!first) lbl += ",\\,"; + lbl += latex_escape(var) + "_{" + std::to_string(tid) + "}=" + + std::to_string(val); + first = false; + } + return lbl + "$"; + }; + + // Pass A: push annotations — writes accumulated between End/Spawn sync points + for (size_t tid = 0; tid < n_threads; ++tid) { + std::map pending; + for (auto& ev : per_thread[tid]) { + if (auto* wr = dynamic_cast(ev.node)) { + pending[wr->var] = wr->value; + } else if (dynamic_cast(ev.node) + || dynamic_cast(ev.node)) { + std::string lbl = format_state(tid, pending); + if (!lbl.empty()) + push_annotation[ev.node] = lbl; + pending.clear(); + } + } + } + + // Pass B: pull annotations — derived from the corresponding push + // Start of spawned thread ← inherits Spawn's push state + // Join ← inherits joinee's End push state + for (size_t tid = 0; tid < n_threads; ++tid) { + for (auto& ev : per_thread[tid]) { + if (auto* sp = dynamic_cast(ev.node)) { + auto it = push_annotation.find(ev.node); + if (it != push_annotation.end() && sp->spawned) + pull_annotation[sp->spawned.get()] = it->second; + } else if (auto* jn = dynamic_cast(ev.node)) { + if (jn->joinee) { + auto it = push_annotation.find(jn->joinee.get()); + if (it != push_annotation.end()) + pull_annotation[ev.node] = it->second; + } + } + } + } + } + // ── Phase 3: emit ───────────────────────────────────────────────────────── std::ofstream f(path); @@ -435,6 +493,17 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa if (has_g_lane) f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; } + // State annotations on g-lane arcs + if (has_g_lane) { + if (push_annotation.count(ev.node)) + f << "\\node[sharedupdate, below=1pt] at ($(" << ev.name + << ")!0.5!(laneG |- " << ev.name << ")$) {" + << push_annotation.at(ev.node) << "};\n"; + if (pull_annotation.count(ev.node)) + f << "\\node[stateupdate, above=1pt] at ($(" << ev.name + << ")!0.5!(laneG |- " << ev.name << ")$) {" + << pull_annotation.at(ev.node) << "};\n"; + } } } f << "\n"; From b50cc9906f8c900e5a07ce0195613ead4529da06 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 23:43:59 +0200 Subject: [PATCH 05/14] better layout for linear --- src/tikz.cc | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/tikz.cc b/src/tikz.cc index 4782143..b8c452f 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -252,13 +252,18 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa const bool has_g_lane = linear_mode; const size_t n_locks = has_g_lane ? 0 : lock_vars.size(); + // In linear mode g sits in the middle: left threads 0..g_mid-1, right threads g_mid..N-1. + const size_t g_mid = has_g_lane ? (n_threads + 1) / 2 : 0; + auto thread_x = [&](size_t tid) -> double { + if (has_g_lane) + return tid < g_mid ? SPACING * tid : SPACING * (tid + 1); return tid == 0 ? 0.0 : SPACING * (n_locks + tid); }; auto lock_x = [&](size_t li) -> double { return SPACING * (li + 1); }; - const double g_x = SPACING * (n_locks + n_threads); + const double g_x = has_g_lane ? SPACING * g_mid : SPACING * (n_locks + n_threads); std::unordered_map lock_idx; for (size_t i = 0; i < n_locks; ++i) @@ -378,8 +383,9 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa // Helper: emit a single event node auto emit_event = [&](const EventInfo& ev) { double x = thread_x(ev.tid); - // Label anchor: thread 0 labels go LEFT (east anchor), others go RIGHT (west anchor) - const char* anchor = (ev.tid == 0) ? "anchor=east, xshift=-3pt" : "anchor=west, xshift=3pt"; + // Label anchor: threads left of g go LEFT (east anchor), threads right go RIGHT (west anchor) + const bool is_left = has_g_lane ? (ev.tid < g_mid) : (ev.tid == 0); + const char* anchor = is_left ? "anchor=east, xshift=-3pt" : "anchor=west, xshift=3pt"; if (ev.is_conflict) { // Conflict event: emit a black outer octagon + red inner with "fail" text. From db4674d8a4500d822804761d0b479490e6f0e46f Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 23:53:46 +0200 Subject: [PATCH 06/14] linear diagrams have more space to breath --- src/tikz.cc | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/src/tikz.cc b/src/tikz.cc index b8c452f..dfd9aab 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -147,8 +147,9 @@ struct ConflictEdge { void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& path, bool linear_mode) { - const double Y_STEP = -0.8; - const double SPACING = 1.3; + const double Y_STEP = -0.8; // gap between regular events + const double Y_SYNC_STEP = -1.2; // gap when either neighbour is a sync event + const double SPACING = 1.8; const size_t n_threads = g.threads.size(); // ── Phase 1: collect events ─────────────────────────────────────────────── @@ -159,6 +160,12 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa std::vector lock_vars; std::vector conflicts; + auto is_sync_node = [](const Node* nd) -> bool { + return dynamic_cast(nd) || dynamic_cast(nd) + || dynamic_cast(nd) || dynamic_cast(nd) + || dynamic_cast(nd) || dynamic_cast(nd); + }; + auto add_lock_var = [&](const std::string& v) { if (std::find(lock_vars.begin(), lock_vars.end(), v) == lock_vars.end()) lock_vars.push_back(v); @@ -240,9 +247,14 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa node_name[n] = ev.name; node_y[n] = y; node_tid[n] = tid; + const Node* next_n = n->next.get(); + // Use extra spacing when the current or next event connects to g so that + // PullPush arcs and annotation boxes don't crowd adjacent events. + const bool near_sync = linear_mode + && (ev.is_sync || (next_n && is_sync_node(next_n))); per_thread[tid].push_back(std::move(ev)); - y += Y_STEP; - n = n->next.get(); + y += near_sync ? Y_SYNC_STEP : Y_STEP; + n = next_n; } } @@ -502,11 +514,11 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa // State annotations on g-lane arcs if (has_g_lane) { if (push_annotation.count(ev.node)) - f << "\\node[sharedupdate, below=1pt] at ($(" << ev.name + f << "\\node[sharedupdate, below=8pt] at ($(" << ev.name << ")!0.5!(laneG |- " << ev.name << ")$) {" << push_annotation.at(ev.node) << "};\n"; if (pull_annotation.count(ev.node)) - f << "\\node[stateupdate, above=1pt] at ($(" << ev.name + f << "\\node[stateupdate, above=8pt] at ($(" << ev.name << ")!0.5!(laneG |- " << ev.name << ")$) {" << pull_annotation.at(ev.node) << "};\n"; } From 383bd1356fcdd2a4b487af2d0db93d3b08e4a2de Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Wed, 1 Jul 2026 11:38:36 +0200 Subject: [PATCH 07/14] better layout that respects ordering of inter-thread event timings --- src/execution_state.hh | 5 + src/graph.hh | 6 +- src/interpreter.cc | 65 ++++++--- src/linear/memory_model.hh | 2 + src/memory_model.hh | 5 + src/thread_trace.hh | 8 +- src/tikz.cc | 276 ++++++++++++++++++++++++++++++++----- 7 files changed, 314 insertions(+), 53 deletions(-) diff --git a/src/execution_state.hh b/src/execution_state.hh index 1c58080..1572ef4 100644 --- a/src/execution_state.hh +++ b/src/execution_state.hh @@ -72,6 +72,11 @@ private: public: Lock& get_lock(std::string); + // Most recent unlock event across ALL lock variables (used by the linear + // memory model so that lock(l2) gets an ordered_after edge to the last + // unlock(l1) that pushed to g, even though l2 was never unlocked before). + std::shared_ptr last_g_push_event = nullptr; + // AST evaluation cache lang::NodeMap cache; diff --git a/src/graph.hh b/src/graph.hh index 566f21b..6b64cfb 100644 --- a/src/graph.hh +++ b/src/graph.hh @@ -144,8 +144,12 @@ struct Lock : Node { struct Unlock : Node { const std::string var; + const std::optional conflict; + std::shared_ptr g_predecessor; - Unlock(const std::string var) : var(var) {} + Unlock(const std::string var, std::optional conflict = std::nullopt, + std::shared_ptr g_predecessor = nullptr) + : var(var), conflict(conflict), g_predecessor(g_predecessor) {} void accept(Visitor *v) const override { v->visitUnlock(this); } }; diff --git a/src/interpreter.cc b/src/interpreter.cc index 0535c2d..db0f358 100644 --- a/src/interpreter.cc +++ b/src/interpreter.cc @@ -306,13 +306,20 @@ std::variant Interpreter::run_statement(Node stmt, Threa lock.owner = thread.tid; + // In the linear model all unlocks push to the same g, so a lock on any + // variable follows the most recent unlock of ANY variable (not just this + // one). Use the global g-push predecessor when the per-lock one is absent. + auto lock_predecessor = (gctx.model->uses_global_lock_ordering() + && !lock.last_unlock_event) + ? gctx.last_g_push_event : lock.last_unlock_event; + if (auto conflict = gctx.model->on_lock(ctx, lock)) { verbose::out << (**conflict) << std::endl; - thread.trace.on_lock(var, lock.last_unlock_event, *conflict); + thread.trace.on_lock(var, lock_predecessor, *conflict); return termination::DataRace(*conflict); } - thread.trace.on_lock(var, lock.last_unlock_event); + thread.trace.on_lock(var, lock_predecessor); verbose::out << "Locked " << var << std::endl; } else if (s == lang::Unlock) { @@ -332,7 +339,9 @@ std::variant Interpreter::run_statement(Node stmt, Threa if (auto conflict = gctx.model->on_unlock(ctx, lock)) { verbose::out << (**conflict) << std::endl; - thread.trace.on_unlock(var, *conflict); + auto g_pred = gctx.model->uses_global_lock_ordering() + ? gctx.last_g_push_event : nullptr; + thread.trace.on_unlock(var, *conflict, g_pred); return termination::DataRace(*conflict); } @@ -340,6 +349,7 @@ std::variant Interpreter::run_statement(Node stmt, Threa lock.owner.reset(); lock.last_unlock_event = thread.trace.on_unlock(var); + gctx.last_g_push_event = lock.last_unlock_event; verbose::out << "Unlocked " << var << std::endl; @@ -633,6 +643,13 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { // Track read nodes that need their source fixed up std::vector, std::shared_ptr>> reads_to_fix; + // Track lock nodes whose ordered_after must be resolved after all threads + // are processed (the predecessor may come from another thread's trace). + std::vector, std::shared_ptr>> locks_ordered_after_fixups; + + // Track conflicting unlock nodes whose g_predecessor must be resolved after all threads. + std::vector, std::shared_ptr>> unlocks_g_predecessor_fixups; + // Map from trace events to graph nodes std::unordered_map, std::shared_ptr> event_to_node; @@ -726,31 +743,30 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { event_to_node[event] = node; }, [&](const LockEvent& arg) { - // Link to the last unlock event using the event-to-node mapping - std::shared_ptr ordered_after = nullptr; - if (arg.last_unlock_event && event_to_node.contains(arg.last_unlock_event)) { - ordered_after = event_to_node[arg.last_unlock_event]; - } - std::optional conflict; if (arg.maybe_conflict) { - // Mark as conflicting with the lock name conflict = graph::Conflict(arg.lock_name); } - auto node = std::make_shared(arg.lock_name, ordered_after, conflict); + // ordered_after may reference another thread's unlock; defer resolution. + auto node = std::make_shared(arg.lock_name, nullptr, conflict); + if (arg.last_unlock_event) { + locks_ordered_after_fixups.push_back({node, arg.last_unlock_event}); + } link_in_program_order(tid, node); event_to_node[event] = node; }, [&](const UnlockEvent& arg) { - auto node = std::make_shared(arg.lock_name); + std::optional unlock_conflict; + if (arg.maybe_conflict) { + unlock_conflict = graph::Conflict(arg.maybe_conflict->object_name()); + } + auto node = std::make_shared(arg.lock_name, unlock_conflict); + if (arg.g_predecessor) { + unlocks_g_predecessor_fixups.push_back({node, arg.g_predecessor}); + } last_unlock_per_lock[arg.lock_name] = node; link_in_program_order(tid, node); event_to_node[event] = node; - - // Mark conflict if present - if (arg.maybe_conflict) { - // TODO: Visualize unlock conflicts - } }, [&](const AssertEvent& arg) { auto node = std::make_shared(arg.condition, arg.pass); @@ -776,6 +792,21 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { } } + // Fix up lock ordered_after edges (predecessor may be in another thread's trace) + for (auto& [lock_node, unlock_event] : locks_ordered_after_fixups) { + if (event_to_node.contains(unlock_event)) { + const_cast&>(lock_node->ordered_after) = + event_to_node[unlock_event]; + } + } + + // Fix up conflicting unlock g_predecessor edges (predecessor is in another thread). + for (auto& [unlock_node, pred_event] : unlocks_g_predecessor_fixups) { + if (event_to_node.contains(pred_event)) { + unlock_node->g_predecessor = event_to_node[pred_event]; + } + } + // Fix up join nodes to point to the actual end of the joined threads for (auto& join_node : joins_to_fix) { ThreadID joinee_tid = join_node->tid; diff --git a/src/linear/memory_model.hh b/src/linear/memory_model.hh index 469cc83..22bcac0 100644 --- a/src/linear/memory_model.hh +++ b/src/linear/memory_model.hh @@ -48,6 +48,8 @@ public: bool is_scheduling_point(SyncOperation op) const override; + bool uses_global_lock_ordering() const override { return true; } + std::unique_ptr make_thread_state(ThreadID tid) const override { return std::make_unique(tid); } diff --git a/src/memory_model.hh b/src/memory_model.hh index 61ce100..98b2c5f 100644 --- a/src/memory_model.hh +++ b/src/memory_model.hh @@ -62,6 +62,11 @@ public: // (i.e., the scheduler should consider switching threads here) virtual bool is_scheduling_point(SyncOperation op) const = 0; + // Returns true if all unlock events share a single global g-lane (linear + // memory model), so that a lock on any variable follows the most recent + // unlock on ANY variable rather than just the same one. + virtual bool uses_global_lock_ordering() const { return false; } + virtual std::string build_revision_graph_dot(const std::vector& thread_states) const = 0; virtual std::ostream &print(std::ostream &os) const = 0; diff --git a/src/thread_trace.hh b/src/thread_trace.hh index 94a7b78..d53193c 100644 --- a/src/thread_trace.hh +++ b/src/thread_trace.hh @@ -24,7 +24,7 @@ struct ReadValue { const size_t value; const std::shared_ptr source_event struct ReadEvent { const std::string var; std::variant> value_or_conflict; }; struct WriteEvent { const std::string var; const size_t value; const FileLocation location; }; struct LockEvent { std::string lock_name; std::shared_ptr maybe_conflict; std::shared_ptr last_unlock_event; }; -struct UnlockEvent { const std::string lock_name; std::shared_ptr maybe_conflict; }; +struct UnlockEvent { const std::string lock_name; std::shared_ptr maybe_conflict; std::shared_ptr g_predecessor = nullptr; }; struct JoinEvent { const ThreadID joinee_tid; std::shared_ptr maybe_conflict; }; struct AssertEvent { const std::string condition; bool pass; }; @@ -173,8 +173,10 @@ private: return append(std::move(lock_name), std::move(conflict), last_unlock_event); } - std::shared_ptr on_unlock(const std::string lock_name, std::shared_ptr conflict = nullptr) { - return append(std::move(lock_name), conflict); + std::shared_ptr on_unlock(const std::string lock_name, + std::shared_ptr conflict = nullptr, + std::shared_ptr g_predecessor = nullptr) { + return append(std::move(lock_name), conflict, g_predecessor); } std::shared_ptr on_join(ThreadID tid, std::shared_ptr conflict = nullptr) { diff --git a/src/tikz.cc b/src/tikz.cc index dfd9aab..f44fc7e 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -147,9 +147,12 @@ struct ConflictEdge { void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& path, bool linear_mode) { - const double Y_STEP = -0.8; // gap between regular events - const double Y_SYNC_STEP = -1.2; // gap when either neighbour is a sync event - const double SPACING = 1.8; + const double Y_STEP = -0.8; // gap between regular events + const double Y_SYNC_STEP = -1.2; // gap when either neighbour is a sync event + const double Y_SPAWN_OFFSET = -0.4; // child thread starts this far below its spawn + const double Y_JOIN_GAP = 0.3; // min gap between joinee's end and join event + const double Y_LOCK_GAP = 0.4; // min gap between ordered_after unlock and lock + const double SPACING = 1.8; const size_t n_threads = g.threads.size(); // ── Phase 1: collect events ─────────────────────────────────────────────── @@ -171,8 +174,12 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa lock_vars.push_back(v); }; + // Spawned threads start just below their parent spawn event rather than at + // y=0, so concurrent events in different threads land at different y values. + std::vector thread_start_y(n_threads, 0.0); + for (size_t tid = 0; tid < n_threads; ++tid) { - double y = 0.0; + double y = thread_start_y[tid]; size_t idx = 0; const Node* n = g.threads[tid].get(); while (n) { @@ -203,9 +210,10 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } }, nd->read_result); } else if (auto* nd = dynamic_cast(n)) { - (void)nd; ev.label = "spawn"; ev.is_sync = true; + if (nd->tid < n_threads && thread_start_y[nd->tid] == 0.0) + thread_start_y[nd->tid] = y + Y_SPAWN_OFFSET; } else if (auto* nd = dynamic_cast(n)) { ev.label = "join"; ev.is_sync = true; @@ -235,6 +243,9 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa ev.label = "unlock(" + latex_escape(nd->var) + ")"; ev.is_sync = true; add_lock_var(nd->var); + if (nd->conflict) { + ev.is_conflict = true; + } } else if (auto* nd = dynamic_cast(n)) { ev.label = "assert(" + latex_escape(nd->cond) + ")"; if (!nd->passed) ev.is_conflict = true; @@ -258,28 +269,132 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } } + // Post-pass 1: enforce causal y-ordering for lock events. + // A lock that follows an unlock in another thread (via ordered_after) must + // appear below that unlock — otherwise the diagram looks like a race even + // when the execution is conflict-free. Process threads in order so that + // multi-hop chains (T0.unlock → T1.lock … T1.unlock → T2.lock) propagate + // correctly in a single pass. + // This must run BEFORE the join pass so that a joined thread's final + // position is already correct when the join pass computes its gap. + for (size_t tid = 0; tid < n_threads; ++tid) { + for (size_t i = 0; i < per_thread[tid].size(); ++i) { + auto& ev = per_thread[tid][i]; + if (auto* lk = dynamic_cast(ev.node)) { + if (lk->ordered_after) { + auto it = node_y.find(lk->ordered_after.get()); + if (it != node_y.end()) { + double required_y = it->second - Y_LOCK_GAP; + if (ev.y > required_y) { + double shift = required_y - ev.y; + for (size_t j = i; j < per_thread[tid].size(); ++j) { + per_thread[tid][j].y += shift; + node_y[per_thread[tid][j].node] = per_thread[tid][j].y; + } + } + } + } + } + } + } + + // Post-pass 1b: enforce causal y-ordering for conflicting unlock events. + // A conflicting unlock must appear below the predecessor unlock that already + // pushed to g — otherwise the FAIL node appears before the push it conflicts + // with, making the diagram look wrong. + for (size_t tid = 0; tid < n_threads; ++tid) { + for (size_t i = 0; i < per_thread[tid].size(); ++i) { + auto& ev = per_thread[tid][i]; + if (auto* ul = dynamic_cast(ev.node)) { + if (ul->g_predecessor) { + auto it = node_y.find(ul->g_predecessor.get()); + if (it != node_y.end()) { + double required_y = it->second - Y_LOCK_GAP; + if (ev.y > required_y) { + double shift = required_y - ev.y; + for (size_t j = i; j < per_thread[tid].size(); ++j) { + per_thread[tid][j].y += shift; + node_y[per_thread[tid][j].node] = per_thread[tid][j].y; + } + } + } + } + } + } + } + + // Post-pass 2: if a join event sits above the last event of the joined thread, + // shift the join and all later events in this thread downward so the join + // arrow always points up-and-across, not sideways or backward. + for (size_t tid = 0; tid < n_threads; ++tid) { + for (size_t i = 0; i < per_thread[tid].size(); ++i) { + auto& ev = per_thread[tid][i]; + if (auto* jn = dynamic_cast(ev.node)) { + if (jn->tid < n_threads && !per_thread[jn->tid].empty()) { + double joinee_end_y = per_thread[jn->tid].back().y; + double required_y = joinee_end_y - Y_JOIN_GAP; + if (ev.y > required_y) { + double shift = required_y - ev.y; + for (size_t j = i; j < per_thread[tid].size(); ++j) { + per_thread[tid][j].y += shift; + node_y[per_thread[tid][j].node] = per_thread[tid][j].y; + } + } + } + } + } + } + // ── Phase 2: layout ─────────────────────────────────────────────────────── - // In linear mode a single "g" lane represents the global sync object and - // replaces per-variable lock lanes in the diagram. const bool has_g_lane = linear_mode; const size_t n_locks = has_g_lane ? 0 : lock_vars.size(); - // In linear mode g sits in the middle: left threads 0..g_mid-1, right threads g_mid..N-1. + std::unordered_map lock_idx; + for (size_t i = 0; i < n_locks; ++i) + lock_idx[lock_vars[i]] = i; + + // In linear mode g sits in the middle of the threads. const size_t g_mid = has_g_lane ? (n_threads + 1) / 2 : 0; + // In branching mode interleave threads with their associated locks: T0, L0, T1, L1, … + // A lock is placed immediately after the first thread that uses it. + std::unordered_map thread_col_x; + std::unordered_map lock_col_x; + if (!has_g_lane) { + std::vector lock_owner(n_locks, -1); + for (size_t tid = 0; tid < n_threads; ++tid) + for (auto& ev : per_thread[tid]) + if (auto* nd = dynamic_cast(ev.node)) { + size_t li = lock_idx.at(nd->var); + if (lock_owner[li] < 0) lock_owner[li] = (int)tid; + } else if (auto* nd = dynamic_cast(ev.node)) { + size_t li = lock_idx.at(nd->var); + if (lock_owner[li] < 0) lock_owner[li] = (int)tid; + } + + double col = 0.0; + std::vector placed(n_locks, false); + for (size_t tid = 0; tid < n_threads; ++tid) { + thread_col_x[tid] = col; col += SPACING; + for (size_t li = 0; li < n_locks; ++li) + if (!placed[li] && lock_owner[li] == (int)tid) { + lock_col_x[li] = col; col += SPACING; + placed[li] = true; + } + } + for (size_t li = 0; li < n_locks; ++li) + if (!placed[li]) { lock_col_x[li] = col; col += SPACING; } + } + auto thread_x = [&](size_t tid) -> double { if (has_g_lane) return tid < g_mid ? SPACING * tid : SPACING * (tid + 1); - return tid == 0 ? 0.0 : SPACING * (n_locks + tid); + return thread_col_x.at(tid); }; auto lock_x = [&](size_t li) -> double { - return SPACING * (li + 1); + return lock_col_x.count(li) ? lock_col_x.at(li) : SPACING * (li + 1); }; - const double g_x = has_g_lane ? SPACING * g_mid : SPACING * (n_locks + n_threads); - - std::unordered_map lock_idx; - for (size_t i = 0; i < n_locks; ++i) - lock_idx[lock_vars[i]] = i; + const double g_x = has_g_lane ? SPACING * g_mid : 0.0; double lane_bottom = -0.5; for (size_t tid = 0; tid < n_threads; ++tid) @@ -341,6 +456,65 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } } } + } else { + // Branching mode: push at Unlock/Spawn/End, pull at Lock/Start(spawned)/Join. + auto format_state = [&](size_t tid, + const std::map& state) -> std::string { + if (state.empty()) return ""; + std::string lbl = "$"; + bool first = true; + for (auto& [var, val] : state) { + if (!first) lbl += ",\\,"; + lbl += latex_escape(var) + "_{" + std::to_string(tid) + "}=" + + std::to_string(val); + first = false; + } + return lbl + "$"; + }; + // Pass A: push annotations. + // Lock resets the accumulator — writes between acquire and release are the + // section that gets staged to the lock at Unlock. + for (size_t tid = 0; tid < n_threads; ++tid) { + std::map pending; + for (auto& ev : per_thread[tid]) { + if (auto* wr = dynamic_cast(ev.node)) + pending[wr->var] = wr->value; + else if (dynamic_cast(ev.node)) + pending.clear(); + else if (dynamic_cast(ev.node) + || dynamic_cast(ev.node) + || dynamic_cast(ev.node)) { + std::string lbl = format_state(tid, pending); + if (!lbl.empty()) push_annotation[ev.node] = lbl; + pending.clear(); + } + } + } + // Pass B: pull annotations. + // Start of spawned thread ← inherits Spawn's push + // Join ← inherits joinee's End push + // Lock ← inherits the ordered_after Unlock's push + for (size_t tid = 0; tid < n_threads; ++tid) { + for (auto& ev : per_thread[tid]) { + if (auto* sp = dynamic_cast(ev.node)) { + auto it = push_annotation.find(ev.node); + if (it != push_annotation.end() && sp->spawned) + pull_annotation[sp->spawned.get()] = it->second; + } else if (auto* jn = dynamic_cast(ev.node)) { + if (jn->joinee) { + auto it = push_annotation.find(jn->joinee.get()); + if (it != push_annotation.end()) + pull_annotation[ev.node] = it->second; + } + } else if (auto* lk = dynamic_cast(ev.node)) { + if (lk->ordered_after) { + auto it = push_annotation.find(lk->ordered_after.get()); + if (it != push_annotation.end()) + pull_annotation[ev.node] = it->second; + } + } + } + } } // ── Phase 3: emit ───────────────────────────────────────────────────────── @@ -364,7 +538,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa // Named coordinates for each lock lane (used with |- notation) for (size_t li = 0; li < n_locks; ++li) { std::string suffix; - for (char c : lock_vars[li]) if (std::isalpha(c)) suffix += c; + for (char c : lock_vars[li]) if (std::isalnum(c)) suffix += c; if (suffix.empty()) suffix = "L" + std::to_string(li); f << "\\coordinate (lane" << suffix << ") at (" << fmt(lock_x(li)) << ", 0);\n"; } @@ -456,7 +630,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } for (size_t li = 0; li < n_locks; ++li) { double lx = lock_x(li); - f << "\\draw[shared lane] (" << fmt(lx) << ", 0.3) -- (" + f << "\\draw[shared lane, ->] (" << fmt(lx) << ", 0.3) -- (" << fmt(lx) << ", " << fmt(lane_bottom) << ");\n"; } if (has_g_lane) @@ -469,38 +643,44 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa for (size_t tid = 0; tid < n_threads; ++tid) { for (auto& ev : per_thread[tid]) { if (auto* nd = dynamic_cast(ev.node)) { - (void)nd; - // g: spawn pulls + pushes if (has_g_lane) + // linear: spawn pulls + pushes g f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; + else if (nd->tid < n_threads && !per_thread[nd->tid].empty()) + // branching: push to spawned thread's start + f << "\\draw[link oneway] (" << ev.name << ") -- (" + << per_thread[nd->tid].front().name << ");\n"; } else if (auto* nd = dynamic_cast(ev.node)) { - (void)nd; - // g: join pulls if (has_g_lane) + // linear: join pulls from g f << "\\draw[link oneway] (laneG |- " << ev.name << ") -- (" << ev.name << ");\n"; + else if (nd->tid < n_threads && !per_thread[nd->tid].empty()) + // branching: pull from joined thread's last node + f << "\\draw[link oneway] (" << per_thread[nd->tid].back().name + << ") -- (" << ev.name << ");\n"; } else if (auto* nd = dynamic_cast(ev.node)) { if (has_g_lane) { - // g: lock pulls + // linear: lock pulls from g f << "\\draw[link oneway] (laneG |- " << ev.name << ") -- (" << ev.name << ");\n"; - } else if (nd->ordered_after) { - // Lock lane: pull from per-variable lane + } else { + // branching: pull from lock lane std::string suffix; - for (char c : nd->var) if (std::isalpha(c)) suffix += c; + for (char c : nd->var) if (std::isalnum(c)) suffix += c; if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(nd->var)); f << "\\draw[link oneway] (lane" << suffix << " |- " << ev.name << ") -- (" << ev.name << ");\n"; } } else if (auto* nd = dynamic_cast(ev.node)) { if (has_g_lane) { - // g: unlock pulls + pushes + // linear: unlock pulls + pushes g f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; } else { - // Lock lane: PullPush to per-variable lane + // branching: push from thread to lock lane only std::string suffix; - for (char c : nd->var) if (std::isalpha(c)) suffix += c; + for (char c : nd->var) if (std::isalnum(c)) suffix += c; if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(nd->var)); - f << "\\PullPush{(" << ev.name << ")}{(lane" << suffix - << " |- " << ev.name << ")}\n"; + f << "\\draw[link oneway] (" << ev.name << ") -- (lane" << suffix + << " |- " << ev.name << ");\n"; } } else if (dynamic_cast(ev.node)) { // g: start pulls @@ -511,7 +691,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa if (has_g_lane) f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; } - // State annotations on g-lane arcs + // State annotations on sync arcs if (has_g_lane) { if (push_annotation.count(ev.node)) f << "\\node[sharedupdate, below=8pt] at ($(" << ev.name @@ -521,6 +701,38 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa f << "\\node[stateupdate, above=8pt] at ($(" << ev.name << ")!0.5!(laneG |- " << ev.name << ")$) {" << pull_annotation.at(ev.node) << "};\n"; + } else if (auto* an = dynamic_cast(ev.node)) { + // push annotation midway along the spawn→child arrow + if (push_annotation.count(ev.node) && an->tid < n_threads + && !per_thread[an->tid].empty()) + f << "\\node[sharedupdate, below=8pt] at ($(" << ev.name + << ")!0.5!(" << per_thread[an->tid].front().name << ")$) {" + << push_annotation.at(ev.node) << "};\n"; + } else if (auto* an = dynamic_cast(ev.node)) { + // pull annotation midway along the joinee-end→join arrow + if (pull_annotation.count(ev.node) && an->tid < n_threads + && !per_thread[an->tid].empty()) + f << "\\node[stateupdate, above=8pt] at ($(" << ev.name + << ")!0.5!(" << per_thread[an->tid].back().name << ")$) {" + << pull_annotation.at(ev.node) << "};\n"; + } else if (auto* an = dynamic_cast(ev.node)) { + if (pull_annotation.count(ev.node)) { + std::string suffix; + for (char c : an->var) if (std::isalnum(c)) suffix += c; + if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(an->var)); + f << "\\node[stateupdate, above=8pt] at ($(" << ev.name + << ")!0.5!(lane" << suffix << " |- " << ev.name << ")$) {" + << pull_annotation.at(ev.node) << "};\n"; + } + } else if (auto* an = dynamic_cast(ev.node)) { + if (push_annotation.count(ev.node)) { + std::string suffix; + for (char c : an->var) if (std::isalnum(c)) suffix += c; + if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(an->var)); + f << "\\node[sharedupdate, below=8pt] at ($(" << ev.name + << ")!0.5!(lane" << suffix << " |- " << ev.name << ")$) {" + << push_annotation.at(ev.node) << "};\n"; + } } } } @@ -546,7 +758,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa auto s1 = get_name(ce.src1); auto unl = get_name(ce.ordered_after); std::string suffix; - for (char c : ce.lock_var) if (std::isalpha(c)) suffix += c; + for (char c : ce.lock_var) if (std::isalnum(c)) suffix += c; if (suffix.empty()) suffix = "L" + std::to_string(lock_idx.at(ce.lock_var)); if (s1 && unl) f << "\\draw[conflict] (" << *s1 << ") -- (" << *unl From f05221b82736be7f10f08f8122244bedf1c094da Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Wed, 1 Jul 2026 13:06:05 +0200 Subject: [PATCH 08/14] better communication messages --- src/tikz.cc | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/src/tikz.cc b/src/tikz.cc index f44fc7e..306cba7 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -422,13 +422,17 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa return lbl + "$"; }; - // Pass A: push annotations — writes accumulated between End/Spawn sync points + // Pass A: push annotations — writes accumulated between sync points. + // Lock resets the accumulator; Unlock, Spawn, and End emit the push. for (size_t tid = 0; tid < n_threads; ++tid) { std::map pending; for (auto& ev : per_thread[tid]) { if (auto* wr = dynamic_cast(ev.node)) { pending[wr->var] = wr->value; - } else if (dynamic_cast(ev.node) + } else if (dynamic_cast(ev.node)) { + pending.clear(); + } else if (dynamic_cast(ev.node) + || dynamic_cast(ev.node) || dynamic_cast(ev.node)) { std::string lbl = format_state(tid, pending); if (!lbl.empty()) @@ -438,9 +442,10 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } } - // Pass B: pull annotations — derived from the corresponding push + // Pass B: pull annotations — derived from the corresponding push. // Start of spawned thread ← inherits Spawn's push state // Join ← inherits joinee's End push state + // Lock ← inherits the ordered_after Unlock's push state for (size_t tid = 0; tid < n_threads; ++tid) { for (auto& ev : per_thread[tid]) { if (auto* sp = dynamic_cast(ev.node)) { @@ -448,8 +453,21 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa if (it != push_annotation.end() && sp->spawned) pull_annotation[sp->spawned.get()] = it->second; } else if (auto* jn = dynamic_cast(ev.node)) { - if (jn->joinee) { - auto it = push_annotation.find(jn->joinee.get()); + // In linear mode, pushes happen at Unlock, so End may be empty. + // Scan the joinee's thread for the last push annotation. + if (jn->tid < per_thread.size()) { + const std::string* last_push = nullptr; + for (auto& jev : per_thread[jn->tid]) { + auto it = push_annotation.find(jev.node); + if (it != push_annotation.end()) + last_push = &it->second; + } + if (last_push) + pull_annotation[ev.node] = *last_push; + } + } else if (auto* lk = dynamic_cast(ev.node)) { + if (lk->ordered_after) { + auto it = push_annotation.find(lk->ordered_after.get()); if (it != push_annotation.end()) pull_annotation[ev.node] = it->second; } From 02efab2695eb42e6164227dcc75413a9a8fde7f2 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Wed, 1 Jul 2026 13:12:37 +0200 Subject: [PATCH 09/14] failing pullpush don't do show the push part on the diagram --- src/tikz.cc | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/tikz.cc b/src/tikz.cc index 306cba7..1602f13 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -690,8 +690,12 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } } else if (auto* nd = dynamic_cast(ev.node)) { if (has_g_lane) { - // linear: unlock pulls + pushes g - f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; + if (ev.is_conflict) + // conflicting unlock: push failed, g notifies thread of conflict + f << "\\draw[link oneway] (laneG |- " << ev.name << ") -- (" << ev.name << ");\n"; + else + // successful unlock: pull + push + f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; } else { // branching: push from thread to lock lane only std::string suffix; From ecf112aef4f98f3087042f1cfa799c177fbf950e Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Wed, 1 Jul 2026 14:03:00 +0200 Subject: [PATCH 10/14] some fixups to alignment --- src/branching/eager/version_store.cc | 4 +- src/branching/lazy/version_store.cc | 4 +- src/interpreter.cc | 16 +++++++ src/tikz.cc | 63 ++++++++++++++++++++++++++-- 4 files changed, 81 insertions(+), 6 deletions(-) diff --git a/src/branching/eager/version_store.cc b/src/branching/eager/version_store.cc index c638461..11b107f 100644 --- a/src/branching/eager/version_store.cc +++ b/src/branching/eager/version_store.cc @@ -157,7 +157,9 @@ std::optional EagerLocalVersionStore::merge_with_commit(const std::sha conflict = Conflict( obj, {commit_a->id, get_loc(commit_a, obj)}, - {it->second->id, get_loc(it->second, obj)}); + {it->second->id, get_loc(it->second, obj)}, + commit_a->changes.at(obj).source_event, + it->second->changes.at(obj).source_event); break; } } diff --git a/src/branching/lazy/version_store.cc b/src/branching/lazy/version_store.cc index a65a1e5..df300f6 100644 --- a/src/branching/lazy/version_store.cc +++ b/src/branching/lazy/version_store.cc @@ -140,7 +140,9 @@ BranchingReadResult LazyLocalVersionStore::get_committed(std::string var) const auto result = BranchingReadResult(Conflict( var, {a, get_loc(writers[0]->changes.at(var))}, - {b, get_loc(writers[1]->changes.at(var))})); + {b, get_loc(writers[1]->changes.at(var))}, + writers[0]->changes.at(var).source_event, + writers[1]->changes.at(var).source_event)); read_cache[var] = result; return result; } diff --git a/src/interpreter.cc b/src/interpreter.cc index db0f358..d3c5184 100644 --- a/src/interpreter.cc +++ b/src/interpreter.cc @@ -650,6 +650,9 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { // Track conflicting unlock nodes whose g_predecessor must be resolved after all threads. std::vector, std::shared_ptr>> unlocks_g_predecessor_fixups; + // Track unlock conflict source fixups: (unlock node, conflict base carrying source events) + std::vector, std::shared_ptr>> unlock_conflict_fixups; + // Map from trace events to graph nodes std::unordered_map, std::shared_ptr> event_to_node; @@ -764,6 +767,9 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { if (arg.g_predecessor) { unlocks_g_predecessor_fixups.push_back({node, arg.g_predecessor}); } + if (arg.maybe_conflict) { + unlock_conflict_fixups.push_back({node, arg.maybe_conflict}); + } last_unlock_per_lock[arg.lock_name] = node; link_in_program_order(tid, node); event_to_node[event] = node; @@ -824,6 +830,16 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { const_cast(*join_node->conflict).sources = {src_a, src_b}; } + // Fix up unlock conflict sources using the source events now that event_to_node is complete + for (auto& [unlock_node, cb] : unlock_conflict_fixups) { + auto [evt_a, evt_b] = cb->source_events(); + std::shared_ptr src_a, src_b; + if (evt_a && event_to_node.count(evt_a)) src_a = event_to_node.at(evt_a); + if (evt_b && event_to_node.count(evt_b)) src_b = event_to_node.at(evt_b); + if (src_a || src_b) + const_cast(*unlock_node->conflict).sources = {src_a, src_b}; + } + // Fix up read nodes to point to their source write events for (auto& [read_node, source_event] : reads_to_fix) { assert(event_to_node.contains(source_event) && "source missing in event_to_node map"); diff --git a/src/tikz.cc b/src/tikz.cc index 1602f13..9dce5fb 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -149,7 +149,7 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa bool linear_mode) { const double Y_STEP = -0.8; // gap between regular events const double Y_SYNC_STEP = -1.2; // gap when either neighbour is a sync event - const double Y_SPAWN_OFFSET = -0.4; // child thread starts this far below its spawn + const double Y_SPAWN_OFFSET = 0.0; // child thread starts at same y as its spawn const double Y_JOIN_GAP = 0.3; // min gap between joinee's end and join event const double Y_LOCK_GAP = 0.4; // min gap between ordered_after unlock and lock const double SPACING = 1.8; @@ -245,6 +245,12 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa add_lock_var(nd->var); if (nd->conflict) { ev.is_conflict = true; + conflicts.push_back({ + nd->conflict->sources.first.get(), + nd->conflict->sources.second.get(), + nd->g_predecessor.get(), + n, "" + }); } } else if (auto* nd = dynamic_cast(n)) { ev.label = "assert(" + latex_escape(nd->cond) + ")"; @@ -345,6 +351,22 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa } } + // Post-pass 3: pull joinee's down to the join's y so that the + // join arrow is perfectly horizontal, matching the spawn↔start alignment. + for (size_t tid = 0; tid < n_threads; ++tid) { + for (auto& ev : per_thread[tid]) { + if (auto* jn = dynamic_cast(ev.node)) { + if (jn->tid < n_threads && !per_thread[jn->tid].empty()) { + auto& end_ev = per_thread[jn->tid].back(); + if (dynamic_cast(end_ev.node)) { + end_ev.y = ev.y; + node_y[end_ev.node] = ev.y; + } + } + } + } + } + // ── Phase 2: layout ─────────────────────────────────────────────────────── const bool has_g_lane = linear_mode; const size_t n_locks = has_g_lane ? 0 : lock_vars.size(); @@ -787,6 +809,34 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa << ") -- (lane" << suffix << " |- " << *unl << ") -- (lane" << suffix << " |- " << *cn << ") -- (" << *cn << ");\n"; + } else if (has_g_lane && ce.lock_var.empty() && ce.ordered_after + && (ce.src1 || ce.src2)) { + // G-lane routing for unlock conflicts: each source routes based on thread. + // Cross-thread: src → g_predecessor → g_lane → conflict. + // Same-thread: src → conflict (direct). + auto pred = get_name(ce.ordered_after); + auto conflict_tid_it = node_tid.find(ce.conflict_node); + size_t conflict_tid = (conflict_tid_it != node_tid.end()) + ? conflict_tid_it->second : SIZE_MAX; + auto emit_unlock_src = [&](const Node* src) { + auto s = get_name(src); + if (!s) return; + auto src_tid_it = node_tid.find(src); + size_t src_tid = (src_tid_it != node_tid.end()) + ? src_tid_it->second : SIZE_MAX; + if (src_tid != conflict_tid && pred) { + const char* arc = (thread_x(src_tid) < g_x) + ? "looseness=.5, out=320, in=210" + : "looseness=.5, out=220, in=330"; + f << "\\draw[conflict] (" << *s << ") -- (" << *pred + << ") to[" << arc << "] (laneG |- " << *pred + << ") -- (laneG |- " << *cn << ") -- (" << *cn << ");\n"; + } else { + f << "\\draw[conflict] (" << *s << ") -- (" << *cn << ");\n"; + } + }; + if (ce.src1) emit_unlock_src(ce.src1); + if (ce.src2) emit_unlock_src(ce.src2); } else if (ce.src1 || ce.src2) { // Emit one conflict path per source. // Same-thread source → direct line along the thread lane. @@ -804,9 +854,8 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa ? src_tid_it->second : SIZE_MAX; if (has_g_lane && src_tid != conflict_tid) { - // Cross-thread: src → End of src thread → (arc) → g → conflict + // Cross-thread (linear): src → End → arc → g lane → conflict const std::string& end_name = per_thread[src_tid].back().name; - // Match the PullPush push-arc direction (event left of g → out=320,in=210) const char* push_arc = (thread_x(src_tid) < g_x) ? "looseness=.5, out=320, in=210" : "looseness=.5, out=220, in=330"; @@ -814,8 +863,14 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa << ") to[" << push_arc << "] (laneG |- " << end_name << ") -- (laneG |- " << *cn << ") -- (" << *cn << ");\n"; + } else if (!has_g_lane && src_tid != conflict_tid + && src_tid < per_thread.size()) { + // Cross-thread (branching): src → End of src thread → conflict + const std::string& end_name = per_thread[src_tid].back().name; + f << "\\draw[conflict] (" << *s << ") -- (" << end_name + << ") -- (" << *cn << ");\n"; } else { - // Same thread (or no g lane): direct line + // Same thread: direct line f << "\\draw[conflict] (" << *s << ") -- (" << *cn << ");\n"; } }; From ff6aa51647fc306ce748141ad0e4e455668f7e95 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Thu, 2 Jul 2026 09:55:43 +0200 Subject: [PATCH 11/14] remove some doublearrows artifacts --- src/tikz.cc | 24 +++++++++--------------- 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/src/tikz.cc b/src/tikz.cc index 9dce5fb..2f62e9a 100644 --- a/src/tikz.cc +++ b/src/tikz.cc @@ -91,19 +91,15 @@ static const char* FORMATTER = R"( \newcommand{\ThreadSyncEventFrom}[5]{% \fill ($(##2)+(0,##3)$) circle (0pt) coordinate (##4) node[##1 code] {##5};} \newcommand{\PullPush}[2]{ - \ifdoublearrows - \path let \p1 = ##1, \p2 = ##2 in \pgfextra{% - \ifdim\x1<\x2 - \draw[link oneway] ##2 to[looseness=.5, out=140, in=30] ##1; - \draw[link oneway] ##1 to[looseness=.5, out=320, in=210] ##2; - \else - \draw[link oneway] ##2 to[looseness=.5, out=40, in=150] ##1; - \draw[link oneway] ##1 to[looseness=.5, out=220, in=330] ##2; - \fi - }; - \else - \draw[link both] ##1 -- ##2; - \fi + \path let \p1 = ##1, \p2 = ##2 in \pgfextra{% + \ifdim\x1<\x2 + \draw[link oneway] ##2 to[looseness=.5, out=140, in=30] ##1; + \draw[link oneway] ##1 to[looseness=.5, out=320, in=210] ##2; + \else + \draw[link oneway] ##2 to[looseness=.5, out=40, in=150] ##1; + \draw[link oneway] ##1 to[looseness=.5, out=220, in=330] ##2; + \fi + }; } \newcommand{\ConflictEvent}[2]{ \node[regular polygon, regular polygon sides=8, @@ -567,8 +563,6 @@ void TikzPrinter::print(const ExecutionGraph& g, const std::filesystem::path& pa << "\\usetikzlibrary{automata,shapes,decorations,arrows,calc," "arrows.meta,fit,positioning,quotes,tikzmark,shadows}\n" << "\n" - << "\\newif\\ifdoublearrows\n" - << "\\doublearrowstrue\n" << FORMATTER << "\n\\begin{document}\n" << "\\begin{tikzpicture}[common timeline styles]\n" From 56a52afad7cea76e0b04c67d419669eb8a27ba3a Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 21 Jul 2026 16:01:11 +0200 Subject: [PATCH 12/14] update gitignore --- .gitignore | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.gitignore b/.gitignore index 7e36968..6cc90b9 100644 --- a/.gitignore +++ b/.gitignore @@ -31,3 +31,7 @@ *.out *.app build + +*.DS_Store +*.vscode +*.dot From eb386141c37ff07c1911cd7f520a7dc2d5fe93f0 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Wed, 22 Jul 2026 15:41:56 +0200 Subject: [PATCH 13/14] Adding support for volatiles: parsing, interpreter, tests, grpahs --- .../accept/semantics/branching/volatile.gm | 2 + .../semantics/branching/volatile_sync.gm | 5 + .../volatile_sync_conflict_two_vars.gm | 7 ++ examples/accept/semantics/linear/volatile.gm | 2 + .../accept/semantics/linear/volatile_sync.gm | 5 + .../linear/volatile_sync_communicate.gm | 5 + .../volatile_sync_communicate_volatile.gm | 5 + .../branching/volatile_sync_conflict.gm | 12 ++ .../volatile_sync_communicate_volatile.gm | 5 + .../linear/volatile_sync_conflict.gm | 7 ++ .../linear/volatile_sync_conflict_two_vars.gm | 7 ++ src/branching/base_memory_model.cc | 51 ++++++++ src/branching/base_memory_model.hh | 11 ++ src/branching/base_version_store.hh | 19 +++ src/execution_state.cc | 29 ++++- src/execution_state.hh | 14 +++ src/graph.hh | 29 +++++ src/graphviz.cc | 36 ++++++ src/graphviz.hh | 2 + src/interpreter.cc | 111 +++++++++++++++++- src/lang.hh | 5 +- src/linear/memory_model.cc | 63 +++++++--- src/linear/memory_model.hh | 16 ++- src/memory_model.hh | 21 +++- src/parser.cc | 1 + src/passes/expressions.cc | 4 +- src/passes/statements.cc | 6 +- src/sync_state.hh | 11 ++ src/thread_trace.hh | 45 +++++++ test_gitmem.py | 41 ++++++- 30 files changed, 547 insertions(+), 30 deletions(-) create mode 100644 examples/accept/semantics/branching/volatile.gm create mode 100644 examples/accept/semantics/branching/volatile_sync.gm create mode 100644 examples/accept/semantics/branching/volatile_sync_conflict_two_vars.gm create mode 100644 examples/accept/semantics/linear/volatile.gm create mode 100644 examples/accept/semantics/linear/volatile_sync.gm create mode 100644 examples/accept/semantics/linear/volatile_sync_communicate.gm create mode 100644 examples/reject/semantics/branching/volatile_sync_communicate_volatile.gm create mode 100644 examples/reject/semantics/branching/volatile_sync_conflict.gm create mode 100644 examples/reject/semantics/linear/volatile_sync_communicate_volatile.gm create mode 100644 examples/reject/semantics/linear/volatile_sync_conflict.gm create mode 100644 examples/reject/semantics/linear/volatile_sync_conflict_two_vars.gm diff --git a/examples/accept/semantics/branching/volatile.gm b/examples/accept/semantics/branching/volatile.gm new file mode 100644 index 0000000..1e0e9dc --- /dev/null +++ b/examples/accept/semantics/branching/volatile.gm @@ -0,0 +1,2 @@ +@v1 = 1; +assert(@v1 == 1); \ No newline at end of file diff --git a/examples/accept/semantics/branching/volatile_sync.gm b/examples/accept/semantics/branching/volatile_sync.gm new file mode 100644 index 0000000..279aaa1 --- /dev/null +++ b/examples/accept/semantics/branching/volatile_sync.gm @@ -0,0 +1,5 @@ +@v = 2; +$t = spawn { + assert(@v == 2); +}; +assert(@v == 2); \ No newline at end of file diff --git a/examples/accept/semantics/branching/volatile_sync_conflict_two_vars.gm b/examples/accept/semantics/branching/volatile_sync_conflict_two_vars.gm new file mode 100644 index 0000000..177ec2b --- /dev/null +++ b/examples/accept/semantics/branching/volatile_sync_conflict_two_vars.gm @@ -0,0 +1,7 @@ + +$t = spawn { + x = 1; + @v1 = 1; +}; +x = 2; +@v2 = 2; \ No newline at end of file diff --git a/examples/accept/semantics/linear/volatile.gm b/examples/accept/semantics/linear/volatile.gm new file mode 100644 index 0000000..1e0e9dc --- /dev/null +++ b/examples/accept/semantics/linear/volatile.gm @@ -0,0 +1,2 @@ +@v1 = 1; +assert(@v1 == 1); \ No newline at end of file diff --git a/examples/accept/semantics/linear/volatile_sync.gm b/examples/accept/semantics/linear/volatile_sync.gm new file mode 100644 index 0000000..279aaa1 --- /dev/null +++ b/examples/accept/semantics/linear/volatile_sync.gm @@ -0,0 +1,5 @@ +@v = 2; +$t = spawn { + assert(@v == 2); +}; +assert(@v == 2); \ No newline at end of file diff --git a/examples/accept/semantics/linear/volatile_sync_communicate.gm b/examples/accept/semantics/linear/volatile_sync_communicate.gm new file mode 100644 index 0000000..279aaa1 --- /dev/null +++ b/examples/accept/semantics/linear/volatile_sync_communicate.gm @@ -0,0 +1,5 @@ +@v = 2; +$t = spawn { + assert(@v == 2); +}; +assert(@v == 2); \ No newline at end of file diff --git a/examples/reject/semantics/branching/volatile_sync_communicate_volatile.gm b/examples/reject/semantics/branching/volatile_sync_communicate_volatile.gm new file mode 100644 index 0000000..18902c2 --- /dev/null +++ b/examples/reject/semantics/branching/volatile_sync_communicate_volatile.gm @@ -0,0 +1,5 @@ +@v = 2; +$t = spawn { + @v = 41; +}; +assert(@v == 2); \ No newline at end of file diff --git a/examples/reject/semantics/branching/volatile_sync_conflict.gm b/examples/reject/semantics/branching/volatile_sync_conflict.gm new file mode 100644 index 0000000..90f9bb7 --- /dev/null +++ b/examples/reject/semantics/branching/volatile_sync_conflict.gm @@ -0,0 +1,12 @@ +// The two volatile writes are releases with no intervening acquire, so they +// establish no happens-before between the x writes: x races. Eager/linear catch +// this at the write; lazy only reports conflicts on variables that are read, and +// x is never read, so lazy accepts it. +// expect branching-lazy: accept + +$t = spawn { + x = 1; + @v = 1; +}; +x = 2; +@v = 2; \ No newline at end of file diff --git a/examples/reject/semantics/linear/volatile_sync_communicate_volatile.gm b/examples/reject/semantics/linear/volatile_sync_communicate_volatile.gm new file mode 100644 index 0000000..b3ae416 --- /dev/null +++ b/examples/reject/semantics/linear/volatile_sync_communicate_volatile.gm @@ -0,0 +1,5 @@ +@v = 2; +$t = spawn { + @v = 41; +}; +assert(@v == 2); diff --git a/examples/reject/semantics/linear/volatile_sync_conflict.gm b/examples/reject/semantics/linear/volatile_sync_conflict.gm new file mode 100644 index 0000000..714cd3e --- /dev/null +++ b/examples/reject/semantics/linear/volatile_sync_conflict.gm @@ -0,0 +1,7 @@ + +$t = spawn { + x = 1; + @v = 1; +}; +x = 2; +@v = 2; \ No newline at end of file diff --git a/examples/reject/semantics/linear/volatile_sync_conflict_two_vars.gm b/examples/reject/semantics/linear/volatile_sync_conflict_two_vars.gm new file mode 100644 index 0000000..177ec2b --- /dev/null +++ b/examples/reject/semantics/linear/volatile_sync_conflict_two_vars.gm @@ -0,0 +1,7 @@ + +$t = spawn { + x = 1; + @v1 = 1; +}; +x = 2; +@v2 = 2; \ No newline at end of file diff --git a/src/branching/base_memory_model.cc b/src/branching/base_memory_model.cc index 68f56a8..389cbbb 100644 --- a/src/branching/base_memory_model.cc +++ b/src/branching/base_memory_model.cc @@ -1,5 +1,6 @@ #include "base_memory_model.hh" #include "overloaded.hh" +#include #include "branching/eager/memory_model.hh" #include "branching/lazy/memory_model.hh" @@ -120,6 +121,54 @@ BranchingMemoryModelBase::on_unlock(ThreadContext &thread, Lock &lock) { return std::nullopt; } +VolatileState& get_store(Volatile& v) { + return static_cast(*v.sync); +} + +std::optional> +BranchingMemoryModelBase::on_volatile_read(ThreadContext &thread, Volatile &v) { + auto& store = get_store(thread); + store.commit_staging(); + + // Acquire: merge the current release so we observe it and everything that + // happened-before it. May conflict on piggybacked non-volatile state. + VolatileState& vstate = get_store(v); + if (vstate.commit != nullptr) { + if (std::optional conflict = store.merge_with_commit(vstate.commit)) { + return std::make_shared(*conflict); + } + } + + // The value (with its writer as provenance) lives on the Volatile object and + // is read there by the interpreter -- @v is not versioned. + return std::nullopt; +} + +std::optional> +BranchingMemoryModelBase::on_volatile_write(ThreadContext &thread, Volatile &v, + ValueWithSource value) { + auto& store = get_store(thread); + store.commit_staging(); + + // Release: absorb the previous release first (so the ordinary state is a + // linear chain, never diverging on @v); this merge may still conflict on + // piggybacked non-volatile state. + VolatileState& vstate = get_store(v); + if (vstate.commit != nullptr) { + if (std::optional conflict = store.merge_with_commit(vstate.commit)) { + return std::make_shared(*conflict); + } + } + + // The thread's current head is the release point a later acquire merges. The + // volatile's value lives on the object, not in a commit -- @v is not + // versioned; `value` carries the write event as provenance for reads. + vstate.commit = store.get_head(); + v.value = value; + + return std::nullopt; +} + std::string BranchingMemoryModelBase::build_revision_graph_dot( const std::vector& thread_states) const { @@ -142,6 +191,8 @@ bool BranchingMemoryModelBase::is_scheduling_point(SyncOperation op) const { case SyncOperation::Lock: case SyncOperation::Unlock: case SyncOperation::Join: + case SyncOperation::VolatileRead: + case SyncOperation::VolatileWrite: return true; case SyncOperation::Spawn: case SyncOperation::Start: diff --git a/src/branching/base_memory_model.hh b/src/branching/base_memory_model.hh index abbdc12..694ac23 100644 --- a/src/branching/base_memory_model.hh +++ b/src/branching/base_memory_model.hh @@ -42,6 +42,13 @@ public: std::optional> on_unlock(ThreadContext &thread, Lock &lock) override; + std::optional> + on_volatile_read(ThreadContext &thread, Volatile &v) override; + + std::optional> + on_volatile_write(ThreadContext &thread, Volatile &v, + ValueWithSource value) override; + std::ostream &print(std::ostream &os) const override; std::string build_revision_graph_dot(const std::vector& thread_states) const override; @@ -51,6 +58,10 @@ public: std::unique_ptr make_lock_state() const override { return std::make_unique(); } + + std::unique_ptr make_volatile_state() const override { + return std::make_unique(); + } }; } // end branching diff --git a/src/branching/base_version_store.hh b/src/branching/base_version_store.hh index 2123f18..d1afddb 100644 --- a/src/branching/base_version_store.hh +++ b/src/branching/base_version_store.hh @@ -132,6 +132,25 @@ public: } }; +// The current released commit of a volatile location -- what each acquire +// (read) synchronises with, and what each new release (write) chains onto. +class VolatileState : public VolatileSyncState { +public: + ~VolatileState() = default; + + std::shared_ptr commit; + + inline std::ostream &print(std::ostream &os) const override { + os << "VolatileState{commit="; + if (commit) + os << commit->id; + else + os << "empty"; + os << "}"; + return os; + } +}; + } // namespace branching } // namespace gitmem \ No newline at end of file diff --git a/src/execution_state.cc b/src/execution_state.cc index eb6317a..6750727 100644 --- a/src/execution_state.cc +++ b/src/execution_state.cc @@ -54,9 +54,26 @@ Lock& GlobalContext::get_lock(std::string lock) { return new_it->second; } +Volatile& GlobalContext::get_volatile(std::string name) { + auto it = volatiles.find(name); + if (it != volatiles.end()) + return it->second; + + auto [new_it, inserted] = volatiles.emplace( + name, + Volatile{ + .name = name, + .sync = model->make_volatile_state() + } + ); + + return new_it->second; +} + bool GlobalContext::operator==(const GlobalContext &other) const { if (threads.size() != other.threads.size() || - locks.size() != other.locks.size()) + locks.size() != other.locks.size() || + volatiles.size() != other.volatiles.size()) return false; // Threads may have been spawned in a different order, so we @@ -76,6 +93,16 @@ bool GlobalContext::operator==(const GlobalContext &other) const { if (lock.owner != other_lock.owner) return false; } + + // A volatile carries an observable value (unlike a lock), so compare it: two + // states differing only in an as-yet-unread volatile must stay distinct, or + // exploration could prune a branch that later diverges on the read. + for (auto &[name, vol] : volatiles) { + if (!other.volatiles.contains(name)) + return false; + if (vol.value != other.volatiles.at(name).value) + return false; + } return true; } diff --git a/src/execution_state.hh b/src/execution_state.hh index 1572ef4..54b2b21 100644 --- a/src/execution_state.hh +++ b/src/execution_state.hh @@ -64,13 +64,27 @@ struct Lock { std::unique_ptr sync; }; +// A volatile variable is a synchronising object like a lock: an acquire (read) +// synchronises-with the previous release (write). Its value lives here on the +// object (not in the versioned store) -- volatiles are race-free, so their +// value is not versioned heap, the same way lock state is not versioned. The +// synchronisation of *ordinary* memory still flows through the model; per-model +// bookkeeping (e.g. the branching release commit) lives in `sync`. +struct Volatile { + std::string name; + std::optional value = std::nullopt; + std::unique_ptr sync; +}; + struct GlobalContext { // Execution state std::deque threads; private: std::unordered_map locks; + std::unordered_map volatiles; public: Lock& get_lock(std::string); + Volatile& get_volatile(std::string); // Most recent unlock event across ALL lock variables (used by the linear // memory model so that lock(l2) gets an ordered_after edge to the last diff --git a/src/graph.hh b/src/graph.hh index 6b64cfb..c4dbf61 100644 --- a/src/graph.hh +++ b/src/graph.hh @@ -21,6 +21,8 @@ struct Start; struct End; struct Write; struct Read; +struct VolatileWrite; +struct VolatileRead; struct Spawn; struct Join; struct Lock; @@ -45,6 +47,8 @@ struct Visitor { virtual void visitEnd(const End *) = 0; virtual void visitWrite(const Write *) = 0; virtual void visitRead(const Read *) = 0; + virtual void visitVolatileWrite(const VolatileWrite *) = 0; + virtual void visitVolatileRead(const VolatileRead *) = 0; virtual void visitSpawn(const Spawn *) = 0; virtual void visitJoin(const Join *) = 0; virtual void visitLock(const Lock *) = 0; @@ -108,6 +112,31 @@ struct Read : Node { void accept(Visitor *v) const override { v->visitRead(this); } }; +// A volatile write is an ordinary write plus the write->write synchronisation +// order: `sync_predecessor` is the prior volatile write (release) this one +// chains onto (null for the first write to the volatile). +struct VolatileWrite : Write { + std::shared_ptr sync_predecessor = nullptr; + + VolatileWrite(const std::string var, const size_t value, const size_t id) + : Write(var, value, id) {} + + void accept(Visitor *v) const override { v->visitVolatileWrite(this); } +}; + +// A volatile read is an ordinary read whose edge to the source write is a +// synchronisation (acquire) edge rather than a plain reads-from edge. +struct VolatileRead : Read { + VolatileRead(const std::string var, const size_t value, const size_t id, + const std::shared_ptr source) + : Read(var, value, id, source) {} + + VolatileRead(const std::string var, const size_t id, Conflict conflict) + : Read(var, id, std::move(conflict)) {} + + void accept(Visitor *v) const override { v->visitVolatileRead(this); } +}; + struct Spawn : Node { const size_t tid; const std::shared_ptr spawned; diff --git a/src/graphviz.cc b/src/graphviz.cc index 36370fa..3566d31 100644 --- a/src/graphviz.cc +++ b/src/graphviz.cc @@ -137,6 +137,42 @@ void GraphvizPrinter::visitRead(const Read *n) { } } +void GraphvizPrinter::visitVolatileWrite(const VolatileWrite *n) { + emitNode(n, "W" + n->var + " = " + to_string(n->value)); + emitProgramOrderEdge(n, n->next.get()); + visitProgramOrder(n->next.get()); + // write->write synchronisation order (release chain). + if (n->sync_predecessor) + emitSyncEdge(n->sync_predecessor.get(), n); +} + +void GraphvizPrinter::visitVolatileRead(const VolatileRead *n) { + std::string label = "R" + n->var + " = "; + + std::visit(overloaded{ + [&](const Read::SuccessfulRead& success) { + label += to_string(success.value); + }, + [&](const Conflict& conflict) { + label += "conflict"; + } + }, n->read_result); + + emitNode(n, label); + emitProgramOrderEdge(n, n->next.get()); + visitProgramOrder(n->next.get()); + + if (auto* conflict = std::get_if(&n->read_result)) { + emitConflict(n, *conflict); + } else { + auto& success = std::get(n->read_result); + // write->read is an acquire: a synchronisation edge, not a reads-from edge. + if (success.source) { + emitSyncEdge(success.source.get(), n); + } + } +} + void GraphvizPrinter::visitSpawn(const Spawn *n) { emitNode(n, "Spawn " + std::to_string(n->tid)); emitProgramOrderEdge(n, n->next.get()); diff --git a/src/graphviz.hh b/src/graphviz.hh index c3e294b..016a79e 100644 --- a/src/graphviz.hh +++ b/src/graphviz.hh @@ -8,6 +8,8 @@ struct GraphvizPrinter : Visitor { void visitEnd(const End *) override; void visitWrite(const Write *) override; void visitRead(const Read *) override; + void visitVolatileWrite(const VolatileWrite *) override; + void visitVolatileRead(const VolatileRead *) override; void visitSpawn(const Spawn *) override; void visitJoin(const Join *) override; void visitLock(const Lock *) override; diff --git a/src/interpreter.cc b/src/interpreter.cc index d3c5184..491b13b 100644 --- a/src/interpreter.cc +++ b/src/interpreter.cc @@ -27,6 +27,19 @@ using namespace trieste; * - t unlocking a lock l, which updates l to have t's versioned memory */ +// Does this subtree evaluate a volatile read? A volatile read (a Volatile node +// in read position) can appear anywhere in an evaluated expression -- an +// assignment RHS, an if/assert condition, inside arithmetic or a comparison. +// We do not descend into a Spawn body: those statements run in the child thread +// later, not as part of this statement. +static bool evaluates_volatile_read(Node n) { + if (n == lang::Spawn) return false; + if (n == lang::Volatile) return true; + for (const auto& child : *n) + if (evaluates_volatile_read(child)) return true; + return false; +} + // Map AST node types to sync operations static std::optional get_sync_operation(Node stmt) { auto s = stmt / lang::Stmt; @@ -37,10 +50,20 @@ static std::optional get_sync_operation(Node stmt) { // Spawn is an expression, not a statement, but we check for assignment of spawn if (s == lang::Assign) { // A little gross but okay for now - auto rhs = s / lang::Expr / lang::Expr; - if (rhs == lang::Spawn) return SyncOperation::Spawn; + + // `@v = ...` writes a volatile (the LVal is a Volatile). + if ((s / lang::LVal) == lang::Volatile) return SyncOperation::VolatileWrite; + + // `... = spawn { ... }` spawns a thread. + if ((s / lang::Expr / lang::Expr) == lang::Spawn) return SyncOperation::Spawn; } + // A volatile read is an acquire wherever it is evaluated, not just as a bare + // `r = @v`. Statements execute atomically here, so the scheduling point is the + // statement boundary regardless of where in the expression the read sits -- + // "when the read happens" collapses to "this statement does a read". + if (evaluates_volatile_read(s)) return SyncOperation::VolatileRead; + return std::nullopt; } @@ -126,6 +149,28 @@ Interpreter::evaluate_expression(trieste::Node expr, Thread& thread) { } else { return termination::UnassignedRead(var); } + } else if (e == lang::Volatile) { + auto var = std::string(expr->location().view()); + + // A volatile read is an acquire: synchronize (the model merges/pulls the + // writer's ordinary state, and may race on that piggybacked non-volatile + // state, exactly like a lock). The volatile's own value lives on the + // object, so we read it directly rather than from the versioned store. + Volatile& vol = gctx.get_volatile(var); + if (auto conflict = gctx.model->on_volatile_read(ctx, vol)) { + verbose::out << (**conflict) << std::endl; + thread.trace.on_volatile_read(var, *conflict); + return termination::DataRace(*conflict); + } + + if (!vol.value) + // invalid: reading a volatile that hasn't been written + return termination::UnassignedRead(var); + + // vol.value->source_event is the writer we synchronized with + thread.trace.on_volatile_read(var, *vol.value); + return vol.value->value; + } else if (e == lang::Var) { auto var = std::string(expr->location().view()); @@ -239,12 +284,38 @@ std::variant Interpreter::run_statement(Node stmt, Threa << std::endl; ctx.locals[var] = *val; + } else if (lhs == lang::Volatile) { + + auto [line, col] = stmt->location().linecol(); + FileLocation loc{stmt->location().source->origin(), line + 1, col + 1}; + + Volatile& vol = gctx.get_volatile(var); + + // The prior volatile write (current release) this one chains onto, for + // the write->write sync edge. Captured before the model overwrites it. + std::shared_ptr sync_pred = + vol.value ? vol.value->source_event : nullptr; + + // The write event is the value's provenance -- a later volatile read + // follows it as the acquire->release edge -- so it must exist before + // the model stages. The release may still race (on non-volatile + // state), in which case we annotate the event we already recorded. + auto write_event = + thread.trace.on_volatile_write(var, *val, std::move(loc), sync_pred); + + if (auto conflict = gctx.model->on_volatile_write(ctx, vol, ValueWithSource{*val, write_event})) { + verbose::out << (**conflict) << std::endl; + thread.trace.on_volatile_write_conflict(write_event, *conflict); + return termination::DataRace(*conflict); + } + } else if (lhs == lang::Var) { auto [line, col] = stmt->location().linecol(); FileLocation loc{stmt->location().source->origin(), line + 1, col + 1}; auto write_event = thread.trace.on_write(var, *val, std::move(loc)); gctx.model->write(ctx, var, ValueWithSource{*val, write_event}); + } else { throw std::runtime_error("Bad left-hand side: " + std::string(lhs->type().str())); @@ -647,6 +718,10 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { // are processed (the predecessor may come from another thread's trace). std::vector, std::shared_ptr>> locks_ordered_after_fixups; + // Track volatile write nodes whose sync_predecessor (the prior volatile + // write) must be resolved after all threads -- it may be another thread's. + std::vector, std::shared_ptr>> volatile_write_sync_fixups; + // Track conflicting unlock nodes whose g_predecessor must be resolved after all threads. std::vector, std::shared_ptr>> unlocks_g_predecessor_fixups; @@ -726,6 +801,31 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { link_in_program_order(tid, node); event_to_node[event] = node; }, + [&](const VolatileWriteEvent& arg) { + auto node = std::make_shared(arg.var, arg.value, tid); + // write->write sync order: link to the prior volatile write (release). + if (arg.sync_predecessor) + volatile_write_sync_fixups.push_back({node, arg.sync_predecessor}); + link_in_program_order(tid, node); + event_to_node[event] = node; + }, + [&](const VolatileReadEvent& arg) { + std::shared_ptr node; + std::visit(overloaded{ + [&](const ReadValue& val) { + // The source is rendered as a write->read sync (acquire) edge. + node = std::make_shared(arg.var, val.value, tid, nullptr); + assert(val.source_event && "source missing"); + reads_to_fix.push_back({node, val.source_event}); + }, + [&](const std::shared_ptr&) { + node = std::make_shared(arg.var, tid, graph::Conflict(arg.var)); + } + }, arg.value_or_conflict); + + link_in_program_order(tid, node); + event_to_node[event] = node; + }, [&](const SpawnEvent& arg) { // Link to the child thread's start node auto node = std::make_shared(arg.child_tid, g.threads[arg.child_tid]); @@ -806,6 +906,13 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { } } + // Fix up volatile write->write sync edges (predecessor may be in another thread). + for (auto& [vwrite_node, pred_event] : volatile_write_sync_fixups) { + if (event_to_node.contains(pred_event)) { + vwrite_node->sync_predecessor = event_to_node[pred_event]; + } + } + // Fix up conflicting unlock g_predecessor edges (predecessor is in another thread). for (auto& [unlock_node, pred_event] : unlocks_g_predecessor_fixups) { if (event_to_node.contains(pred_event)) { diff --git a/src/lang.hh b/src/lang.hh index ede6bb0..afab22b 100644 --- a/src/lang.hh +++ b/src/lang.hh @@ -12,6 +12,7 @@ Reader reader(); // Variables inline const auto Reg = TokenDef("reg", flag::print); inline const auto Var = TokenDef("var", flag::print); +inline const auto Volatile = TokenDef("volatile", flag::print); // Constants inline const auto Const = TokenDef("const", flag::print); @@ -60,13 +61,13 @@ inline const auto Then = TokenDef("then"); (Top <<= File) | (File <<= Block) | (Block <<= Stmt++[1]) - | (Expr <<= (Reg | Var | Const | Spawn | Eq | Neq | Add)) + | (Expr <<= (Reg | Var | Volatile | Const | Spawn | Eq | Neq | Add)) | (Spawn <<= Block) | (Eq <<= (Lhs >>= Expr) * (Rhs >>= Expr)) | (Neq <<= (Lhs >>= Expr) * (Rhs >>= Expr)) | (Add <<= Expr++[2]) | (Stmt <<= (Nop | Assign | Join | Lock | Unlock | Assert | If)) - | (Assign <<= ((LVal >>= (Reg | Var)) * Expr))[LVal] + | (Assign <<= ((LVal >>= (Reg | Var | Volatile)) * Expr))[LVal] | (Join <<= Expr) | (Lock <<= Var) | (Unlock <<= Var) diff --git a/src/linear/memory_model.cc b/src/linear/memory_model.cc index 5344df1..583b5f5 100644 --- a/src/linear/memory_model.cc +++ b/src/linear/memory_model.cc @@ -70,17 +70,13 @@ std::string LinearMemoryModel::build_revision_graph_dot( } std::optional -LinearMemoryModel::push(LocalVersionStore &local) { +LinearMemoryModel::pullpush(LocalVersionStore &local) { if (auto conflict = _global_store.check_conflicts({local.thread(), local.timestamp()}, local.staged_changes())) { return *conflict; } - uint64_t new_base = _global_store.apply_changes( - local.thread(), local.timestamp(), local.staged_changes()); - - local.clear_staging(); - local.advance_base(new_base); + push(local); return std::nullopt; } @@ -95,6 +91,14 @@ LinearMemoryModel::pull(LocalVersionStore &local) { return std::nullopt; } +void LinearMemoryModel::push(LocalVersionStore &local) { + uint64_t new_base = _global_store.apply_changes( + local.thread(), local.timestamp(), local.staged_changes()); + + local.clear_staging(); + local.advance_base(new_base); +} + LinearMemoryModel::~LinearMemoryModel() = default; ReadResult LinearMemoryModel::read(ThreadContext &ctx, @@ -123,9 +127,9 @@ void LinearMemoryModel::write(ThreadContext &ctx, const std::string &var, std::optional> LinearMemoryModel::on_spawn(ThreadContext &parent, ThreadContext &child) { - // push parent to global history + // pullpush parent to global history auto& store = get_store(parent); - if (auto conflict = push(store)) + if (auto conflict = pullpush(store)) return std::make_shared(std::move(*conflict)); // pull into the child @@ -139,7 +143,7 @@ LinearMemoryModel::on_spawn(ThreadContext &parent, ThreadContext &child) { std::optional> LinearMemoryModel::on_join(ThreadContext &joiner, ThreadContext &joinee) { - // we assume the joinee has already terminated and pushed + // we assume the joinee has already terminated and pullpushed // pull changes into parent auto& store = get_store(joiner); @@ -161,9 +165,9 @@ LinearMemoryModel::on_start(ThreadContext &thread) { std::optional> LinearMemoryModel::on_end(ThreadContext &thread) { - // push changes to global history + // pullpush changes to global history auto& store = get_store(thread); - if (auto conflict = push(store)) + if (auto conflict = pullpush(store)) return std::make_shared(std::move(*conflict)); return std::nullopt; @@ -181,14 +185,43 @@ LinearMemoryModel::on_lock(ThreadContext &thread, Lock &lock) { std::optional> LinearMemoryModel::on_unlock(ThreadContext &thread, Lock &) { - // push changes to global history + // pullpush changes to global history auto& store = get_store(thread); - if (auto conflict = push(store)) + if (auto conflict = pullpush(store)) return std::make_shared(std::move(*conflict)); return std::nullopt; } +std::optional> +LinearMemoryModel::on_volatile_read(ThreadContext &thread, Volatile &v) { + auto& store = get_store(thread); + if (auto conflict = pullpush(store)) + return std::make_shared(std::move(*conflict)); + + return std::nullopt; +} + +std::optional> +LinearMemoryModel::on_volatile_write(ThreadContext &thread, Volatile &v, + ValueWithSource value) { + auto& store = get_store(thread); + + // Release: publish the thread's ordinary staged writes through g so a later + // acquire sees them. May report a conflict on those *non-volatile* changes; + // never on @v itself -- @v is not versioned. + if (auto conflict = pull(store)) + return std::make_shared(std::move(*conflict)); + push(store); + + // The volatile's value lives on the object, not the versioned store. `value` + // carries the write event as its source so a later volatile read observes it + // as the writer synchronized with. + v.value = value; + + return std::nullopt; +} + bool LinearMemoryModel::is_scheduling_point(SyncOperation op) const { switch (op) { case SyncOperation::Lock: @@ -196,7 +229,9 @@ bool LinearMemoryModel::is_scheduling_point(SyncOperation op) const { case SyncOperation::Join: case SyncOperation::Spawn: case SyncOperation::Start: - case SyncOperation::End: return true; } + case SyncOperation::End: + case SyncOperation::VolatileRead: + case SyncOperation::VolatileWrite: return true; } assert(false && "Unknown SyncOperation"); } diff --git a/src/linear/memory_model.hh b/src/linear/memory_model.hh index 22bcac0..24f0118 100644 --- a/src/linear/memory_model.hh +++ b/src/linear/memory_model.hh @@ -14,8 +14,11 @@ namespace linear { class LinearMemoryModel final : public MemoryModel { GlobalVersionStore _global_store; - std::optional push(LocalVersionStore &local); + std::optional pullpush(LocalVersionStore &local); std::optional pull(LocalVersionStore &local); + // push staged changes without a conflict check; only safe when the base is + // already current (e.g. immediately after a pull). + void push(LocalVersionStore &local); public: ~LinearMemoryModel() override; @@ -42,6 +45,13 @@ public: std::optional> on_unlock(ThreadContext &thread, Lock &lock) override; + std::optional> + on_volatile_read(ThreadContext &thread, Volatile &v) override; + + std::optional> + on_volatile_write(ThreadContext &thread, Volatile &v, + ValueWithSource value) override; + std::ostream &print(std::ostream &os) const override; std::string build_revision_graph_dot(const std::vector& thread_states) const override; @@ -57,6 +67,10 @@ public: std::unique_ptr make_lock_state() const override { return nullptr; } + + std::unique_ptr make_volatile_state() const override { + return nullptr; + } }; } // namespace linear diff --git a/src/memory_model.hh b/src/memory_model.hh index 98b2c5f..fe0e849 100644 --- a/src/memory_model.hh +++ b/src/memory_model.hh @@ -23,7 +23,9 @@ enum class SyncOperation { Start, End, Lock, - Unlock + Unlock, + VolatileRead, + VolatileWrite }; class MemoryModel { @@ -32,6 +34,7 @@ public: virtual std::unique_ptr make_thread_state(ThreadID tid) const = 0; virtual std::unique_ptr make_lock_state() const = 0; + virtual std::unique_ptr make_volatile_state() const = 0; // Read a shared variable into the thread context virtual ReadResult read(ThreadContext &ctx, const std::string &var) = 0; @@ -58,6 +61,22 @@ public: virtual std::optional> on_unlock(ThreadContext &thread, Lock &lock) = 0; + // A volatile read is an acquire: it synchronises-with the previous release + // (write) of `v`. Like on_lock it reports only a conflict (from racing on the + // piggybacked non-volatile state); the value observed is obtained separately + // via `read`, whose source_event identifies the writer synchronized with. + virtual std::optional> + on_volatile_read(ThreadContext &thread, Volatile &v) = 0; + + // A volatile write is a release: it publishes `value` for `v`. It may itself + // conflict (release ordering) but never on the volatile's own value -- + // volatiles are race-free by construction. The ValueWithSource carries the + // write event as provenance so a later volatile read can follow it as the + // acquire->release edge (not for conflict blame). + virtual std::optional> + on_volatile_write(ThreadContext &thread, Volatile &v, + ValueWithSource value) = 0; + // Returns true if the given sync operation is a scheduling point for this protocol // (i.e., the scheduler should consider switching threads here) virtual bool is_scheduling_point(SyncOperation op) const = 0; diff --git a/src/parser.cc b/src/parser.cc index 78b1a3b..423d1f7 100644 --- a/src/parser.cc +++ b/src/parser.cc @@ -90,6 +90,7 @@ Parse parser() { // Variables R"(\$[_[:alpha:]][_[:alnum:]]*)" >> [](auto &m) { m.add(Reg); }, + R"(\@[_[:alpha:]][_[:alnum:]]*)" >> [](auto &m) { m.add(Volatile); }, R"([_[:alpha:]][_[:alnum:]]*)" >> [](auto &m) { m.add(Var); }, // Grouping diff --git a/src/passes/expressions.cc b/src/passes/expressions.cc index 152a413..2bf7067 100644 --- a/src/passes/expressions.cc +++ b/src/passes/expressions.cc @@ -7,12 +7,12 @@ namespace lang { using namespace trieste; PassDef expressions() { - auto Operand = T(Expr) << (T(Reg, Var, Const, Add)); + auto Operand = T(Expr) << (T(Reg, Volatile, Var, Const, Add)); return {"expressions", expressions_wf, dir::bottomup, { - --In(Expr) * T(Const, Reg, Var)[Expr] >> + --In(Expr) * T(Const, Reg, Volatile, Var)[Expr] >> [](Match &_) -> Node { return Expr << _(Expr); }, --In(Expr) * T(Spawn)[Spawn] << (T(Brace) * End) >> diff --git a/src/passes/statements.cc b/src/passes/statements.cc index 91e4a2e..f3826db 100644 --- a/src/passes/statements.cc +++ b/src/passes/statements.cc @@ -7,7 +7,7 @@ namespace lang { using namespace trieste; PassDef statements() { - auto RVal = T(Expr) << (T(Reg, Var, Add, Const, Spawn)); + auto RVal = T(Expr) << (T(Reg, Var, Volatile, Add, Const, Spawn)); auto Condition = T(Expr) << (T(Eq, Neq)); return { "statements", @@ -34,7 +34,7 @@ PassDef statements() { --In(Stmt) * T(Unlock) << ((T(Expr) << T(Var)[Var]) * End) >> [](Match &_) -> Node { return Stmt << (Unlock << _(Var)); }, - --In(Stmt) * T(Assign) << ((T(Expr) << (T(Reg, Var)[LVal] * End)) * + --In(Stmt) * T(Assign) << ((T(Expr) << (T(Reg, Var, Volatile)[LVal] * End)) * RVal[Expr] * End) >> [](Match &_) -> Node { return Stmt << (Assign << _(LVal) << _(Expr)); @@ -110,7 +110,7 @@ PassDef statements() { "Expected right-hand side to assignment"); }, - --In(Stmt) * T(Assign) << ((T(Expr) << T(Reg, Var)) * Any[Expr]) >> + --In(Stmt) * T(Assign) << ((T(Expr) << T(Reg, Var, Volatile)) * Any[Expr]) >> [](Match &_) -> Node { return Error << (ErrorAst << _(Expr)) << (ErrorMsg ^ diff --git a/src/sync_state.hh b/src/sync_state.hh index 2d7d680..6bede1e 100644 --- a/src/sync_state.hh +++ b/src/sync_state.hh @@ -28,4 +28,15 @@ public: } }; +class VolatileSyncState { +public: + virtual ~VolatileSyncState() = default; + + virtual std::ostream &print(std::ostream &os) const = 0; + friend std::ostream &operator<<(std::ostream &os, + const VolatileSyncState &state) { + return state.print(os); + } +}; + } \ No newline at end of file diff --git a/src/thread_trace.hh b/src/thread_trace.hh index d53193c..fb93108 100644 --- a/src/thread_trace.hh +++ b/src/thread_trace.hh @@ -23,6 +23,8 @@ struct SpawnEvent { const ThreadID child_tid; }; struct ReadValue { const size_t value; const std::shared_ptr source_event; }; struct ReadEvent { const std::string var; std::variant> value_or_conflict; }; struct WriteEvent { const std::string var; const size_t value; const FileLocation location; }; +struct VolatileReadEvent { const std::string var; std::variant> value_or_conflict; }; +struct VolatileWriteEvent { const std::string var; const size_t value; const FileLocation location; std::shared_ptr maybe_conflict = nullptr; std::shared_ptr sync_predecessor = nullptr; }; struct LockEvent { std::string lock_name; std::shared_ptr maybe_conflict; std::shared_ptr last_unlock_event; }; struct UnlockEvent { const std::string lock_name; std::shared_ptr maybe_conflict; std::shared_ptr g_predecessor = nullptr; }; struct JoinEvent { const ThreadID joinee_tid; std::shared_ptr maybe_conflict; }; @@ -40,6 +42,8 @@ struct Event { SpawnEvent, ReadEvent, WriteEvent, + VolatileReadEvent, + VolatileWriteEvent, LockEvent, UnlockEvent, JoinEvent, @@ -79,6 +83,24 @@ inline std::ostream& operator<<(std::ostream& os, const WriteEvent& e) { return os << ")"; } +inline std::ostream& operator<<(std::ostream& os, const VolatileReadEvent& e) { + os << "VolatileReadEvent(var=\"" << e.var << "\", "; + std::visit(overloaded{ + [&os](const ReadValue& val) { os << "value=" << val.value << " (from " << val.source_event->eid << ")"; }, + [&os](const std::shared_ptr&) { os << "conflict"; } + }, e.value_or_conflict); + os << ")"; + return os; +} + +inline std::ostream& operator<<(std::ostream& os, const VolatileWriteEvent& e) { + os << "VolatileWriteEvent(var=\"" << e.var << "\", value=" << e.value; + os << ", at " << e.location.linecol(); + if (e.maybe_conflict) + os << ", conflict"; + return os << ")"; +} + inline std::ostream& operator<<(std::ostream& os, const LockEvent& e) { os << "LockEvent(lock_name=\"" << e.lock_name << "\""; if (e.last_unlock_event) @@ -167,6 +189,29 @@ private: return append(std::move(text), value, std::move(location)); } + std::shared_ptr on_volatile_read(const std::string text, ValueWithSource value) { + return append(std::move(text), ReadValue{value.value, value.source_event}); + } + + std::shared_ptr on_volatile_read(const std::string text, std::shared_ptr conflict) { + return append(std::move(text), conflict); + } + + + std::shared_ptr on_volatile_write(const std::string text, const size_t value, + FileLocation location, + std::shared_ptr sync_predecessor = nullptr) { + return append(std::move(text), value, std::move(location), + nullptr, std::move(sync_predecessor)); + } + + // The volatile-write event is the value's provenance, so it is created before + // the model checks the release; attach a conflict here if the release raced. + void on_volatile_write_conflict(const std::shared_ptr& event, + std::shared_ptr conflict) { + std::get(event->data).maybe_conflict = std::move(conflict); + } + std::shared_ptr on_lock(const std::string lock_name, std::shared_ptr last_unlock_event, std::shared_ptr conflict = nullptr) { diff --git a/test_gitmem.py b/test_gitmem.py index b03bce0..0976dd0 100644 --- a/test_gitmem.py +++ b/test_gitmem.py @@ -1,4 +1,5 @@ import os +import re import subprocess import sys import argparse @@ -12,6 +13,32 @@ "branching-lazy": {"sync": "branching", "branching_mode": "lazy"}, } +# A test's expected outcome defaults to its accept/reject directory, but a model +# may legitimately diverge -- e.g. lazy branching only reports a conflict on a +# variable that is actually read, so it accepts unread races that eager/linear +# reject. A test can override the expectation for specific models with a comment +# directive (the program itself is untouched): +# +# // expect branching-lazy: accept +# +# The model name must match a key in SYNC_KINDS; the outcome is accept|reject. +EXPECT_RE = re.compile( + r"//\s*expect\s+([A-Za-z0-9_-]+)\s*[:=]\s*(accept|reject)\b", + re.IGNORECASE, +) + +def parse_expectation_overrides(file_path): + overrides = {} + try: + with open(file_path, "r") as f: + for line in f: + m = EXPECT_RE.search(line) + if m and m.group(1) in SYNC_KINDS: + overrides[m.group(1)] = (m.group(2).lower() == "accept") + except (OSError, UnicodeDecodeError): + pass + return overrides + def supports_color(): return sys.stdout.isatty() and os.getenv("NO_COLOR") is None @@ -26,7 +53,7 @@ def green(text): def red(text): return color(text, "31") -def run_gitmem_test(gitmem_path, file_path, should_accept, sync_kind): +def run_gitmem_test(gitmem_path, file_path, should_accept, sync_kind, overridden=False): sync_config = SYNC_KINDS[sync_kind] cmd = [ @@ -58,7 +85,9 @@ def run_gitmem_test(gitmem_path, file_path, should_accept, sync_kind): sys.exit(1) status = green("PASS") if accepted else red("FAIL") - print(f"[{status}] {file_path} [{sync_kind}] (exit code: {result.returncode})") + expected = "accept" if should_accept else "reject" + note = f" (override: expect {expected})" if overridden else "" + print(f"[{status}] {file_path} [{sync_kind}]{note} (exit code: {result.returncode})") return accepted def main(): @@ -140,11 +169,15 @@ def main(): total_tests += 1 results[expectation][category][sync_kind]["total"] += 1 + overrides = parse_expectation_overrides(file_path) + effective_accept = overrides.get(sync_kind, should_accept) + passed = run_gitmem_test( gitmem_path, file_path, - should_accept, - sync_kind + effective_accept, + sync_kind, + overridden=(sync_kind in overrides) ) if not passed: From bec6481e7dd1469af20b2e50ecfa31300ec33de6 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Thu, 23 Jul 2026 12:07:48 +0200 Subject: [PATCH 14/14] Linear volatile read is pull only not pullpush --- .../volatile_read_is_pull_not_push.gm | 26 +++++++++++++++++++ .../linear/volatile_read_is_pull_not_push.gm | 26 +++++++++++++++++++ src/linear/memory_model.cc | 2 +- 3 files changed, 53 insertions(+), 1 deletion(-) create mode 100644 examples/accept/semantics/branching/volatile_read_is_pull_not_push.gm create mode 100644 examples/accept/semantics/linear/volatile_read_is_pull_not_push.gm diff --git a/examples/accept/semantics/branching/volatile_read_is_pull_not_push.gm b/examples/accept/semantics/branching/volatile_read_is_pull_not_push.gm new file mode 100644 index 0000000..41f28f5 --- /dev/null +++ b/examples/accept/semantics/branching/volatile_read_is_pull_not_push.gm @@ -0,0 +1,26 @@ +// This test demonstrates that volatile reads are pull actions, not push actions. +// In particular, the read of @v in t2 should not push the changes from t2 to t1, +// and so the assertion on y should always succeed. + +@v = 0; +x = 0; +y = 0; + +t1 = spawn { + x = 1; + @v = 1; + assert(y == 0); +}; + +t2 = spawn { + y = 1; + if (@v == 1) { + assert(x == 1); + } else { + assert(x == 0); + } + join t1; +}; + +join t1; +join t2; \ No newline at end of file diff --git a/examples/accept/semantics/linear/volatile_read_is_pull_not_push.gm b/examples/accept/semantics/linear/volatile_read_is_pull_not_push.gm new file mode 100644 index 0000000..41f28f5 --- /dev/null +++ b/examples/accept/semantics/linear/volatile_read_is_pull_not_push.gm @@ -0,0 +1,26 @@ +// This test demonstrates that volatile reads are pull actions, not push actions. +// In particular, the read of @v in t2 should not push the changes from t2 to t1, +// and so the assertion on y should always succeed. + +@v = 0; +x = 0; +y = 0; + +t1 = spawn { + x = 1; + @v = 1; + assert(y == 0); +}; + +t2 = spawn { + y = 1; + if (@v == 1) { + assert(x == 1); + } else { + assert(x == 0); + } + join t1; +}; + +join t1; +join t2; \ No newline at end of file diff --git a/src/linear/memory_model.cc b/src/linear/memory_model.cc index 583b5f5..0cca510 100644 --- a/src/linear/memory_model.cc +++ b/src/linear/memory_model.cc @@ -196,7 +196,7 @@ LinearMemoryModel::on_unlock(ThreadContext &thread, Lock &) { std::optional> LinearMemoryModel::on_volatile_read(ThreadContext &thread, Volatile &v) { auto& store = get_store(thread); - if (auto conflict = pullpush(store)) + if (auto conflict = pull(store)) return std::make_shared(std::move(*conflict)); return std::nullopt;