Reescrevi um algoritmo de roteirização em Bend e medi contra Java

O problema, em um parágrafo

Uma distribuidora atende algumas dezenas de cidades a partir de um depósito. Cada caminhão tem capacidade limitada, o motorista tem jornada limitada, e quando a rota não cabe em um dia o caminhão dorme em um hotel aprovado e continua no dia seguinte. O algoritmo lança uma “formiga” que monta um plano inteiro tomando decisões probabilísticas a cada parada, e repete isso 6 milhões de vezes (15.000 iterações com 400 formigas cada), guardando o melhor plano.

Para o benchmark, o que importa é o formato da carga: as formigas de uma iteração são independentes entre si. Nenhuma escreve em nada que outra leia. É paralelismo de livro-texto.

Primeiro contato: Bend não é Java com sintaxe diferente

A primeira versão não compilou nem perto. Bend tem um conjunto de restrições que, no começo, parecem arbitrárias, e depois de um tempo você percebe que quase todas existem para garantir que o programa possa ser cortado em pedaços paralelos sem análise complicada.

Não existe if. Você casa padrão em um parâmetro:

def pickf(c: Bool, a: F32, b: F32) -> F32:
  match c:
    case True{}:
      a
    case False{}:
      b

E o match só funciona sobre parâmetros ou variáveis de padrão, nunca sobre um valor que você acabou de calcular. Isso empurra o código para continuation-passing: em vez de calcular e destrinchar, você passa o valor para uma função que o recebe como parâmetro. Metade do port virou funções auxiliares com nomes como city_stats e city_pick por causa disso.

Não existe recursão mútua. O laço original em Java tinha duas fases que se chamavam: escolher a próxima parada e aplicar o movimento. Em Bend virou um laço só, com uma flag choosing dizendo em qual fase ele está:

def ant(fuel: Nat, go: Bool, choosing: Bool, st: Stats, pk: Pick, ...) -> Sol:
  match fuel go choosing st pk:
    case 1n+f True{} True{} Stats{...} _:
      # fase 1: olhar as opções e sortear a próxima parada
    case 1n+f True{} False{} _ Pick{...}:
      # fase 2: mover, e calcular as opções do próximo passo
    case 1n+_ False{} _ _ _:
      # terminou
    case _ _ _ _ _:
      # acabou o combustível

O guia é explícito sobre o motivo: “Termination is mandatory and mutual recursion is not allowed. Both restrictions keep Bend’s proofs sound, as a function that never returns could otherwise prove anything.” Existe um verificador de terminação que quer provar que sua recursão diminui, lendo os argumentos da esquerda para a direita. Um laço que termina por condição lógica, como o da formiga, não diminui nada, então ou você marca a função com @unsafe ou passa um combustível: um número natural que encolhe a cada chamada e dá o teto da recursão. O combustível da formiga vem de um raciocínio simples, no máximo uma visita, uma pernoite e um retorno ao depósito por cidade, duas chamadas cada. O verificador é literal quanto à ordem: uma das funções não passava só porque o argumento que encolhia era o segundo, e o primeiro mudava antes dele. Inverter os parâmetros resolveu.

Valores são afins. Por padrão você usa cada valor uma vez, e para reutilizar marca com +, o que faz o valor ser compartilhado por contagem de referência. Esse + vai no parâmetro, não no tipo (+tab: Tab), e foi um bom punhado de erros de sintaxe até acertar.

Nenhuma dessas restrições é gratuita para quem escreve. Mas todas empurram para o mesmo lugar: estrutura imutável, sem aliasing surpresa. É o preço de entrada do paralelismo automático.

O que muda na cabeça de quem vem de Java

A diferença não está na sintaxe, e essa foi a parte que me pegou. Em Java a formiga é uma classe com estado: um objeto com o caminhão atual, a carga, os minutos que sobraram do dia, a lista de cidades já atendidas, o gerador aleatório. Cada passo é um método que mexe nesses campos. Você lê o código de cima para baixo e o estado vai mudando junto.

final class Ant {
    final boolean[] delivered = new boolean[n];
    int left = c;
    int cur = 0, load = 0, trucks = 0;
    double j1 = journey, j2 = journey;
    ...
}

