Se pudéssemos viajar no tempo até 1974, talvez tivéssemos encontrado Leslie Lamport na padaria de seu bairro atarefado, lutando com o seguinte número. A padaria tinha várias caixas, mas se mais de uma pessoa se aproximasse de uma única caixa ao mesmo tempo, essa caixa tentaria falar com todas elas ao mesmo tempo e ficaria confusa. Lamport percebeu que precisava haver alguma forma de garantir que as pessoas se aproximassem dos caixas, uma de cada vez. Este problema lembrou Lamport de uma questão que foi colocada em um artigo anterior pelo cientista da computação Edsger Dijkstra sobre outra questão mundana: como compartilhar utensílios de jantar ao redor de uma mesa de jantar. Um dos desafios da coordenação era garantir que cada utensílio fosse usado por no máximo um restaurante de cada vez, o que veio a ser generalizado como o problema de exclusão mútua, exatamente o desafio que Lamport enfrentou na padaria.

Uma manhã de 1974, veio à Lamport uma ideia sobre como os clientes da padaria poderiam resolver a exclusão mútua entre si, sem depender da padaria para obter ajuda. Funcionou mais ou menos assim: as pessoas escolhem os números quando entram na padaria, e depois são servidas no caixa de acordo com o seu pedido de números. Para escolher um número, um cliente pede o número de todos à sua volta e escolhe um número superior a todos os outros.

Esta simples ideia tornou-se um algoritmo elegante para resolver o problema da exclusão mútua sem requerer operações indivisíveis de nível inferior. Era também uma rica fonte de ideias futuras, uma vez que muitas questões tinham de ser resolvidas. Por exemplo, alguns clientes de padaria demoraram muito tempo para verificar outros números e, enquanto isso, mais clientes chegaram e selecionaram números adicionais. Em outra ocasião, o gerente da padaria queria obter um instantâneo de todos os números de clientes, a fim de preparar pastelaria suficiente. Lamport disse mais tarde: “Durante alguns anos após a minha descoberta do algoritmo da padaria, tudo o que aprendi sobre a concorrência veio do estudo do mesmo”.

O Algoritmo de Padaria e os outros trabalhos pioneiros de Lamport — muitos com nomes divertidos e parábolas associadas — tornaram-se pilares da ciência da computação. Sua coleção forma a base de amplas áreas em concorrência, e influenciou a especificação, desenvolvimento e verificação de sistemas concorrentes.

Após graduar-se com um PhD em matemática pela Universidade Brandeis em 1972, Lamport trabalhou como cientista da computação na Massachusetts Computer Associates de 1970 a 1977, na SRI International de 1977 a 1985, e no Digital Equipment Corporation Systems Research Center (mais tarde de propriedade da Compaq) de 1985 a 2001. Em 2001 ingressou na Microsoft Research em Mountain View, Califórnia.

A sua carreira de pesquisa em ambientes de pesquisa industrial não foi um acidente. “Eu gosto de trabalhar em um laboratório de pesquisa industrial, por causa da entrada”, disse Lamport. “Se eu apenas trabalhasse sozinho e tivesse problemas, eu inventaria um pequeno número de coisas, mas se eu for para o mundo, onde as pessoas estão trabalhando em sistemas de computadores reais, há um milhão de problemas lá fora. Quando olho para trás para a maioria das coisas em que trabalhei – generais bizantinos, Paxos – eles vieram de problemas do mundo real”.

Os seus trabalhos lançam luz sobre questões fundamentais de programas concorrentes, para os quais não havia uma teoria formal na altura. Ele se debateu com conceitos fundamentais como causalidade e tempo lógico, registros atômicos e compartilhados regularmente, consistência seqüencial, replicação de máquinas de estado, concordância bizantina e liberdade de espera. Ele trabalhou em algoritmos que se tornaram prática padrão de engenharia para sistemas distribuídos tolerantes a falhas. Ele também desenvolveu um corpo substancial de trabalho na especificação formal e verificação de sistemas simultâneos, e contribuiu para o desenvolvimento de ferramentas automatizadas aplicando estes métodos. Vamos abordar apenas algumas das suas contribuições.

1. As soluções de Exclusão Mútua e o algoritmo Bakery

