Filosofia de engenharia: Leslie Lamport, pense antes de programar

Principais conclusões

• Pense antes de programar, e coloque o pensamento no papel. Uma especificação é o equivalente, no software, à planta de um arquiteto – “não pensar garante que” cometeremos erros.
• O tempo não é global; a causalidade é o que de fato existe. Sem um relógio compartilhado em que se possa confiar, você deixa de perguntar quando um evento aconteceu e passa a perguntar o que causou o quê.
• A relação aconteceu-antes e os relógios lógicos tornam a causalidade formal. A ordem parcial de Lamport – e o contador por processo que a implementa – é a semente dos relógios vetoriais e da resolução de conflitos moderna.
• Defina a correção com precisão e então prove-a. Segurança e vivacidade, o consenso de Paxos, a tolerância a falhas bizantinas e a linguagem de especificação TLA+ nascem todos de tratar a computação distribuída como matemática, e não como folclore.

O princípio

“Um sistema distribuído é aquele no qual a falha de um computador cuja existência você nem sabia pode deixar o seu próprio computador inutilizável.” – Leslie Lamport¹

Ele enviou essa frase a um quadro de avisos em seu laboratório em 1987, e ela é a frase mais citada da computação distribuída porque nomeia aquilo em que a intuição se recusa a acreditar.¹ Você acha que está executando um programa no seu computador. Não está. Você o está executando sobre uma população de máquinas cuja existência você não enumerou, cujos relógios discordam, e qualquer uma delas pode falhar no exato instante que importa. O sistema que você consegue manter na cabeça e o sistema que de fato roda são sistemas diferentes, e a distância entre eles é onde mora todo bug distribuído.

A obra de toda a vida de Lamport é a recusa em encobrir essa distância com otimismo. Sua convicção é a de que sistemas concorrentes e distribuídos são sutis demais para serem raciocinados pela intuição, então você raciocina sobre eles com matemática, no papel, antes de escrever uma linha de código. “Pensar não garante que não vamos cometer erros”, disse ele à Wired em 2013. “Mas não pensar garante que vamos.”² O pensamento precisa ser colocado no papel, porque é na escrita que o raciocínio desleixado fica exposto: “Para pensar, você tem que escrever. Se você está pensando sem escrever, você só acha que está pensando.”³ Arquitetos desenham uma planta antes de assentar um tijolo; o equivalente no software é uma especificação, e Lamport passou a segunda metade de sua carreira argumentando que a razão pela qual nossos sistemas quebram é que pulamos essa etapa.⁴

O movimento mais profundo diz respeito ao próprio tempo. No mundo físico não existe um relógio global em que você possa confiar para ordenar eventos entre máquinas – então você precisa deixar de perguntar quando algo aconteceu e começar a perguntar o que causou o quê. A causalidade, e não o relógio de parede, é a estrutura real de uma computação distribuída.⁵ Quase tudo o que Lamport construiu decorre de levar esse único fato a sério, e é a mesma convicção que sustenta a barreira de evidências: você não pode supor a ordenação que gostaria que fosse verdadeira; você tem que estabelecê-la.

Contexto

Leslie Lamport nasceu em 7 de fevereiro de 1941, na cidade de Nova York.⁶ Formou-se bacharel em matemática pelo MIT em 1960, depois fez mestrado e – em 1972 – doutorado em matemática pela Brandeis, com uma tese sobre singularidades em equações diferenciais parciais.⁶ Ele não se formou como cientista da computação. Formou-se como matemático, e nunca deixou de se comportar como tal. A característica que define sua carreira é que ele trouxe os padrões da matemática – definições precisas, premissas declaradas, provas em vez de testes – para um campo que era, em grande parte, programação no feeling.

O trabalho aconteceu em quatro instituições. Na Massachusetts Computer Associates, nos anos 1970, ele fez o raciocínio fundacional sobre a ordenação de eventos. Na SRI International (1977–1985) produziu o trabalho sobre os generais bizantinos. No Systems Research Center da Digital Equipment Corporation (1985, seguindo pela aquisição pela Compaq até 2001) escreveu o Paxos e iniciou o trabalho de especificação. De 2001 até sua aposentadoria, no início de 2025, esteve na Microsoft Research.⁶ Em tudo isso o método foi constante: encontrar um problema da computação distribuída ou concorrente que todos tratavam como folclore, defini-lo com precisão suficiente para enunciar um teorema, e então provar o teorema.

