A static analysis tool for Go that supports expressing lock dependency rules and verifies lock-related preconditions, postconditions, invariants, and side effects in shared-memory concurrent programs.
TODO (copy from proposal/paper)
Concurrency bugs such as data races and deadlocks in shared-memory systems using mutual exclusion locks arise only under particular runtime timing conditions. In languages like Go, programs do not encode lock ordering or the programmer's intended synchronization patterns, so these properties cannot be checked statically.
By allowing programmers to provide lightweight annotations, lock dependencies and patterns can be verified statically. This is similar to a function signature enforcing a contract at compile time. This enables earlier detection of deadlocks and race-prone locking patterns, before deployment and runtime.
go run main.go -file <path to file>or
go run main.go -pkg <path to pkg>Use -v flag for verbose logging features.
Use -l for lenient mode (utilizes heuristics to lower warnings emitted based on observable goroutine paths in the code):
go run main.go -pkg <path to pkg> -lUse -s for strict mode (does not assume anything about the thread the code is running in):
go run main.go -pkg <path to pkg> -s-l and -s are mutually exclusive.
/analyzer: SSA and CFG analysis/ir: internal representation for the analysis tool after the parser completes/parse: parse annotations from the source file or package
Run all tests from repo root:
go test ./...Run examples end-to-end suite only:
go test ./tests/e2eRegenerate expected snapshot files after intentional analyzer output changes:
go test ./tests/e2e -run Expected -updateGolden snapshot naming convention:
*.lenient.expected: expected findings for lenient mode (non-strict run)*.strict.expected: expected findings for strict mode
Example:
tests/e2e/testdata/examples__simple__simple.lenient.expectedtests/e2e/testdata/examples__simple__simple.strict.expected