Synapse

Synapse

Decoupling Protocol, Topology, and Policy for Automated Synthesis of Coherence Controllers

Read the paper Get the code Run the artifact Watch the demo
ProtocolMESI
TopologyL1 + L2 + LLC
Policyinclusive, write-back
Synapse
Simulated controllersSLICC for gem5
Available
Hardware controllersvia Chipyard
WIP
Write the three specs once. Synapse composes them into verified controllers; a different design means changing one spec, not rewriting a controller.

Why

Every new architecture needs new coherence controllers: a second socket, an accelerator, a CXL memory pool. Today each one is written by hand, as a state machine full of transient states, and then debugged and verified on its own. The protocol, the place in the hierarchy and the cache policy are tangled together in the same code, so changing one of them means starting over.

Synapse keeps the three apart. You write them once, and recombine them for every new design.

How it works

Every coherence controller, whatever its protocol and wherever it sits, reduces to three state machines. The protocol spec provides the client and the manager, the policy spec provides the policy, and the topology spec only says where each controller sits: who is its parent, who are its children.

Client

Asks its parent for data and permissions, like a cache.

Manager

Tracks what its children hold, like a directory.

Policy

Decides when to allocate, update or replace a block.

The three machines speak different languages, and at a bridge the child may speak MESI while the parent speaks CXL. Synapse labels every state and request, in any protocol, with one tuple, ⟨Permission, Data, Coherence⟩, then fuses the transitions whose labels match. The result is one concrete controller, transient states included.

The compiler

  1. Specs

    Written in the Synapse DSL.

    protocoltopologypolicy

  2. Synthesis

    Builds every controller in the topology, then checks deadlock freedom with Murφ and memory consistency with litmus tests.

  3. Code generation

    Emits SLICC controllers and the gem5 simulation setup.

  4. gem5

    Run and measure the design like any hand-written protocol.

Try it

Generate controllers for your own hierarchy with the Synapse generator, or reproduce every experiment in the paper with the artifact.

Generate controllers

git clone https://github.com/NicCarp11/Synapse
cd Synapse
pip install -r requirements.txt
python synapse.py generate specs/topologies/smp.yaml --out out/smp

Python 3.10 or newer. generate writes the SLICC controllers and the gem5 setup of the system; verify model-checks them with CMurphi.

Reproduce the paper

Start with the prebuilt Docker image; the functional test finishes in under a minute.

git clone https://github.com/TUM-DSE/Synapse
cd Synapse
docker pull carpeniem/synapse-artifact-s1_2_3:prebuilt
just shell-s1_2_3-prebuilt

# inside the container
./S1_2_3_experiments/scripts/run-functional.sh

Any x86-64 machine with Docker. Plan for about 12 GB of RAM per concurrent simulation. just is optional: every shortcut maps to a script in the repository.

ACM badge: Artifacts Available v1.1 ACM badge: Artifacts Evaluated, Functional v1.1 ACM badge: Results Reproduced v1.1

Four scenarios from the paper

SMP

Synthesized controllers against gem5's hand-written ones.

On-core
MESIMOESI
Off-core
single node
just fig8Fig. 8 · gem5 v23

NUMA

Which off-core protocol to use across four sockets.

On-core
MESI
Off-core
MESIMOESIMESIF incl.MESIF excl.
just fig9Fig. 9 · gem5 v23

Multi-host CXL

Which protocol the bridge between hosts should speak, on YCSB-C.

On-core
MESI
Off-core
MESIMOESIMESIFCXL
just fig10Fig. 10 · gem5 v23

Heterogeneous chiplets

Write-back against write-through accelerator chiplets.

On-core
MESI-RC
Off-core
MESICXL
Policy
WBWT
just fig11Fig. 11 · gem5 v20

The chiplet scenario runs on its own image, carpeniem/synapse-artifact-s4.

Build on Synapse

Synapse is meant to grow with the people who use it. Every protocol, topology, policy or back end added once composes with everything already there.

Use it

Generate controllers for your own hierarchy, or reproduce the paper with the artifact.

Extend it

Add a protocol, a topology, a policy or a new back end. Hardware controllers through Chipyard are work in progress.

Cite Synapse

Nicolo Carpentieri, Anatole Lefort, David Schall, Julian Pritzi, Pramod Bhatotia. Decoupling Protocol, Topology, and Policy for Automated Synthesis of Coherence Controllers. MICRO 2026, Athens, Greece.

@inproceedings{carpentieri2026synapse,
  title     = {Decoupling Protocol, Topology, and Policy for
               Automated Synthesis of Coherence Controllers},
  author    = {Carpentieri, Nicolo and Lefort, Anatole and Schall, David
               and Pritzi, Julian and Bhatotia, Pramod},
  booktitle = {Proceedings of the 59th IEEE/ACM International
               Symposium on Microarchitecture (MICRO)},
  year      = {2026},
  address   = {Athens, Greece}
}

People

Systems Research Group, Technical University of Munich