Feature/volatile - #18
Open
lukecheeseman wants to merge 16 commits into
Open
Conversation
There was a problem hiding this comment.
Pull request overview
This PR introduces volatile variables (@v) as acquire/release-style synchronization objects across the interpreter and memory models, expands execution-graph provenance/conflict metadata, and adds a TikZ (.tex) execution-graph output option alongside the existing Graphviz (.dot) output. It also updates the Python test harness to support per-model expectation overrides embedded in example files.
Changes:
- Add parsing/AST support for
@volatileidentifiers and implement volatile acquire (read) / release (write) behavior in the interpreter and both linear/branching memory models. - Extend execution traces/graphs and conflict objects to carry source-event provenance; add TikZ execution-graph printing and CLI format selection.
- Add/adjust example programs and test harness logic to accommodate model-dependent accept/reject outcomes.
Reviewed changes
Copilot reviewed 39 out of 40 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| test_gitmem.py | Add per-model expectation overrides via // expect ... directives. |
| src/tikz.hh | Declare TikZ execution-graph printer. |
| src/tikz.cc | Implement TikZ execution-graph rendering. |
| src/thread_trace.hh | Add volatile read/write trace events and unlock g-predecessor tracking. |
| src/sync_state.hh | Add VolatileSyncState interface. |
| src/passes/statements.cc | Allow Volatile token in assignment/value forms. |
| src/passes/expressions.cc | Allow Volatile token as an expression operand. |
| src/parser.cc | Tokenize @name as Volatile. |
| src/memory_model.hh | Add volatile sync ops + model hooks; add global lock ordering flag. |
| src/linear/version_store.cc | Include source events in conflicts. |
| src/linear/memory_model.hh | Add volatile hooks; rename push to pullpush; global lock ordering true. |
| src/linear/memory_model.cc | Implement volatile acquire/release and new pull/push split. |
| src/lang.hh | Add Volatile token and grammar support. |
| src/interpreter.hh | Include TikZ/linear headers for execution-graph printing decisions. |
| src/interpreter.cc | Implement volatile eval + tracing; add global lock ordering predecessor; TikZ output path. |
| src/graphviz.hh | Add visitor hooks for volatile read/write nodes. |
| src/graphviz.cc | Render volatile read/write nodes and sync edges in Graphviz output. |
| src/graph.hh | Add volatile graph node types; extend unlock with conflict + g-predecessor. |
| src/gitmem.cc | Add --format option and adjust default output extension. |
| src/execution_state.hh | Add Volatile object storage and global last-g-push tracking. |
| src/execution_state.cc | Implement get_volatile; include volatiles in global-state equality. |
| src/conflict.hh | Add conflict source-event provenance plumbing. |
| src/branching/lazy/version_store.cc | Include source events in conflicts. |
| src/branching/eager/version_store.cc | Include source events in conflicts; add <queue> include. |
| src/branching/base_version_store.hh | Add VolatileState for branching volatile release tracking. |
| src/branching/base_memory_model.hh | Add volatile acquire/release hooks; create volatile state. |
| src/branching/base_memory_model.cc | Implement volatile acquire/release semantics for branching models. |
| examples/reject/semantics/linear/volatile_sync_conflict.gm | New volatile conflict example (linear reject). |
| examples/reject/semantics/linear/volatile_sync_conflict_two_vars.gm | New volatile conflict example (linear reject). |
| examples/reject/semantics/linear/volatile_sync_communicate_volatile.gm | New volatile communication example (linear reject). |
| examples/reject/semantics/branching/volatile_sync_conflict.gm | New volatile conflict example (branching reject; lazy override). |
| examples/reject/semantics/branching/volatile_sync_communicate_volatile.gm | New volatile communication example (branching reject). |
| examples/accept/semantics/linear/volatile.gm | New basic volatile example (linear accept). |
| examples/accept/semantics/linear/volatile_sync.gm | New volatile sync example (linear accept). |
| examples/accept/semantics/linear/volatile_sync_communicate.gm | New volatile sync communication example (linear accept). |
| examples/accept/semantics/branching/volatile.gm | New basic volatile example (branching accept). |
| examples/accept/semantics/branching/volatile_sync.gm | New volatile sync example (branching accept). |
| examples/accept/semantics/branching/volatile_sync_conflict_two_vars.gm | New two-volatile example (branching accept). |
| CMakeLists.txt | Add src/tikz.cc to build. |
| .gitignore | Ignore additional local/editor artifacts and .dot outputs. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+380
to
+385
| // 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; |
Comment on lines
+112
to
+115
| if (output_path.empty()) { | ||
| std::string ext = (output_format == "tikz") ? ".tex" : ".dot"; | ||
| output_path = input_path.stem().replace_extension(ext); | ||
| } |
Comment on lines
+1
to
+9
| #include "tikz.hh" | ||
| #include "overloaded.hh" | ||
| #include <fstream> | ||
| #include <unordered_map> | ||
| #include <map> | ||
| #include <algorithm> | ||
| #include <optional> | ||
| #include <cstdio> | ||
|
|
Comment on lines
+162
to
+166
| auto is_sync_node = [](const Node* nd) -> bool { | ||
| return dynamic_cast<const Start*>(nd) || dynamic_cast<const End*>(nd) | ||
| || dynamic_cast<const Spawn*>(nd) || dynamic_cast<const Join*>(nd) | ||
| || dynamic_cast<const Lock*>(nd) || dynamic_cast<const Unlock*>(nd); | ||
| }; |
Comment on lines
+196
to
+207
| } else if (auto* nd = dynamic_cast<const Write*>(n)) { | ||
| ev.label = "W(" + latex_escape(nd->var) + "$_{" + std::to_string(tid) + "}$) = " + std::to_string(nd->value); | ||
| } else if (auto* nd = dynamic_cast<const Read*>(n)) { | ||
| std::visit(overloaded{ | ||
| [&](const Read::SuccessfulRead& sr) { | ||
| 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) + "$_{" + std::to_string(tid) + "}$) = ?"; | ||
| ev.is_conflict = true; | ||
| } | ||
| }, nd->read_result); |
Comment on lines
+723
to
+731
| } else if (dynamic_cast<const Start*>(ev.node)) { | ||
| // g: start pulls | ||
| if (has_g_lane) | ||
| f << "\\draw[link oneway] (laneG |- " << ev.name << ") -- (" << ev.name << ");\n"; | ||
| } else if (dynamic_cast<const End*>(ev.node)) { | ||
| // g: end pulls + pushes | ||
| if (has_g_lane) | ||
| f << "\\PullPush{(" << ev.name << ")}{(laneG |- " << ev.name << ")}\n"; | ||
| } |
Comment on lines
174
to
183
| 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); } |
EliasC
approved these changes
Jul 22, 2026
EliasC
left a comment
EliasC
left a comment
Contributor
There was a problem hiding this comment.
LGTM. Let's see if copilot finds anything
Contributor
There was a problem hiding this comment.
Duplicate of examples/accept/semantics/linear/volatile_sync.gm
Contributor
There was a problem hiding this comment.
Duplicate of examples/reject/semantics/linear/volatile_sync_conflict.gm
…te statements to allow for correct schuedling decisions in the model explorer. Correct some missing volatile wf trieste info, and render the dump correctly
…te temporaries to allow for the multiple scheduling points. This includes re-rerendering the original line and rendering the new line in the explorer output
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.