Em Bend não existe campo para mexer. Tudo que a formiga sabe vira parâmetro, e o parâmetro é repassado a cada chamada. O mesmo laço tem dezoito argumentos, porque cada pedacinho de estado que em Java morava num campo agora viaja explicitamente: a posição atual, a carga, os dois dias de jornada, a distância acumulada, os caminhões, as cidades atendidas como bitmask, a semente aleatória, a rota montada até ali. O arquivo inteiro tem setenta e nove definições, quase todas pequenas, porque o match só funciona sobre parâmetro e qualquer valor calculado precisa ser passado para outra função para ser aberto.

Isso tem um efeito colateral que dói na hora de mudar as coisas. Em Java, acrescentar uma informação ao algoritmo é adicionar um campo. Quando eu quis que a formiga lesse também a árvore de feromônio, tive que enfiar um argumento novo em seis funções encadeadas, cada uma com a sua lista de parâmetros já longa, e ajustar todas as chamadas. Não é difícil, é chato, e é o tipo de coisa que faz você pensar duas vezes antes de experimentar uma ideia.

A contrapartida é que o estado fica onde dá para ver. Sem campo mutável não existe “alguém mexeu nisso em outro lugar”, e foi isso que permitiu rodar a mesma função em onze núcleos sem pensar em sincronização. O que em Java é liberdade barata, alias para todo lado e escrita em qualquer lugar, em Bend é uma decisão explícita: reusar um valor exige marcar com +, e o compilador cobra a conta em contagem de referência.

O compilador, aliás, é professor rígido e de poucas palavras. As mensagens que mais vi foram três: consumed more than once, quando um valor é usado duas vezes sem o +; expected a decreasing self-call, quando a recursão não convence o verificador; e a recusa de um match aninhado, que obriga a criar mais uma definição só para abrir um registro. Cada uma delas é uma regra pequena, e juntas elas te empurram para um estilo bem específico. No começo parece que a linguagem está atrapalhando. Depois de um tempo eu percebi que estava escrevendo código que não tinha como ter condição de corrida, porque a forma de escrever errado nem compila.

A dificuldade que eu não previ foi depurar. Código puro em Bend não imprime, porque efeito vive no bloco de IO, então não dá para espalhar um print no meio do laço da formiga e ver o que acontece. O que sobra é devolver valor e medir o programa inteiro. Foi exatamente assim que eu descobri para onde ia o tempo do feromônio, compilando três versões do programa e comparando o relógio. Funciona, e é muito mais lento de fazer do que um System.out.println dentro do laço.

Se eu tivesse que resumir a diferença em uma frase: em Java eu descrevo o que a máquina deve fazer com a memória, e em Bend eu descrevo como o dado se transforma. A segunda forma custa mais para escrever, principalmente quando o algoritmo tem estado por natureza, e devolve um programa que a máquina consegue paralelizar sozinha. Nem sempre vale a troca. No caso das formigas, que são independentes por definição, valeu.

O modelo de paralelismo

A construção central é um let de duas pernas:

a b = colony(p, rows, lo, mid) colony(p, rows, mid, hi)
better(a, b)

As duas chamadas podem rodar em núcleos diferentes. Não tem anotação de thread, não tem pool, não tem join. Você escreve a árvore de forks e o runtime distribui.

O detalhe que muda tudo na prática está no guia: “Bend’s current scheduler is a contention-free, binary fork-join machine: every task is handed to a core exactly once and never moved afterwards. That makes it fast and GPU-friendly, but you must keep the workload balanced.” Sem migração de tarefa não tem contenção, e o mesmo modelo serve para GPU. Em compensação, se você gerar 4 tarefas gordas e tiver 11 núcleos, 7 ficam ociosos até o fim, e se uma tarefa for muito maior que as outras, o tempo total é o dela.

A regra de design que sai disso é larga e rasa, com folhas equilibradas. No ACO isso saiu natural, porque as formigas são todas parecidas: a solução é uma árvore binária balanceada de forks sobre o intervalo de formigas, e cada folha roda um punhado delas em sequência.

def colony(+depth: Nat, +rows: TabW, +it: U32, +lo: U32, +hi: U32) -> Sol:
  match depth:
    case 0n:
      ants(U32.is_lt(lo, hi), rows, it, lo, (hi - lo : U32), Sol{INF(), 0, []})
    case 1n+p:
      +mid = (lo + ((hi - lo : U32) >> 1n : U32) : U32)
      a b = colony(p, rows, it, lo, mid) colony(p, rows, it, mid, hi)
      better(a, b)

