anishathalye/porcupine

A fast linearizability checker written in Go 🔎

Porcupine

Porcupine is a fast linearizability checker used in both academia and industry for testing the correctness of distributed systems. It takes a sequential specification as executable Go code, along with a concurrent history, and it determines whether the history is linearizable with respect to the sequential specification. Porcupine also implements a visualizer for histories and linearization points.

(click for interactive version)

Porcupine implements the algorithm described in Faster linearizability checking via P-compositionality, an optimization of the algorithm described in Testing for Linearizability.

Porcupine is faster and can handle more histories than Knossos's linearizability checker. Testing on the data in test_data/jepsen/, Porcupine is generally 1,000x-10,000x faster and has a much smaller memory footprint. On histories where it can take advantage of P-compositionality, Porcupine can be millions of times faster.

Usage

Porcupine takes an executable model of a system along with a history, and it runs a decision procedure to determine if the history is linearizable with respect to the model. Porcupine supports specifying history in two ways, either as a list of operations with given call and return times, or as a list of call/return events in time order. Porcupine can also visualize histories, along with partial linearizations, which may aid in debugging.

See the documentation for how to write a model and specify histories. You can also check out some example implementations of models from the tests.

Once you've written a model and have a history, you can use the CheckOperations and CheckEvents functions to determine if your history is linearizable. If you want to visualize a history, along with partial linearizations, you can use the Visualize function.

Testing linearizability

Suppose we're testing linearizability for operations on a read/write register that's initialized to 0. We write a sequential specification for the register like this:

type registerInput struct {
    op    bool // false = put, true = get
    value int
}

// a sequential specification of a register
registerModel := porcupine.Model{
    Init: func() interface{} {
        return 0
    },
    // step function: takes a state, input, and output, and returns whether it
    // was a legal operation, along with a new state
    Step: func(state, input, output interface{}) (bool, interface{}) {
        regInput := input.(registerInput)
        if regInput.op == false {
            return true, regInput.value // always ok to execute a put
        } else {
            readCorrectValue := output == state
            return readCorrectValue, state // state is unchanged
        }
    },
}

Suppose we have the following concurrent history from a set of 3 clients. In a row, the first | is when the operation was invoked, and the second | is when the operation returned.

C0:  |-------- put('100') --------|
C1:     |--- get() -> '100' ---|
C2:        |- get() -> '0' -|

We encode this history as follows:

events := []porcupine.Event{
    // C0: put('100')
    {Kind: porcupine.CallEvent, Value: registerInput{false, 100}, Id: 0, ClientId: 0},
    // C1: get()
    {Kind: porcupine.CallEvent, Value: registerInput{true, 0}, Id: 1, ClientId: 1},
    // C2: get()
    {Kind: porcupine.CallEvent, Value: registerInput{true, 0}, Id: 2, ClientId: 2},
    // C2: Completed get() -> '0'
    {Kind: porcupine.ReturnEvent, Value: 0, Id: 2, ClientId: 2},
    // C1: Completed get() -> '100'
    {Kind: porcupine.ReturnEvent, Value: 100, Id: 1, ClientId: 1},
    // C0: Completed put('100')
    {Kind: porcupine.ReturnEvent, Value: 0, Id: 0, ClientId: 0},
}

We can have Porcupine check the linearizability of the history as follows:

ok := porcupine.CheckEvents(registerModel, events)
// returns true

Porcupine can visualize the linearization points as well:

Now, suppose we have another history:

C0:  |---------------- put('200') ----------------|
C1:    |- get() -> '200' -|
C2:                           |- get() -> '0' -|

We can check the history with Porcupine and see that it's not linearizable:

events := []porcupine.Event{
    // C0: put('200')
    {Kind: porcupine.CallEvent, Value: registerInput{false, 200}, Id: 0, ClientId: 0},
    // C1: get()
    {Kind: porcupine.CallEvent, Value: registerInput{true, 0}, Id: 1, ClientId: 1},
    // C1: Completed get() -> '200'
    {Kind: porcupine.ReturnEvent, Value: 200, Id: 1, ClientId: 1},
    // C2: get()
    {Kind: porcupine.CallEvent, Value: registerInput{true, 0}, Id: 2, ClientId: 2},
    // C2: Completed get() -> '0'
    {Kind: porcupine.ReturnEvent, Value: 0, Id: 2, ClientId: 2},
    // C0: Completed put('200')
    {Kind: porcupine.ReturnEvent, Value: 0, Id: 0, ClientId: 0},
}

ok := porcupine.CheckEvents(registerModel, events)
// returns false

See porcupine_test.go for more examples on how to write models and histories.

Visualizing histories

