diff --git a/collection/skipmap/linearizability_test.go b/collection/skipmap/linearizability_test.go
new file mode 100644
index 0000000..4112ecd
--- /dev/null
+++ b/collection/skipmap/linearizability_test.go
@@ -0,0 +1,242 @@
+// Copyright 2021 ByteDance Inc.
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package skipmap
+
+import (
+ "fmt"
+ "math/rand"
+ "os"
+ "sync"
+ "sync/atomic"
+ "testing"
+ "time"
+
+ "github.com/anishathalye/porcupine"
+)
+
+const (
+ opLoad = iota
+ opLoadOrStore
+ opStore
+ opLoadAndDelete
+ numOps
+)
+
+type skipmapInput struct {
+ Op int
+ Key string
+ Value int
+}
+
+type skipmapOutput struct {
+ Value int
+ Ok bool
+}
+
+type perKeyState struct {
+ Exists bool
+ Value int
+}
+
+var skipmapModel = porcupine.Model{
+ Init: func() interface{} { return perKeyState{} },
+ Step: func(state, input, output interface{}) (bool, interface{}) {
+ st := state.(perKeyState)
+ inp := input.(skipmapInput)
+ out := output.(skipmapOutput)
+
+ switch inp.Op {
+ case opLoad:
+ if st.Exists {
+ return out.Ok && out.Value == st.Value, st
+ }
+ return !out.Ok && out.Value == 0, st
+ case opLoadOrStore:
+ if st.Exists {
+ return out.Ok && out.Value == st.Value, st
+ }
+ if !out.Ok && out.Value == inp.Value {
+ return true, perKeyState{Exists: true, Value: inp.Value}
+ }
+ return false, st
+ case opStore:
+ return true, perKeyState{Exists: true, Value: inp.Value}
+ case opLoadAndDelete:
+ if st.Exists {
+ if out.Ok && out.Value == st.Value {
+ return true, perKeyState{}
+ }
+ return false, st
+ }
+ return !out.Ok && out.Value == 0, st
+ default:
+ return false, st
+ }
+ },
+ Equal: func(a, b interface{}) bool {
+ return a.(perKeyState) == b.(perKeyState)
+ },
+ DescribeOperation: func(input, output interface{}) string {
+ inp := input.(skipmapInput)
+ out := output.(skipmapOutput)
+ switch inp.Op {
+ case opLoad:
+ if out.Ok {
+ return fmt.Sprintf("Load(%s) -> %d", inp.Key, out.Value)
+ }
+ return fmt.Sprintf("Load(%s) -> nil", inp.Key)
+ case opLoadOrStore:
+ if out.Ok {
+ return fmt.Sprintf("LoadOrStore(%s, %d) -> loaded %d", inp.Key, inp.Value, out.Value)
+ }
+ return fmt.Sprintf("LoadOrStore(%s, %d) -> stored", inp.Key, inp.Value)
+ case opStore:
+ return fmt.Sprintf("Store(%s, %d)", inp.Key, inp.Value)
+ case opLoadAndDelete:
+ if out.Ok {
+ return fmt.Sprintf("LoadAndDelete(%s) -> %d", inp.Key, out.Value)
+ }
+ return fmt.Sprintf("LoadAndDelete(%s) -> nil", inp.Key)
+ default:
+ return "?"
+ }
+ },
+ DescribeState: func(state interface{}) string {
+ st := state.(perKeyState)
+ if st.Exists {
+ return fmt.Sprintf("value=%d", st.Value)
+ }
+ return "absent"
+ },
+}
+
+func executeSkipmapOp(m *StringMap, input skipmapInput) skipmapOutput {
+ switch input.Op {
+ case opLoad:
+ value, ok := m.Load(input.Key)
+ if ok {
+ return skipmapOutput{Value: value.(int), Ok: true}
+ }
+ return skipmapOutput{}
+ case opLoadOrStore:
+ actual, loaded := m.LoadOrStore(input.Key, input.Value)
+ return skipmapOutput{Value: actual.(int), Ok: loaded}
+ case opStore:
+ m.Store(input.Key, input.Value)
+ return skipmapOutput{}
+ case opLoadAndDelete:
+ value, loaded := m.LoadAndDelete(input.Key)
+ if loaded {
+ return skipmapOutput{Value: value.(int), Ok: true}
+ }
+ return skipmapOutput{}
+ default:
+ return skipmapOutput{}
+ }
+}
+
+func checkPerKeyLinearizability(operations []porcupine.Operation, timeout time.Duration) (bool, []porcupine.LinearizationInfo) {
+ byKey := make(map[string][]porcupine.Operation)
+ for _, op := range operations {
+ byKey[op.Input.(skipmapInput).Key] = append(byKey[op.Input.(skipmapInput).Key], op)
+ }
+
+ var mu sync.Mutex
+ var failures []porcupine.LinearizationInfo
+ var wg sync.WaitGroup
+
+ for _, ops := range byKey {
+ wg.Add(1)
+ go func(ops []porcupine.Operation) {
+ defer wg.Done()
+ result, info := porcupine.CheckOperationsVerbose(skipmapModel, ops, timeout)
+ if result == porcupine.Illegal {
+ mu.Lock()
+ failures = append(failures, info)
+ mu.Unlock()
+ }
+ }(ops)
+ }
+ wg.Wait()
+
+ return len(failures) == 0, failures
+}
+
+// TestSkipMapLinearizability runs a mixed linearizability test with concurrent
+// clients exercising all skipmap operations on a shared key set.
+func TestSkipMapLinearizability(t *testing.T) {
+ if testing.Short() {
+ t.Skip("Skipping linearizability tests in short mode")
+ }
+
+ const (
+ numClients = 16
+ numOpsPerClient = 200
+ numKeys = 10
+ )
+
+ m := NewString()
+ localOps := make([][]porcupine.Operation, numClients)
+ var wg sync.WaitGroup
+ startTime := time.Now()
+
+ for clientId := 0; clientId < numClients; clientId++ {
+ wg.Add(1)
+ go func(cid int) {
+ defer wg.Done()
+ ops := make([]porcupine.Operation, 0, numOpsPerClient)
+
+ for opId := 0; opId < numOpsPerClient; opId++ {
+ key := fmt.Sprintf("key_%d", rand.Intn(numKeys))
+ value := cid*100000 + opId
+ op := rand.Intn(numOps)
+ input := skipmapInput{Op: op, Key: key, Value: value}
+
+ var callTime int64
+ atomic.StoreInt64(&callTime, time.Since(startTime).Nanoseconds())
+ output := executeSkipmapOp(m, input)
+ returnTime := time.Since(startTime).Nanoseconds()
+
+ ops = append(ops, porcupine.Operation{
+ ClientId: cid,
+ Input: input,
+ Call: callTime,
+ Output: output,
+ Return: returnTime,
+ })
+ }
+ localOps[cid] = ops
+ }(clientId)
+ }
+ wg.Wait()
+
+ var operations []porcupine.Operation
+ for _, ops := range localOps {
+ operations = append(operations, ops...)
+ }
+
+ ok, failures := checkPerKeyLinearizability(operations, 30*time.Second)
+ if !ok {
+ for i, info := range failures {
+ filename := fmt.Sprintf("violation_skipmap_%d_%s.html", i, time.Now().Format("20060102_150405"))
+ if file, err := os.Create(filename); err == nil {
+ porcupine.Visualize(skipmapModel, info, file)
+ file.Close()
+ t.Logf("visualization written to %s", filename)
+ }
+ }
+ t.Fatalf("linearizability violation: %d key(s) failed", len(failures))
+ }
+}
diff --git a/collection/skipmap/violation_skipmap_1.html b/collection/skipmap/violation_skipmap_1.html
new file mode 100644
index 0000000..1162722
--- /dev/null
+++ b/collection/skipmap/violation_skipmap_1.html
@@ -0,0 +1,1039 @@
+
+
+
+
+ Porcupine
+
+
+
+
+
+
+
+