Onde isso doeu foi em outro algoritmo, escrito depois: uma busca local iterativa (ALNS). Lá o trabalho é naturalmente sequencial e comprido, uma cadeia de milhares de melhorias sucessivas. Rodar 16 cadeias em 11 núcleos rendeu 1,8× de ganho, não 11×. A saída foi reescrever a busca em rodadas: cada rodada forka 256 cadeias curtas a partir do melhor plano até então e fica com a melhor. Ficou mais paralelizável e, no fim, mais rápido em qualidade por segundo. Só que isso é uma mudança de algoritmo, não de código. A linguagem obriga a repensar a forma do problema.

Os números

Tudo num MacBook Pro M3 Pro, comparando com um port em Java do mesmo algoritmo, com arrays e ForkJoinPool. Mesma instância, mesmo gerador de números aleatórios, mesma ordem de candidatos, então dá para comparar passo a passo, não só o resultado final.

A linha do feromônio persistente é a que eu repeti mais vezes, porque foi a que me surpreendeu. No cenário 1, com a máquina parada, o Java resolve em 18,3 s e o Bend em 111,7 s, duas execuções seguidas com o mesmo número. Rodando os cinco cenários, a média fica em 17,2 s contra 108,4 s. Os dois planos usam sete caminhões e ficam a 0,8% um do outro.

A qualidade das soluções ficou igual dentro de ~2% em todos os casos, que é a variação natural entre execuções desses algoritmos. Não é uma troca de precisão por velocidade.

Sobre escalabilidade nos núcleos, com 200 × 400 formigas:

Esse é o resultado mais interessante do benchmark para mim. O Bend perde por constante, não por paralelismo: ele aproveita os núcleos um pouco melhor que o meu código Java com ForkJoinPool, só que parte de um ponto mais alto.

Por que a razão varia tanto: 2,4× ou 8×?

O número muda conforme o programa, e o padrão é claro. A razão piora quanto mais o programa aloca.

O ACO original é um laço aritmético sobre uma tabela imutável construída uma vez. Quase não cria estrutura nova, e fica em 2,4×.

O ALNS cria lista nova o tempo todo, porque cada rota candidata é uma lista nova, e cada distância entre duas cidades é uma descida numa árvore em vez de um dist[i][j]. Medi a operação isolada: avaliar uma rota custa ~1,1 µs no Bend contra ~0,1 µs no Java. Daí os 8×.

Vale dizer que muito disso é negociável com esforço. A primeira versão que funcionava rodava em 12,6 s em single thread; depois de reorganizar a instância como uma árvore balanceada percorrida uma vez por passo, e de trocar pow por multiplicações no laço quente, a mesma carga caiu para 2,7 s. A forma dos dados importa muito mais em Bend do que em Java, porque sem acesso indexado em memória contígua uma estrutura mal escolhida não tem como ser salva pelo hardware.

O experimento que me ensinou a pensar em Bend

O caso do feromônio virou a parte mais instrutiva do trabalho, e vale contar em detalhe porque eu errei duas vezes antes de entender.

A versão com feromônio precisa de uma matriz que todas as formigas leem e que é atualizada ao fim de cada iteração. Em Java isso é um double[][] e você escreve nele. Em Bend, a implementação monta uma árvore de feromônio, evapora ela inteira por iteração, deposita nas arestas da melhor rota e monta a tabela de pesos que as formigas leem. Meu primeiro palpite foi que aquilo era desperdício puro, e que a linguagem precisava de um array com escrita no lugar.

Fui conferir na documentação antes de publicar, e o array já existe: “An Array<T> is a Type, so it has exactly one owner at all times. That is what lets a[5] <- 42 overwrite the slot and hand back the same array, with no copy.” É o mecanismo que eu ia pedir, já implementado. Só que o guia de shaders traz a restrição que decide o caso: “An Array has one owner, so it cannot go down a fork tree: build lists.” Qualquer estrutura lida por milhões de tarefas em paralelo tem que ser uma árvore compartilhada mesmo. Array não se aplica aqui.

Então fui medir onde o tempo realmente estava, com 500 iterações de 400 formigas em 11 threads:

Evaporar e depositar custa 28 ms em 500 iterações, ou 0,06 ms por iteração. É ruído. Os 3,6 ms por iteração que eu achava que eram manutenção do feromônio são, na verdade, montar a tabela de pesos que as formigas leem.

A correção óbvia seria não montar tabela nenhuma: deixar as formigas lerem a árvore da instância e a árvore do feromônio em paralelo, passo a passo. Reescrevi assim, e o resultado foi o contrário do esperado:

