no xaur/verificar-arrendamentos-de-design

Verificar arrendamentos (leases) de design

crates/server/tla/DesignLeases.tla é um modelo TLA+ de dois servidores Finite que compartilham um armazenamento, e um design que se move entre eles. O TLC, o verificador de modelos TLA+, tenta todas as ordens de seus passos dentro de limites pequenos e verifica duas regras:

• StoredEditsStay (fencing): uma vez que o armazenamento aceita uma edição, nenhuma cópia obsoleta em outro servidor a sobrescreve. Se isso falhar, um servidor que travou acorda e apaga edições que o novo proprietário salvou.
• AckedEditsStay: uma edição que uma ferramenta MCP reportou como concluída está no armazenamento, ou em uma cópia que ainda pode salvá-la, a menos que seu servidor tenha falhado ou seu lease tenha expirado antes de a edição ser salva. Se isso falhar, um agente é informado de que sua edição funcionou, e então a edição desaparece. Os visualizadores a veem sumir, e nada informa o agente.

O código atual passa na primeira regra e falha na segunda de quatro maneiras conhecidas. Elas estão listadas em "Descobertas conhecidas" abaixo.

Sua alteração toca nisso?

Sim, se ela alterar qualquer função nesta tabela. Cada passo do modelo nomeia o código que representa, e um revisor pode abrir ambos lado a lado.

Passo do modelo	Código
CallStarts, CallFindsHandle, CallLoads, CallEdits, CallReads	mcp/mod.rs design, edit_checked; api.rs open; hub/mod.rs Hub::open, handle_for; hub/design.rs DesignHandle::load, edit
SaveTakes, SaveWrites, SaveFenced, SaveFails, SaveReleases, SaveDrops	hub/mod.rs persist; hub/design.rs take_save, save_failed
Unload	hub/mod.rs Hub::sweep; hub/design.rs unload_if_idle, is_idle
TickRenews … TickDiscovers	hub/mod.rs Hub::tick, let_go, remove, drop_copy, discover, summaries; hub/design.rs retire, end, lease
Owns, LeaseLapses, HeartbeatExpires	cluster.rs Members::now, lapsed, renewed, Cluster::owns, owner
CanClaim, Claimed, escritas no armazenamento	postgres/mod.rs claim, save, append, release, held; store.rs trait Store (o armazenamento compartilhado em memória deve corresponder)
Start, Crash	hub/mod.rs Hub::shared

Os caminhos estão sob crates/server/src/.

Commit de sincronização: 6606714. Esse é o último commit no qual o modelo foi verificado contra este código. Para ver o que mudou no código coberto desde então, execute:

git diff 6606714 -- crates/server/src/hub crates/server/src/mcp/mod.rs crates/server/src/api.rs crates/server/src/cluster.rs crates/server/src/postgres/mod.rs crates/server/src/store.rs

Se o diff tocar em uma função da tabela, releia o passo do modelo ao lado dela antes de confiar em uma aprovação. Avance o commit de sincronização, neste arquivo, somente depois de confirmar que cada passo alterado ainda corresponde ao código no novo commit.

Execute

crates/server/tla/check.sh          # a verificação diária, cerca de 2 minutos
crates/server/tla/check.sh --full   # adiciona Finding4.cfg e AllFixes.cfg, cerca de 3 minutos a mais

O script baixa o TLC (tla2tools.jar v1.7.4, SHA-256 verificado) em ~/.cache/finite na primeira execução. Você precisa do Java 11 ou mais recente. Cada configuração imprime ok quando dá o resultado registrado para o código atual, e FAIL caso contrário. Quando uma regra falha, a saída do TLC, com o caminho mais curto para a falha, é salva como crates/server/tla/<config>.out. O Git ignora esses arquivos.

