Feature/linear and branching

CMakeLists.txt

@@ -14,14 +14,23 @@ FetchContent_MakeAvailable(trieste)
 set(CMAKE_CXX_STANDARD 23)
 set(CMAKE_CXX_STANDARD_REQUIRED True)
 
+include_directories(src)
+
 add_executable(gitmem
   src/gitmem.cc
   src/reader.cc
   src/parser.cc
+  src/execution_state.cc
   src/passes/expressions.cc
   src/passes/statements.cc
   src/passes/check_refs.cc
   src/passes/branching.cc
+  src/linear/sync_protocol.cc
+  src/linear/version_store.cc
+  src/branching/base_sync_protocol.cc
+  src/branching/base_version_store.cc
+  src/branching/lazy/version_store.cc
+  src/branching/eager/version_store.cc
   src/interpreter.cc
   src/debugger.cc
   src/model_checker.cc

README.md

@@ -1,48 +1,231 @@
 # gitmem
 
-Experimental interpreter for creating execution diagrams for a new
-concurrency model.
+An experimental interpreter and model checker for exploring concurrent programs with Git-inspired memory semantics. Gitmem allows you to write multi-threaded programs and automatically explore all possible interleavings to detect data races, deadlocks, and assertion failures.
 
-## Building and Running
+## Overview
+
+Gitmem is a research tool that models concurrent memory operations using version control semantics. It provides:
+
+- **Multiple sync protocols**: Linear and branching (with eager/lazy variants) semantics for thread synchronization
+- **Automatic model checking**: Explores all possible execution paths to find concurrency bugs
+- **Interactive debugging**: Step through different thread schedules interactively
+- **Execution visualization**: Generates GraphViz diagrams showing execution traces and revision graphs
+
+## Language Features
 
-To build you need CMake and Ninja. CMake will fetch any other dependencies.
+The gitmem language supports:
 
-The following commands should set you up:
+- **Shared variables**: `x = value` (global shared state)
+- **Thread-local registers**: `$r = value` (prefixed with `$`)
+- **Thread operations**: `spawn { ... }`, `join $thread`
+- **Synchronization**: `lock var`, `unlock var`
+- **Control flow**: `if (condition) { ... } else { ... }`
+- **Assertions**: `assert(condition)`
+- **Operators**: `==`, `!=`, `+`
 
+### Example Program
+
+```gitmem
+x = 0;
+$t1 = spawn {
+    lock l;
+    x = x + 1;
+    unlock l;
+};
+$t2 = spawn {
+    lock l;
+    x = x + 1;
+    unlock l;
+};
+join $t1;
+join $t2;
+assert(x == 2);
 ```
+
+## Building and Running
+
+### Prerequisites
+
+- CMake (3.14+)
+- Ninja build system
+- C++23 compatible compiler (Clang recommended)
+- Python 3 (for tests)
+
+### Build Instructions
+
+```bash
 mkdir build
 cd build
 cmake -G Ninja .. -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug
 ninja
 ```
 
-If you need, set the C standard with `-DCMAKE_CXX_STANDARD=20`.
-If you are running a recent version of CMake, you may need
-`-DCMAKE_POLICY_VERSION_MINIMUM=3.5`.
+Optional CMake flags:
+- `-DCMAKE_CXX_STANDARD=23` - Set C++ standard (if needed)
+- `-DCMAKE_BUILD_TYPE=Release` - Build optimized version
 
-You can test if the build was successful by running the following
-command in the `build` directory:
+### Quick Test
 
-```
+Test your build with:
+
+```bash
 ./gitmem -e ../examples/race_condition.gm
 ```
 
-The build script creates two executables:
+## Usage
+
+### Basic Execution
+
+Run a single execution trace:
+
+```bash
+./gitmem examples/race_condition.gm
+```
+
+This generates a GraphViz `.dot` file showing the execution trace.
+
+### Model Checking Mode
+
+Explore all possible execution paths:
+
+```bash
+./gitmem -e examples/race_condition.gm
+```
+
+Model checking will:
+- Try all possible thread interleavings
+- Report data races, deadlocks, and assertion failures
+- Generate execution diagrams for failing traces
+- Exit with status 0 if all paths succeed, non-zero if any fail
+
+### Interactive Mode
+
+Step through executions manually:
+
+```bash
+./gitmem -i examples/singleton.gm
+```
+
+Commands in interactive mode:
+- `?` - Show help
+- `s` - Show current state
+- `n` - Step one thread forward
+- `r` - Run to next synchronization point
 
-- `gitmem` parses source code and runs the interpreter in order to
-  create an execution diagram (work in progress). You can run the
-  interpreter interactively with the `-i` flag, and automatically
-  explore all possible traces with the `-e` flag (showing failing
-  runs).
-- `gitmem_trieste` is the default
-  [Trieste](https://github.com/microsoft/Trieste) driver which can
-  be used to inspect the parsed source code and test the parser.
-  Running `gitmem_trieste build foo.gm` will create a file
-  `foo.trieste` with the parsed source code as an S-expression.
+### Sync Protocols
+
+Gitmem supports different memory models:
+
+#### Linear (Default)
+```bash
+./gitmem --sync linear program.gm
+```
+Traditional sequential consistency model.
+
+#### Branching (Eager)
+```bash
+./gitmem --sync branching --branching-mode eager program.gm
+```
+Git-like branching semantics where threads create branches that merge at synchronization points. Conflicts are detected eagerly.
+
+#### Branching (Lazy)
+```bash
+./gitmem --sync branching --branching-mode lazy program.gm
+```
+Lazy conflict detection variant that defers checking until synchronization.
+
+Additional flags:
+- `--include-empty-commits` - Include empty commits in branching output
+- `--raise-early-conflicts` - Raise conflicts before write suppression (lazy mode only)
+- `-v, --verbose` - Enable verbose interpreter output
+- `-o, --output <file>` - Specify output file path
+
+## Testing
+
+Run the test suite:
+
+```bash
+# From build directory
+ninja run_gitmem_tests
+
+# Or using CTest
+ctest
+```
+
+The test suite includes:
+- **Accept tests**: Programs that should execute successfully
+- **Reject tests**: Programs with errors (deadlocks, races, assertion failures)
+- Tests for both linear and branching semantics
+
+## Project Structure
+
+```
+src/
+  ├── gitmem.cc              - Main entry point
+  ├── lang.hh                - Language token definitions
+  ├── parser.cc              - Parser implementation
+  ├── interpreter.cc         - Interpreter core
+  ├── model_checker.cc       - Model checking engine
+  ├── debugger.cc            - Interactive debugger
+  ├── execution_state.hh     - Thread and memory state
+  ├── sync_protocol.hh       - Sync protocol interface
+  ├── linear/                - Linear sync protocol
+  └── branching/             - Branching sync protocols
+      ├── base_sync_protocol.cc
+      ├── eager/             - Eager conflict detection
+      └── lazy/              - Lazy conflict detection
+
+examples/
+  ├── accept/semantics/      - Valid programs
+  │   ├── linear/            - Linear semantics tests
+  │   └── branching/         - Branching semantics tests
+  └── reject/semantics/      - Programs with bugs
+      ├── linear/            - Deadlocks, races for linear
+      └── branching/         - Bugs for branching semantics
+```
+
+## Executables
+
+The build produces two binaries:
+
+### `gitmem`
+The main interpreter and model checker. Executes programs and generates execution diagrams.
+
+### `gitmem_trieste`
+Parser diagnostic tool built on [Trieste](https://github.com/microsoft/Trieste). Use it to inspect the AST:
+
+```bash
+./gitmem_trieste build program.gm
+# Creates program.trieste with S-expression AST
+```
 
 ## VSCode Extension
 
-You should be able to use `Developer: Install Extension from
-Location` in the VSCode command palette to install a rudimentary
-extension in the `gitmem-extension` directory and get syntax
-highlighting..
+A syntax highlighting extension is available in `gitmem-extension/`.
+
+Install via:
+1. Open VSCode Command Palette (`Cmd+Shift+P` / `Ctrl+Shift+P`)
+2. Run: `Developer: Install Extension from Location`
+3. Select the `gitmem-extension` directory
+
+This provides syntax highlighting for `.gm` files.
+
+## Output
+
+Gitmem generates GraphViz `.dot` files visualizing:
+
+- **Execution traces**: Thread operations and memory states
+- **Revision graphs**: For branching semantics, shows branch/merge structure
+- **Conflict detection**: Highlights data races and conflicts
+
+View `.dot` files with GraphViz:
+
+```bash
+dot -Tpng output.dot -o output.png
+```
+
+## Exit Codes
+
+- `0` - All execution paths succeeded
+- `1` - Assertion failure, deadlock, data race, or error detected
+- Other non-zero codes indicate internal errors

examples/passing/semantics/conditional_non_race.gm → examples/accept/semantics/branching/conditional_non_race.gm

@@ -12,6 +12,7 @@ $t2 = spawn {
 };
 join $t1;
 join $t2;
+// FIXME in branching these assertions are always true, but not in linear
 assert (x != 0);
 assert (y != 0);
 assert (x == y);

examples/passing/semantics/join_pulled_variable.gm → examples/accept/semantics/branching/join_pulled_variable.gm

@@ -9,6 +9,7 @@ t = spawn {
   };
   assert(x == 2);
 };
+assert (x == 0);
 join t;
 assert (x == 2);
 join t2;

examples/accept/semantics/branching/lock_relock_as_sync.gm

@@ -0,0 +1,11 @@
+x = 0;
+$t = spawn {
+  lock l1;
+  x = 42;
+  unlock l1;
+};
+lock l1;
+x = 2;
+unlock l1;
+lock l1;
+unlock l1;

examples/accept/semantics/branching/singleton.gm

@@ -0,0 +1,41 @@
+// Construct the singleton pattern:
+// A shared variable should be initialised only once by any thread
+// Once initialised all threads should read the same value
+// Perform the initialisation using double checked locking
+// Each thread:
+//  1.    Checks the variable
+//  1a.   If it is uninitialised (here we use 0), then take the lock
+//  1b.   Taking the lock may pull in other thread updates, so check if the
+//        variable is still uninitialised
+//  1bi.  If the variable is still uninitialised then we know we need to
+//        initialise it. So do that and store the initialised value in a local
+//        var.
+//  1bii. Otherwise the variable was initialised and we can read the value
+//  2a.   Otherwise the variable was initialised and we can read the value
+//  3.    Check that in all code paths we read the expected initialised value
+
+instance = 0;
+
+$t1 = spawn {
+  if (instance == 0) {
+    lock l;
+    if (instance == 0) {
+      instance = 100;
+    }
+    unlock l;
+  }
+  assert(instance == 100);
+};
+
+
+if (instance == 0) {
+  lock l;
+  if (instance == 0) {
+    instance = 100;
+  }
+  unlock l;
+}
+assert(instance == 100);
+
+join $t1;
+assert(instance == 100);

examples/accept/semantics/linear/addition.gm

@@ -0,0 +1,4 @@
+$r1 = 1;
+x = 2;
+y = $r1 + x;
+assert(y + 1 != x + 1);

examples/accept/semantics/linear/conditional_non_race.gm

@@ -0,0 +1,18 @@
+x = 0;
+y = 0;
+$t1 = spawn {
+    if (x == 0) {
+        y = 1;
+    }
+};
+$t2 = spawn {
+    if (y == 0) {
+        x = 1;
+    }
+};
+join $t1;
+join $t2;
+
+// We don't know the interleaving of the two threads, but we know that they won't conflict,
+// and that the reads are reading consistent values.
+// We can get all of x = 0,  y = 1; x = 1, y = 0; or x = 1, y = 1; but we won't get x = 0, y = 0.

examples/accept/semantics/linear/globals.gm

@@ -0,0 +1,5 @@
+nop;
+x = 0;
+x = 2;
+y = 2;
+assert(x == y);

examples/accept/semantics/linear/if.gm

@@ -0,0 +1,13 @@
+$r = 0;
+x = 0;
+if ($r == 0) {
+    x = x + 1;
+} else {
+    x = 0;
+}
+if ($r == 1) {
+    x = 0;
+} else {
+    x = x + 1;
+}
+assert (x == 2);