Static analyzers help us to avoid a whole slew of errors and are used widely in the industry. This proposal is for making static analyzers even more powerful and helpful for programmers by letting programmers specify rules they would like the analyzer to check for voilations of in their programs. The rules are specified in the form of annotations within the program. If a rule is to be enforced in multiple sections within a program, for example, a rule like "every mu.Lock() must be followed by mu.UnLock()" would apply to all instances where mu.Lock() is called. If the static analyzer can check for voilations after being once specified, it would lift the burder from the programmer of manually scanning through every instsance of mu.Lock() and checking if the Unlock call appropriately follows.
Consider the following section from a redacted go program.
func (rf *Raft) RequestVote(args *RequestVoteArgs, reply *RequestVoteReply) {
...
// Note that since the body of persist might require a lock, we need to unlock
// before we call persist.
rf.mu.Unlock()
rf.persist()
...
}
The programmer, aptly, notes that calling rf.persist() without unlocking the mutex might result in a deadlock. Note that this also assumes that it is the responsibility of the persist function to use locks where needed. However, since the program is long and call to persist appers in many other places within the program, this is a knowledge that must be used throghout the program. For example, below is an another section from the same go program (redacted) where this issue occurs. Without support from static analyzer, these kinds of rules must be remembered by the programmer themselves. While easy to remember once, it's easy for the programmer to miss applying the rule in every instance where necessary. This is where static analyzers can help.
func (rf *Raft) AppendEntries(args *AppendEntriesArgs, reply *AppendEntriesReply) {
...
rf.mu.Unlock()
reply.Term = currentTerm
rf.persist()
...
}
TODO: