Os três níveis de software: por que o código que nunca dá errado ainda pode estar errado

Atualização 3/20/2019: As versões anteriores deste post usavam muito a terminologia Nível 1/Nível 2/Nível 3 e “bug Nível 3”. Estou diminuindo isso em favor de “Runtime/Concrete Implementation/Logic level” e “Error of modular reasoning”, porque as pessoas começaram a usar “Level 3” para significar “Tudo sobre o código que eu não gosto que não pode causar uma saída incorreta”.

Você já parou para pensar o que significa um programa estar errado? Quer dizer, realmente parou para considerar? Tipo, “é errado se ele travar - mas e se as condições de colisão forem apenas hipoteticamente alcançáveis - mas espere…”. Vamos ao fundo disso. Aqui está uma primeira tentativa:

Definição #1

Um programa está errado se for executado e produzir um resultado errado.

(Onde “resultado errado” é amplamente definido para incluir bugs de desempenho, bugs de usabilidade, etc.)

Então coloco meu pão na torradeira e, em vez de me dar um pedaço de torrada, ele me dá um rinoceronte. Não era o que eu queria. Definitivamente um inseto (erro, mamífero).

Os programas ainda podem produzir o resultado correto, mas estão errados. Então eu recebo uma torradeira nova, e eu nunca tive um problema com ela. Então eu descubro que, se eu colocar uma fatia fina de centeio bávaro quando há uma lua cheia para fora, e eu usei a torradeira exatamente duas vezes nas últimas 24 horas, então ela fritará seus circuitos. Parece um bug. Então, nós o alteramos para uma 2ª definição.

Definição #2

Um programa está errado se existir algum ambiente, sequência de eventos ou outra “entrada” sob a qual ele produz um resultado errado.

Agora vamos eliminar tudo isso. Eu corrigi o software na minha torradeira, e eu provei que o código estava correto, e um trilhão de macacos testaram todas as situações imagináveis. Agora não há nada que você possa fazer a não ser pegar uma marreta que fará a torradeira funcionar mal.

Ainda é possível que o código esteja errado.

Como? Simples. Digamos que em algum lugar dessa torradeira, ele soma todos os elementos de uma matriz - mas acidentalmente passa por um. Erro de memória? Bem, ele está escrito em C, então ele apenas adiciona o que estiver no próximo endereço na memória. Esse endereço é um byte que é sempre 0 por qualquer motivo, então ele recebe a resposta certa todas as vezes.

O código ainda está errado. Ele pode nunca falhar, mas o raciocínio para por que o código deve funcionar tem um buraco: o que deveria ter sido um argumento simples de ler uma matriz agora depende de suposições complexas sobre o compilador e o layout de memória, bem como uma verificação de programa inteiro de que esse byte é sempre 0. E esse buraco pode causar uma falha real em versões futuras do programa: alguém reorganiza os campos em uma estrutura e o código que nunca deveria ter sido afetado começa a falhar.

Chegamos à nossa terceira definição:

Definição #3

Um programa está errado se o raciocínio para que ele deva ser correto é falho.

Progresso! Passamos de uma definição clara e simples para uma que é mão ondulada e impossível de usar. Na verdade, é bastante rigoroso, mas terei que ensinar alguns conceitos da verificação formal para torná-la mais concreta.

Todas as três definições estão corretas para uso em momentos diferentes. Este é um dos meus principais ensinamentos: que, quando falamos de programas, falamos em um dos três níveis. Esses três níveis são:

  • Nível 1: Tempo de execução. O nível de tempo de execução lida com valores específicos e um ambiente específico de uma única execução do programa. Muitas depurações são feitas no nível de tempo de execução.
  • Nível 2: Implementação/Código Concreto. No nível da implementação concreta, pensamos no que a implementação atual poderia fazer quando dados dados inputs arbitrários e um ambiente arbitrário. Comportamentos que não podem acontecer não são considerados, mesmo que exija raciocínio global para descartá-los. Muito trabalho de implementação é feito no nível do código.
  • Nível 3: Design/Lógica: No nível da lógica, consideramos a especificação abstrata de cada unidade de um programa. Ao usar outras unidades, consideramos apenas as garantias feitas pela especificação, e presumimos que elas podem ser substituídas a qualquer momento por uma implementação diferente. Muitos programas que estão corretos quando vistos no nível de implementação concreto não estão corretos quando vistos no nível lógico, porque eles dependem de um comportamento que não é garantido em todas as versões futuras. Chamamos isso de erro de raciocínio modular, porque funções com tais erros carecem de uma propriedade desejável: a capacidade de argumentar que a função está correta apenas a partir do código da função e dos contratos das dependências da função, sem necessidade de sequer olhar para as dependências. A maioria dos projetos de software é feita no nível da lógica.