Porcupine provides functionality to visualize histories, along with the linearization (or partial linearizations and illegal linearization points, in the case of a non-linearizable history). The result is an HTML page that draws an interactive visualization using JavaScript. The output looks like this:

You can see the full interactive version here.

The visualization is by partition: all partitions are essentially independent, so with the key-value store example above, operations related to each unique key are in a separate partition.

Statically, the visualization shows all history elements, along with linearization points for each partition. If a partition has no full linearization, the visualization shows the longest partial linearization. It also shows, for each history element, the longest partial linearization containing that event, even if it's not the longest overall partial linearization; these are greyed out by default. It also shows illegal linearization points, history elements that were checked to see if they could occur next but which were illegal to linearize at that point according to the model.

When a history element is hovered over, the visualization highlights the most relevant partial linearization. When it exists, the longest partial linearization containing the event is shown. Otherwise, when it exists, the visualization shows the longest partial linearization that ends with an illegal LP that is the event being hovered over. Hovering over an event also shows a tooltip showing extra information, such as the previous and current states of the state machine, as well as the time the operation was invoked and when it returned. This information is derived from the currently selected linearization.

Clicking on a history element selects it, which highlights the event with a bold border. This has the effect of making the selection of a partial linearization "sticky", so it's possible to move around the history without de-selecting it. Clicking on another history element will select that one instead, and clicking on the background will deselect.

All that's needed to visualize histories is the CheckOperationsVerbose / CheckEventsVerbose functions, which return extra information that's used by the visualization, and the Visualize function, which produces the visualization. For the visualization to be good, it's useful to fill out the DescribeOperation and DescribeState fields of the model. See visualization_test.go for an end-to-end example of how to visualize a history using Porcupine.

Notes

If Porcupine runs really slowly on your model/history, it may be inevitable, due to state space explosion. See this issue for a discussion of this challenge in the context of a particular model and history.

Users

Porcupine is used in both academia and industry. It can be helpful to look at existing uses of Porcupine to learn how you can design a robust testing framework with linearizability checking at its core.

