gitmem

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.

Overview

Gitmem is a research tool that models concurrent memory operations using version control semantics. It provides:

• Multiple memory models: 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

The gitmem language supports:

• 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

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

mkdir build
cd build
cmake -G Ninja .. -DCMAKE_CXX_COMPILER=clang++ -DCMAKE_BUILD_TYPE=Debug
ninja

Optional CMake flags:

• -DCMAKE_CXX_STANDARD=23 - Set C++ standard (if needed)
• -DCMAKE_BUILD_TYPE=Release - Build optimized version

Quick Test

Test your build with:

./gitmem -e ../examples/race_condition.gm

Usage

Basic Execution

Run a single execution trace:

./gitmem examples/race_condition.gm

This generates a GraphViz .dot file showing the execution trace.

Model Checking Mode

Explore all possible execution paths:

./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:

./gitmem -i examples/race_condition.gm

Commands in interactive mode:

• ? - Show help
• s <tid> - Step thread <tid> to its next scheduling point
• <tid> - Shortcut for stepping thread <tid>
• l - List current threads and state
• f - Finish execution automatically
• r - Restart from the beginning
• g - Toggle automatic graph printing
• p - Print graph immediately
• q - Quit interactive mode

Memory Models

Gitmem supports different memory models:

Linear (Default)

./gitmem --sync linear program.gm

Multi-version concurrency control like consistency model. Threads operate in isolation and synchronisation pulls from and pushes to a global shared version history. Each variable is versioned throughout its history.

Branching (Eager)

./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)

./gitmem --sync branching --branching-mode lazy program.gm

Lazy conflict detection variant that defers checking until variables are read.

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:

# 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 and CLI
├── lang.hh - Language/token definitions (+ entry_block helper)
├── parser.cc - Parser implementation
├── interpreter.cc - Interpreter core
├── model_checker.cc - Model checking engine
├── debugger.cc - Interactive debugger
├── execution_state.hh - Runtime state (threads, locks, model state)
├── memory_model.hh - Memory model interface
├── linear/
│ ├── memory_model.hh/.cc - Linear memory model
│ └── version_store.hh/.cc
└── branching/
├── base_memory_model.hh/.cc
├── base_version_store.hh/.cc
├── eager/memory_model.hh - Eager branching model
└── lazy/memory_model.hh - Lazy branching model
examples/
├── accept/ - Passing test inputs
└── reject/ - Failing test inputs

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. Use it to inspect the AST:

./gitmem_trieste build program.gm
# Creates program.trieste with S-expression AST

VSCode Extension

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:

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