Apresentando FizzBee: simplificando métodos formais para todos

Dois anos atrás, compartilhamos um artigo no The New Stack sobre o uso de métodos formais pela Amazon para verificar seus sistemas distribuídos desde 2012. Agora, grandes players como Amazon, Google, Microsoft, MongoDB, Confluent, Oracle, Elastic, CockroachDB e muitos mais estão todos adotando métodos formais para seus sistemas. Apesar dos imensos benefícios e relevância desta técnica no desenvolvimento de software moderno, a sua adoção generalizada tem sido dificultada pela complexidade das ferramentas existentes.

Neste artigo, apresentaremos o FizzBee, um novo sistema de métodos formais que você pode dominar em apenas um fim de semana.

O que são métodos formais?

Os métodos formais abrangem técnicas rigorosas empregadas para especificar, modelar, projetar e verificar sistemas complexos usando lógica matemática. Particularmente relevantes para engenheiros de software que trabalham em SaaS baseados em nuvem ou sistemas distribuídos, programação simultânea e domínios semelhantes, esses métodos oferecem uma abordagem sistemática para garantir correção e confiabilidade em sistemas de software e hardware.

Os métodos formais encontram bugs nos projetos de sistemas que não podem ser encontrados por meio de nenhuma outra técnica que conhecemos.

— Chris Newcombe, AWS

Como encontramos bugs de design de sistema hoje?

Hoje, contamos com a elaboração de documentos de design e revisões de equipe para descobrir bugs de design de sistema. No entanto, esta abordagem é insuficiente devido à sua ineficiência e eficácia limitada. Contamos com a correspondência de padrões com base em experiências passadas e antipadrões conhecidos para identificar falhas de design porque nos falta capacidade mental e tempo para explorar todos os resultados possíveis. É aqui que os computadores se destacam: explorando bilhões de estados sem esforço em minutos.

Por que os métodos formais não estão pegando

A ferramenta de métodos formais mais popular para especificação de sistemas distribuídos é o TLA+. Embora muitos reconheçam o seu potencial para melhorar o seu trabalho, a barreira reside na falta de tempo para aprender ou usar o TLA+.

Mesmo na Amazon, Chris Newcombe, que começou a usar o TLA+ na Amazon, enfrentou desafios para convencer os colegas a adotar o TLA+, já que os engenheiros têm pouco tempo livre, a menos que sejam obrigados por necessidade ou mandato executivo.

O TLA+ oferece recursos de verificação poderosos para projetos de sistemas. No entanto, sua sintaxe e abordagem matemática podem ser intimidantes para muitos engenheiros de software, especialmente aqueles mais acostumados com linguagens de programação convencionais como Python. Expressar certos algoritmos em TLA+ pode exigir formulações matemáticas complexas, enquanto a mesma lógica pode ser facilmente transmitida usando a sintaxe familiar do Python.”

FizzBee: métodos formais para todos

FizzBee, uma adição recente aos sistemas de métodos formais, preenche a lacuna de acessibilidade com sua interface amigável e sintaxe semelhante ao Python. Isso torna mais fácil para desenvolvedores de todos os níveis expressar algoritmos complexos e projetos de sistemas.

1. Fácil de aprender: se você escreveu alguns scripts Python, poderá compreender o código FizzBee em apenas 10 minutos. Então, você poderá aprender os princípios de verificação de modelo em poucas horas.
2. Legibilidade aprimorada: as especificações do FizzBee são projetadas para fácil compreensão por revisores e desenvolvedores. Ao contrário de outras ferramentas como TLA+, a sintaxe familiar do FizzBee garante que mesmo não-autores possam entender as especificações, facilitando processos de revisão e implementação mais suaves.
3. Flexibilidade multiparadigma: FizzBee oferece opções versáteis de programação, incluindo estilos funcionais, imperativos, estruturados, procedurais e orientados a objetos. Isto permite aos desenvolvedores escolher a melhor abordagem para cada problema, levando a soluções concisas e adaptáveis.
4. Visualização: O gráfico de transição de estado do FizzBee auxilia na depuração, fornecendo uma representação visual. Isto também melhora a compreensão do processo de verificação do modelo e ajuda os usuários a identificar e resolver problemas de forma mais eficaz.
5. Playground Online: FizzBee oferece um playground online para praticar, experimentar e explorar exemplos, tornando-o acessível tanto para aprendizagem quanto para exploração.