A obra

O tempo, os relógios e a relação aconteceu-antes

“Time, Clocks, and the Ordering of Events in a Distributed System” foi publicado em Communications of the ACM em 1978, e está entre os artigos mais citados de toda a ciência da computação – venceu o Prêmio Dijkstra em 2000, dado ao trabalho mais influente da computação distribuída.⁵⁶ Sua percepção é enganosamente pequena. Em um sistema distribuído não existe um relógio compartilhado e confiável, então você não consegue ordenar dois eventos comparando carimbos de tempo. O que você consegue saber é se um evento poderia ter causado outro: o evento A aconteceu-antes do evento B se A e B estão no mesmo processo, com A primeiro, ou se A é o envio de uma mensagem e B é o seu recebimento. Encadeie isso e você obtém a relação aconteceu-antes – a causalidade tornada formal.⁵

A consequência crucial e contraintuitiva é que aconteceu-antes é apenas uma ordem parcial, não total. Dois eventos em processos diferentes, sem nenhuma cadeia de mensagens entre eles, são genuinamente concorrentes: não há fato algum sobre qual veio primeiro, e qualquer sistema que finja o contrário está inventando uma ordenação que não existe.⁵ Lamport então apresentou o algoritmo hoje universalmente chamado de relógio de Lamport: cada processo mantém um contador, incrementa-o a cada evento e carimba toda mensagem que envia com ele; um receptor avança seu contador para uma unidade acima do maior entre o seu próprio valor e o carimbo de tempo da mensagem.⁷ Essa regra simples produz carimbos de tempo consistentes com a causalidade, e é a semente dos relógios vetoriais, dos vetores de versão e de todo o maquinário de resolução de conflitos dos bancos de dados distribuídos modernos.

A razão pela qual esse artigo importa para além de seu algoritmo é que ele mudou a pergunta. Antes de Lamport, supunha-se que “que horas isso aconteceu?” tivesse resposta em um sistema distribuído. Depois de Lamport, a resposta honesta passou a ser “pergunta errada – pergunte o que o causou.” É esse reenquadramento que faz com que se atribua a ele ter transformado a computação distribuída em ciência, e não em ofício artesanal.

Paxos, consenso e máquinas de estado replicadas

Se não há relógio global e as máquinas falham, como é que um grupo de computadores chega a concordar sobre qualquer coisa – qual transação foi confirmada, quem detém o bloqueio, qual é a próxima entrada no log? Essa pergunta é o problema do consenso, e a resposta de Lamport é o Paxos, o algoritmo no cerne de praticamente todo sistema tolerante a falhas construído desde então. Ele o combinou com a abordagem da máquina de estado replicada: se cada réplica começa no mesmo estado e aplica a mesma sequência de comandos na mesma ordem, elas permanecem idênticas – de modo que todo o problema de manter um sistema distribuído consistente se reduz a concordar sobre a ordem dos comandos, que é exatamente o que o Paxos fornece.⁶

A história de como o Paxos foi publicado é a parábola de advertência mais famosa do campo. Lamport o redigiu como “The Part-Time Parliament”, enquadrando o algoritmo como o procedimento legislativo de uma fictícia ilha grega antiga chamada Paxos, completo com legisladores que carregavam transliterações pseudogregas dos nomes de seus colegas.⁸ A piada foi uma catástrofe. Os revisores acharam que ele não estava falando sério; o artigo foi rejeitado por insignificante; quem assistia às suas palestras lembrava do enredo à la Indiana Jones, e não do algoritmo.⁸ Ele ficou anos sem ser publicado. O editor de Communications of the ACM acabou publicando-o em ACM Transactions on Computer Systems em 1998 – ainda envolto na parábola.⁸ Quando o campo continuou a ignorá-lo, Lamport finalmente se rendeu e escreveu “Paxos Made Simple” em 2001, retirando a roupagem grega para revelar o que ele insistia ser um algoritmo genuinamente simples por baixo.⁸ A lição que ele extraiu não foi “as pessoas são burras.” Foi a de que mesmo uma ideia correta e importante fracassa se você obscurece o pensamento – a apresentação é parte do trabalho, não algo separado dele.

O problema dos generais bizantinos

