Merge pull request #14902 from serathius/linearizability-issue14685

Refactor etcd model

tests/linearizability/model.go

@@ -43,10 +43,13 @@ type EtcdResponse struct {
 }
 
 type EtcdState struct {
-	Key          string
+	Key            string
-	Value        string
+	PossibleValues []ValueRevision
-	LastRevision int64
+}
-	FailedWrite  *EtcdRequest
+
+type ValueRevision struct {
+	Value    string
+	Revision int64
 }
 
 var etcdModel = porcupine.Model{
@@ -93,121 +96,77 @@ var etcdModel = porcupine.Model{
 }
 
 func step(state EtcdState, request EtcdRequest, response EtcdResponse) (bool, EtcdState) {
-	if request.Key == "" {
+	if len(state.PossibleValues) == 0 {
-		panic("invalid request")
+		state.Key = request.Key
-	}
+		if ok, v := initValueRevision(request, response); ok {
-	if state.Key == "" {
+			state.PossibleValues = append(state.PossibleValues, v)
-		return true, initState(request, response)
+		}
+		return true, state
 	}
 	if state.Key != request.Key {
-		panic("Multiple keys not supported")
+		panic("multiple keys not supported")
+	}
+	if response.Err != nil {
+		for _, v := range state.PossibleValues {
+			newV, _ := stepValue(v, request)
+			state.PossibleValues = append(state.PossibleValues, newV)
+		}
+	} else {
+		var i = 0
+		for _, v := range state.PossibleValues {
+			newV, expectedResponse := stepValue(v, request)
+			if expectedResponse == response {
+				state.PossibleValues[i] = newV
+				i++
+			}
+		}
+		state.PossibleValues = state.PossibleValues[:i]
+	}
+	return len(state.PossibleValues) > 0, state
+}
+
+func initValueRevision(request EtcdRequest, response EtcdResponse) (ok bool, v ValueRevision) {
+	if response.Err != nil {
+		return false, ValueRevision{}
 	}
 	switch request.Op {
 	case Get:
-		return stepGet(state, request, response)
+		return true, ValueRevision{
+			Value:    response.GetData,
+			Revision: response.Revision,
+		}
 	case Put:
-		return stepPut(state, request, response)
+		return true, ValueRevision{
+			Value:    request.PutData,
+			Revision: response.Revision,
+		}
 	case Delete:
-		return stepDelete(state, request, response)
+		return true, ValueRevision{
+			Value:    "",
+			Revision: response.Revision,
+		}
 	default:
 		panic("Unknown operation")
 	}
 }
 
-func initState(request EtcdRequest, response EtcdResponse) EtcdState {
+func stepValue(v ValueRevision, request EtcdRequest) (ValueRevision, EtcdResponse) {
-	state := EtcdState{
+	resp := EtcdResponse{}
-		Key:          request.Key,
-		LastRevision: response.Revision,
-	}
 	switch request.Op {
 	case Get:
-		state.Value = response.GetData
+		resp.GetData = v.Value
 	case Put:
-		if response.Err == nil {
+		v.Value = request.PutData
-			state.Value = request.PutData
+		v.Revision += 1
-		} else {
-			state.FailedWrite = &request
-		}
 	case Delete:
-		if response.Err != nil {
+		if v.Value != "" {
-			state.FailedWrite = &request
+			v.Value = ""
+			v.Revision += 1
+			resp.Deleted = 1
 		}
 	default:
-		panic("Unknown operation")
+		panic("unsupported operation")
 	}
-	return state
+	resp.Revision = v.Revision
-}
+	return v, resp
-
-func stepGet(state EtcdState, request EtcdRequest, response EtcdResponse) (bool, EtcdState) {
-	if state.Value == response.GetData && state.LastRevision == response.Revision {
-		state.FailedWrite = nil
-		return true, state
-	}
-	if state.FailedWrite != nil && state.LastRevision < response.Revision {
-		var ok bool
-		switch state.FailedWrite.Op {
-		case Get:
-			panic("Expected write")
-		case Put:
-			ok = response.GetData == state.FailedWrite.PutData
-		case Delete:
-			ok = response.GetData == ""
-		default:
-			panic("Unknown operation")
-		}
-		if ok {
-			state.Value = response.GetData
-			state.LastRevision = response.Revision
-			state.FailedWrite = nil
-			return true, state
-		}
-	}
-	return false, state
-}
-
-func stepPut(state EtcdState, request EtcdRequest, response EtcdResponse) (bool, EtcdState) {
-	if response.Err != nil {
-		state.FailedWrite = &request
-		return true, state
-	}
-	if response.Revision <= state.LastRevision {
-		return false, state
-	}
-	if response.Revision != state.LastRevision+1 && state.FailedWrite == nil {
-		return false, state
-	}
-	state.Value = request.PutData
-	state.LastRevision = response.Revision
-	state.FailedWrite = nil
-	return true, state
-}
-
-func stepDelete(state EtcdState, request EtcdRequest, response EtcdResponse) (bool, EtcdState) {
-	if response.Err != nil {
-		state.FailedWrite = &request
-		return true, state
-	}
-	// revision should never decrease
-	if response.Revision < state.LastRevision {
-		return false, state
-	}
-	deleteSucceeded := response.Deleted != 0
-	keySet := state.Value != ""
-
-	// non-existent key cannot be deleted.
-	if deleteSucceeded != keySet && state.FailedWrite == nil {
-		return false, state
-	}
-	//if key was deleted, response revision should increase
-	if deleteSucceeded && (response.Revision != state.LastRevision+1 || !keySet) && (state.FailedWrite == nil || response.Revision < state.LastRevision+2) {
-		return false, state
-	}
-	//if key was not deleted, response revision should not change
-	if !deleteSucceeded && state.LastRevision != response.Revision && state.FailedWrite == nil {
-		return false, state
-	}
-
-	state.Value = ""
-	state.LastRevision = response.Revision
-	return true, state
 }

tests/linearizability/model_test.go

@@ -105,8 +105,6 @@ func TestModel(t *testing.T) {
 				// Two failed request, two persisted.
 				{req: EtcdRequest{Op: Put, Key: "key", PutData: "3"}, resp: EtcdResponse{Err: errors.New("failed")}},
 				{req: EtcdRequest{Op: Put, Key: "key", PutData: "4"}, resp: EtcdResponse{Err: errors.New("failed")}},
-				{req: EtcdRequest{Op: Get, Key: "key"}, resp: EtcdResponse{GetData: "3", Revision: 3}, failure: true},
-				{req: EtcdRequest{Op: Get, Key: "key"}, resp: EtcdResponse{GetData: "3", Revision: 4}, failure: true},
 				{req: EtcdRequest{Op: Get, Key: "key"}, resp: EtcdResponse{GetData: "4", Revision: 4}},
 			},
 		},
@@ -220,15 +218,18 @@ func TestModel(t *testing.T) {
 		},
 	}
 	for _, tc := range tcs {
-		var ok bool
 		t.Run(tc.name, func(t *testing.T) {
 			state := etcdModel.Init()
 			for _, op := range tc.operations {
-				t.Logf("state: %v", state)
+				ok, newState := etcdModel.Step(state, op.req, op.resp)
-				ok, state = etcdModel.Step(state, op.req, op.resp)
 				if ok != !op.failure {
+					t.Logf("state: %v", state)
 					t.Errorf("Unexpected operation result, expect: %v, got: %v, operation: %s", !op.failure, ok, etcdModel.DescribeOperation(op.req, op.resp))
 				}
+				if ok {
+					state = newState
+					t.Logf("state: %v", state)
+				}
 			}
 		})
 	}