Configuração	Correções ativadas	Limites	Resultado atual
Fencing.cfg	nenhuma	1 edição, 1 leitura, 2 identificadores, todo comportamento até 18 passos	aprovado, cerca de 2.8M estados, 2 minutos
DesignLeases.cfg	nenhuma	1 edição, 2 identificadores	descoberta 1, segundos
Finding2.cfg	FixRetire	1 edição, 2 identificadores	descoberta 2
Finding3.cfg	FixRetire, FixOrphan	2 edições, 2 identificadores	descoberta 3
Finding4.cfg	+ FixStaleDrop	2 edições, 2 identificadores	descoberta 4, cerca de 1 minuto
AllFixes.cfg	todas as quatro	2 edições, 2 identificadores	aprovado, cerca de 16M estados, 2 minutos

Cada configuração limita a época do armazenamento a 3, e nenhuma inclui falha ou gravação com erro. Uma leitura é uma chamada que carrega o design sem editá-lo, como uma ferramenta de leitura MCP ou o socket do visualizador. O fencing precisa de uma, porque uma cópia obsoleta só pode existir quando duas chamadas carregaram o design. Seu espaço de estados completo com essa leitura não terminou em 30 minutos, então check.sh o executa com aprofundamento iterativo do TLC (-dfid 18): todo comportamento de até 18 passos. A sobrescrição obsoleta mais curta leva 17. As configurações de descoberta exploram tudo dentro de seus limites. O TLC para na primeira regra quebrada, então cada configuração de descoberta ativa as correções propostas para as descobertas anteriores. As constantes Fix* são interruptores hipotéticos. Com todas elas FALSE, o modelo é o código como está hoje.

Leia o resultado

Leia cada resultado com o skill /statechart. Ele transforma o caminho mais curto do TLC para uma regra quebrada em uma lista numerada de passos em palavras simples, e quando uma configuração passa, ele desenha um gráfico de como o design se move entre servidores.

Quando uma configuração imprime FAIL, decida se o bug está no código ou no modelo:

• Um bug real dá um caminho que você pode reproduzir no código. Percorra cada passo, abra a função da tabela e verifique se o código permite aquele passo naquela ordem. Em seguida, relate o caminho nas palavras do código, como as descobertas abaixo fazem. Não enfraqueça uma regra ou um limite até que a verificação passe, e não altere o código do produto a menos que lhe tenham pedido.
• Um erro de modelagem dá um passo que o código não pode executar. Exemplos: dois passos que o código executa sob um mesmo bloqueio (o mutex de estado, o mutex de persistência), separados no modelo; um passo do modelo sem uma guarda que o código tem; ou uma pulsação cardíaca que expira logo após uma renovação. Corrija o modelo para corresponder ao código e diga o que corrigiu.
• Uma falha em Fencing.cfg vem da execução com profundidade limitada, cujo caminho não nomeia seus passos. Para obter um caminho mais curto nomeado, execute a mesma configuração em largura: cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla. Ele para na primeira falha, o que levou cerca de 6 segundos para a falha em "Quando você altera o código coberto propositalmente".
• error significa que o TLC não terminou: um erro de análise sintática, ou uma variável que uma ação deixa sem atribuição. Leia o arquivo .out.

Um FAIL onde o código costumava quebrar a regra e agora passa é uma boa notícia. A tabela de descobertas em "Descobertas conhecidas" mostra como registrá-la.

Quando você altera o código coberto propositalmente

1. Altere o passo do modelo no mesmo commit que o código e mantenha o comentário que nomeia a função.
2. Se sua alteração corrige uma descoberta, coloque a correção no modelo como código, não como um interruptor: exclua a constante Fix*, faça o passo se comportar como o novo código e remova o interruptor de cada configuração. A configuração da próxima descoberta se torna a configuração padrão, e check.sh obtém os novos resultados esperados.
3. Antes de confiar em uma aprovação, quebre o código propositalmente em uma cópia de rascunho, espelhe a quebra no modelo e verifique se a configuração a detecta. Por exemplo, se você remover AND epoch = $3 de PgStore::save e remover x.ptok = store.epoch de SaveWrites, Fencing.cfg quebra StoredEditsStay. Uma verificação que você nunca viu falhar não prova nada.
4. Execute check.sh --full, então avance o commit de sincronização.

Descobertas conhecidas

Cada uma é uma condição de corrida no código em 6606714. Em cada uma, a chamada de ferramenta do agente retorna sucesso e a edição desaparece.

