Não duplicar e não perder: modele o retry antes de escolher a ordem das gravações

Em uma apresentação na InfoQ, Hillel Wayne explica como encontrar defeitos de arquitetura a partir de uma descrição mínima do sistema.[18] Seu exemplo mostra o dilema de marcar uma tarefa como concluída antes do efeito ou executar o efeito antes da marcação: uma ordem pode perder trabalho; a outra pode permitir duplicidade.[18] Trocar as linhas de lugar não cria automaticamente uma garantia.

O que muda para quem desenvolve

Wayne separa propriedades de segurança, como impedir duas execuções, e progresso, ou liveness, como assegurar ao menos uma execução.[18] Ele também distingue variáveis internas de efeitos no mundo: reverter uma marca não desfaz um pacote já enviado.[18]

Na minha análise, esse vocabulário ajuda a evitar requisitos que parecem claros e não são. Uma linha com estado concluído é evidência sobre o banco. O objetivo do produto pode ser que o destinatário receba uma mensagem, que uma cobrança não seja duplicada ou que uma publicação não desapareça. Escreva a propriedade em termos desse resultado observável.

A apresentação propõe reduzir o sistema a variáveis suficientes para preservar seus riscos e explorar transições e interleavings.[18] Também recomenda raciocínio adversarial sobre temporização, concorrência, entradas e disponibilidade.[18] Um modelo pequeno não precisa carregar o framework inteiro para revelar um contraexemplo relevante.

Como aplicar

Considere um fluxo hipotético que envia uma notificação e grava a conclusão. Modele apenas posição de cada executor, marca compartilhada e quantidade de envios. Esse é um exercício de projeto, não um teste já realizado.

Defina primeiro duas expectativas: a solicitação não deve produzir envios duplicados e deve terminar enviada ou em um estado explícito de falha tratável. Depois liste as premissas: pode haver concorrência? O envio retorna confirmação? A mesma solicitação conserva sua identidade ao tentar novamente?

Explore interrupções após cada etapa. Se a marca vier primeiro, examine uma falha antes do envio. Se o envio vier primeiro, examine uma falha antes da marca e a entrada de outro executor. Registre a sequência de estados que viola a expectativa, em vez de apenas afirmar que existe uma corrida.

Use o contraexemplo para decidir entre idempotência no destino, deduplicação, coordenação ou enfraquecimento explícito da promessa. A escolha depende do efeito e do que o sistema externo permite. Só depois transforme a decisão em testes de implementação.

Cuidados e limites

A ausência de contraexemplos no modelo não cobre comportamentos omitidos.[18] Progresso também depende das premissas sobre falhas: permitir tentativas infinitas não garante uma conclusão se o ambiente falhar indefinidamente.[18]

Wayne distingue verificar código ou pipeline de verificar comportamento de agentes, para o qual não apresenta uma solução estabelecida.[18] Ele alerta que LLMs podem gerar invariantes fracos ou tautológicos e lidar mal com liveness.[18] Use a assistência para reduzir trabalho de escrita, não para aceitar uma propriedade que apenas repete o estado interno. O valor do modelo está em tornar a promessa e suas condições contestáveis.

Fonte

[18] Fonte: InfoQ, apresentação de Hillel Wayne com transcrição