• etcd. etcd uses Porcupine's linearizability checker and visualizer in its robustness tests [KubeCon 2023eu talk].
• PingCAP TiPocket. PingCAP uses Porcupine to test the TiDB distributed database.
• Amazon MemoryDB (SIGMOD'24). Amazon uses Porcupine to test MemoryDB consistency.
• LEGOStore (VLDB'22). Porcupine is used to test the linearizability of LEGOStore.
• Resonate. Resonate's test harness uses Porcupine as its linearizability checker.
• MIT 6.5840 (Distributed Systems) key-value store. Porcupine was originally developed for use in MIT's distributed systems class to test the linearizability of the Raft-based distributed key-value store.

Does your system use Porcupine? Send a PR to add it to this list!

Citation

If you use Porcupine in any way in academic work, please cite the following:

@misc{athalye2017porcupine,
  author = {Anish Athalye},
  title = {Porcupine: A fast linearizability checker in {Go}},
  year = {2017},
  howpublished = {\url{https://github.com/anishathalye/porcupine}}
}

License

Copyright (c) Anish Athalye. Released under the MIT License. See LICENSE.md for details.

porcupine's Issues

Should return sequence that violates linearizability

When Knossos fails, it gives output showing the sequence of events that violated linearizability. Porcupine seems to just return "false" from the checker. It would be great if it would show the underlying linearizability violation in a manner similar to Knossos.

if and only if ??

porcupine/model.go

Line 28 in 1c86176

// Partition functions, such that a history is linearizable if an only

Visualization should support adding non-linearization related events

Porcupine visualization is a great tool to view history of operations done in model. However it only graphs event history outputted from linearization.

In the real system there might be events that are not directly part of model of linearization, still they might have a influence of correctness of the system. For example we might want to test database like etcd correctness under different types of disruptions, like process kill. Process kill event is not directly part of linearization, however it would be really useful to be able to show the event in the visualization.

Would be great to have a method linearizationInfo.AddEvent(start, end int, name string), that allows to additional block that will be showed on the visualization. Additional recommendation would be to make linearizationInfo public struct. Having a public function returning private struct is a antipattern in Go.

As a workaround, it is possible to add this event as no-op operation to model. This however this will have negative impact on performance.

etcd test write timeout

I think the etcd specification is incorrect:

porcupine/porcupine_test.go

Lines 151 to 152 in 7cbc834

	// write
	return true, inp.arg1

A write can timeout

porcupine/test_data/jepsen/etcd_000.log

Line 61 in 7cbc834

INFO jepsen.util - 4 :info :write :timed-out

In this case, the Step function should not apply the write

RWLock'd map deemed not linearizable

Hey @anishathalye,

Thanks for the library, we're making pretty heavy use of this now in etcd and I spent the day to play around with it and check a toy database of mine.

While doing that, I came across an odd issue with sync.RWMutex which guards the three main operations (Get with ReadLock and Put+Delete with a WriteLock).

From sync.RWMutex:

A RWMutex is a reader/writer mutual exclusion lock. The lock can be held by an arbitrary number of readers or a single writer. The zero value for a RWMutex is an unlocked mutex.
If a goroutine holds a RWMutex for reading and another goroutine might call Lock, no goroutine should expect to be able to acquire a read lock until the initial read lock is released. In particular, this prohibits recursive read locking. This is to ensure that the lock eventually becomes available; a blocked Lock call excludes new readers from acquiring the lock.

Given this is implemented correctly in Go (I would assume so), this should give us linearizability over concurrent map operations. A single threaded happy path test runs correctly, the multi-goroutine one sadly returns Illegal.

The full code can be found in this commit: thomasjungblut@d01d216

And should be reproducible with a simple go test on the rwlock package.

I would love to attach a better visualization of this issue, however there's some issue with the JS in this particular case:

The more complex case from my toy database looks like this:

I'm rather curious as to why the "Get" was allowed to run during the "Put" and even the "Put" can overlap with another.
BTW I also suspect a clock resolution / backward movement issue with time.Now here...

EDIT: this also happens with a simple sync.Mutex.

Let me know what you think, especially if I screwed up the model somehow.

how to check the write fail event

Hi @anishathalye

I write a simple check like:

type Request struct {
	// 0 for read, 1 for put
	Op int
	// put value
	Value int
}

type Resposne struct {
	// for read value
	Value int
	// for put ok
	Ok bool
}

func main() {
	m := porcupine.Model{
		Init: func() interface{} {
			return 5
		},
		Step: func(state interface{}, input interface{}, output interface{}) (bool, interface{}) {
			st := state.(int)
			inp := input.(Request)
			out := output.(Resposne)

			if inp.Op == 0 {
				// read
				ok := out.Value == st
				return ok, st
			}

			return out.Ok, inp.Value
		},
	}

	events := []porcupine.Event{
		porcupine.Event{Kind: porcupine.CallEvent, Value: Request{Op: 0}, Id: 1},
		porcupine.Event{Kind: porcupine.CallEvent, Value: Request{Op: 1, Value: 10}, Id: 2},
		porcupine.Event{Kind: porcupine.ReturnEvent, Value: Resposne{Ok: false}, Id: 2},
		porcupine.Event{Kind: porcupine.ReturnEvent, Value: Resposne{Value: 5}, Id: 1},
	}

	if !porcupine.CheckEvents(m, events) {
		panic("must be linearizable")
	}
}

The history is very easy, the init state is 5, event 1 does the read operation and event 2 writes 10 but fails. I think the history may be a linearizability but to my surprised, it panics. If I change the write Ok to true, it will work.

Can you tell me why or what do I need to change for the case?

Thank you very much.

verify 400 events is too slow for my bank case

Hi @anishathalye

I use Porcupine to verify my bank case but find it can't stop and run for a long time. I don't know why, but seem that my bank Model is right. see
https://github.com/siddontang/chaos/blob/master/db/tidb/bank.go#L222

You can check out the chaos repo and make verifier to build the chaos verifier, then run

./bin/chaos-verifier -names tidb_bank -history ./history.log

The history log is here

history.log

It is very appreicated that you can help me figure the problem out.

Huge visualization files

When testing changes to etcd robustness testing we have managed to generate 1.5GB visualization file.

The operation history is about 3k operatons, which is pretty short, however due to high request failure rate (50%) the linearization times out on 5 minutes. I expect the most of those 1.5GB comes from huge number of partial linearizations. Which makes sense as there might be exponential number of them.

The file is too big to be loaded by browser, could we maybe limit the size of partial linearizations to ensure that file size doesn't explode and we can still open it?

If you want to check out the file see https://github.com/etcd-io/etcd/actions/runs/9178286126?pr=17833, download one of the artifacts and look for "history.html" files in the archive.

Check 5000 events OOM

Hi @anishathalye

I write a simple model to check bank transfer, see https://github.com/siddontang/chaos/blob/master/tidb/bank.go#L170

And I generate 5000 events, but to my surprise, the linearizability check is killed with OOM, but my server has 128 GB memory.

Here is the history log
history.log.zip
and I use https://github.com/siddontang/chaos/blob/master/tidb/bank.go#L246 to parse the history and verify it.

Access longest linearizable path

After calling CheckOperationsVerbose and getting a result I would love be able to access the "longest linearizable path" found. In the case of an Ok result this would be equivalent to the path shown in the visualization. In the case of an Illegal result the visualization can show a few different paths, in this case either the longest or all the paths would be useful to have access to.

The reason I am hoping to access this information is because we have written a step function that looks like this

func(state, input, output interface{}) (bool, interface{}) {
	model := state.(*Model)
	req := input.(*Req)
	res := output.(*Res)

	updatedModel, err := dst.Step(model, req.time, res.time, req.req, res.res, res.err)
	if err != nil {
		return false, model
	}

	return true, updatedModel
}

Our dst function returns an updated model and an error that contains additional useful information. In the case where the error is non nil, we report false to porcupine and the error information is effectively lost. If I could access the longest path (I'm hoping for a slice of type []porcupine.Operation) I could feed this information back into our dst model and report the error that occurs, this would be super helpful for debugging and developing.

If this is something that is possible and something you are up to add to porcupine I am happy to create a PR :)

how to check strong consistency of database

Hi @anishathalye,

Currently, I am using https://github.com/pingcap/chaos to check strong consistency of TiDB. But porcupine don't work with too many events so all my tests are out of memory before my chaos run.

Can you give me any solution to check strong consistency of database with chaos?

Besides, I propose that we can run continuously test ( about 200 events logs per test) and use porcupine to check them. If all tests passed, the database would be strong consistency. Is that true?

How does porcupine handle timeouts?

How can one represent the ambiguity of timeout responses with porcupine?

When my application fails to handle a request by some specified deadline, it is unclear whether the request took effect or not. Knossos handles this ambiguity with the :info response type, but porcupine doesn't seem to have an equivalent. I think this concern needs to be built into the checker.

So how can porcupine handle ambiguous histories created by phenomena like timeouts?

how to write a correct bank transfer check

Hi @anishathalye

I want to use porcupine in our bank transfer case. Our case has two operations:

1. read: read all account balances
2. transfer: random select two accounts and transfer some money

For simplicity, let's assume we only have two accounts 0 and 1. And I try to use porcupine like this:

package main

import (
	"reflect"

	"github.com/anishathalye/porcupine"
)

type bankRequest struct {
	// 0: read
	// 1: transfer from -> to with amount
	op     int
	from   int
	to     int
	amount int
}

type bankResponse struct {
	// read result
	balances []int64
        // read or transfer ok
	ok       bool
}

func newBankEvent(v interface{}, id uint) porcupine.Event {
	if _, ok := v.(bankRequest); ok {
		return porcupine.Event{Kind: porcupine.CallEvent, Value: v, Id: id}
	}

	return porcupine.Event{Kind: porcupine.ReturnEvent, Value: v, Id: id}
}

func getBankModel() porcupine.Model {
	return porcupine.Model{
		Init: func() interface{} {
                        // account 0 and 1 both have 1000 at first
			v := make([]int64, 2)
			for i := 0; i < 2; i++ {
				v[i] = 1000
			}
			return v
		},
		Step: func(state interface{}, input interface{}, output interface{}) (bool, interface{}) {
			st := state.([]int64)
			inp := input.(bankRequest)
			out := output.(bankResponse)

			if inp.op == 0 {
				// read
				ok := !out.ok || reflect.DeepEqual(st, out.balances)
				return ok, state
			}

			// for transfer
			if out.ok {
				newSt := append([]int64{}, st...)
				newSt[inp.from] -= int64(inp.amount)
				newSt[inp.to] += int64(inp.amount)
				return true, newSt
			}

			return false, st
		},
		Equal: func(state1, state2 interface{}) bool {
			return reflect.DeepEqual(state1, state2)
		},
	}
}

func main() {
	m := getBankModel()

	events := []porcupine.Event{
		newBankEvent(bankRequest{op: 0}, 1),
		newBankEvent(bankResponse{ok: true, balances: []int64{1000, 1000}}, 1),
                // try to transfer 500 from 0 to 1
		newBankEvent(bankRequest{op: 1, from: 0, to: 1, amount: 500}, 2),
		// In our case, the transfer may return fail because of some reasons, but the balance
		// is already transfered, so for next read, we will read the corrent data.
		newBankEvent(bankResponse{ok: false}, 2),
		newBankEvent(bankRequest{op: 0}, 3),
		newBankEvent(bankResponse{ok: true, balances: []int64{500, 1500}}, 3),
	}

	if !porcupine.CheckEvents(m, events) {
		panic("must be linearizable")
	}
}

Sadly, the check fails, but I have no idea how to fix this. Can you help me figure it out why the check can't work? Thank you.