Bugs em implementações de Raft com compute abundante
Bugs em implementações de Raft com compute abundante
A Antithesis, plataforma de testes autônomos para sistemas distribuídos, encontrou bugs em todas as implementações de Raft que testou - incluindo HashiCorp Raft, Aeron Cluster, OpenRaft e MicroRaft. Os bugs violam a propriedade central de segurança do protocolo (state machine safety / total order delivery), mesmo essas implementações tendo passado por métodos formais, code review, testes unitários e anos em produção.
Abordagem de teste
A equipe usou um workload chamado Chain of Blocks: um cluster de 3 nós com uma máquina de estado que apenas faz hash dos comandos recebidos e um cliente stateless que envia arrays de bytes aleatórios. Um engenheiro júnior conseguiria implementar isso em menos de um dia. A chave é que o sistema roda dentro do ambiente de simulação determinística da Antithesis, com injeção agressiva de falhas (partições de rede, turbulência). Apenas partições de rede já foram suficientes para revelar divergências.
Bugs no HashiCorp Raft
Três bugs distintos foram encontrados:
Bug 1 - Consenso quebrado por heartbeats assíncronos (segurança): Heartbeats (AppendEntries sem entradas) são processados na thread de I/O em vez da thread principal, criando uma race condition. Isso pode fazer um nó criar uma entrada de log com o termo errado, levando a divergência de estado entre réplicas. Também pode causar violação de election safety (dois líderes no mesmo termo) quando o handler assíncrono de heartbeat regride o currentTerm para um valor menor após um voto já ter sido concedido para um termo superior.
Bug 2 - Deadlock após transferência de liderança (liveness): Durante uma transferência de liderança, se o líder original perde a liderança por outro motivo, a goroutine de transferência fica bloqueada para sempre com uma flag global "transferência em progresso" ativa. Se esse nó for reeleito líder no futuro, recusará todas as requisições de clientes indefinidamente.
Bug 3 - Livelock na instalação de snapshots (liveness): A implementação não descarta o log existente ao instalar um snapshot (violando a Regra 7 da Figura 13 do paper). Isso cria um ciclo infinito: o follower rejeita AppendEntries por causa de entradas de log stale, o líder responde com novo InstallSnapshot, e assim por diante.
Reflexões sobre por que os bugs existem
O paper identifica quatro suposições implícitas no paper do Raft que implementadores frequentemente violam:
- Cada nó é um processo síncrono - a spec TLA+ assume transições atômicas, mas nenhuma implementação real é puramente síncrona.
- Cada resposta pode ser mapeada a uma requisição - correlação request/response é crucial para corretude, mas não é óbvia em implementações sobre TCP/UDP.
currentTermevotedForsão consistentes - devem ser persistidos atomicamente, mas mudam em pontos diferentes do protocolo.- O protocolo inteiro é formalmente verificado -
InstallSnapshote extensões como leadership transfer não estão na spec TLA+, deixando implementadores sem guia.
Conclusão
Métodos formais são necessários mas insuficientes: verificam o modelo, não a implementação. A abundância de compute torna viável testar sistemas sob falhas de forma que métodos básicos revelam bugs que antes exigiriam meses de teste manual.