As duas versões encontram exatamente o mesmo plano, e em single thread elas praticamente empatam. Em 11 threads a segunda trava. O motivo está no guia, numa frase que eu tinha lido sem entender: “a + value read by every lane costs an atomic per read”. Cada leitura de estrutura compartilhada custa uma operação atômica de contagem, então ler duas árvores por passo dobra esse tráfego e come o paralelismo.

A lição que eu levo é essa: em Bend, reconstruir dados pode sair mais barato que compartilhar uma estrutura a mais. É o inverso do instinto que eu trouxe de Java, onde alocação é cara e leitura de estrutura compartilhada é de graça.

A GPU: excelente e inútil, dependendo do programa

Em Bend, mandar uma chamada para a GPU é trocar f(x) por f!(x). Compila um kernel Metal junto com o binário, e é uma das coisas mais impressionantes de usar.

O resultado depende inteiramente do formato do trabalho. O ACO na GPU rodou em 8,6 s contra 33 s na CPU, e contra 13,7 s do Java em 11 threads: as formigas fazem todas o mesmo laço curto sobre a mesma tabela, que é o caso ideal. Já o ALNS na GPU ficou 16 a 28× mais lento que o próprio Bend na CPU, porque cada cadeia toma um ramo diferente a cada passo, aloca o tempo todo e lê uma tabela compartilhada.

O guia avisa isso antes de você tentar: “The GPU shines on uniform numeric work like mandelbrot or nbody; divergent work like n-queens stays faster on the CPU.” Os planos gerados na GPU e na CPU foram idênticos, então a divergência é só de desempenho. A lição é a mesma de CUDA, com uma facilidade de uso que não tem comparação.

Provas: a parte da linguagem que eu não esperava usar

A primeira linha do guia da Bend diz que ela combina “Lean-like formal proofs with C-like speeds and CUDA-like parallelism”. Eu tinha lido isso como marketing e fui atrás só no fim do trabalho, quando já tinha três implementações do mesmo algoritmo e queria saber se elas concordavam por acaso ou por construção.

O mecanismo é direto. Você escreve uma lei, que é um enunciado com quantificadores e uma igualdade:

law truck_capacity:
  for k: Nat
  for it: U32
  for a: U32
  {Rules.capacity(plan(k, it, a), 0) == True{} : Bool}

E prova essa lei com uma definição de mesmo nome em outro arquivo. Rodar o arquivo de provas checa tudo e falha enquanto sobrar lei em aberto, com uma mensagem seca: Error: 11 TODOs found. The code is incomplete, and not a valid proof yet. Um arquivo diz o que deve valer, o outro diz por quê, e o compilador não deixa você confundir os dois.

A prova mais simples é {==}, que é reflexividade: o verificador avalia os dois lados e vê o mesmo valor. Isso fecha qualquer lei que seja um termo fechado. As leis sobre os parâmetros do modelo saem assim, e três fatos sobre a instância também saíram, por análise de casos sobre as 81 localidades: a distância não depende do sentido, ficar parado custa zero, e a demanda de cada cidade cabe em um caminhão.

O que não saiu foram as leis interessantes. Dizer que toda formiga respeita a capacidade exige indução sobre o laço da formiga, mostrando que cada passo preserva o invariante. A Bend consegue expressar essa prova, mas escrevê-la é um projeto do tamanho do próprio algoritmo, e eu não escrevi. Tentei um atalho que parecia esperto, enunciar a lei para uma formiga específica, o que vira um termo fechado que o verificador poderia simplesmente avaliar. Ele precisa normalizar uma formiga inteira sobre 58 cidades e não tinha terminado depois de 14 minutos. Prova por avaliação alcança parâmetros e fatos sobre a instância, não uma execução do solver.

Mesmo sem as provas, o exercício pagou, e por um motivo que não é o que a propaganda vende. Para enunciar as regras eu tive que escrevê-las como funções que leem a instância crua e recebem um plano pronto, sem confiar em nada que o solver tivesse pré-calculado. Isso deu um juiz independente, e um juiz independente é exatamente o que faltava para eu comparar implementações. Como as leis são executáveis, elas valem como teste: rodei os checadores em 400 formigas, com o feromônio inicial e de novo depois de vinte iterações, e as regras que o programa garante passam em todas. As que ele não garante aparecem falsas, que é precisamente o que eu queria que a ferramenta me dissesse.