Lamport’s trabalhos influentes dos anos 70 e 80 vieram em uma época em que havia apenas uma pequena compreensão das questões fundamentais sobre programação para múltiplos processadores simultâneos.

Por exemplo, sabia-se que a execução correta pode exigir atividades paralelas para excluir umas às outras durante períodos em “seções críticas” quando manipulam os mesmos dados, a fim de evitar a intercalação indesejada de operações. As origens deste problema de exclusão mútua são do trabalho pioneiro de Edsger Dijkstra, que inclui a sua solução. O algoritmo de Dijkstra, embora correto, depende dos acessos à memória compartilhada serem atômicos – que um processador leia quando outro estiver escrevendo será feito para esperar, em vez de retornar um valor possivelmente falsificado. De certa forma, ele constrói uma solução de alto nível a partir da exclusão mútua de baixo nível já implementada pelo hardware.

Lamport’s notavelmente elegante e intuitivo “Bakery Algorithm” não faz isso. Sua solução organiza os processos em uma fila implícita de acordo com sua ordem de chegada, muito parecida com uma fila de espera em uma padaria. No entanto, não importa se um processador que está lendo dados que estão sendo atualizados por outro processador recebe lixo. O algoritmo ainda funciona.

Lamport recorda a sua descoberta do Algoritmo de Padaria.

O algoritmo de Padaria tornou-se material de livro de texto, e a maioria dos licenciados em Informática encontram-no no decurso dos seus estudos.

2. Fundamentos da programação concorrente

Novos conceitos importantes emanados do trabalho do Algoritmo de Padaria, uma tendência que se repetiu várias vezes na carreira de Lamport. A experiência de conceber algoritmos simultâneos e verificar a correção fez com que ele se concentrasse nos fundamentos básicos que fariam com que os multiprocessadores se comportassem de uma forma que os programadores pudessem raciocinar matematicamente. Ao trabalhar em uma solução para um problema concreto específico, Lamport inventou abstrações e regras gerais necessárias para raciocinar sobre sua correção, e essas contribuições conceituais tornaram-se então pilares teóricos da programação concorrente.

Loop-freedom: O trabalho de Algoritmo de Padaria introduziu um importante conceito chamado “loop freedom”. Algumas soluções óbvias que vêm à mente para o problema da exclusão mútua pré-atribuem ‘turnos’ em rotação entre os processos. Mas isto força os processos a esperar por outros que são lentos e ainda nem sequer chegaram ao ponto de contenção. Usando a analogia da padaria, seria semelhante a chegar a uma padaria vazia e ser convidado a esperar por um cliente que ainda nem chegou à padaria. Em contraste, a liberdade de loop-freedom expressa a capacidade dos processos de progredir independentemente da velocidade dos outros processos. Como o Algoritmo de Panificação atribui voltas aos processos na ordem da sua chegada, ele tem liberdade de laço. Este é um conceito crucial que tem sido usado no desenho de muitos algoritmos subsequentes, e no desenho de arquitecturas de memória. A liberdade de espera, uma condição que requer progresso independente apesar das falhas, tem as suas raízes claras na noção de liberdade de laço e no conceito de porta da padaria. Foi posteriormente explorada extensivamente por outros, incluindo Maurice Herlihy .

Consistência sequencial: Trabalhando com uma arquitetura multi-core que tinha memória cache distribuída levou Lamport a criar especificações formais para um comportamento de cache coerente em sistemas multiprocessadores. Esse trabalho trouxe alguma ordem ao caos desse campo ao inventar a consistência sequencial , que se tornou o padrão ouro para modelos de consistência de memória. Esta noção simples e intuitiva fornece exatamente o nível certo de “atomicidade” para permitir que o software funcione. Hoje nós projetamos sistemas de hardware com pedido de timestamp ou pedido parcial de loja, com instruções adicionais de cerca de memória, o que permite aos programadores fazer o hardware parecer sequencialmente consistente. Os programadores podem então implementar algoritmos que fornecem fortes propriedades de consistência. Isto é fundamental para os modelos de consistência de memória de Java e C++. Nossos processadores multicore rodam hoje baseados nos princípios descritos por Leslie Lamport em 1979.

Registros atômicos e regulares: O Algoritmo de Padaria também levou Lamport a questionar-se sobre a semântica precisa da memória quando múltiplos processos interagem para compartilhar dados. Levou quase uma década para formalizar, e o resultado é a abstração de registros regulares e atômicos .

