Porcupine: a linearizability checker whose input is a Go function

The specification is two functions, not a DSL

Porcupine takes a sequential specification as executable Go code along with a concurrent history, and decides whether the history is linearizable with respect to that specification. The specification is a porcupine.Model with two required pieces and one optional. Init returns the initial state. Step takes a state, an input and an output and returns whether the operation was legal plus the new state. Hash computes a hash of a state and is optional, with the comment that it improves performance. The register example in the README initialises to 0, accepts any put as always legal, and accepts a get only when the output equals the current state, leaving the state unchanged. There is no modelling language to learn, and the model is ordinary Go that your editor understands and your tests can exercise.

Events versus operations, two ways to feed it a history

History can be specified two ways, and the README is clear about what each is. As a list of operations with given call and return times, which is what CheckOperations consumes, or as a list of call and return events in time order, which is what CheckEvents consumes. The event form is what Jepsen style output looks like once you have flattened it: each Event carries a Kind of CallEvent or ReturnEvent, a Value, an Id and a ClientId, and the checker reconstructs the operations by matching ids. That reconstruction is why ClientId exists: real time ordering interleaves operations from several clients, and a history without client identity cannot be checked for per-client program order at all.

One boolean, and a counterexample you can look at

The interface is a single call. In the README's first example the history is linearizable and CheckEvents returns true: a put of 100 overlaps with two gets, one returning 100 and one returning 0, which can be linearized with the zero read before the put. The second history is not linearizable and the checker returns false: a get returns 200 while the put of 200 is still in flight, and a later get returns 0 with no write in between to explain it. That second case is the value of the tool. When a Jepsen run finds an anomaly you can hand the history to the checker with your model and get a definitive answer about whether your service violated linearizability or whether your model was wrong.

P-compositionality is the reason for the speed claim

Porcupine implements the algorithm described in Faster linearizability checking via P-compositionality, which is an optimization of the algorithm in the original Testing for Linearizability paper. The practical effect is stated as a measurement: testing on the data in test_data/jepsen/, Porcupine is generally 1,000x to 10,000x faster than Knossos's linearizability checker with a much smaller memory footprint, and on histories where it can take advantage of P-compositionality it can be millions of times faster. Two things to hold onto. The comparison is against one named tool on one corpus, in this project and in Knossos's own framing, and the millions of times case is conditional on the structure of the history. For a linearizability checker, deciding a history is not linearizable is often the easy direction and the hard histories are the legal ones, which is exactly where a search space reduction matters.

Visualize turns a false into a diagram

Porcupine also implements a visualizer for histories and linearization points. The Visualize function is documented alongside CheckOperations and CheckEvents, and the README says it can visualize a history along with partial linearizations, which may aid in debugging. That phrase is doing real work: a partial linearization is the checker's best effort so far, so what you get to look at is not a proof but the point where the search got stuck. The repository has a visualization.go and a visualization/ directory with their own test file, plus hosted interactive examples linked from the README, so the output is meant to be looked at rather than read as text. For a team whose Jepsen failures currently get pasted into an issue as a wall of timestamps, this is the part that changes the workflow.

go.mod declares go 1.16, and the source is six files

It is an ordinary Go module with no dependencies, so adding it to a checker is the standard fetch:

go get github.com/anishathalye/porcupine

The dependency story is unusually simple: module github.com/anishathalye/porcupine and go 1.16, with nothing in require. The root listing explains why: bitset.go, checker.go, model.go, porcupine.go and visualization.go sit next to porcupine_test.go and visualization_test.go, so the library is small enough to read end to end. A checker that decides whether your storage layer is correct is exactly the kind of code where reading it is a reasonable alternative to trusting it, and here that option exists. The floor of go 1.16 is old in the other direction, though: it means the module claims compatibility with a language generation that nothing else in your build probably supports, so check what that does to your toolchain pinning before you depend on it.

Against Knossos and against reading the trace

The obvious alternative is Knossos, which is where Porcupine positions itself and where the speed comparison is drawn. The difference in approach is the optimisation: both solve the same problem from the same lineage of papers, and Porcupine's contribution is a faster search over histories that decompose well. That matters most when you are checking continuously in CI rather than occasionally after a failed run, since the cost per check falls by orders of magnitude on the common shapes. The other alternative is to not check at all and read the trace, which works until a history has a hundred thousand operations and a human is looking for the one operation that broke ordering. A third option is a model checker written per service, which is what this is: the general part is solved, the specification is yours.

Editorial conclusion

Porcupine fits a team running Jepsen style testing against a Go service that needs a verdict computed at test time rather than a trace read by hand, since the model is a Go function you can unit test and the checker returns a boolean. Skip it if your histories are enormous and P-compositionality does not apply to your specification, because the speed advantage the README claims is a property of that optimisation, not a constant, and treat the reported 1000x to 10000x over Knossos as the project's own measurement on the Jepsen data in test_data/. Before adopting, write the model before you trust the checker, because a wrong Step function produces a confident wrong answer, and note that go.mod declares go 1.16 so the module has no dependency floor to reason about. The last push was on 2026-09-21, there are no GitHub releases, and the licence is MIT.

Frequently asked questions

Official sources

1. anishathalye/porcupine on GitHub
2. Issues
3. License: MIT
4. Project website
5. README