Modelando um sistema de transferência eletrônica

Vamos modelar uma transferência simples de dinheiro entre duas contas, um exemplo clássico que mostra a consistência das transações do banco de dados. O objetivo é garantir que nenhum dinheiro seja perdido ou ganho inesperadamente, mantendo o valor total para todos os usuários do sistema no final do dia.

Primeira Implementação

Vamos simplificar, temos dois usuários: Alice e Bob. Somente Alice tem permissão para iniciar transferências eletrônicas para Bob.

Ações:

Açõessão blocos de construção da especificação de comportamento do sistema, representando vários comportamentos, operações ou eventos, como interações do usuário ou eventos de timer. O verificador de modelo chama essas ações repetidamente em sequências diferentes para explorar os estados potenciais do sistema.

Em nosso modelo, definimos duas ações usando o Açãopalavra-chave. O primeiro é Iniciar, uma ação especial chamada primeiro e apenas uma vez. A segunda ação é Transferência de fundosque é a única ação em nosso modelo e é chamada repetidamente.

Estado:

As variáveis ​​definidas no Iniciar as ações tornam-se as variáveis ​​de estado do sistema, que ações posteriores podem modificar. Em nosso exemplo, uma única variável de estado é representada por um dicionário Python contendo duas contas com saldos de 3 e 2.

Não determinismo:

Ao testar uma implementação, geralmente testamos com um único valor. Porém, com o FizzBee, você especifica os valores possíveis e o verificador de modelo explora todas as combinações.

Neste exemplo, você seleciona um valor a ser transferido no intervalo de 0 a 100. qualquer é uma das duas palavras-chave usadas para especificar o não determinismo. Sintaticamente, isso é equivalente a um Python paradeclaração, permitindo que você execute novamente o mesmo teste com quantidades diferentes.

O código restante é simples: se Alice tiver fundos para transferir, o valor será deduzido de sua conta e adicionado à conta de Bob.

Invariantes:

Na modelagem de sistemas, é crucial garantir que certas propriedades sejam verdadeiras. Uma propriedade essencial é que a soma dos saldos de todas as contas deve ser igual a 5.

Existem três tipos de invariantes: segurança (condições que devem ser sempre verdadeiras), vivacidade (condições que eventualmente devem se tornar verdadeiras) e estabilidade (condições que devem eventualmente se tornar verdadeiras e permanecer verdadeiras).

Comecemos com a afirmação de que os saldos devem sempre coincidir, à semelhança das transferências entre contas do mesmo banco. As invariantes são especificadas usando a palavra-chave “assertion”.

Invariantes são implementados usando o afirmaçãopalavra-chave.

Uma afirmação é semelhante a uma função Python, mas espera um valor de retorno booleano. Verdadeiroimplica que a condição é verdadeira nesse estado.

O semprepalavra-chave implica que esta condição deve ser verdadeira em todos os estados.

Execute o verificador de modelo.

O verificador de modelo indicará uma falha, mostrando um rastreamento onde ocorre uma mudança de contexto após a dedução da conta de Alice, mas antes de creditar a conta de Bob.

Correção: coloque essas duas etapas em uma transação.

palavra-chave atômica:

Usar atômicogarante que ambas as etapas intermediárias ocorram juntas ou não ocorram, protegendo-as do resto do sistema. Durante o desenvolvimento, isso se traduz em uma transação ou bloqueio. Por padrão, o comportamento é serial, mas você pode especificar explicitamente o contrário.

Depois de aplicar atômico, a execução do verificador de modelo será bem-sucedida. Você também pode revisar o gráfico de estado completo para observar o comportamento do sistema.

Transferência bancária – transferência de dinheiro não atômica

Vamos alterar o requisito para dizer que assim que uma solicitação de transferência eletrônica for recebida, a conta de Alice será deduzida imediatamente, mas a conta de Bob poderá não ser creditada imediatamente. Queremos apenas garantir que ele será creditado eventualmente.

Comecemos pela afirmação. Em vez de dizer sempre, mude de sempre que sempre eventualmente. De qualquer estado, eventualmente alcançará um estado onde os predicados se tornarão verdadeiros. Isso é chamado de expectativa de vivacidade. (A expectativa de estabilidade é especificada com eventualmente sempreisso é menos usado e não é abordado aqui).