A sua teoria dá a cada operação em um registro compartilhado uma duração explícita, começando com uma invocação e terminando com um resultado. Os registros podem ser implementados por uma variedade de técnicas, tais como a replicação. No entanto, as interações dos processos com um registro atômico devem “parecer” acessos em série à memória compartilhada real. A teoria também inclui uma semântica de interação mais fraca, como as de um registro regular. Um registro regular captura situações em que os processos lêem diferentes réplicas do registro enquanto ele está sendo atualizado. A qualquer momento, algumas réplicas podem ser atualizadas enquanto outras não o são e, eventualmente, todas as réplicas manterão o valor atualizado. Importante, estas semânticas mais fracas são suficientes para suportar a exclusão mútua: o algoritmo Bakery funciona corretamente se um leitor sobreposto a um escritor obtém de volta qualquer valor arbitrário.

Lamport descreve seu trabalho para definir precisamente abstrações para registros atômicos, regulares e seguros.

Este trabalho iniciou um subcampo distinto de pesquisa em computação distribuída que ainda está florescendo. Os objetos atômicos de Lamport suportavam apenas operações de leitura e escrita, ou seja, eles eram registros atômicos. A noção foi generalizada para outros tipos de dados por Maurice Herlihy e Jeannette Wing , e seu termo “linearidade” tornou-se sinônimo de atomicidade. Hoje, essencialmente todos os sistemas de armazenamento não-relacionais desenvolvidos por empresas como Amazon, Google e Facebook adotam linearidade e consistência seqüencial para suas garantias de coerência de dados.

3. Fundamentos de Sistemas Distribuídos

Um tipo especial de sistema concorrente é um sistema distribuído, caracterizado por ter processos que utilizam mensagens para interagir uns com os outros. Leslie Lamport tem tido um enorme impacto na forma como pensamos em sistema distribuído, bem como nas práticas de engenharia do campo.

Relógios lógicos: Muitas pessoas perceberam que uma noção global de tempo não é natural para um sistema distribuído. Lamport foi o primeiro a fazer uma noção alternativa precisa de “relógios lógicos”, que impõem uma ordem parcial dos eventos baseada na relação causal induzida pelo envio de mensagens de uma parte do sistema para outra . Seu trabalho sobre “Tempo, Relógios e Ordenação de Eventos em um Sistema Distribuído” se tornou o mais citado dos trabalhos de Lamport, e na linguagem da informática os relógios lógicos são muitas vezes apelidados de Lamport timestamps. Seu trabalho ganhou o Prêmio Influential Paper Principles of Distributed Computing Conference 2000 (mais tarde renomeado Edsger W. Dijkstra Prize in Distributed Computing), e ganhou o Prêmio ACM SIGOPS Hall of Fame em 2007.

Lamport descreve seu trabalho “Tempo, Relógios…” e sua relação com a relatividade especial.

Para entender porque esse trabalho se tornou tão influente, reconheça que na época da invenção não havia uma boa maneira de capturar o atraso de comunicação em sistemas distribuídos, exceto usando o tempo real. Lamport percebeu que o atraso na comunicação tornava esses sistemas muito diferentes de um sistema multiprocessador de memória compartilhada. A percepção veio quando se lia um artigo sobre bases de dados replicadas e se percebia que sua ordenação lógica de comandos poderia violar a causalidade.

Usar a ordenação de eventos como uma forma de provar a correção do sistema é o que as pessoas fazem hoje em dia para provas intuitivas de algoritmos de sincronização simultâneos. Outra contribuição poderosa deste trabalho foi demonstrar como replicar uma máquina de estado usando relógios lógicos, que é explicado abaixo.

