Add linearization tests for SimpleDB (#19)

* update to go 1.19 * add simple porcupine linearizability check * add multi-threaded test * fix model * bigger test * wire up linearization tests, update codeql * add porcupine to crash tests * moving to the generic implementation * remove model, use make test * add documentation Co-authored-by: Thomas Jungblut <[email protected]>
thomasjungblut · Dec 2, 2022 · d1f11e9 · d1f11e9
1 parent c799425
commit d1f11e9
Show file tree

Hide file tree

Showing 16 changed files with 555 additions and 99 deletions.
diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml
@@ -7,10 +7,10 @@ name: "CodeQL"
 
 on:
   push:
-    branches: [main]
+    branches: [ main ]
   pull_request:
     # The branches below must be a subset of the branches above
-    branches: [main]
+    branches: [ main ]
   schedule:
     - cron: '0 11 * * 1'
 
@@ -22,31 +22,28 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        # Override automatic language detection by changing the below list
-        # Supported options are ['csharp', 'cpp', 'go', 'java', 'javascript', 'python']
-        language: ['go']
-        # Learn more...
-        # https://docs.github.com/en/github/finding-security-vulnerabilities-and-errors-in-your-code/configuring-code-scanning#overriding-automatic-language-detection
-
+        language: [ 'go' ]
     steps:
-    - name: Checkout repository
-      uses: actions/checkout@v2
-      with:
-        # We must fetch at least the immediate parents so that if this is
-        # a pull request then we can checkout the head.
-        fetch-depth: 2
+      - name: Checkout repository
+        uses: actions/checkout@v2
+        with:
+          # We must fetch at least the immediate parents so that if this is
+          # a pull request then we can checkout the head.
+          fetch-depth: 2
 
-    # If this run was triggered by a pull request event, then checkout
-    # the head of the pull request instead of the merge commit.
-    - run: git checkout HEAD^2
-      if: ${{ github.event_name == 'pull_request' }}
+      # If this run was triggered by a pull request event, then checkout
+      # the head of the pull request instead of the merge commit.
+      - run: git checkout HEAD^2
+        if: ${{ github.event_name == 'pull_request' }}
 
-    # Initializes the CodeQL tools for scanning.
-    - name: Initialize CodeQL
-      uses: github/codeql-action/init@v1
-      with:
-        languages: ${{ matrix.language }}
-    - name: Autobuild
-      uses: github/codeql-action/autobuild@v1
-    - name: Perform CodeQL Analysis
-      uses: github/codeql-action/analyze@v1
+      # Initializes the CodeQL tools for scanning.
+      - name: Initialize CodeQL
+        uses: github/codeql-action/init@v2
+        with:
+          languages: ${{ matrix.language }}
+      - name: Autobuild
+        uses: github/codeql-action/autobuild@v2
+      - name: Perform CodeQL Analysis
+        uses: github/codeql-action/analyze@v2
+        with:
+          languages: ${{ matrix.language }}
diff --git a/.github/workflows/go.yml b/.github/workflows/go.yml
diff --git a/.github/workflows/simpledb-test.yml b/.github/workflows/simpledb-test.yml
@@ -0,0 +1,23 @@
+name: simpledb-test
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Set up Go
+        uses: actions/setup-go@v2
+        with:
+          go-version: 1.19
+      - name: Linearization Test
+        run: make linear-simpledb
+      - uses: actions/upload-artifact@v2
+        if: always()
+        with:
+          path: simpledb/porcupine/*.html
+      - name: Crash Test
+        run: make crash-simpledb
diff --git a/.github/workflows/unit-test.yml b/.github/workflows/unit-test.yml
@@ -0,0 +1,19 @@
+name: unit-test
+on:
+  push:
+    branches: [ main ]
+  pull_request:
+    branches: [ main ]
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Set up Go
+        uses: actions/setup-go@v2
+        with:
+          go-version: 1.19
+      - name: Go vet
+        run: make vet
+      - name: Test
+        run: make unit-test
diff --git a/Makefile b/Makefile
@@ -69,6 +69,13 @@ crash-simpledb:
 	$(GO) clean -testcache
 	$(GO) test -v -timeout 30m --tags simpleDBcrash $(GOFLAGS) ./simpledb/_crash_tests $(TESTFLAGS)
 
+.PHONY: linear-simpledb
+linear-simpledb:
+	@echo
+	@echo "==> Running simpledb linearizability tests <=="
+	$(GO) clean -testcache
+	$(GO) test -v -timeout 30m --tags simpleDBlinear $(GOFLAGS) ./simpledb/porcupine $(TESTFLAGS)
+
 .PHONY: generate-test-files
 generate-test-files:
 	@echo
@@ -82,5 +89,5 @@ vet:
 	@echo "==> Go vet <=="
 	$(GO) vet $(TESTS)
 
-.PHONY: full-test
-full-test: vet unit-test race-simpledb crash-simpledb
+.PHONY: test
+test: vet unit-test linear-simpledb race-simpledb crash-simpledb
diff --git a/go.mod b/go.mod
@@ -1,6 +1,7 @@
 module github.com/thomasjungblut/go-sstables
 
 require (
+	github.com/anishathalye/porcupine v0.1.2
 	github.com/golang/snappy v0.0.0-20180518054509-2e65f85255db
 	github.com/libp2p/go-buffer-pool v0.0.2
 	github.com/ncw/directio v1.0.5
@@ -18,4 +19,6 @@ require (
 	gopkg.in/yaml.v3 v3.0.0-20200313102051-9f266ea9e77c // indirect
 )
 
-go 1.18
+replace github.com/anishathalye/porcupine v0.1.2 => github.com/tjungblu/porcupine v0.0.0-20221116095144-377185aa0569
+
+go 1.19
diff --git a/go.sum b/go.sum
@@ -19,6 +19,8 @@ github.com/steakknife/hamming v0.0.0-20180906055917-c99c65617cd3/go.mod h1:hpGUW
 github.com/stretchr/objx v0.1.0/go.mod h1:HFkY916IF+rwdDfMAkV7OtwuqBVzrE8GR6GFx+wExME=
 github.com/stretchr/testify v1.7.0 h1:nwc3DEeHmmLAfoZucVR881uASk0Mfjw8xYJ99tb5CcY=
 github.com/stretchr/testify v1.7.0/go.mod h1:6Fq8oRcR53rry900zMqJjRRixrwX3KX962/h/Wwjteg=
+github.com/tjungblu/porcupine v0.0.0-20221116095144-377185aa0569 h1:acDBvgSBtnyBidmpmTEgxStjXeuYyfG3fF72khP24/Y=
+github.com/tjungblu/porcupine v0.0.0-20221116095144-377185aa0569/go.mod h1:+z336r1WR0gcwl1ALfoNBpDTCW06vO5DzBwunEcSvcs=
 golang.org/x/exp v0.0.0-20181210123644-7d6377eee41f h1:wJ3O7VtAmBlW5LFzggOI2U6CBWIkG+/IYf4Q/VGJdaA=
 golang.org/x/exp v0.0.0-20181210123644-7d6377eee41f/go.mod h1:CJ0aWSM057203Lf6IL+f9T1iT9GByDxfZKAQTCR3kQA=
 golang.org/x/xerrors v0.0.0-20191204190536-9bdfabe68543/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=

diff --git a/simpledb/README.md b/simpledb/README.md
@@ -136,4 +136,12 @@ The latter can be run using `make crash-simpledb`, which will start a webserver
 REST. The test code will then try a couple of deterministic and random patterns while killing the database and checking
 its results continuously.
 
-The test suite is reusable for other databases, as long as they implement the REST interface. .
+The test suite is reusable for other databases, as long as they implement the REST interface.
+
+## Linearizability Testing
+
+Using [Porcupine](https://github.com/anishathalye/porcupine/) we can verify whether a sequence of operations on the database are linearizable.
+
+The test suite in the porcupine folder will create a small database client that tracks operations with their results and their timings. With that history the framework can then reconstruct whether given operation on the state was valid or not.
+
+The tests in the porcupine folder are running a synthetic get/put/delete sequence (also from multiple goroutines) with overlapping keys. The crash tests described above also have a client recording the operations. After all runs the linearizability of the test is verified, in addition to the existing assertions. 
diff --git a/simpledb/_crash_tests/.gitignore b/simpledb/_crash_tests/.gitignore
@@ -0,0 +1 @@
+*.html