From c03f477e79e72e459fbb44e61a135ecd40cf2ce3 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 17:55:53 +0200 Subject: [PATCH 01/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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"