Algumas das falhas mais perigosas dos sistemas podem ser detectadas antes de o código ser escrito, se o próprio design for tratado como um sistema passível de análise. Esse é o foco da apresentação de Hillel Wayne, que explica como os princípios dos métodos formais ajudam a examinar sistemas futuros e a detectar problemas de resiliência, concorrência e falhas antes que se transformem em erros operacionais.
Wayne começa com um exemplo simplificado do que chama de «executor de tarefas»: o sistema verifica se a tarefa foi concluída, depois marca a conclusão e, em seguida, executa a tarefa. A sequência parece lógica, mas falha quando ocorre um erro durante a execução. A tentativa pode ser repetida depois de a tarefa ter sido registrada como concluída, fazendo com que ela não seja realmente executada. Quando o registro da conclusão é transferido para depois da execução, surge outro problema: dois executores concorrentes podem executar a mesma tarefa duas vezes antes de qualquer um deles registrar sua conclusão.
Esse não é apenas um problema teórico; a apresentação o relaciona a exemplos como sistemas de envio de encomendas que podem enviar o pedido duas vezes, sistemas de agendamento que podem reservar o mesmo horário para duas pessoas e mecanismos de instalação de aplicativos que podem entrar em comportamento destrutivo quando o pedido é repetido.
Comece definindo o que significa «correto»
Wayne propõe formular os requisitos do sistema na forma de propriedades binárias: ou são verdadeiras ou são falsas. Entre os exemplos estão a propriedade de que a tarefa não seja executada mais de uma vez, uma propriedade de segurança que impede que algo ruim aconteça, e a de que a tarefa seja executada pelo menos uma vez, uma propriedade de vivacidade que garante que algo desejado aconteça.
A apresentação enfatiza que as propriedades não têm todas a mesma força. Um sistema capaz de processar 10.000 consultas por segundo satisfaz automaticamente a propriedade de processar duas consultas por segundo, mas o inverso não é verdadeiro. Assim, passar em uma propriedade forte pode ser uma evidência da correção de um conjunto de propriedades mais fracas, enquanto a falha de uma propriedade mais fraca ajuda a restringir a causa do problema. Wayne relaciona essa ideia à pirâmide de testes: muitos testes unitários podem ser mais úteis para diagnosticar o erro do que um número limitado de testes de ponta a ponta.
O modelo simplificado revela o problema fundamental
Em vez de representar o sistema com todos os seus detalhes, Wayne recomenda construir um modelo abstrato que contenha o mínimo de estado necessário: a etapa atual do algoritmo, se a tarefa está marcada como concluída e o número de vezes que foi executada. Isso permite explorar os estados possíveis e os caminhos que o sistema pode seguir, incluindo estados de falha e novas tentativas.
Nos métodos formais, esse modelo e essas propriedades podem ser codificados usando fórmulas lógicas e então verificados com ferramentas como verificadores de modelos e solucionadores SMT. Mas a ideia prática apresentada não exige o uso direto dessas ferramentas; o engenheiro pode adotar a mesma forma de pensar acompanhando os estados e as transições possíveis.
O fator «adversário» na concorrência e nas falhas
Wayne propõe imaginar cada fonte de não determinismo, como entrada do usuário, concorrência, aleatoriedade, tempos limite e interrupções de servidores, como um «adversário» que sempre escolhe o pior resultado possível. Se o sistema pode repetir a tentativa indefinidamente, esse adversário escolherá a falha todas as vezes, revelando que a propriedade de vivacidade não é garantida, mesmo que o sucesso seja teoricamente possível.
Ele também explica que a existência de executores concorrentes exige representar algumas variáveis como locais para cada processo e outras como compartilhadas entre o sistema e o mundo externo. Ao explorar diferentes ordens de execução, é possível chegar a um estado em que a tarefa seja executada duas vezes, mesmo quando cada executor parece correto isoladamente.
As suposições fazem parte do design
A correção do sistema não depende apenas de suas propriedades, mas também das suposições sobre o ambiente em que ele opera. Um design pode exigir a forte suposição de que o processo nunca falha, enquanto outro pode funcionar se a falha ocorrer um número limitado de vezes. Wayne observa que reordenar as etapas pode reduzir as suposições de vivacidade, mas aumentar os requisitos de segurança, como a necessidade de garantir que exista apenas um executor por vez.
A situação também muda quando o ambiente operacional muda. Depender de consistência forte em um banco de dados e depois migrar para consistência eventual pode fazer com que propriedades antes corretas deixem de ser garantidas, mesmo que o código do sistema não tenha mudado. Portanto, as suposições sobre o provedor de serviços ou o banco de dados não devem ser consideradas detalhes externos; elas são condições diretas para a correção do design.
O que muda na prática?
O valor prático do método não está em substituir os testes nem em defender o uso de ferramentas formais em todos os projetos, mas em tornar as perguntas de design mais rigorosas: quais são os estados possíveis? Qual é a pior ordem dos eventos? O que realmente controlamos? E quais suposições a equipe não tem como garantir? Quanto mais forte for a propriedade exigida ou menos previsível for o ambiente, mais complexo precisará ser o design do sistema, ou será necessário flexibilizar a propriedade exigida, como transformar a condição «processar todas as mensagens» em «processar as mensagens ou enviá-las para uma fila de mensagens mortas».
Wayne apresenta essas ideias como ferramentas de pensamento derivadas dos métodos formais, não como um substituto pronto para o julgamento de engenharia. A questão em aberto em todo sistema continua sendo o grau de precisão do modelo e das suposições utilizadas; se um estado for ignorado ou a equipe presumir um comportamento que o ambiente não garante, a análise poderá provar a correção de um modelo que não se parece com o sistema real.