Ante: uma nova forma de combinar verificação de empréstimos e contagem de referências

• Ante é um projeto de linguagem de sistemas que busca combinar a flexibilidade da contagem de referências com a segurança da verificação de empréstimos, evitando pânicos em tempo de execução no estilo Rust ou a sobrecarga das verificações de acesso exclusivo em tempo de execução no estilo Swift
• O mecanismo central é a shape-stability e a temporary uniq conversion: ele cria com segurança empréstimos mutáveis para campos de valores com contagem de referências e trata valores dentro de uniões como uniq apenas em escopos limitados
• Rc<RefCell<T>> em Rust pode gerar pânico em tempo de execução se usado incorretamente, e o borrowing system do Swift inclui verificações de acesso exclusivo em tempo de execução, mas Ante tenta lidar com alguns casos por meio de regras em tempo de compilação
• Ainda é um projeto work-in-progress, apenas parcialmente implementado; como é preciso analisar tipos recursivamente para determinar se um objeto específico é alcançável, adicionar campos pode se tornar uma breaking API change
• Essa abordagem enfraquece a premissa de que shared mutable borrowing é sempre impossível e, junto com técnicas como Vale, group borrowing e Rust GhostCell, amplia a zona de exceções no projeto de segurança de memória

---

A combinação que Ante busca

• Ante é uma linguagem de programação de sistemas que busca ser um Rust mais simples, com segurança de memória e segurança de threads
• O modelo básico é de propriedade única e verificação de empréstimos, e os valores ficam inline na stack ou dentro da estrutura/array que os contém
• Quando se quer priorizar a simplicidade, é possível escolher contagem de referências adicionando a palavra-chave shared ao tipo
• A função balance de uma red-black tree usando shared type Color e shared type RbTree t é tão curta quanto o exemplo em Python e menor que os exemplos em C++ e Rust
• A questão central é como lidar com o empréstimo mutável de dados com contagem de referências sem o risco de pânico de borrow_mut() em Rust nem verificações de acesso exclusivo em tempo de execução como no Swift
• Ante ainda está em estado work-in-progress: algumas partes foram implementadas, outras são teóricas, e o design continua mudando
  • O progresso pode ser acompanhado no site do Ante e no Discord

shape-stability e múltiplas referências mutáveis

• A shape-stability de Ante é a ideia de que “uma referência a um alvo com stable shape permanece sempre válida, independentemente de quaisquer alterações que ocorram em outro lugar”
• Graças a esse conceito, é possível ter várias referências de empréstimo mutável ao mesmo tempo para a mesma estrutura
• No exemplo heal (healer: mut Entity) (target: mut Entity), é possível chamar self_heal passando a mesma Entity como os dois argumentos, fazendo a entidade curar a si mesma
  • Mesmo que healer e target apontem para a mesma Entity, esse código não pode destruir a Entity, portanto as duas referências continuam válidas
• Também podem ser permitidas simultaneamente referências mutáveis à própria estrutura, a seus campos e aos campos desses campos
  • Mesmo usando ship: mut Spaceship e engine_alias: mut Engine = ship.engine ao mesmo tempo, considera-se que ship e o engine dentro dela não serão destruídos durante a execução da função
• Rust e Swift não permitem uma forma em que várias referências &mut apontem simultaneamente para os mesmos dados

Empréstimo mutável de campos em valores com contagem de referências

• Em Ante, adicionar shared antes da definição de um tipo faz com que esse tipo passe automaticamente a usar contagem de referências
• No exemplo shared mut type Spaceship, launch mantém uma Spaceship equivalente a um Rc enquanto passa mut ship.engine para set_fuel
• Como launch mantém vivo o objeto contêiner, Spaceship, é possível concluir que seu campo engine também está vivo
• A regra geral é que sempre é possível criar uma referência de empréstimo mut para um campo de um tipo shared mut
  • Porém, nem sempre é possível criar empréstimos mutáveis para todos os alvos contidos dentro desse campo; regras separadas são necessárias
• Os exemplos posteriores usam a notação mais explícita Rc Spaceship em vez do açúcar sintático shared mut type Spaceship
  • shared mut type Spaceship se torna type Spaceship, e var ship: Spaceship se torna var ship: Rc Spaceship

Onde uniões criam problemas de segurança

• Uniões armazenam o conteúdo inline, reduzindo o rastreamento de ponteiros e cache misses, o que favorece a velocidade
  • Quando uma union Engine em C fica dentro de uma struct Spaceship, StringTheoryEngine e ImpulseEngine ficam localizados dentro da memória de Spaceship
  • Isso contrasta com a abordagem baseada em interfaces e ponteiros, como em Java