Em 1982, com Robert Shostak e Marshall Pease, Lamport publicou “The Byzantine Generals Problem”, que deu ao campo sua linguagem para o tipo mais difícil de falha.⁶ Um componente que trava é fácil comparado a um bizantino – um componente que não para, mas mente, enviando informações diferentes e contraditórias a diferentes pares, seja por um bug, por corrupção ou por malícia. O enquadramento do artigo: divisões de um exército, cada uma liderada por um general, precisam concordar com um único plano – atacar ou recuar – por mensageiro, enquanto um subconjunto desconhecido de generais é de traidores tentando ativamente impedir o acordo. Lamport provou o limiar exato de quantos traidores um sistema pode tolerar e ainda assim chegar a um acordo, transformando “e se um nó mentir?” de uma preocupação vaga em um teorema com um limite declarado.

Esse teorema é a raiz intelectual de todo sistema que precisa continuar funcionando enquanto alguns de seus participantes são adversários – e é por isso que, décadas depois, a palavra bizantino está no centro do consenso em blockchain. Lamport não partiu para viabilizar criptomoedas; partiu para definir, com exatidão, o que significa tolerância a falhas quando “falha” inclui traição.

TLA+ e a especificação (e, sim, o LaTeX)

O fio condutor da carreira de Lamport é a convicção de que você precisa especificar antes de programar, e o TLA+ é essa convicção transformada em ferramenta. A Temporal Logic of Actions é uma linguagem para escrever uma descrição matemática precisa do que um sistema deve fazer – seus estados, os passos entre eles e as propriedades que ele deve sempre satisfazer (segurança: nada de ruim jamais acontece) e por fim alcançar (vivacidade: algo de bom acaba acontecendo), dois conceitos que ele formalizou.⁶ Você escreve a especificação, e um verificador de modelos explora o espaço de estados para encontrar a intercalação sutil que quebra sua invariante – o bug que você nunca teria encontrado testando, porque ele só aparece quando três máquinas fazem três coisas em uma ordem que você jamais imaginou. Seu argumento é a planta do arquiteto: você desenha o prédio antes de despejar o concreto, e uma especificação de software é a mesma planta, escrita em matemática porque a matemática é a linguagem mais precisa que temos.⁴

E há um monumento mais discreto. No início dos anos 1980, partindo do TeX de Donald Knuth, Lamport escreveu o LaTeX – o sistema de macros que se tornou a forma padrão pela qual cientistas e matemáticos diagramam documentos, a razão pela qual uma geração de artigos e teses tem a aparência que tem.⁶ É um artefato caracteristicamente lamportiano: ele precisava redigir seu próprio trabalho com precisão, então construiu a ferramenta que permitiu a todos fazer o mesmo. O instinto que produziu o TLA+ – uma notação que força a precisão – é o mesmo instinto que produziu o LaTeX.

O método

O método é uma única ideia aplicada incansavelmente por cinquenta anos: o pensamento é o trabalho, e o pensamento precisa ser colocado no papel antes do código.

Raciocine sobre causalidade, não sobre tempo. Não há relógio global em que confiar, então pare de ordenar eventos por quando aconteceram e ordene-os pelo que causou o quê. A relação aconteceu-antes, não o relógio de parede, é a estrutura real – e aceitar que dois eventos são genuinamente concorrentes é mais honesto do que inventar uma ordem.⁵

Especifique antes de programar. Para qualquer coisa sem uma solução estabelecida, pare e pense primeiro, e o pensamento é independente da programação. Escreva a planta – a especificação – em matemática, porque a matemática é simples e precisa onde a prosa é vaga.⁴ “Não pensar garante que” cometeremos erros.²

Escreva para descobrir se você está pensando. A escrita é o teste de se um pensamento é real. “Se você está pensando sem escrever, você só acha que está pensando.”³ Uma especificação que você não consegue escrever é uma ideia que você ainda não tem de fato.

Defina a falha com exatidão. “E se um nó mentir?” é folclore até você enunciá-lo como os generais bizantinos e provar o limite de tolerância. Definições precisas transformam preocupações em teoremas.⁶

A apresentação é parte da correção. O Paxos esteve correto por anos antes que alguém pudesse usá-lo, porque a parábola grega enterrou a ideia. Um resultado correto que ninguém consegue entender ainda não terminou de ser engenhado.⁸

Cadeia de influência

Quem o moldou

