-
Notifications
You must be signed in to change notification settings - Fork 28
/
porcupine.go
75 lines (65 loc) · 1.67 KB
/
porcupine.go
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
package porcupine
import (
"fmt"
"log"
"github.com/anishathalye/porcupine"
"github.com/pingcap/chaos/pkg/core"
)
// Checker is a linearizability checker powered by Porcupine.
type Checker struct{}
// Check checks the history of operations meets liearizability or not with model.
// False means the history is not linearizable.
func (Checker) Check(m core.Model, ops []core.Operation) (bool, error) {
pModel := porcupine.Model{
Init: m.Init,
Step: m.Step,
Equal: m.Equal,
}
events, err := ConvertOperationsToEvents(ops)
if err != nil {
return false, err
}
log.Printf("begin to verify %d events", len(events))
return porcupine.CheckEvents(pModel, events), nil
}
// Name is the name of porcupine checker
func (Checker) Name() string {
return "porcupine_checker"
}
// ConvertOperationsToEvents converts core.Operations to porcupine.Event.
func ConvertOperationsToEvents(ops []core.Operation) ([]porcupine.Event, error) {
if len(ops)%2 != 0 {
return nil, fmt.Errorf("history is not complete")
}
procID := map[int64]uint{}
id := uint(0)
events := make([]porcupine.Event, 0, len(ops))
for _, op := range ops {
if op.Action == core.InvokeOperation {
event := porcupine.Event{
Kind: porcupine.CallEvent,
Id: id,
Value: op.Data,
}
events = append(events, event)
procID[op.Proc] = id
id++
} else {
if op.Data == nil {
continue
}
matchID := procID[op.Proc]
delete(procID, op.Proc)
event := porcupine.Event{
Kind: porcupine.ReturnEvent,
Id: matchID,
Value: op.Data,
}
events = append(events, event)
}
}
if len(procID) != 0 {
return nil, fmt.Errorf("history is not complete")
}
return events, nil
}