anishathalye / porcupine

A fast linearizability checker written in Go 🔎
https://anishathalye.com/testing-distributed-systems-for-linearizability/
MIT License
878 stars 50 forks source link

Access longest linearizable path #21

Open dfarr opened 1 month ago

dfarr commented 1 month ago

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 :)

serathius commented 1 month ago

+1 to that from etcd. It would be really useful to get the linearization to be able to validate etcd watch, the eventually consistent stream that of changes to etcd.