A própria matemática. A formação de Lamport foi um doutorado em matemática, não em ciência da computação, e toda a forma de sua contribuição é a importação dos padrões matemáticos – definições, axiomas, provas – para um campo que vinha programando pela intuição.⁶ (Influência formadora)

Os problemas de tolerância a falhas dos sistemas reais dos anos 1970. O trabalho da SRI em sistemas confiáveis para aeronaves e o horror prático de máquinas que falham no meio de um protocolo deram a ele problemas concretos – falhas bizantinas, consenso – que exigiam o tratamento formal que ele estava preparado para dar.⁶ (Influência direta)

Edsger Dijkstra. A convicção de que a correção se estabelece por prova, e não por teste, e de que programas concorrentes precisam ser raciocinados formalmente, é de Dijkstra antes de ser de Lamport. O prêmio que Lamport ganhou por seu artigo sobre relógios leva o nome de Dijkstra. (Influência direta)

Quem ele moldou

Todo banco de dados distribuído, plataforma de nuvem e blockchain. Os relógios lógicos sustentam a resolução de conflitos em armazenamentos distribuídos; o Paxos (e seu descendente Raft) é o núcleo de consenso do Chubby e do Spanner do Google, do ZooKeeper, do etcd e da camada de coordenação de essencialmente toda nuvem. O resultado dos generais bizantinos é o piso teórico sob o Bitcoin e sob todo protocolo de consenso tolerante a falhas desde então.

Métodos formais na indústria. A Amazon Web Services notoriamente usa TLA+ para especificar e verificar o S3, o DynamoDB e outros serviços centrais antes de lançá-los – encontrando bugs sutis no projeto, e não em produção. O argumento da planta de Lamport saiu da heresia para a prática.

O vocabulário do campo. Aconteceu-antes, segurança e vivacidade, máquinas de estado replicadas, consistência sequencial, falha bizantina – estas não são contribuições de Lamport para a linguagem dos sistemas distribuídos; elas em grande parte são essa linguagem.

O fio condutor

Edsger Dijkstra argumentava que você prova um programa correto antes de executá-lo – que o teste mostra a presença de bugs, nunca a sua ausência – e Lamport é o herdeiro direto, carregando a prova-antes-da-execução dos programas sequenciais para o mundo muito mais difícil da concorrência, onde o bug para o qual você não consegue testar é a regra, e não a exceção. Barbara Liskov tornou o raciocínio formal sobre o comportamento de programas uma primitiva de trabalho com a abstração de dados e a substituibilidade; Lamport tornou padrão o raciocínio formal sobre o comportamento de sistemas ao longo do tempo, especificando não o que um objeto garante, mas o que um sistema concorrente inteiro precisa sempre e por fim fazer. E Donald Knuth trouxe o rigor matemático à análise de algoritmos e, quase de passagem, construiu o TeX para que esse trabalho pudesse ser registrado com precisão – uma rima quase exata com Lamport, que construiu o LaTeX em cima dele pela mesma razão e fez da própria especificação um ato matemático. Três matemáticos que se recusaram a deixar que “parece funcionar” contasse como saber. (Ponte da série)

O que eu tiro disso

A lição que guardo é a de que o pensamento é o trabalho, e o pensamento não é real até estar no papel. O argumento da planta de Lamport é incômodo porque é correto: a razão pela qual um sistema quebra em produção quase nunca é que o código foi digitado errado – é que ninguém especificou o que o sistema deveria de fato fazer sob concorrência e falha, então não havia um enunciado contra o qual conferir o código. A disciplina é escrever a especificação antes da implementação, em uma linguagem precisa o suficiente para que suas contradições se tornem visíveis. É o mesmo padrão de a qualidade ser a única variável: a pergunta nunca é “isso passa no caminho feliz?”, mas “eu enunciei, com exatidão, o que precisa ser sempre verdadeiro – e provei que o projeto honra isso?” É por isso que me apoio tanto em escrever o PRD antes do código; um PRD é uma especificação de Lamport vestida de roupa de trabalho.