Conheci programadores que confundem o tempo de execução e os níveis concretos de implementação/código, mas não muitos. Os níveis de tempo de execução e código são concretos o suficiente: você vê o nível de tempo de execução executando sob um depurador e inspecionando a pilha, enquanto vê o nível de implementação concreto apenas lendo o código e pensando no que poderia acontecer. Mas a maioria dos programadores tem muito mais dificuldade em conseguir que haja mesmo um nível lógico, e eu vi muita confusão vir de quando um programador está falando sobre o que um componente é garantido fazer, e o outro está falando sobre o que ele acontece de fazer. A maioria dos programadores será ensinada a diferença entre interface e implementação em um alto nível. Mas poucos conseguem ver os detalhes completos do que define uma “interface” além de apenas “lista de funções”. Isso só pode ser visto quando se faz uma verificação formal, onde as propriedades e suposições de um programa são escritas tão concretamente quanto seu código-fonte. No desenvolvimento cotidiano, toda essa estrutura e raciocínio ainda está lá; ele está apenas espalhado pela documentação, comentários e cabeças dos programadores.

Declarações em diferentes níveis não se misturam. Portanto, se o protocolo cliente/servidor proposto diz que o cliente deve enviar uma solicitação duas vezes e descarta o primeiro resultado (uma instrução Level 3/design-level), e o designer diz que é porque há três tipos diferentes de manipuladores de solicitação na base de código, e Bob’s às vezes erra na primeira vez (uma instrução Level 2/implementation-level), você deve ficar confuso. Você deve estar tão confuso quanto se alguém quisesse chamar um arquivo ou gravar em uma função.

Nosso objetivo não é entregar software funcional aos clientes e, portanto, a correção no nível de implementação concreta é tudo o que é importante? Não, nosso objetivo é ser capaz de continuar a entregar software funcional no futuro. O nível lógico é sobre o quão modulares são as interações entre os componentes do seu software, e isso é importante se você se preocupa em ter versões diferentes desses componentes, como, por exemplo, se você quiser reescrever um deles amanhã. Joel Spoelsky relata como o Sim City original teve um erro de uso após livre. No nível concreto de implementação/código, isso foi totalmente bom, já que a memória liberada no DOS era válida até o próximo malloc, e assim o programa funcionou. No nível lógico, isso foi um defeito, porque a especificação de graça diz que você precisa agir como se a memória fosse devorada por um dragão assim que você liberá-lo, e qualquer implementação livre futura pode realmente comê-lo. Com certeza, uma vez que o Windows 3.1 rolou com um novo gerenciador de memória, SimCity começaria a falhar. A Microsoft teve que adicionar um caso especial para verificar se SimCity estava em execução e mudar para um gerenciador de memória herdado em caso afirmativo.

People sometimes tell me about how software is so easy and you can just have an idea and make it and it’s so cheap because there’s nothing physical to build. Hogwash. Software is a domain where we make decisions that can’t be undone and have to be supported for all eternity. The HTTP “referer” is forever misspelled, and that SimCity special-casing code is still there 30 years later.

This is why it’s important to get programs right at the logical level, making it so you can argue each component is correct independently of the rest of the program, even if the overall program passes all your testing and meets external requirements.

And, lesson for API designers: This is why it’s important to make your APIs conform as strictly to the spec as possible, at least in Debug mode. This all could have been avoided if DOS’s free were to deliberately zero-out the memory.

Agora tenho dois anos de experiência ensinando engenheiros a entender melhor como evitar a complexidade, melhorar o encapsulamento e tornar o código à prova de futuro. Mas, em última análise, todo esse conhecimento deriva dessa única visão mestra: as partes mais importantes de nosso ofício não lidam com o código, mas com a lógica por baixo. A camada lógica pode estar escondida, mas não é mística: temos mais de 40 anos de teoria por trás; Veja o posfácio abaixo para ter um gostinho dos detalhes. Quando você aprende a ver o raciocínio por trás do seu sistema tão claramente quanto o código, então você alcançou a iluminação do software.

Próxima vez: por que isso implica manter o design e a implementação separados.

Postscript: Detalhes Técnicos

