Creating a new visualisation to create tikz diagrams

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

src/branching/eager/version_store.cc

@@ -2,6 +2,7 @@
 #include "debug.hh"
 #include "thread_trace.hh"
 
+#include <queue>
 #include <unordered_set>
 
 namespace gitmem {
@@ -156,7 +157,9 @@ std::optional<Conflict> 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;
     }
   }

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;
 }

src/conflict.hh

@@ -1,11 +1,14 @@
 #pragma once
 
 #include <iostream>
+#include <memory>
 #include <optional>
 #include <string>
 
 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<FileLocation, FileLocation> source_locations() const = 0;
+  virtual std::pair<std::shared_ptr<Event>, std::shared_ptr<Event>> 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<VersionID, FileLocation> version_a;
   std::pair<VersionID, FileLocation> version_b;
+  std::shared_ptr<Event> source_event_a;
+  std::shared_ptr<Event> source_event_b;
 
   Conflict(std::string var,
            std::pair<VersionID, FileLocation> version_a,
-           std::pair<VersionID, FileLocation> version_b)
-      : var(std::move(var)), version_a(std::move(version_a)), version_b(std::move(version_b)) {}
+           std::pair<VersionID, FileLocation> version_b,
+           std::shared_ptr<Event> source_event_a = nullptr,
+           std::shared_ptr<Event> 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<Event>, std::shared_ptr<Event>> 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;

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<Event> last_g_push_event = nullptr;
+
   // AST evaluation cache
   lang::NodeMap<size_t> cache;
 

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;
 

src/graph.hh

@@ -144,8 +144,12 @@ struct Lock : Node {
 
 struct Unlock : Node {
   const std::string var;
+  const std::optional<Conflict> conflict;
+  std::shared_ptr<const Node> g_predecessor;
 
-  Unlock(const std::string var) : var(var) {}
+  Unlock(const std::string var, std::optional<Conflict> conflict = std::nullopt,
+         std::shared_ptr<const Node> g_predecessor = nullptr)
+      : var(var), conflict(conflict), g_predecessor(g_predecessor) {}
 
   void accept(Visitor *v) const override { v->visitUnlock(this); }
 };

src/interpreter.cc

@@ -306,13 +306,20 @@ std::variant<int, TerminationStatus> 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,14 +339,17 @@ std::variant<int, TerminationStatus> 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);
     }
 
     // lock.globals = ctx.globals;
     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;
 
@@ -627,9 +637,22 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() {
   // Track join nodes that need fixing up after all threads are processed
   std::vector<std::shared_ptr<graph::Join>> joins_to_fix;
 
+  // Track join conflict source fixups: (join node, conflict base carrying source events)
+  std::vector<std::pair<std::shared_ptr<graph::Join>, std::shared_ptr<ConflictBase>>> join_conflict_fixups;
+
   // Track read nodes that need their source fixed up
   std::vector<std::pair<std::shared_ptr<graph::Read>, std::shared_ptr<Event>>> 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::pair<std::shared_ptr<graph::Lock>, std::shared_ptr<Event>>> locks_ordered_after_fixups;
+
+  // Track conflicting unlock nodes whose g_predecessor must be resolved after all threads.
+  std::vector<std::pair<std::shared_ptr<graph::Unlock>, std::shared_ptr<Event>>> unlocks_g_predecessor_fixups;
+
+  // Track unlock conflict source fixups: (unlock node, conflict base carrying source events)
+  std::vector<std::pair<std::shared_ptr<graph::Unlock>, std::shared_ptr<ConflictBase>>> unlock_conflict_fixups;
+
   // Map from trace events to graph nodes
   std::unordered_map<std::shared_ptr<Event>, std::shared_ptr<graph::Node>> event_to_node;
 
@@ -655,6 +678,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<bool> 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 +701,7 @@ graph::ExecutionGraph Interpreter::build_execution_graph_from_traces() {
           auto node = std::make_shared<graph::End>();
           link_in_program_order(tid, node);
           event_to_node[event] = node;
+          thread_has_end[tid] = true;
         },
         [&](const WriteEvent& arg) {
           auto node = std::make_shared<graph::Write>(arg.var, arg.value, tid);
@@ -705,43 +733,46 @@ 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<graph::Conflict> 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<graph::Join>(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;
         },
         [&](const LockEvent& arg) {
-          // Link to the last unlock event using the event-to-node mapping
-          std::shared_ptr<graph::Node> 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<graph::Conflict> conflict;
           if (arg.maybe_conflict) {
-            // Mark as conflicting with the lock name
             conflict = graph::Conflict(arg.lock_name);
           }
-          auto node = std::make_shared<graph::Lock>(arg.lock_name, ordered_after, conflict);
+          // ordered_after may reference another thread's unlock; defer resolution.
+          auto node = std::make_shared<graph::Lock>(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<graph::Unlock>(arg.lock_name);
+          std::optional<graph::Conflict> unlock_conflict;
+          if (arg.maybe_conflict) {
+            unlock_conflict = graph::Conflict(arg.maybe_conflict->object_name());
+          }
+          auto node = std::make_shared<graph::Unlock>(arg.lock_name, unlock_conflict);
+          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;
-
-          // Mark conflict if present
-          if (arg.maybe_conflict) {
-            // TODO: Visualize unlock conflicts
-          }
         },
         [&](const AssertEvent& arg) {
           auto node = std::make_shared<graph::Assertion>(arg.condition, arg.pass);
@@ -751,8 +782,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);
@@ -766,13 +798,48 @@ 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<std::shared_ptr<const graph::Node>&>(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;
     // thread_tails[joinee_tid] now points to the end (or pending) of that thread
     const_cast<std::shared_ptr<const graph::Node>&>(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<graph::Node> 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<graph::Conflict&>(*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<graph::Node> 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<graph::Conflict&>(*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");
@@ -784,8 +851,14 @@ 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") {
+    bool linear_mode = dynamic_cast<linear::LinearMemoryModel*>(gctx.model.get()) != nullptr;
+    graph::TikzPrinter tikz;
+    tikz.print(exec_graph, output_path, linear_mode);
+  } else {
+    graph::GraphvizPrinter gv(output_path);
+    gv.visit(exec_graph.entry.get());
+  }
 }
 
 int interpret(const Node ast, const std::filesystem::path &output_path,

src/interpreter.hh

@@ -3,6 +3,8 @@
 #include "execution_state.hh"
 #include "graph.hh"
 #include "graphviz.hh"
+#include "tikz.hh"
+#include "linear/memory_model.hh"
 #include "lang.hh"
 #include "progress_status.hh"
 #include <trieste/trieste.h>

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<ThreadSyncState> make_thread_state(ThreadID tid) const override {
     return std::make_unique<LocalVersionStore>(tid);
   }

src/linear/version_store.cc

@@ -97,7 +97,9 @@ std::optional<Conflict> 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;