Makefile


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

test:
	go clean -testcache
	go test ./... -v

# verify: static + dynamic correctness checks. Fast enough for routine use.
#   go vet / staticcheck  - static analysis
#   go test -race -short  - race detector over the (size-capped) test + property
#                           suites; -short keeps the million-element cases out so
#                           the race build stays quick. See docs/verification.md.
verify:
	go vet ./...
	staticcheck ./...
	go test -race -short ./...

# verify-model: exhaustively model-check the concurrent sleep sort with TLA+/TLC
# (a model of sort/sleep.go, not the Go code itself). See formal/tla/README.md.
verify-model:
	java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \
		-metadir /tmp/tlc-sleepsort \
		-config formal/tla/SleepSort.cfg formal/tla/SleepSort.tla
	java -cp $(HOME)/tools/tlaplus/tla2tools.jar tlc2.TLC -workers auto \
		-metadir /tmp/tlc-parallelsort \
		-config formal/tla/ParallelSort.cfg formal/tla/ParallelSort.tla

# verify-formal: machine-checked deductive proof of a monomorphized insertion
# sort with Gobra (Go verifier, Viper+Z3 backend), run from its container image.
# See formal/README.md.
verify-formal:
	podman run --rm -v $(PWD)/formal:/gobra/formal:z \
		ghcr.io/viperproject/gobra:latest \
		-i /gobra/formal/insertion.go /gobra/formal/selection.go
bench:
	go test -run=xxx -bench=. ./... | tee bench.out
sortbench:
	go test -run=xxx -bench=. ./sort | tee sortbench.out
queuebench:
	go test -run=xxx -bench=. ./queue | tee queuebench.out
searchbench:
	go test -run=xxx -bench=. ./search | tee searchbench.out
profile:
	go test -run=xxx -bench=BenchmarkQuickSort ./sort -memprofile memprofile.out -cpuprofile cpuprofile.out
	go tool pprof cpuprofile.out