• O problema é que é difícil oferecer suporte seguro a uniões em linguagens com segurança de memória
• Em um exemplo em que Engine é StringTheoryEngine(str: String) ou ImpulseEngine(fuel: I32), pode ocorrer uma falha de segmentação quando ship e other_ship apontam para a mesma Spaceship
  • Primeiro, pega-se uma referência interna à string com match uniq ship.engine
  • Depois, o mesmo engine é trocado por outra variante com other_ship.engine := ImpulseEngine 0x42
  • Em seguida, modificar o str anterior cria o problema de usar o interior depois que o contêiner foi destruído
• Portanto, Ante precisa impedir a criação de uma referência de empréstimo mutável para uma das variantes quando uma referência de empréstimo mutável aponta para uma união
• Isso é o oposto da regra para estruturas
  • Quando há uma referência mut para uma estrutura, é possível criar uma referência mut para um campo
  • Quando há uma referência mut para uma união, não é possível criar uma referência mut para o interior de uma variante

uniq e temporary uniq conversion

• uniq significa exclusive mutable reference, ou seja, referência mutável exclusiva
• Se uma variável contém uniq Spaceship, ela é a única referência disponível para essa Spaceship
  • É um conceito parecido com &mut Spaceship em Rust
• Para lidar com segurança com o interior de uniões, Ante usa temporary uniq conversion
• A regra central é que, se outras referências possivelmente aliasadas não forem usadas em um determinado escopo, é possível obter temporariamente uma referência uniq
  • No trecho match uniq ship.engine, ship.engine é acessado como se fosse uniq
  • Durante esse trecho, o compilador impede o uso de outras variáveis existentes que possam conter indiretamente a Spaceship
• Enquanto Rust impede a própria existência de um uniq pelo motivo de que “outras referências podem existir em algum lugar”, Ante permite uniq sob a condição de que essas referências não sejam usadas naquele escopo
• Nesse caso, uniq Spaceship não é de fato uma referência globalmente única, mas a única referência disponível dentro daquele escopo
  • A nuance é semelhante à de ponteiros restrict em C

Acessos permitidos e rejeitados

• Dentro do escopo de match uniq ship.engine, acessar other_ship: Rc Spaceship deve gerar erro de compilação
  • other_ship.engine pode ser um alias de ship.engine
  • E alterar other_ship.engine enquanto ship.engine está em uso poderia causar um drop
• Outra estrutura que tenha Rc Spaceship como campo, como HasAShip, também é rejeitada pelo mesmo motivo
  • other.ship.engine também pode alcançar indiretamente a mesma Spaceship
• Por outro lado, um inteiro como new_fuel: I32 pode ser usado
  • Isso porque I32 não pode conter referência a Spaceship
• Se a própria Spaceship contiver um campo como follow_ship: Rc Spaceship, a conversão é rejeitada
  • Nesse caso, uniq Spaceship também voltaria a ser alcançável por meio de um caminho interno dela mesma, portanto em geral não é possível fazer conversão mut -> uniq em tipos recursivos

Restrições em chamadas de função e retornos

• A conversão mut -> uniq também pode ocorrer em chamadas de função
• Quando foo (var ship: Rc Spaceship) (new_res: Resonator) chama maybe_use_resonator ship new_res, ship é convertido para uniq Spaceship no ponto da chamada
  • O compilador só precisa verificar se outros argumentos podem conter uma referência a Spaceship
  • No exemplo, Resonator não contém tal referência, então é permitido
• Em retornos, a referência uniq convertida não pode ser devolvida como um uniq comum
  • Isso porque, após o retorno, a verificação do compilador de “não usar variáveis possivelmente aliasadas dentro do escopo” deixa de se aplicar
• Em vez disso, o tipo de retorno pode ser especificado como local uniq Foo
  • Internamente, ao converter de mut ref para uniq ref, o que é criado na prática é sempre um local uniq
  • Na maioria dos casos, ele pode ser usado como um uniq comum, mas ao retornar é preciso explicitá-lo

Custos de design e alternativas

• Ante consegue converter uma referência com contagem de referências, como Rc Spaceship, em uma uniq Spaceship temporária sem erros em tempo de execução
• A desvantagem é que o compilador precisa inspecionar tipos recursivamente para responder perguntas como “é possível alcançar Spaceship a partir de Engine?”
• Essa análise pode ser frágil
  • Adicionar um campo a uma estrutura pode se tornar uma breaking API change
• Jake, criador de Ante, está procurando uma forma melhor de manter essa garantia
  • Uma abordagem como group borrowing e Flix references, que adiciona um tipo de marca anônimo e único a cada tipo mutável compartilhado
  • Uma abordagem que elimina a análise de tipos adicionando um efeito como Mutates 'a ao alterar tipos compartilhados
  • Uma abordagem em que o usuário verifica em tempo de execução se duas referências apontam para objetos diferentes, ou fornece uma verificação unsafe encapsulada em uma API safe
  • Uma abordagem em que o compilador rastreia valores que não são armazenados indiretamente dentro de um Rc e, portanto, não podem virar aliases
