Esperar que race conditions surjam em produção não é testar. É esperança disfarçada de diligência.
Você pode executar seu app por semanas, monitorar seus dashboards de metrics e ainda assim lançar um bug de concorrência que só é disparado quando duas requests atingem exatamente a mesma janela de evicção de cache. O problema não é que você tenha azar. O problema é que sua estratégia de teste depende do scheduler ser malicioso a seu favor, no momento exato, enquanto você acontece de estar olhando.
Há uma maneira melhor. O model checking permite explorar todos os interleavings possíveis da sua lógica concorrente em segundos, não em dias. Ele encontrará a race condition para a qual você não pensou em escrever um teste.
O que o model checking realmente faz
O model checking não é um fuzzer. Ele não joga inputs aleatórios no seu código e reza. Ele constrói um modelo matemático dos estados possíveis do seu sistema e os percorre de forma exaustiva.
Pense no seu programa concorrente como um grafo. Cada node é um estado: os valores das suas variáveis, o conteúdo das suas queues, qual thread tem qual lock. Cada aresta é um passo: uma thread lendo um valor, adquirindo um mutex ou enviando uma mensagem. O scheduler escolhe qual thread roda em seguida, e essa escolha ramifica o grafo.
Um model checker percorre cada caminho nesse grafo. Se algum caminho leva a duas threads escrevendo na mesma memória sem sincronização, ele reporta um counterexample: a sequência exata de passos que dispara o bug.
O insight chave é que o model checker controla o scheduler. Em produção, você está à mercê do sistema operacional. Em um model checker, você é o sistema operacional. Você pode pausar uma thread antes que ela execute uma linha crítica, deixar outra thread rodar seu método inteiro, depois retomar a primeira. Você pode explorar o interleaving que na vida real exigiria um raio cósmico e uma falha de rede para ser reproduzido.
Uma race condition que os model checkers pegam em milissegundos
Aqui está um bug clássico: duas goroutines incrementando um counter compartilhado.
package main
import (
"fmt"
"sync"
)
func main() {
var counter int
var wg sync.WaitGroup
for i := 0; i < 2; i++ {
wg.Add(1)
go func() {
defer wg.Done()
// Read, increment, write: three steps
val := counter
val++
counter = val
}()
}
wg.Wait()
fmt.Println(counter) // Expected 2, often prints 1
}Execute isso mil vezes e ele pode imprimir 2 sempre. O scheduler não é seu inimigo sob demanda. Mas um model checker vê a sequência read-increment-write de três passos e sabe: se a goroutine A lê 0, depois a goroutine B lê 0, então ambas incrementam e escrevem 1, o counter termina em 1 em vez de 2.
Ele não precisa rodar por dias. Precisa explorar dois branches.
Como fazer model checking do seu próprio código
Você não precisa verificar formalmente toda a sua codebase para obter valor do model checking. A maioria das equipes obtém 80% do benefício modelando os 20% do código onde a concorrência realmente importa.
O workflow se parece com isto:
-
Isole o componente concorrente. Remova os HTTP handlers, as queries de banco de dados e o logging. Foque na state machine: quais threads ou goroutines existem, qual shared state elas tocam e quais são as primitivas de sincronização?
-
Escreva um modelo abstrato. Substitua estruturas de dados reais por versões simplificadas que capturem o comportamento que você se importa. Se você está verificando uma job queue, não precisa do payload real do job. Você precisa de uma queue, workers e uma flag que diga se um job está em andamento.
-
Defina as properties que você quer que se mantenham. Essas são suas invariantes. “Dois workers nunca processam o mesmo job.” “Um job nunca se perde.” “O cache e o banco de dados nunca discordam.”
-
Deixe o model checker rodar. Ele dirá “todas as invariantes se mantêm” ou lhe entregará um counterexample trace.
Aqui está como um modelo mínimo se parece em Python usando um simples explicit-state checker:
from collections import namedtuple
# Abstract model of a counter with two threads
State = namedtuple('State', ['counter', 'pc1', 'pc2'])
def successors(state):
"""Return all states reachable in one step."""
results = []
c, pc1, pc2 = state
# Thread 1: three-step increment
if pc1 == 0:
results.append(State(c, 1, pc2)) # read
elif pc1 == 1:
results.append(State(c, 2, pc2)) # increment
elif pc1 == 2:
results.append(State(c + 1, 3, pc2)) # write
# Thread 2: three-step increment
if pc2 == 0:
results.append(State(c, pc1, 1))
elif pc2 == 1:
results.append(State(c, pc1, 2))
elif pc2 == 2:
results.append(State(c + 1, pc1, 3))
return results
def check():
initial = State(0, 0, 0)
visited = set()
stack = [initial]
while stack:
state = stack.pop()
if state in visited:
continue
visited.add(state)
# Invariant: if both threads finished, counter must be 2
if state.pc1 == 3 and state.pc2 == 3 and state.counter != 2:
print(f"BUG: counter={state.counter}")
return
stack.extend(successors(state))
print("No race condition found in model.")
check()Isso não é pronto para produção. São vinte linhas de Python que demonstram a ideia. Um model checker real como TLA+, Spin ou mCRL2 lida com deduplicação de estados, properties de lógica temporal e partial-order reduction para que você possa verificar sistemas com milhões de estados. Mas o modelo mental é o mesmo: codifique seu sistema, estabeleça as invariantes, explore.
A ressalva: explosão do espaço de estados
O model checking não é de graça. Se você tem quatro threads, cada uma com dez possíveis próximos passos, seu grafo de estados cresce exponencialmente. Adicione um inteiro de 64 bits e o espaço de estados se torna literalmente inchecável.
A solução é abstração. Você não modela seu cache real. Você modela “cache tem a key” ou “cache não tem a key”. Você não modela seu banco de dados real. Você modela “committed” ou “uncommitted”.
Esta é a parte que faz as pessoas tropeçarem. Elas tentam fazer model checking do código real e o checker roda para sempre. Então abandonam o model checking por completo, o que é como abandonar unit tests porque você tentou testar a aplicação inteira em um único test case.
A disciplina é: modele a concorrência, não a business logic. Se sua race condition depende do valor exato de um user ID, você já perdeu. Race conditions acontecem por causa do interleaving, não por causa dos valores dos dados.
Ferramentas que realmente funcionam
Se você quer começar a fazer model checking de código real, tem opções.
Para Go: gosim permite que você execute programas Go com um scheduler determinístico que você controla a partir de um model checker. Ele encontrará o interleaving que quebra suas suposições sobre sync.Mutex.
Para Rust: shuttle é um framework de teste de concorrência determinístico da AWS Labs. Ele executa seu código async milhares de vezes com diferentes escolhas de scheduler e encontrará races que o loom (outra ferramenta excelente) verifica no nível do memory model.
Para sistemas distribuídos: TLA+ é a escolha de força industrial. A Amazon o usou para encontrar bugs no DynamoDB e S3 antes de lançá-los. A curva de aprendizado é real, mas o retorno sobre o investimento para sistemas críticos é mensurável.
Para um começo suave: Escreva um script Python como o acima. Leva uma hora, encontra bugs e constrói a intuição que torna o TLA+ menos misterioso quando você precisa dele.
O que isso não substitui
O model checking encontra logic errors em código concorrente. Ele não encontra performance regressions, memory leaks ou bugs que só aparecem sob carga de produção. Ele não vai te dizer que sua contenção de mutex explode a 10.000 requests por segundo.
Use-o junto com stress testing, não em vez dele. O stress testing te diz se seu sistema sobrevive à carga. O model checking te diz se seu sistema sobrevive aos interleavings que essa carga cria.
Por onde começar
Escolha um componente concorrente que já tenha te mordido antes. Uma job queue, um connection pool, um rate limiter. Escreva as invariantes em plain English. Depois passe uma tarde construindo um modelo minúsculo.
Você provavelmente encontrará um bug que você não sabia que existia. Ou vai ganhar confiança de que o bug que você estava preocupado não pode acontecer. Qualquer um dos dois resultados vale mais do que outra semana olhando gráficos de produção e esperando.
Se você quer um passo concreto a seguir, o tutorial Learn TLA+ vai te levar de zero a verificar um protocol de consensus distribuído em um fim de semana. Para Go e Rust, adicione shuttle ou loom à sua test suite e execute em CI. Na primeira vez que ele pegar uma race antes do code review, você vai se perguntar por que um dia confiou no scheduler para fazer seu testing por você.