how to write a correct bank transfer check

[siddontang]

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.

[anishathalye]

I don't think this comment:

// 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.

makes sense. For event 2, how could ok == false but the amount is transferred anyways? This isn't a valid step even in the single-threaded model.

[siddontang]

@anishathalye

It can be, for a MySQL execution, like update accounts set balance = balance + 1 where id = 0, after we send this query to the MySQL, and the MySQL executes it, but at this time, the connection is broken with timeout, so we will get an error in the client, but the MySQL can still execute the query successfully.

Maybe here I must add a timeout field in the response, but if the timeout is true, what do I return?

[anishathalye]

Ah, I see. Yeah, I think the right way to handle this is to add a timeout field in the response, and add the event as executing sometime between invocation time and infinity (because you can't tell when in the future a timed out operation will appear to execute).

You can see how the "unknown" case is handled here: https://github.com/anishathalye/porcupine/blob/master/porcupine_test.go#L96

[siddontang]

Thanks @anishathalye

It works now, I will add more tests later.