Feature/volatile

.gitignore

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

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
@@ -49,6 +50,7 @@ add_executable(gitmem
   src/debugger.cc
   src/model_checker.cc
   src/graphviz.cc
+  src/tikz.cc
 )
 
 add_executable(gitmem_trieste
@@ -58,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
 )
 

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

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,10 @@
+// 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;
+  @v = 1;
+};
+x = 2;
+@v = 2;

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;

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;

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;

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,71 @@ 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 -- 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> 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.
+  return std::nullopt;
+}
+
+std::optional<std::shared_ptr<ConflictBase>>
+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();
+
+  // 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> conflict = store.merge_with_commit(vstate.commit)) {
+      return std::make_shared<BranchingConflict>(*conflict);
+    }
+  }
+
+  // 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<Conflict>(&probe))
+    return std::make_shared<BranchingConflict>(*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;
+
+  return std::nullopt;
+}
+
 std::string BranchingMemoryModelBase::build_revision_graph_dot(
     const std::vector<const ThreadSyncState*>& thread_states) const {
 
@@ -142,6 +208,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 {
@@ -119,6 +120,13 @@ std::optional<Conflict> 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<std::shared_ptr<const Commit>, bool> ff_memo;
+  if (can_reach(head, commit, ff_memo))
+    return std::nullopt;
+
   // Find lowest common ancestor of the two heads
   std::shared_ptr<const Commit> lca = find_lowest_common_ancestor(head, commit);
   verbose::out << "found lca of "
@@ -144,10 +152,12 @@ std::optional<Conflict> 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<WriteEvent>(&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<WriteEvent>(&it->second.source_event->data))
+      return we->location;
+    // Volatile writes can race (write-write with no happens-before).
+    if (auto* vwe = std::get_if<VolatileWriteEvent>(&it->second.source_event->data))
+      return vwe->location;
+    throw std::logic_error("conflicting source event is not a write");
   };
   std::optional<Conflict> conflict;
   for (const auto& [obj, commit_a] : branch_a) {
@@ -156,7 +166,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;
     }
   }