- TLA+ é uma linguagem para modelar software em um nível mais alto que o código, e modelar hardware em um nível mais alto que o nível de circuitos
- Fornece um ambiente de desenvolvimento integrado (IDE) para escrever e verificar modelos
- A ferramenta mais usada por engenheiros é o verificador de modelos TLC, e também há um verificador de provas
- TLA+ é baseado em matemática e não se parece com nenhuma linguagem de programação
- Para a maioria dos engenheiros, é mais fácil começar com PlusCal do que com TLA+
- Um modelo em TLA+ geralmente é chamado de "especificação (Specification)". Na introdução abaixo, ele é chamado de
modelo
PlusCal
- PlusCal é uma linguagem para escrever algoritmos, especialmente algoritmos paralelos e distribuídos
- É usado para escrever algoritmos como código preciso e testável, em vez de pseudocódigo
- Parece uma linguagem de programação simples e fornece construções para expressar concorrência e não determinismo
- Pode usar fórmulas matemáticas como expressões, o que o torna muito expressivo
- Algoritmos em PlusCal são convertidos em modelos TLA+ e podem ser verificados com as ferramentas de TLA+
- Por se parecer com uma linguagem de programação, é fácil de aprender, mas TLA+ é mais adequado para estruturar modelos complexos
O que é um modelo
- Computadores e redes seguem leis físicas contínuas, mas é natural modelar seu comportamento como um conjunto de eventos discretos
- Não existe modelo que descreva perfeitamente um sistema real; um modelo descreve alguns aspectos do sistema para um objetivo específico
- TLA+ é uma linguagem de modelagem baseada em estados e representa a execução de um sistema como uma sequência de estados
- Um evento é representado por um par de dois estados consecutivos, chamado de 'passo (step)'
- Um sistema é modelado como um conjunto de ações que descreve todas as execuções possíveis
Modelagem acima do nível de código
- TLA+ é usado para modelar sistemas acima do nível de código
- Por exemplo, o algoritmo de Euclides pode ser descrito como um procedimento para calcular o máximo divisor comum (GCD), e não como código
- definir a variável x como M e y como N
- subtrair repetidamente o menor valor do maior entre x e y
- repetir até que x e y sejam iguais, e esse valor será o GCD
- Essa descrição omite detalhes como tipos de variáveis ou tratamento de exceções, expressando apenas o conceito essencial do algoritmo
- Se você se concentrar apenas em codificar, fica difícil encontrar bons algoritmos → é necessário pensar de forma abstrata
- A maioria dos programadores começa a codificar sem um modelo de alto nível, e isso leva a erros de projeto
- TLA+ é uma linguagem de modelagem de alto nível capaz de descrever com clareza o comportamento e o funcionamento do código
- Quanto mais complexo o sistema, mais importante é simplificá-lo, e isso é alcançado por pensamento de alto nível, não por habilidade de escrita de código
- Em um projeto industrial, houve um caso em que a modelagem com TLA+ reduziu o tamanho do código de um sistema operacional de tempo real para um décimo
- Modelagem é eficaz para encontrar erros de projeto com antecedência e é mais confiável do que testes ou correções no código
Modelagem de sistemas paralelos
- Um sistema paralelo é composto por vários componentes (processos) operando ao mesmo tempo
- Em sistemas distribuídos, processos separados espacialmente se comunicam por mensagens
- TLA+ modela o estado total do sistema como um estado global
- Com base em mais de 40 anos de experiência, modelar sistemas distribuídos com base em estado global é, em geral, o mais útil
Máquina de estados (State Machine)
- TLA+ define um conjunto de comportamentos com os dois elementos a seguir:
- condição inicial: especifica os possíveis estados iniciais
- relação de próximo estado: especifica os possíveis passos (pares de estados consecutivos)
- O conjunto de comportamentos que satisfaz essas duas condições é o modelo
- Esse tipo de modelo é chamado de máquina de estados (state machine)
- Uma máquina de estados finitos (finite-state machine) é uma máquina de estados com número finito de estados
- Uma máquina de Turing é um exemplo de máquina de estados; em uma máquina de Turing determinística, cada estado tem no máximo um próximo estado
- Uma forma prática de explicar com precisão o significado de uma linguagem de programação é a semântica operacional, que a converte em uma máquina de estados
- A ação de próximo estado especifica apenas os passos que podem ocorrer, e não implica que eles necessariamente ocorram
- Para declarar a ocorrência obrigatória de um passo, é preciso adicionar uma condição de justiça (fairness property)
- Mesmo sem justiça, isso basta para encontrar erros de comissão (commission), mas erros por omissão (omission) não são detectados
- Na maioria dos casos, há mais erros de comissão, e iniciantes devem começar escrevendo a condição inicial e a relação de próximo estado
Verificação de propriedades
- Escreve-se um modelo para verificar se o sistema funciona como desejado
- É possível verificar com as ferramentas de TLA+ se o modelo satisfaz determinada propriedade para todos os comportamentos possíveis
- Exemplo: mesmo que em 99% dos estados iniciais o comportamento termine normalmente, deve-se verificar que todos os comportamentos terminam normalmente
- A propriedade mais comum é a propriedade de invariância (invariance property), que deve ser sempre verdadeira em todos os estados
- Modelos com condição de justiça também devem verificar propriedades de vivacidade (liveness property) → por exemplo: a execução deve necessariamente terminar
- Propriedades mais complexas podem ser expressas como máquinas de estados, e é possível verificar se outra máquina de estados as implementa
- Em TLA+, não há distinção formal entre máquina de estados e propriedade; ambos são expressos da mesma forma, como fórmulas matemáticas
- Dizer que uma máquina de estados implementa outra significa que a fórmula correspondente está logicamente contida
- Na prática, a maioria verifica apenas invariâncias e propriedades simples de vivacidade, mas entender conceitos mais complexos também ajuda a evitar erros no código
A própria linguagem TLA+
- TLA+ é uma linguagem baseada em matemática e não se parece com uma linguagem de programação
- Como programadores estão mais acostumados com linguagens de programação do que com expressões matemáticas, isso pode parecer difícil no começo
- Mas, na prática, a matemática é mais expressiva do que linguagens de programação
- Exemplo: é possível definir o GCD como o maior inteiro positivo que divide dois números (sem precisar descrever o método de cálculo)
- Definições matemáticas permitem manter apenas o essencial necessário ao objetivo e abstrair detalhes de implementação desnecessários
- Proceduralização não fornece abstração; apenas esconde o código em outro lugar
- PlusCal é adequado para começar com TLA+, e até usuários experientes o preferem para modelos simples
- Mas, para pensar matematicamente e fazer modelagem de alto nível, é importante aprender a própria linguagem TLA+
3 comentários
https://cacm.acm.org/research/… é bem usado na AWS.
Programar não é programação
Como isso foi mencionado neste texto, fui pesquisar.
Eu também vi isso pela primeira vez neste artigo e fui pesquisar.