anishathalye / porcupine

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

how to check the write fail event #2

Closed siddontang closed 7 years ago

siddontang commented 7 years ago

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.

siddontang commented 7 years ago

I see that in your etcd test, you can skip the fail write response. so do we need to handle failure like timeout too?

siddontang commented 7 years ago

If write ok = false, I try to return true + origin state, seem it can work. Is it reasonable?

anishathalye commented 7 years ago

(sorry for the delay)

Yeah, that sounds reasonable. That's basically what I'm doing with the etcd test.

siddontang commented 7 years ago

Thanks @anishathalye