Fotografias distribuídas: Uma vez definida a ordem causal, a noção de estados globais consistentes segue naturalmente. Isso levou a outro trabalho perspicaz. Lamport e Mani Chandy inventaram o primeiro algoritmo para ler o estado (tirando um `snapshot’) de um sistema distribuído arbitrário . Esta é uma noção tão poderosa que outros a utilizaram mais tarde em diferentes domínios, como redes, auto-estabilização, depuração, e sistemas distribuídos. Este trabalho recebeu o prêmio ACM SIGOPS Hall of Fame de 2013.

4. Tolerância a falhas e Replicação de Máquina de Estado

“Um sistema distribuído é aquele em que a falha de um computador que você nem sabia que existia pode tornar seu próprio computador inutilizável” é um famoso quip Lamport. Muito do seu trabalho está preocupado com a tolerância a falhas.

State Machine Replication (SMR): Talvez a mais significativa das muitas contribuições de Lamport é o paradigma da Replicação de Máquina Estatal, que foi introduzido no famoso artigo sobre “Time, Clocks, and the Ordering of Events in a Distributed System”, e desenvolvido logo após . A abstração captura qualquer serviço como uma máquina de estado centralizada — uma espécie de mecanismo de computação universal semelhante a uma máquina Turing. Ela tem um estado interno, e processa comandos em sequência, cada um resultando em um novo estado interno e produzindo uma resposta. Lamport percebeu que a tarefa assustadora de replicar um serviço em vários computadores pode se tornar notavelmente simples se você apresentar a mesma seqüência de comandos de entrada para todas as réplicas e elas prosseguirem através de uma sucessão idêntica de estados.

Este paradigma SMR perspicaz está subjacente a muitos sistemas confiáveis, e é considerado uma abordagem padrão para construir sistemas distribuídos replicados devido à sua elegância. Mas antes de Lamport desenvolver uma solução completa usando para SMR, ele precisava abordar um ingrediente central, o acordo, que foi abordado em seu próximo trabalho.

Acordo Bizantino: Enquanto as abordagens de máquinas de estado que são resistentes a falhas de crash são suficientes para muitas aplicações, sistemas mais críticos, como para aviônica, precisam de um modelo ainda mais extremo de tolerância a falhas que seja impermeável a nós que possam perturbar o sistema a partir de dentro.

No Stanford Research Institute (mais tarde chamado SRI International) na década de 1970, Lamport fez parte de uma equipe que ajudou a NASA a projetar um sistema de controle de aviônica robusto. As garantias formais eram uma necessidade absoluta devido à natureza de missão crítica da tarefa. A segurança tinha de ser garantida contra a avaria mais extrema do sistema que se pudesse imaginar. Um dos primeiros desafios que a equipe da SRI foi solicitada a enfrentar foi provar a correção de um esquema de controle do cockpit, que a NASA havia projetado, com três sistemas de computador que utilizam votação majoritária para mascarar qualquer componente defeituoso.

O resultado do trabalho da equipe foi vários conceitos fundamentais e insights a respeito desses tipos rigorosos de sistemas robustos. O trabalho incluiu uma definição fundamental de robustez neste cenário, uma abstração do problema de coordenação que está subjacente a qualquer sistema replicado até esta data, e uma revelação surpreendente de que sistemas com três computadores nunca podem executar com segurança um cockpit de missão crítica!

Indeed, em dois trabalhos seminais (“LPS”) publicados com Pease e Shostak , a equipe primeiro identificou uma vulnerabilidade algo peculiar. O LPS afirmou que “um componente falhado pode exibir um tipo de comportamento que é frequentemente negligenciado — nomeadamente, enviar informações conflituosas para diferentes partes do sistema”. Mais geralmente, um componente defeituoso pode funcionar de uma maneira completamente inconsistente com seu comportamento prescrito, e pode parecer quase malicioso.

O novo modelo de falha precisava de um nome. Na época, houve um desafio clássico relacionado à coordenação de dois computadores comunicantes, introduzido num artigo de 1975 e referido por Jim Gray como o “The Two Generals Paradox”. Isto levou Lamport a pensar nos computadores de controle em um cockpit como um exército de generais bizantinos, com o exército tentando formar um ataque coordenado enquanto dentro dos traidores enviava sinais conflitantes. O nome “Falhas Bizantinas” foi adotado para este modelo de falha, e seguiu-se uma enxurrada de trabalho acadêmico. O modelo de falha bizantina ainda está em uso para capturar o pior tipo de contratempos e falhas de segurança em sistemas.

Lamport explica o uso de uma história sobre “Generais Bizantinos” para enquadrar um problema em sistemas distribuídos tolerantes a falhas.

Byzantine Failures analisa as coisas ruins que podem acontecer. Mas e quanto às coisas boas que precisam acontecer? O LPS também deu uma formulação abstrata do problema de alcançar a coordenação apesar das falhas bizantinas; isto é conhecido como o problema do “Acordo Bizantino”. Esta formulação sucinta expressa a tarefa de coordenação de controle como o problema de formar uma decisão de acordo para um bit individual, começando com a entrada de bits potencialmente diferentes para cada componente. Uma vez que você tem acordo sobre um único bit, é possível usá-lo repetidamente a fim de manter todo um sistema complexo coordenado. O papel mostra que são necessários quatro computadores para formar um acordo sobre um único bit em face de uma única avaria. Três não são suficientes, porque com três unidades, uma unidade defeituosa pode enviar valores conflitantes para as outras duas unidades, e formar uma maioria diferente com cada uma delas. Mais genericamente, eles mostraram que 3F+1 unidades são necessárias para superar F simultaneamente componentes defeituosos. Para provar isso, eles utilizaram um belo argumento de simetria que ficou conhecido como o “argumento hexágono”. Este argumento de arquétipo encontrou outros usos sempre que se argumenta que uma unidade defeituosa que envia informações conflitantes para diferentes partes do sistema parece indistinguível de uma situação simétrica na qual as funções corretas e defeituosas são invertidas.

LPS também demonstraram que as unidades 3F+1 são suficientes, e apresentaram uma solução para alcançar o Acordo Bizantino entre as unidades 3F+1 nas rondas de comunicação síncrona de F+1. Eles também demonstraram que se você usar assinaturas digitais, apenas 2F+1 unidades são suficientes e necessárias.

O problema do Acordo Bizantino e suas soluções tornaram-se a marca registrada dos sistemas tolerantes a falhas. A maioria dos sistemas construídos com redundância utilizam-no internamente para replicação e para coordenação. O próprio Lamport usou-o mais tarde na formação do paradigma de replicação da máquina estatal discutido a seguir, que dá a base algorítmica da replicação.

O trabalho de 1980 recebeu o Prémio Edsger W. Dijkstra 2005 em Computação Distribuída, e o trabalho de 1982 recebeu o Prémio Jean-Claude Laprie em Computação Confiável.

Paxos: Com um entendimento crescente do problema do acordo para a computação distribuída, era hora de Lamport voltar para a replicação da máquina estatal e resolver as falhas lá. A primeira solução SMR que ele apresentou em seu trabalho de 1978 assumiu que não existem falhas, e faz uso do tempo lógico para passar réplicas através da mesma seqüência de comandos. Em 1989, Lamport projetou um algoritmo tolerante a falhas chamado Paxos . Continuando sua tendência de contar parábolas humorísticas, o artigo apresenta a história imaginária de um parlamento governamental em uma antiga ilha grega chamada Paxos, onde a ausência de qualquer número de seus membros, ou possivelmente de todos eles, pode ser tolerada sem perder a consistência.

Lamport descreve as origens do seu algoritmo Paxos para computação distribuída tolerante a falhas.

Felizmente, a configuração como parábola grega dificultou a compreensão do artigo pela maioria dos leitores, e levou nove anos desde a submissão à publicação em 1998. Mas o relatório técnico do DEC de 1989 foi notado. O colega de Lamport, Butler Lampson, evangelizou a idéia para a comunidade da computação distribuída. Pouco depois da publicação da Paxos, o sistema Chubby do Google e o ZooKeeper de código aberto do Apache ofereceram a State Machine Replication como um serviço externo, amplamente utilizado.

Paxos costura uma sucessão de decisões de acordo em uma seqüência de comandos de máquina do estado de forma otimizada. Importante, a primeira fase do componente de acordo dado no papel Paxos (chamado Sínodo) pode ser evitada quando o mesmo líder preside múltiplas decisões; essa fase precisa ser executada apenas quando um líder precisa ser substituído. Esta descoberta explica grande parte da popularidade da Paxos, e foi posteriormente chamada Multi-Paxos pela equipa da Google. O papel da Lamport Paxos ganhou o prêmio ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award em 2012.

SMR e Paxos tornaram-se a estrutura padrão de facto para a concepção e raciocínio sobre consenso e métodos de replicação. Muitas empresas construindo sistemas de informação críticos, incluindo Google, Yahoo, Microsoft e Amazon, adotaram as fundações da Paxos.

5. Especificação formal e verificação de programas

Nos primeiros dias da teoria da concorrência surgiu a necessidade de boas ferramentas para descrever soluções e provar sua correção. Lamport tem feito contribuições centrais para a teoria da especificação e verificação de programas concorrentes. Por exemplo, ele foi o primeiro a articular as noções de propriedades de segurança e propriedades de vivacidade para algoritmos distribuídos assíncronos. Estas foram a generalização das propriedades de “partial correctness” e “total correctness” previamente definidas para programas sequenciais. Hoje, as propriedades de segurança e vivacidade formam a classificação padrão para propriedades de correção de algoritmos distribuídos assíncronos.

Outro trabalho, com Martin Abadi , introduziu uma abstração especial chamada variáveis de profecia a um modelo de algoritmo, para lidar com uma situação em que um algoritmo resolve uma escolha não determinística antes que a especificação o faça. Abadi e Lamport apontaram situações onde tais problemas surgem, e desenvolveram a teoria necessária para suportar esta extensão à teoria. Além disso, eles provaram que sempre que um algoritmo distribuído satisfaz uma especificação, onde ambos são expressos como máquinas de estado, a correspondência entre eles pode ser provada usando uma combinação de variáveis de profecia e noções anteriores, tais como variáveis de história. Este trabalho ganhou o prémio LICS Test-Of-Time 2008.

Formal Modeling Languages and Verification Tools: Além de desenvolver as noções básicas acima, Lamport desenvolveu a linguagem TLA (Temporal Logic of Actions) e o conjunto de ferramentas TLA+, para modelagem e verificação de algoritmos e sistemas distribuídos.

Lamport descreve TLA e sua conexão com o mapeamento de refinamento.

TLA e TLA+ suportam especificação e prova de propriedades de segurança e vivacidade, usando notação baseada em lógica temporal. A Lamport supervisionou o desenvolvimento de ferramentas de verificação baseadas no TLA+, nomeadamente o verificador do modelo TLC construído por Yuan Yu. TLA+ e TLC têm sido utilizados para descrever e analisar sistemas reais. Por exemplo, estas ferramentas foram utilizadas para encontrar um erro importante no protocolo de coerência utilizado no hardware para a Xbox 360 da Microsoft antes do seu lançamento em 2005. Na Intel, foi utilizado para a análise de um protocolo de coerência de cache do Intel Quick Path Interconnect conforme implementado no processador central Nehalem. Para ensinar aos engenheiros como utilizar as suas ferramentas de especificação formal, Lamport escreveu um livro . Mais recentemente, Lamport desenvolveu a linguagem formal PlusCAL e ferramentas para uso na verificação de algoritmos distribuídos; este trabalho se baseia em TLA+.

6. LaTeX

Ao criar uma coleção tão vasta de papéis impactantes, é natural desejar uma ferramenta de composição tipográfica conveniente. Lamport não desejava apenas uma, ele criou uma para toda a comunidade. Fora do campo de concorrência está o sistema Latex de Lamport , um conjunto de macros para uso com o sistema de composição TeX de Donald Knuth. LaTeX adicionou três coisas importantes ao TeX:

1. O conceito de ‘ambiente de composição tipográfica’, que teve origem no sistema Scribe de Brian Reid.
2. Uma forte ênfase na marcação estrutural em vez de tipográfica.
3. Um design genérico de documentos, suficientemente flexível para ser adequado a uma grande variedade de documentos.

Lamport não originou estas ideias, mas ao empurrá-las tanto quanto possível criou um sistema que proporciona a qualidade do TeX e muita da sua flexibilidade, mas que é muito mais fácil de usar. Latex tornou-se o padrão de fato para publicação técnica em informática e muitas outras áreas.

Existem muitos outros trabalhos importantes de Leslie Lamport — muitos demais para descrever aqui. Eles estão listados em ordem cronológica na página inicial de Lamport , acompanhados de notas históricas que descrevem a motivação e o contexto de cada resultado.

Quando você acessa um computador moderno, é provável que você seja impactado pelos algoritmos de Leslie Lamport. E todo esse trabalho começou com a busca de entender como organizar uma fila em uma padaria local.

Autor: Dahlia Malkhi
Contribuidores adicionais: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese, e Len Shustek