From c03f477e79e72e459fbb44e61a135ecd40cf2ce3 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 30 Jun 2026 17:55:53 +0200 Subject: [PATCH 01/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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/16] 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; From e26c50ec3a5a7cad088681f80c4013cc837eaabe Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Tue, 11 Aug 2026 17:14:40 +0200 Subject: [PATCH 15/16] Split compound volatile reads and writes in one statement into seperate statements to allow for correct schuedling decisions in the model explorer. Correct some missing volatile wf trieste info, and render the dump correctly --- CMakeLists.txt | 2 ++ .../branching/volatile_sync_conflict.gm | 8 ++--- src/branching/base_memory_model.cc | 33 ++++++++++++++----- src/branching/eager/version_store.cc | 17 +++++++--- src/branching/lazy/version_store.cc | 17 +++++++--- src/execution_state.cc | 4 +-- src/internal.hh | 11 ++++--- src/interpreter.cc | 11 ++++--- src/linear/memory_model.cc | 17 +++++----- src/linear/version_store.cc | 13 +++++--- src/reader.cc | 1 + 11 files changed, 88 insertions(+), 46 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index f7807de..b9cde7e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -38,6 +38,7 @@ add_executable(gitmem src/passes/expressions.cc src/passes/statements.cc src/passes/check_refs.cc + src/passes/hoist_volatiles.cc src/passes/branching.cc src/linear/memory_model.cc src/linear/version_store.cc @@ -59,6 +60,7 @@ add_executable(gitmem_trieste src/passes/expressions.cc src/passes/statements.cc src/passes/check_refs.cc + src/passes/hoist_volatiles.cc src/passes/branching.cc ) diff --git a/examples/reject/semantics/branching/volatile_sync_conflict.gm b/examples/reject/semantics/branching/volatile_sync_conflict.gm index 90f9bb7..ed8df44 100644 --- a/examples/reject/semantics/branching/volatile_sync_conflict.gm +++ b/examples/reject/semantics/branching/volatile_sync_conflict.gm @@ -1,8 +1,6 @@ -// 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 +// The two volatile writes to @v are concurrent with no happens-before between +// them (write->write is not a synchronizes-with edge, only write->read is), so +// they race -- and so do the piggybacked x writes. All models detect it. $t = spawn { x = 1; diff --git a/src/branching/base_memory_model.cc b/src/branching/base_memory_model.cc index 389cbbb..46c416f 100644 --- a/src/branching/base_memory_model.cc +++ b/src/branching/base_memory_model.cc @@ -131,7 +131,9 @@ BranchingMemoryModelBase::on_volatile_read(ThreadContext &thread, Volatile &v) { 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. + // happened-before it -- this launders that write into happens-before for our + // own later writes. A read never stages @v, so it never races. 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)) { @@ -140,7 +142,7 @@ BranchingMemoryModelBase::on_volatile_read(ThreadContext &thread, Volatile &v) { } // The value (with its writer as provenance) lives on the Volatile object and - // is read there by the interpreter -- @v is not versioned. + // is read there by the interpreter. return std::nullopt; } @@ -148,11 +150,18 @@ std::optional> BranchingMemoryModelBase::on_volatile_write(ThreadContext &thread, Volatile &v, ValueWithSource value) { auto& store = get_store(thread); + + // Version @v in the DAG, in addition to the atomic value we keep on the + // object. Two volatile writes with no happens-before between them race + // (write->write is not a synchronizes-with edge, only write->read is) -- + // even though each store is atomic. Staging @v makes such a concurrent write + // land in a divergent branch, so the merge below reports it as a conflict. + write(thread, v.name, value); 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. + // Merge the previous release. If a concurrent writer's @v sits in a divergent + // branch this reports the write-write race; it also catches piggybacked + // non-volatile races. VolatileState& vstate = get_store(v); if (vstate.commit != nullptr) { if (std::optional conflict = store.merge_with_commit(vstate.commit)) { @@ -160,9 +169,17 @@ BranchingMemoryModelBase::on_volatile_write(ThreadContext &thread, Volatile &v, } } - // 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. + // Lazy defers merge-conflict detection to read time, and a volatile read + // observes the object rather than the store -- so the deferred write-write + // race would never surface. Probe @v in the store here to force it. (Eager + // already reported any conflict at the merge above, so this is a no-op there.) + auto probe = store.read(v.name); + if (auto* conflict = std::get_if(&probe)) + return std::make_shared(*conflict); + + // Record the new release. The atomic value (with provenance) lives on the + // object -- that single current value is what reads observe; the DAG version + // exists only to detect the race. vstate.commit = store.get_head(); v.value = value; diff --git a/src/branching/eager/version_store.cc b/src/branching/eager/version_store.cc index 11b107f..7d079f9 100644 --- a/src/branching/eager/version_store.cc +++ b/src/branching/eager/version_store.cc @@ -120,6 +120,13 @@ std::optional EagerLocalVersionStore::merge_with_commit(const std::sha if (head == commit) return std::nullopt; + // Fast-forward: if the incoming commit is already in our history there is + // nothing to merge. Building a merge commit here would add a redundant parent + // edge straight to an old ancestor, which can mislead ancestor queries. + std::unordered_map, bool> ff_memo; + if (can_reach(head, commit, ff_memo)) + return std::nullopt; + // Find lowest common ancestor of the two heads std::shared_ptr lca = find_lowest_common_ancestor(head, commit); verbose::out << "found lca of " @@ -145,10 +152,12 @@ std::optional EagerLocalVersionStore::merge_with_commit(const std::sha auto it = c->changes.find(obj); if (it == c->changes.end() || !it->second.source_event) throw std::logic_error("missing source event for conflicting write"); - auto* we = std::get_if(&it->second.source_event->data); - if (!we) - throw std::logic_error("conflicting source event is not a WriteEvent"); - return we->location; + if (auto* we = std::get_if(&it->second.source_event->data)) + return we->location; + // Volatile writes can race (write-write with no happens-before). + if (auto* vwe = std::get_if(&it->second.source_event->data)) + return vwe->location; + throw std::logic_error("conflicting source event is not a write"); }; std::optional conflict; for (const auto& [obj, commit_a] : branch_a) { diff --git a/src/branching/lazy/version_store.cc b/src/branching/lazy/version_store.cc index df300f6..2cc3bd3 100644 --- a/src/branching/lazy/version_store.cc +++ b/src/branching/lazy/version_store.cc @@ -19,6 +19,13 @@ std::optional LazyLocalVersionStore::merge_with_commit(const std::shar if (head == commit) return std::nullopt; + // Fast-forward: if the incoming commit is already in our history there is + // nothing to merge (and a redundant merge commit's extra parent edge can + // mislead ancestor queries). + std::unordered_map, bool> ff_memo; + if (can_reach(head, commit, ff_memo)) + return std::nullopt; + // Create merge commit (no changes itself) auto merge_commit = std::make_shared( Commit{ @@ -130,10 +137,12 @@ BranchingReadResult LazyLocalVersionStore::get_committed(std::string var) const auto get_loc = [](const ValueWithSource& vws) -> FileLocation { if (!vws.source_event) throw std::logic_error("missing source event for conflicting write"); - auto* we = std::get_if(&vws.source_event->data); - if (!we) - throw std::logic_error("conflicting source event is not a WriteEvent"); - return we->location; + if (auto* we = std::get_if(&vws.source_event->data)) + return we->location; + // Volatile writes can race (write-write with no happens-before). + if (auto* vwe = std::get_if(&vws.source_event->data)) + return vwe->location; + throw std::logic_error("conflicting source event is not a write"); }; auto a = writers[0]->id; auto b = writers[1]->id; diff --git a/src/execution_state.cc b/src/execution_state.cc index 6750727..b37ca72 100644 --- a/src/execution_state.cc +++ b/src/execution_state.cc @@ -2,6 +2,7 @@ #include "execution_state.hh" #include "memory_model.hh" +#include "render.hh" namespace gitmem { @@ -119,9 +120,8 @@ std::ostream& operator<<(std::ostream& os, const Thread& thread) { os << " "; } - // This should be somewhere else // Fix indentation of nested blocks - auto s = std::string(stmt->location().view()); + auto s = lang::render(stmt); s = std::regex_replace(s, std::regex("\n"), "\n "); os << s << ";" << std::endl; diff --git a/src/internal.hh b/src/internal.hh index c258ab7..8747f06 100644 --- a/src/internal.hh +++ b/src/internal.hh @@ -11,11 +11,12 @@ Parse parser(); PassDef expressions(); PassDef statements(); PassDef check_refs(); +PassDef hoist_volatiles(); PassDef branching(); -inline const auto parse_token = Reg | Var | Const | Nop | Brace | Paren | - Spawn | Join | Lock | Unlock | Assert | If | - Else; +inline const auto parse_token = Reg | Var | Volatile | Const | Nop | Brace | + Paren | Spawn | Join | Lock | Unlock | Assert | + If | Else; inline const auto parse_op = Group | Assign | Eq | Neq | Add | Semi; @@ -46,7 +47,7 @@ inline const auto parse_op = Group | Assign | Eq | Neq | Add | Semi; inline const wf::Wellformed expressions_wf = parser_wf | (File <<= ~expressions_op) - | (Expr <<= (Reg | Var | Const | Spawn | Eq | Neq | Add)) + | (Expr <<= (Reg | Var | Volatile | Const | Spawn | Eq | Neq | Add)) | (Brace <<= ~expressions_op) | (Paren <<= ~expressions_op) | (Semi <<= (expressions_op - Semi)++[1]) @@ -70,7 +71,7 @@ inline const auto parse_op = Group | Assign | Eq | Neq | Add | Semi; | (Spawn <<= Block) | (Block <<= Stmt++[1]) | (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/interpreter.cc b/src/interpreter.cc index 491b13b..5d37515 100644 --- a/src/interpreter.cc +++ b/src/interpreter.cc @@ -8,6 +8,7 @@ #include "interpreter.hh" #include "memory_model.hh" #include "overloaded.hh" +#include "render.hh" namespace gitmem { @@ -122,7 +123,7 @@ std::optional Interpreter::pending_statement(ThreadID tid) const { return std::nullopt; } - return std::string(thread.block->at(thread.pc)->location().view()); + return lang::render(thread.block->at(thread.pc)); } bool Interpreter::same_state_as(const GlobalContext& other) const { @@ -143,14 +144,14 @@ Interpreter::evaluate_expression(trieste::Node expr, Thread& thread) { auto e = expr / lang::Expr; if (e == lang::Reg) { // It is invalid to read a previously unwritten value - auto var = std::string(expr->location().view()); + auto var = std::string(e->location().view()); if (ctx.locals.contains(var)) { return ctx.locals[var]; } else { return termination::UnassignedRead(var); } } else if (e == lang::Volatile) { - auto var = std::string(expr->location().view()); + auto var = std::string(e->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 @@ -172,7 +173,7 @@ Interpreter::evaluate_expression(trieste::Node expr, Thread& thread) { return vol.value->value; } else if (e == lang::Var) { - auto var = std::string(expr->location().view()); + auto var = std::string(e->location().view()); auto result = gctx.model->read(ctx, var); @@ -888,7 +889,7 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { if (thread.pc < thread.block->size()) { // Thread is stuck waiting at a specific statement trieste::Node stmt = thread.block->at(thread.pc); - auto pending = std::make_shared(std::string(stmt->location().view())); + auto pending = std::make_shared(lang::render(stmt)); link_in_program_order(tid, pending); } else { // Thread has finished all statements but hasn't terminated yet diff --git a/src/linear/memory_model.cc b/src/linear/memory_model.cc index 0cca510..56ed2f1 100644 --- a/src/linear/memory_model.cc +++ b/src/linear/memory_model.cc @@ -207,16 +207,17 @@ 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)) + // Version @v in g, in addition to the atomic value on the object. Then + // publish, checking for conflicts at the current base: a concurrent write to + // @v -- one not happens-before ours -- is caught here as a write-write race + // (write->write is not a synchronizes-with edge, only write->read is). We + // must NOT pull first: that would absorb the concurrent write and hide it. + store.stage(v.name, value); + if (auto conflict = pullpush(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. + // The single current value (with provenance) lives on the object; the g + // version exists only to detect the race. v.value = value; return std::nullopt; diff --git a/src/linear/version_store.cc b/src/linear/version_store.cc index f825994..d35dd9c 100644 --- a/src/linear/version_store.cc +++ b/src/linear/version_store.cc @@ -79,11 +79,14 @@ std::optional GlobalVersionStore::check_conflicts( if (!value.source_event) throw std::logic_error("missing source event for conflicting write"); - auto* write = std::get_if(&value.source_event->data); - if (!write) - throw std::logic_error("conflicting source event is not a WriteEvent"); - - return write->location; + if (auto* write = std::get_if(&value.source_event->data)) + return write->location; + // Volatile writes can race (write-write with no happens-before), so a + // volatile write may legitimately be party to a conflict. + if (auto* vwrite = std::get_if(&value.source_event->data)) + return vwrite->location; + + throw std::logic_error("conflicting source event is not a write"); }; for (const auto &[obj, local_value] : changes) { diff --git a/src/reader.cc b/src/reader.cc index 37bf9fe..c4a2ca7 100644 --- a/src/reader.cc +++ b/src/reader.cc @@ -13,6 +13,7 @@ Reader reader() { expressions(), statements(), check_refs(), + hoist_volatiles(), branching(), }, gitmem::lang::parser(), From a411d89f04c8a63c505dac83aebeecd29562d7f2 Mon Sep 17 00:00:00 2001 From: Luke Cheeseman Date: Wed, 12 Aug 2026 11:15:51 +0200 Subject: [PATCH 16/16] Add hositing of multiple volatile access in one statement into seperate temporaries to allow for the multiple scheduling points. This includes re-rerendering the original line and rendering the new line in the explorer output --- .../branching/volatile_increment_race.gm | 9 +++ .../branching/volatile_write_write_race.gm | 8 ++ .../linear/volatile_write_write_race.gm | 8 ++ src/graph.hh | 3 + src/graphviz.cc | 10 ++- src/interpreter.cc | 19 +++++ src/passes/hoist_volatiles.cc | 63 +++++++++++++++ src/render.hh | 77 +++++++++++++++++++ volatile.trieste | 27 +++++++ 9 files changed, 221 insertions(+), 3 deletions(-) create mode 100644 examples/reject/semantics/branching/volatile_increment_race.gm create mode 100644 examples/reject/semantics/branching/volatile_write_write_race.gm create mode 100644 examples/reject/semantics/linear/volatile_write_write_race.gm create mode 100644 src/passes/hoist_volatiles.cc create mode 100644 src/render.hh create mode 100644 volatile.trieste diff --git a/examples/reject/semantics/branching/volatile_increment_race.gm b/examples/reject/semantics/branching/volatile_increment_race.gm new file mode 100644 index 0000000..e82edfe --- /dev/null +++ b/examples/reject/semantics/branching/volatile_increment_race.gm @@ -0,0 +1,9 @@ +// Two volatile writes to @v with no happens-before between them (write->write +// is not a synchronizes-with edge). The stores are atomic but they still race: +// the final value is order-dependent. A concurrent write-write on a volatile is +// a race and must be rejected. +@v = 0; +$t = spawn { + @v = @v + 1; +}; +@v = @v + 1; diff --git a/examples/reject/semantics/branching/volatile_write_write_race.gm b/examples/reject/semantics/branching/volatile_write_write_race.gm new file mode 100644 index 0000000..bcc7598 --- /dev/null +++ b/examples/reject/semantics/branching/volatile_write_write_race.gm @@ -0,0 +1,8 @@ +// Two volatile writes to @v with no happens-before between them (write->write +// is not a synchronizes-with edge). The stores are atomic but they still race: +// the final value is order-dependent. A concurrent write-write on a volatile is +// a race and must be rejected. +$t = spawn { + @v = 1; +}; +@v = 2; diff --git a/examples/reject/semantics/linear/volatile_write_write_race.gm b/examples/reject/semantics/linear/volatile_write_write_race.gm new file mode 100644 index 0000000..bcc7598 --- /dev/null +++ b/examples/reject/semantics/linear/volatile_write_write_race.gm @@ -0,0 +1,8 @@ +// Two volatile writes to @v with no happens-before between them (write->write +// is not a synchronizes-with edge). The stores are atomic but they still race: +// the final value is order-dependent. A concurrent write-write on a volatile is +// a race and must be rejected. +$t = spawn { + @v = 1; +}; +@v = 2; diff --git a/src/graph.hh b/src/graph.hh index c4dbf61..ddd1fac 100644 --- a/src/graph.hh +++ b/src/graph.hh @@ -117,6 +117,9 @@ struct Read : Node { // chains onto (null for the first write to the volatile). struct VolatileWrite : Write { std::shared_ptr sync_predecessor = nullptr; + // A volatile write can race (write-write with no happens-before); when it + // does, this holds the conflict so the node renders as an error. + std::optional conflict = std::nullopt; VolatileWrite(const std::string var, const size_t value, const size_t id) : Write(var, value, id) {} diff --git a/src/graphviz.cc b/src/graphviz.cc index 3566d31..3afb8bc 100644 --- a/src/graphviz.cc +++ b/src/graphviz.cc @@ -62,12 +62,13 @@ void GraphvizPrinter::emitConflict(const Node *n, const Conflict &conflict) { emitFillColor(n, "red"); // emitShape(n, "doubleoctagon"); - // Only draw conflict edges if we have actual source nodes + // Only draw conflict edges to actual *other* source nodes (a racing write is + // often one of the two sources itself; don't draw a self-loop). auto [s1, s2] = conflict.sources; - if (s1) { + if (s1 && s1.get() != n) { emitConflictEdge(n, s1.get()); } - if (s2) { + if (s2 && s2.get() != n) { emitConflictEdge(n, s2.get()); } } @@ -144,6 +145,9 @@ void GraphvizPrinter::visitVolatileWrite(const VolatileWrite *n) { // write->write synchronisation order (release chain). if (n->sync_predecessor) emitSyncEdge(n->sync_predecessor.get(), n); + // A concurrent write-write race renders the node as an error. + if (n->conflict) + emitConflict(n, n->conflict.value()); } void GraphvizPrinter::visitVolatileRead(const VolatileRead *n) { diff --git a/src/interpreter.cc b/src/interpreter.cc index 5d37515..66c0089 100644 --- a/src/interpreter.cc +++ b/src/interpreter.cc @@ -723,6 +723,10 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { // write) must be resolved after all threads -- it may be another thread's. std::vector, std::shared_ptr>> volatile_write_sync_fixups; + // Track conflicting volatile write nodes: (node, conflict base carrying the + // racing source events). + std::vector, std::shared_ptr>> volatile_write_conflict_fixups; + // Track conflicting unlock nodes whose g_predecessor must be resolved after all threads. std::vector, std::shared_ptr>> unlocks_g_predecessor_fixups; @@ -807,6 +811,11 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { // 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}); + // A volatile write can race (write-write); render it as an error. + if (arg.maybe_conflict) { + node->conflict = graph::Conflict(arg.maybe_conflict->object_name()); + volatile_write_conflict_fixups.push_back({node, arg.maybe_conflict}); + } link_in_program_order(tid, node); event_to_node[event] = node; }, @@ -948,6 +957,16 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() { const_cast(*unlock_node->conflict).sources = {src_a, src_b}; } + // Fix up conflicting volatile write sources (the two racing writes). + for (auto& [vwrite_node, cb] : volatile_write_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) + vwrite_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/passes/hoist_volatiles.cc b/src/passes/hoist_volatiles.cc new file mode 100644 index 0000000..8e488df --- /dev/null +++ b/src/passes/hoist_volatiles.cc @@ -0,0 +1,63 @@ +#include "../internal.hh" + +namespace gitmem { + +namespace lang { + +using namespace trieste; + +// Give every statement at most one volatile (synchronisation) access. +// +// A statement executes atomically and is a single scheduling point, so a +// statement that performs more than one volatile access -- e.g. `@v = @v + 1`, +// which reads @v and writes @v -- collapses two sync actions into one. The +// scheduler can then never interleave between the read and the write, so the +// read/write race (both threads read the old value, both write) is never +// explored. +// +// This pass hoists volatile reads that share a statement with another sync +// action into their own preceding `$tmp = @v;` statement (lifted to the +// enclosing block), until the only volatile read left in any statement is a +// bare `$reg = @v` -- which is already its own scheduling point. A volatile +// read feeding an ordinary register/variable (`$r = @v`, `x = @v`) is the sole +// sync action of its statement and is left alone. +// +// Generated statements keep their original AST locations; the state/graph +// listings pretty-print statements from the tree (see render.hh), so the split +// is shown faithfully without perturbing the file positions used in diagnostics. +PassDef hoist_volatiles() { + return { + "hoist_volatiles", + statements_wf, + dir::bottomup, + { + // A volatile read used as an operand of arithmetic or a comparison + // is not isolated: hoist it into a fresh temporary. + In(Add, Eq, Neq) * (T(Expr) << (T(Volatile)[Volatile] * End)) >> + [](Match &_) -> Node { + auto tmp = _.fresh({"vtmp"}); + return Seq << (Lift << Block + << (Stmt << (Assign << (Reg ^ tmp) + << (Expr << _(Volatile))))) + << (Expr << (Reg ^ tmp)); + }, + + // `@v = @w;` reads @w and writes @v in one statement: hoist the read + // so the write stands alone. (A read into a register or ordinary + // variable is the statement's only sync action, so is not matched.) + T(Assign) + << (T(Volatile)[LVal] * + (T(Expr) << (T(Volatile)[Volatile] * End))) >> + [](Match &_) -> Node { + auto tmp = _.fresh({"vtmp"}); + return Seq << (Lift << Block + << (Stmt << (Assign << (Reg ^ tmp) + << (Expr << _(Volatile))))) + << (Assign << _(LVal) << (Expr << (Reg ^ tmp))); + }, + }}; +} + +} // namespace lang + +} // namespace gitmem diff --git a/src/render.hh b/src/render.hh new file mode 100644 index 0000000..b86f156 --- /dev/null +++ b/src/render.hh @@ -0,0 +1,77 @@ +#pragma once + +#include "lang.hh" +#include + +namespace gitmem { + +namespace lang { + +using namespace trieste; + +// Pretty-print a statement or expression from the AST, so listings reflect the +// actual (possibly pass-transformed) tree rather than the original source span. +// Node locations are left untouched -- they still carry the true file position +// used for diagnostics -- this is display only. +inline std::string render(const Node &n); + +inline std::string render_block(const Node &block) { + std::string s = "{\n"; + for (const auto &stmt : *block) + s += " " + render(stmt) + ";\n"; + s += "}"; + return s; +} + +inline std::string render(const Node &n) { + const auto &t = n->type(); + + if (t == Reg || t == Var || t == Volatile || t == Const) + return std::string(n->location().view()); + + if (t == Expr || t == Stmt) + return render(n->front()); + + if (t == Add) { + std::string s; + bool first = true; + for (const auto &c : *n) { + if (!first) + s += " + "; + first = false; + s += render(c); + } + return s; + } + + if (t == Eq) + return render(n / Lhs) + " == " + render(n / Rhs); + if (t == Neq) + return render(n / Lhs) + " != " + render(n / Rhs); + + if (t == Spawn) + return "spawn " + render_block(n / Block); + if (t == Assign) + return render(n / LVal) + " = " + render(n / Expr); + if (t == Assert) + return "assert(" + render(n / Expr) + ")"; + if (t == Join) + return "join " + render(n / Expr); + if (t == Lock) + return "lock " + render(n / Var); + if (t == Unlock) + return "unlock " + render(n / Var); + if (t == Nop) + return "nop"; + if (t == Jump) + return "jump " + render(n / Const); + if (t == Cond) + return "if (" + render(n / Expr) + ") jump " + render(n / Const); + + // Fallback: original source span. + return std::string(n->location().view()); +} + +} // namespace lang + +} // namespace gitmem diff --git a/volatile.trieste b/volatile.trieste new file mode 100644 index 0000000..0897ebc --- /dev/null +++ b/volatile.trieste @@ -0,0 +1,27 @@ +gitmem +branching +(top + {} + (file 44:examples/accept/semantics/linear/volatile.gm|0|26 + (block |0|25 + { + @v1 = = + vtmp$0 = =} + (stmt |0|7 + (= |0|7 + (volatile |0|3:@v1) + (expr |6|1 + (const |6|1:1)))) + (stmt |16|3 + (= |16|3 + (reg 6:vtmp$0) + (expr |16|3 + (volatile |16|3:@v1)))) + (stmt |9|16 + (assert |9|16 + (expr |16|8 + (== |16|8 + (expr |16|3 + (reg 6:vtmp$0)) + (expr |23|1 + (const |23|1:1)))))))))