1. Uma edição cai em uma cópia que já está salvando seu último instantâneo. O servidor A tem o design carregado, e uma chamada MCP passou por Hub::open. O servidor B entra e ganha o design (um lease vencido em A também faz isso). O tick de A chama let_go, então retire marca a cópia como Retiring. A tarefa de salvamento take_save pega o último instantâneo. Então a chamada DesignHandle::edit pega o bloqueio e confirma na cópia que está se aposentando, porque edit nunca olha para life. A tarefa de salvamento salva o instantâneo sem a edição, libera o lease e drop_copy limpa pending. B carrega o design sem a edição. Para acionar isso no aplicativo real, as edições já devem estar esperando no bloqueio do design quando o tick for executado, como vários agentes executando grandes chamadas write_html. Desfazer, refazer, importar e atualizações de comentários seguem o mesmo caminho.
2. Uma edição cai em um identificador que o hub já removeu de sua lista. O handle_for de uma chamada retorna um identificador que não está carregado. B entra, e o let_go de A não vê nada carregado, então chama remove. A chamada load reivindica o lease e carrega uma cópia nesse identificador. A lista loaded do próximo tick vem da lista do hub, que não tem mais este identificador. Então o tick libera o lease, e o próximo salvamento da cópia falha com Fenced. Isso não precisa de travamento, apenas de um servidor entrando.
3. O tick descarta uma cópia que foi carregada novamente após o tick lê-la. Um servidor, nenhuma alteração de associação. O tick lê lease() (token 1). Então o design é descarregado e uma chamada o carrega novamente (token 2) e confirma uma edição. O tick lê held() (token 2), vê que 2 ≠ 1, e chama drop_copy. drop_copy encerra a nova cópia, edição pendente e tudo. A janela tem duas leituras de distância, então é estreita, mas ocorre a cada tick.
4. Um servidor que acabou de renovar seu lease atende sua cópia obsoleta. B trava além de seu lease, A assume o design e salva uma edição. B acorda. Seu tick renova a pulsação cardíaca e, a partir desse momento, Members::now conta B como ativo e novamente o proprietário. Mas o loop let_go ainda não foi executado. Uma chamada em B carrega a cópia obsoleta ainda Live e confirma uma edição, que depois falha com Fenced. Precisa primeiro de uma travada.

AllFixes.cfg verifica uma correção proposta para cada descoberta: edit recusa uma cópia que não está Live (1) ou um identificador que não está listado (2). O tick descarta uma cópia apenas se seu token for o que leu (3). Um servidor que renovou após uma expiração se conta como fora até ter liberado (4). Com todas as quatro, AckedEditsStay se mantém nestes limites.

O que isso não cobre

• Um design, dois servidores, edições MCP. Desfazer, refazer, importar, comentários e renomear seguem o mesmo caminho de bloqueio e confirmação, mas não são modelados individualmente. Também não cobre Hub::delete.
• O armazenamento de arquivos e as transferências de FINITE_NODES (hand_off_one, adopt) e o roteador.
• Hub::flush no desligamento, limites de compactação de diário (COMPACT_AFTER, COMPACT_BYTES) e Recent, o buffer por trás da retomada do visualizador.
• Temporização. O TLC tenta toda ordem de passos, então o modelo mostra que uma corrida existe, não com que frequência ela acontece. Ele assume que o próprio temporizador de lease de um servidor (Members::lapsed) expira o mais tardar quando o banco de dados conta sua pulsação cardíaca como expirada. Isso é válido quando os dois relógios rodam na mesma taxa.
• Limites maiores. Mais edições, leituras, identificadores ou épocas, travamentos e gravações com falha não estão nas configurações diárias. AllFixes.cfg também passou com 1 edição, 1 travamento e 1 gravação com falha (3.4M estados). O fencing além de 18 passos não terminou: com 1 edição e 1 leitura passou por 50M estados distintos e ainda estava em andamento. Não confie em uma aprovação de fencing mais antiga sem leitura: apenas uma edição carrega apenas uma cópia, então nada pode ficar obsoleto.