Feature/volatile

.gitignore

@@ -31,3 +31,7 @@
 *.out
 *.app
 build
+
+*.DS_Store
+*.vscode
+*.dot

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

examples/accept/semantics/branching/volatile.gm

@@ -0,0 +1,2 @@
+@v1 = 1;
+assert(@v1 == 1);

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;

examples/accept/semantics/branching/volatile_sync.gm

@@ -0,0 +1,5 @@
+@v = 2;
+$t = spawn {
+  assert(@v == 2);
+};
+assert(@v == 2);

examples/accept/semantics/branching/volatile_sync_conflict_two_vars.gm

@@ -0,0 +1,7 @@
+
+$t = spawn {
+  x = 1;
+  @v1 = 1;
+};
+x = 2;
+@v2 = 2;

examples/accept/semantics/linear/volatile.gm

@@ -0,0 +1,2 @@
+@v1 = 1;
+assert(@v1 == 1);

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;

examples/accept/semantics/linear/volatile_sync.gm

@@ -0,0 +1,5 @@
+@v = 2;
+$t = spawn {
+  assert(@v == 2);
+};
+assert(@v == 2);

examples/accept/semantics/linear/volatile_sync_communicate.gm

@@ -0,0 +1,5 @@
+@v = 2;
+$t = spawn {
+  assert(@v == 2);
+};
+assert(@v == 2);

examples/reject/semantics/branching/volatile_sync_communicate_volatile.gm

@@ -0,0 +1,5 @@
+@v = 2;
+$t = spawn {
+  @v = 41;
+};
+assert(@v == 2);

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;

examples/reject/semantics/linear/volatile_sync_communicate_volatile.gm

@@ -0,0 +1,5 @@
+@v = 2;
+$t = spawn {
+  @v = 41;
+};
+assert(@v == 2);

examples/reject/semantics/linear/volatile_sync_conflict.gm

@@ -0,0 +1,7 @@
+
+$t = spawn {
+  x = 1;
+  @v = 1;
+};
+x = 2;
+@v = 2;

examples/reject/semantics/linear/volatile_sync_conflict_two_vars.gm

@@ -0,0 +1,7 @@
+
+$t = spawn {
+  x = 1;
+  @v1 = 1;
+};
+x = 2;
+@v2 = 2;

src/branching/base_memory_model.cc

@@ -1,5 +1,6 @@
 #include "base_memory_model.hh"
 #include "overloaded.hh"
+#include <stdexcept>
 #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<VolatileState&>(*v.sync);
+}
+
+std::optional<std::shared_ptr<ConflictBase>>
+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> conflict = store.merge_with_commit(vstate.commit)) {
+      return std::make_shared<BranchingConflict>(*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<std::shared_ptr<ConflictBase>>
+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> conflict = store.merge_with_commit(vstate.commit)) {
+      return std::make_shared<BranchingConflict>(*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<const ThreadSyncState*>& 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:

src/branching/base_memory_model.hh

@@ -42,6 +42,13 @@ public:
   std::optional<std::shared_ptr<ConflictBase>>
   on_unlock(ThreadContext &thread, Lock &lock) override;
 
+  std::optional<std::shared_ptr<ConflictBase>>
+  on_volatile_read(ThreadContext &thread, Volatile &v) override;
+
+  std::optional<std::shared_ptr<ConflictBase>>
+  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<const ThreadSyncState*>& thread_states) const override;
@@ -51,6 +58,10 @@ public:
   std::unique_ptr<LockSyncState> make_lock_state() const override {
     return std::make_unique<LockState>();
   }
+
+  std::unique_ptr<VolatileSyncState> make_volatile_state() const override {
+    return std::make_unique<VolatileState>();
+  }
 };
 
 } // end branching

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<const branching::Commit> 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

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;