Minha conclusão sobre essa parte é menos entusiasmada que o slogan e mais útil que ele. Enunciar é barato e imediato, provar é caro e continua sendo trabalho humano. O ganho real de ter o sistema de provas na mesma linguagem do programa é que a especificação para de ser um comentário e vira código que o compilador checa, roda e cobra de você. Isso eu levaria para qualquer projeto, independentemente de um dia fechar a prova.

O que eu ainda pediria para a linguagem

Depois de conferir minha lista contra a documentação, sobraram três pedidos.

Balanceamento de carga no escalonador é o primeiro. O comportamento atual é assumido e coerente, e o próprio guia usa a palavra “current”, o que sugere que os autores veem isso como um estágio. Hoje o balanceamento é responsabilidade de quem escreve, e foi ele que transformou “rodar 16 cadeias” em “reescrever a busca em rodadas”.

O segundo é potência com expoente constante. F32.pow existe como primitiva, mas não achei nada sobre especializar expoente literal, e na prática ela foi um quinto do tempo até virar multiplicação na mão.

O terceiro é um profiler. Não há nada no guia nem flag na CLI além de --threads e --gpu. Hoje se descobre onde o tempo foi medindo variações do programa inteiro, que foi exatamente o que eu tive que fazer para achar o custo da tabela de pesos. Saber quantas interações cada definição consumiu mudaria o ciclo de otimização.

Uma observação que vale mais que a lista: a documentação da Bend é densa e responde muito mais do que parece na primeira leitura. Duas das minhas conclusões erradas estavam corrigidas lá, em uma frase cada.

Esse problema é bom para Bend?

Metade dele é, e vale separar bem as duas metades.

A geração de candidatos é um caso quase ideal. Milhões de simulações curtas, independentes, todas fazendo o mesmo tipo de trabalho sobre uma tabela que ninguém escreve. É o formato em que o paralelismo automático brilha, e foi aqui que um ! colocou a GPU 1,6× à frente do Java em 11 threads, sem uma linha de kernel escrita. Se o seu problema tem essa cara, como Monte Carlo, varredura de parâmetros ou avaliação de população em algoritmo genético, Bend entrega o que promete.

O refino de uma solução é um caso ruim. Busca local é uma cadeia sequencial e comprida de pequenas modificações, com desvio a cada passo e acesso aleatório a estruturas. Não paraleliza sozinha, não gosta de GPU, e é onde a tensão entre “compartilhado por muitas tarefas” e “acesso indexado rápido” aparece inteira, porque as duas coisas não se combinam hoje. Dá para reformular em rodadas curtas e largas, como eu fiz, mas aí você está mudando o algoritmo para caber na máquina, e um algoritmo diferente pode simplesmente ser pior.

A conclusão prática é que a granularidade tem que ser escolhida com o escalonador em mente, não com o problema. Em Java eu decidiria isso pensando em cache e contenção. Em Bend eu decido pensando em quantas folhas parecidas eu consigo gerar, e em quantas estruturas compartilhadas cada folha precisa ler.

Análise final

Depois de algumas semanas nisso, minha leitura é essa.

O que a Bend entrega de verdade é paralelismo sem você escrever nada de paralelismo. Não teve mutex, não teve condição de corrida, não teve deadlock para depurar. O programa que roda em 1 thread é exatamente o que roda em 11, e o que roda na GPU muda um caractere. Essa é a parte do trabalho que costuma consumir mais tempo e gerar mais bug sutil.

O que ela cobra é um fator de 2 a 8 contra Java bem escrito, e quase nada disso vem do escalonador. Vem da representação dos dados, e uma parte vem de decisões de modelagem que só ficam óbvias depois de medir, como a da tabela de pesos.

Ganhei uma coisa que não esperava. Reescrever o algoritmo sem nenhum estado mutável deixou explícitas várias decisões que estavam implícitas na versão Java, e quando as duas versões passaram a dar respostas equivalentes eu tinha bem mais confiança no que o algoritmo realmente fazia. Reescrever em uma linguagem com regras mais duras é uma forma cara, mas eficaz, de revisar o próprio código.

No fim, Bend hoje não é a escolha para espremer o último ciclo, e Java, Rust ou C ainda vencem isso. Ela é a escolha quando o gargalo é o seu tempo, e a pergunta é quantos núcleos, ou qual GPU, você consegue usar sem transformar seu código em um campo minado de sincronização.