No mundo em que construo hoje – agentes, laços de ferramentas, sistemas multiagente – a lição de Lamport é a que quase todo mundo pula, e paga por isso. Um sistema de agentes é um sistema distribuído: processos independentes, sem relógio global, mensagens que chegam fora de ordem ou não chegam, e componentes que falham em silêncio ou, pior, mentem. Os bugs nunca estão no prompt; estão na ordenação – dois agentes agindo sobre estado defasado, uma chamada de ferramenta cujo resultado chega depois da decisão que dele precisava, um par de eventos “concorrentes” que o orquestrador fingiu ordenar. A disciplina de Lamport é parar de confiar na intuição do relógio de parede, raciocinar explicitamente sobre causalidade e falha, e colocar no papel o que precisa ser sempre verdadeiro antes de conectar qualquer coisa. A convicção de que você especifica antes de construir, de que você raciocina sobre um sistema em vez de cutucá-lo – esse é o fio condutor que vai de um artigo de 1978 sobre relógios a uma camada local de agentes de 2026, e é exatamente por isso que trato o desempenho e a correção de um sistema como uma propriedade que você projeta de antemão, nunca como algo que você espera depurar de volta mais tarde.

FAQ

Qual é a filosofia de engenharia de Leslie Lamport?

A convicção de Lamport é a de que sistemas concorrentes e distribuídos são sutis demais para serem raciocinados pela intuição, então você precisa pensar com matemática, no papel, antes de escrever código – do jeito que um arquiteto desenha uma planta antes de assentar um tijolo. A planta do software é uma especificação, escrita em matemática porque a matemática é a linguagem mais precisa disponível.⁴ Por baixo disso há uma postura em relação ao tempo: em um sistema distribuído não há relógio global em que confiar, então a estrutura real de uma computação é a causalidade – o que causou o quê – e não quando as coisas aconteceram.⁵ “Pensar não garante que não vamos cometer erros”, disse ele, “mas não pensar garante que vamos.”²

O que é um relógio de Lamport e a relação aconteceu-antes?

A relação aconteceu-antes é a formalização da causalidade que Lamport faz em um sistema distribuído: o evento A aconteceu-antes do evento B se ambos estão no mesmo processo, com A primeiro, ou se A envia uma mensagem e B a recebe, ou pelo encadeamento dessas situações.⁵ É apenas uma ordem parcial – dois eventos em processos diferentes, sem nenhuma mensagem conectando-os, são genuinamente concorrentes, e nenhum sistema correto pode afirmar que um veio primeiro.⁵ Um relógio de Lamport implementa isso com um contador por processo: incremente-o a cada evento, carimbe com ele toda mensagem que sai e, ao receber, avance seu contador para uma unidade acima do maior entre o seu próprio valor e o carimbo de tempo da mensagem.⁷ O resultado é um conjunto de carimbos de tempo consistente com a causalidade – a base dos relógios vetoriais e da resolução de conflitos distribuída moderna.

O que são o Paxos e o problema dos generais bizantinos?

O Paxos é o algoritmo de Lamport para consenso – fazer com que um grupo de máquinas não confiáveis e possivelmente sujeitas a falhas concorde sobre um único valor, como o próximo comando em um log replicado – e sustenta a camada de coordenação de praticamente todo sistema distribuído moderno. Notoriamente, ele o publicou primeiro como uma parábola sobre um parlamento grego fictício (“The Part-Time Parliament”, ACM TOCS 1998); a piada obscureceu tanto a ideia que ele acabou reescrevendo-a como “Paxos Made Simple” em 2001.⁸ O problema dos generais bizantinos (Lamport, Shostak e Pease, 1982) define o modo de falha mais difícil – componentes que não apenas travam, mas mentem, enviando informações contraditórias – como generais tentando concordar com um plano enquanto traidores entre eles sabotam o acordo, e prova quantos traidores um sistema pode tolerar.⁶ É a raiz teórica do consenso em blockchain.

Por que Leslie Lamport ganhou o Prêmio Turing?

A ACM concedeu a Lamport o Prêmio A.M. Turing de 2013 “por contribuições fundamentais à teoria e à prática de sistemas distribuídos e concorrentes, notadamente a invenção de conceitos como causalidade e relógios lógicos, segurança e vivacidade, máquinas de estado replicadas e consistência sequencial.”⁶ A citação capta a amplitude de sua obra: ele transformou a computação distribuída de folclore em ciência, com definições e provas precisas, deu ao campo boa parte de seu vocabulário, criou a linguagem de especificação TLA+ para tornar o “especifique antes de programar” uma disciplina prática e – partindo do TeX de Knuth – escreveu o LaTeX, o sistema de diagramação que se tornou padrão em toda a ciência e a matemática.⁶

Fontes