Agora, como primeira tentativa, remova a palavra-chave atomic (ou substitua-a pela palavra-chave serial). Portanto, o débito e o crédito acontecem em duas etapas distintas

Agora, ao executar o comando, você verá que ele falhou com esse rastreamento.

Isto indica que, após a dedução, o sistema poderia colidir e se isso acontecer, ele perde as próximas etapas e gaguejar Stutter indica que o sistema pode não fazer mais nenhum progresso.

As ações indicam o que pode acontecer no sistema, não o que deve acontecer. Precisamos especificar o que deve acontecer. Isso é feito adicionando palavras-chave justo para uma ação.

Nota: neste caso, se marcarmos a ação FundTransfer como justa, isso implica apenas que Alice poderá continuar enviando o dinheiro, mas será possível, o dinheiro nunca chegará a Bob.

Implementando transferência eletrônica

Isso acontece em duas ações. Na primeira ação, atomicamente, registre a solicitação de transferência e desconte na conta de Alice. Em uma segunda ação, marque novamente atomicamente a transferência como concluída e credite na conta de Bob.

Aqui, mantemos uma lista de solicitações de transferência eletrônica indicando as solicitações pendentes de transferência eletrônica que precisam ser concluídas. E a ação DepositWireTransfer completa a etapa creditando a conta de Alice.

Execute este modelo, você notará um erro – Deadlock.

Isso ocorre porque, à medida que o sistema começa a transferir fundos de Alice para Bob, Alice fica sem dinheiro e o sistema não consegue fazer nenhum progresso. Este é um problema com a nossa declaração de problema, e não com o modelo ou implementação. Podemos consertar isso facilmente, permitindo que Bob transfira dinheiro de volta para Alice. Faremos essa alteração mais tarde. Por enquanto, para manter as coisas simples, vamos fazer um pequeno truque: adicionar uma ação que não faça nada. O código real nunca precisaria disso.

Nota: Pass é uma palavra-chave padrão do Python para representar um bloco vazio.

Agora execute este verificador de modelo, você notará que o verificador de modelo é aprovado. Isso implica que este design está correto.

Nota: O modelo não será transferível diretamente para o código porque wire_requests não pode ser implementado na forma atual. É um banco de dados no mesmo banco do remetente? Assim, o banco do destinatário não poderá atualizar atomicamente junto com o crédito do remetente. Abordaremos isso em uma postagem posterior.

Você pode ler mais sobre o FizzBee e experimentar outros exemplos em https://fizzbee.io.

A verificação formal é testar seu design antes da codificação

A verificação formal permite testar seu design antes da codificação. Conforme demonstrado acima, ajuda você a se concentrar no essencial e abstrair os detalhes, semelhante a explicar um design usando um exemplo básico em um quadro branco.

Ao usar a verificação formal, você pode ter certeza de que seu design está claro e correto antes de iniciar a codificação. Entretanto, é essencial lembrar que, embora a verificação formal teste bem o projeto, ela não substitui a necessidade de testes regulares. Bugs ainda podem surgir durante a implementação, mas geralmente são mais fáceis de corrigir.

Pensamentos finais:

Os métodos formais destacam-se como a principal escolha para validação de projetos. Os profissionais destacam consistentemente a simplificação significativa do projeto e a implementação mais rápida. Por exemplo, em um projeto recente em que redesenhei um sistema v1 com bugs, especificar o design do sistema v2 com TLA+ levou a uma redução de 4x no tamanho do código, ao mesmo tempo que incorporava recursos adicionais. No entanto, é importante observar que ferramentas como o TLA+ são notoriamente desafiadoras de usar.

Conforme mostrado no exemplo acima, o código FizzBee é fácil de ler e escrever, ao contrário do TLA+, tornando-o uma alternativa atraente para engenheiros de software experientes iniciarem métodos formais pela primeira vez. Com o verificador de modelo do FizzBee, a correção do projeto é garantida, enquanto suas especificações concisas e claras comunicam e documentam o projeto.

A postagem Apresentando o FizzBee: simplificando métodos formais para todos apareceu pela primeira vez em The New Stack.