A ferramenta open-source de análise estática do Facebook, Infer, foi recentemente atualizada com detecção de condição-de-corrida (race conditions) em códigos Java via RacerD. RacerD identifica condiçoes-de-corrida nos métodos das classes que fazem uso da anotação @ThreadSafe.
O Facebook utilizou o RaceD em seus códigos no último ano, e foram identificados mais de 1.000 problemas de multithread antes de entrar em produção. Esta capacidade de avaliar concorrência chega agora para os desenvolvedores Java que utilizam o Infer para detecção de bugs.
Uma condição-de-corrida é um tipo de erro de concorrência que ocorre quando duas threads acessam o mesmo objeto sem sincronização, fazendo uma sobreposição de execução, e pelo menos um dos acessos à variável é para realizar uma escrita. Problemas de concorrência são difíceis de realizar o debug, e mais difícil ainda de reproduzir depois de encontrado o problema.
O RacerD executa uma análise de concorrência rápida e útil em escala. O RacerD é rápido pois não analisa todo o código, e sim apenas o código que pode ser executado concorrentemente.
O RacerD classifica como um código que pode ser executado concorrentemente procurando por classes, métodos, e interfaces que são explicitamente anotadas com @ThreadSafe ou por locks criados pelo comando synchronized. Quando uma classe ou interface é anotada com @ThreadSafe, todas as subclasses/implementações também são avaliadas. Para aumentar a cobertura de código com o RecerD, algumas anotações podem ser úteis como: @ThreadConfined, @Functional, @ReturnsOwnership, ou @VisibleForTesting.
A análise do RecerD pode ser iniciada através do próprio comando infer, que roda também outras análises do Infer, ou pelo comando infer --racerd-only, que roda apenas o RacerD. Por exemplo, o comando infer --racerd-only -- javac StockPortifolio.java rodará o RacerD no StockPortifolio.java.
O código a seguir, quando inspecionado pelo RacerD, alertará uma condição-de-corrida.
@ThreadSafe
public class StockPortfolio {
int shares = 0;
public void buy(int count) {
if (count > 0) {
shares += count;
}
}
public int sell(int count){
if (count >= 0 && shares - count >= 0) {
shares -= count;
return shares;
} else {
return 0;
}
}
}
O RacerD aponta a seguinte falha:
Read/Write race. Public method int StockPortfolio.sell(int) reads from field StockPortfolio.shares. Potentially races with writes in methods void StockPortfolio.buy(int), int StockPortfolio.sell(int)
O RacerD alerta que há dados com condições-de-corrida em leitura e escrita. Atualmente o RacerD limita-se apenas a análise de condição-de-corrida em dados; não checa outros tipos de condição-de-corrida como deadlock e atomicidade. O RacerD também não avalia em casos para dados:
- Alising
- Objetos declarados localmente fora de escopo
- Acessos protegidos por locks diferentes
- Objetos locais contendo objetos não pertencentes
- Referências do tipo weak e comando volatile
Essas limitações derivam do objetivo do projeto para reduzir falsos positivos, mesmo que ele leve a falsos negativos.
Co-authors Sam Blackshear and Peter O'Hearn wrote in their announcement:
O co-autor Sam Blackshear e Peter O'Hearn descreveram em seu anúncio:
O Infer é utilizado pelo Facebook tanto em deployments rodando em bash quanto como um bot em code-review. No deployment para revisão de código, o Infer executa como parte do sistema de Integração Contínua (CI) do Facebook. Para cada código alterado por um desenvolvedor, o CI roda o Infer para os jobs de compilação e teste.
O RacerD está disponível no GitHub, e mais detalhes podem ser encontrados em seu guia do usuário.