My first exposure to AST instrumentation in Go
Published:
Intro to Go Concurrency Verification
Due to its simplicity and functionality, Go is receiving attention among developers. However, there are not that many tools to focus on the correctness of Go concurrency. Two recent Go static verification papers (1, 2) extract a system of type equations from the Go source code SSA IR 1 equivalent. A calculus mirrors channel-based behaviors of Go programs (goroutines, functions, channel create/communicate/close, etc.) in the form of mutually recursive definitions. Table1 explains the syntax of MiGo. The behavioral typing system derives from MiGo can be checked for liveness and safety in three steps:
Single Static Assignment (SSA) is a form property of Intermediate Representation (IR), which requires that each variable assigned precisely once. Go has a package that generates SSA IR from source. ↩