• Ideias semelhantes à iso permission do Pony, ou permissões temporárias que permitem olhar para dentro da estrutura mas impedem o uso de referências que apontem para fora, também continuam sendo possibilidades
• A parte difícil é preservar os objetivos de Ante — usabilidade, legibilidade e simplicidade — mantendo essa flexibilidade

O fluxo mais amplo da segurança de memória

• shared mutable borrowing já foi considerado impossível, e há a perspectiva de que Rust também foi projetado com base nessa crença
• Várias exceções vêm se acumulando
  • Ante consegue obter referências de empréstimo uniq a partir de dados shared-mutable por meio de regras de local uniqueness
  • Vale consegue obter referências de empréstimo imutáveis a partir de dados shared-mutable por meio de pure functions
  • group borrowing consegue criar referências de empréstimo shared-mutable mesmo sem shape-stable
  • GhostCell em Rust permite que grafos de objetos apontem livremente uns para os outros, mas em um determinado momento só pode haver uma referência mutável para um deles
• Esse movimento sugere que talvez existam princípios mais gerais para lidar com shared mutable borrowing no design de segurança de memória

Comparação com Cell em Rust

• Usuários de Rust podem perguntar qual é a diferença entre colocar Cell em campos de uma estrutura e a abordagem de Ante
• No exemplo de Ante, é possível obter uma referência mut String para status: String a partir de Rc Spaceship e anexar diretamente " (refueling)"
• Com a abordagem Cell<String> de Rust, não é possível obter &mut String a partir de Rc<Spaceship>
  • Em vez disso, é preciso inserir um valor padrão temporário com status_ref.replace(String::new())
  • Modificar a String retirada
  • E, no fim, colocá-la de volta com outro replace(status)
• Essa abordagem tem algumas desvantagens
  • É preciso criar uma instância padrão como ""
  • Há o risco de esquecer a chamada final a replace
  • Há o risco de alguém ler status enquanto o valor foi substituído
• Ante permite obter temporariamente uma referência à string status e o compilador impede que outro código a acesse durante esse período

[GN⁺]

Opiniões no Lobste.rs

• A ideia de que “empréstimo mutável compartilhado” seria impossível não era apenas um sacrifício que Rust aceitou para atingir seu objetivo, mas algo muito próximo do próprio objetivo central de Rust
  porque estado mutável compartilhado dificulta o raciocínio local sobre o código
  "References are like jumps" by withoutboats aborda bem esse ponto. Impedir mudanças acidentais em estado com alias é essencial para facilitar a construção de sistemas que funcionem corretamente, e a tese é que as regras de lifetime de Rust não são apenas um mecanismo para evitar coleta de lixo, mas uma estrutura mais profunda para garantir previsibilidade em uma linguagem que permite ao mesmo tempo estado mutável e estado com alias

  • Tive a mesma impressão quando o autor falou antes sobre o borrow checker do Mojo. O borrow checker de Rust preserva a semântica de valor mesmo em programas de thread única

• Parece bem interessante
  Se entendi corretamente, a mágica de passar de uma referência compartilhada para uma referência mutável só é possível porque se limita a tipos que não são compartilhados entre threads, e a unicidade de Rc parece ser garantida ao tratar todos os objetos do mesmo tipo como se tivessem sido emprestados com o mesmo lifetime
  Pode ser questão de gosto preferir sintaxe explícita ou sintaxe natural, mas isso mostra que, se o compilador souber mais sobre Cell, ele pode permitir referências mutáveis a ele com mais flexibilidade
  E também evita a terminologia confusa de Rust, em que mut é usado como se significasse não mutabilidade, mas exclusividade/unicidade

  • Fiquei curioso sobre como isso funciona entre threads. Minha dúvida era algo como: “a promoção para uniq significa adquirir um lock?”, mas entendi que a comparação não é com Arc, e sim com Rc
  • Você poderia explicar um pouco melhor essa parte sobre mut significar exclusividade/unicidade?

• Fico curioso se alguém tem alguma ideia de qual seria o princípio unificador insinuado no final

• Também vale conferir discussões anteriores sobre posts do blog antelang.org

• Não entendi muito bem como isso funciona. Parece querer dizer algo como “se você tem um ponteiro mutável para um objeto, pode obter uma referência mutável para um slice desse objeto”
  Mas, se for isso, então parece que algo como mutref someobjext = …, mutref subfield = someobjext.a.b, someobjext.a = somethingelse poderia acontecer, e aí subfield poderia ser invalidado ou quebrar ao ter seu valor alterado
  O texto tinha muitas explicações, comparações com outras linguagens e exemplos de código, mas foi difícil encontrar uma apresentação básica da semântica passo a passo de como isso funciona de fato