Eu poderia falar um livro sobre harmonia e composição, mas você aprenderia mais ouvindo uma música e vendo a partitura. Da mesma forma, eu poderia divagar sobre raciocínio e suposições, mas para realmente entendê-lo, você precisa ver os objetos em estudo. Os três níveis lidam com diferentes visões de um programa: execuções, código e especificações. Cada um corresponde ao seu próprio tipo de raciocínio. 1 Vamos trazer a matemática!

Nível 1: Traços e estados

Os objetos de estudo do Nível 1, o nível de tempo de execução, são traços e estados. Um rastreamento é uma sequência de eventos que ocorreram em uma execução de programa. Um rastreio tem a seguinte aparência:

Digite o método postProfileUpdateToServer
Ler o perfil do campo para a variável local p
Enter método saveCurrentState Leave método saveCurrentState

…

Os rastreamentos podem ser de nível muito alto, como os microsserviços executados ou de nível muito baixo, envolvendo o agendamento de instruções na CPU. Eles contam exatamente o que aconteceu e dão as informações para construir o estado atual.

O estado é uma coleção de células com seu valor atual. Fica assim:

{ p=Profile(name=”Bob”, id=42, …), 
  this=NetworkClient(socket=..., baseUrl=”http://mywebsite.com/api/”),
  __messages_output=[“Initializing MyApp version 5”, “Welcome, Bob!”, …],
  …
}

Na maioria das vezes, o estado consiste apenas em valores na memória, embora possa ser útil incluir também partes do ambiente ou uma lista do que já foi emitido ou enviado pelo fio.

Qualquer instrução que possa ser formulada em termos de rastreamentos e estados específicos é uma instrução de nível de tempo de execução. Essas construções devem ser familiares aos programadores: as impressões permitem exibir fragmentos de um rastreamento, enquanto um depurador permite observar o estado atual.

A maneira correspondente de raciocínio automatizado é o raciocínio fundamentado. Raciocínio fundamentado significa raciocinar apenas sobre valores concretos sem quantificadores. Então, suponha que eu tenha este código:

1:       left = x - 10;
2:       if (left < 0)
3:         left = 0;
4:       right = min(x+10, 100);
5:       print(right);

Digamos que eu saiba pela impressão que direito=50 em um determinado rastreamento, e eu quero saber se é possível que o ramal na linha 3 tenha sido executado. Eu poderia responder a essa pergunta pedindo a um solucionador para encontrar uma atribuição satisfatória para a seguinte fórmula:

left<0 ∧ (left=x-10 
         ∧ right=(if x+10<=100 then x+10 else 100)
         ∧ right=50)

Nível 2: Código

O objeto de estudo do Nível 2, o nível de implementação concreta, é o código. Sim, código, as coisas com as quais você trabalha todos os dias. Qualquer instrução que possa ser formulada em termos de código, mas não um rastreamento ou estado específico, é uma instrução em nível de código. Vejamos o exemplo a seguir, que calcula um bônus de dano em um jogo hipotético:

public double computeDamageBonus(int creature1AttackSkill,
                                 int creature1ArmorPiercing,
                                 int creature2DefenseSkill) {

  int adjDefense = creature2DefenseSkill - creature1ArmorPiercing;

  if (adjDefense <= 0) {
    return 10;
  }

  double factor = (double)creature1AttackSkill / 
                     (creature2DefenseSkill - creature1ArmorPiercing);

  if (factor > 10)
    return 10;
  else
    return factor;
}

Ao selecionar entradas específicas para essa função, ela produzirá um rastreamento e uma sequência de estados. Mas este programa codifica um número exponencialmente grande de possíveis vestígios e estados. No nível de tempo de execução, podemos perguntar: “Essa execução sofreu um erro de divisão por zero?” No nível de implementação concreta, podemos perguntar: “Existe alguma execução dessa função que experimente um erro de divisão por zero?”

O modo correspondente de raciocínio é a lógica de primeira ordem. Isso significa que podemos anotar fórmulas que dizem “para todas as entradas X, essa propriedade se mantém?” ou “existe uma entrada Y, de modo que essa função trave?” O que não podemos fazer é quantificar outras funções. Aqui está uma fórmula de primeira ordem que afirma que a função computeDamageBonus nunca pode ter um erro de divisão por zero:

∀creature1AttackSkill, creature1ArmorPiercing, creature2DefenseSkill.
  (adjDefense = creature1ArmorPiercing - creature2DefenseSkill∧
  ¬(adjDefense ≤ 0))
    ⇒ creature1ArmorPiercing - creature2DefenseSkill ≠ 0

Nível 3: Especificações

O objeto de estudo do Nível 3, a camada da lógica, é a especificação. Eu também chamo isso de nível de projeto, porque a maioria dos termos de engenharia de software, como modularidade e encapsulamento, só pode ser definida em termos de lógica e especificação. Há muitas, muitas maneiras de escrever especificações, mas uma popular é a tripla Hoare: pré-condições e pós-condições. Aqui está um para malloc:

malloc(n)
Pre: n > 0
Post: retval ≠ NULL ⇒ alloc(retval, n)

No nível de implementação concreta, poderíamos fazer perguntas sobre uma implementação específica de malloc, como “Quanta sobrecarga de memória ele usa?” No nível lógico, podemos fazer perguntas sobre todas as implementações possíveis de malloc, como “este programa tem um erro de memória?”

O modo correspondente de raciocínio é a lógica de ordem superior. A lógica de ordem superior é como a lógica de primeira ordem, mas agora podemos quantificar sobre funções. Primeiro, vamos traduzir a especificação acima2:

MallocSpec(m) = ∀n. n > 0 ⇒ m(n) ≠ NULL ⇒ alloc(m(n), n)

Agora, se hipoteticamente tivéssemos uma especificação formal para a função PlaySimCity, uma especificação que funciona para qualquer implementação de malloc seria algo como

∀m. MallocSpec(m) ⇒ SimCitySpec(m, PlaySimCity)

E isso, meus amigos, é modularidade reduzida a uma fórmula.

Uma coisa realmente importante sobre as especificações é que elas podem envolver propriedades que não aparecem no código. Definimos malloc em termos desse predicado de alocação, que não tem nenhum significado intrínseco além de “coisas devolvidas por malloc”. Mas o que isso faz é relacionar malloc com outras operações. Podemos dar ao ato de desreferenciar o ponteiro x uma pré-condição ∃a,n. a≤x<a+n ∧ alloc(a,n), e dar à função free(x) uma especificação que destrói o predicado alloc(x,n). Agora, ter uma prova de aloc(a, n) ao raciocinar sobre o programa significa que “essa memória foi devolvida por malloc, sem intervenção livre” – exatamente nossa noção intuitiva de memória sendo alocada!

O que mostramos aqui é que “essa memória está alocada” é uma noção de nível de especificação que é independente do código. E, de fato, pode não haver nada dentro do programa que indique que um pedaço de memória foi alocado. É possível que ser alocado corresponda a alguma estrutura de dados interna do gerenciador de memória, mas também é possível que seu código seja compilado para uma máquina com memória infinita.

Agora posso afirmar exatamente em que sentido o código SimCity estava errado: Uma pré-condição para desreferenciar um ponteiro é que o ponteiro esteja alocado para memória alocada. Eles tentaram desreferenciar um ponteiro sem atender a essa pré-condição, ou seja: nenhuma prova de aloc(a,n). Então, seu código funcionou bem para uma implementação de malloc, mas, como eles infelizmente aprenderam, não para todos eles.

Ao projetar software, eu sempre recomendo tentar pensar em conceitos puros e, em seguida, traduzir isso para a linguagem de programação, da mesma forma que os designers de banco de dados escrevem diagramas de ER antes de traduzi-los em tabelas. Portanto, se você está discutindo acoplamento ou segurança, sempre pense nos componentes do seu software em termos de interface, suas premissas e garantias, e os traduza mentalmente em fórmulas como as acima. Muita coisa fica mais clara quando você faz, pois a lógica é a linguagem do design de software.

Confirmações

Obrigado a Elliott Jin e Jonathan Paulson pelos comentários sobre rascunhos deste post.

1 Não se prenda muito às analogias entre os níveis de software e os modos de raciocínio, há muitas exceções. Por exemplo, grande parte do progresso na análise de programas/verificação/pesquisa de síntese vem de encontrar todos os tipos de truques para codificar problemas mais complicados em uma forma que pode ser resolvida pelo raciocínio básico, já que temos bons solucionadores. Isso provavelmente não será muito relevante para você, a menos que você trabalhe em ferramentas de programação.
2 Estou mentindo um pouco neste exemplo - o tipo de fórmula lógica que dei é realmente apenas para funções puras. Para lidar com malloc corretamente, gostaríamos de usar a lógica de separação.

Artigo Original