Recursive Mutexes in Separation Logic

Resumo Técnico: Mutexes Recursivos em Lógica de Separação

Declaração do Problema
Embora a lógica de separação concorrente mecanizada tenha avançado ao ponto de verificar programas do mundo real em linguagens como C++ e Rust usando ferramentas como VST, BRiCk e RustBelt, permanece uma lacuna na verificação formal de bibliotecas de concorrência padrão. Especificamente, os mutexes recursivos (comuns em C++ e Java) carecem de especificações de lógica de separação estabelecidas. Diferente dos mutexes padrão, que um thread não pode adquirir se já os detém, os mutexes recursivos permitem que um único thread adquira o mesmo lock múltiplas vezes. Essa capacidade possibilita padrões de código idiomáticos onde uma função que detém um lock pode chamar com segurança outra função que também tenta adquirir o mesmo lock (por exemplo, transfer chamando update_a na Figura 1). As especificações de mutexes padrão falham em suportar essa transparência e encapsulamento, muitas vezes forçando desenvolvedores a criar funções alternativas sem lock ou a realizar análises de caso complexas sobre a propriedade do lock.

Metodologia
Os autores propõem uma nova especificação de lógica de separação para mutexes recursivos que trata a aquisição e a liberação de lock de forma uniforme, independentemente do estado atual de propriedade do thread chamador. A metodologia introduz dois componentes primários:

1. Handles Fracionários e Predicados Específicos de Thread:

   • Um mutex recursivo $\gamma$ com invariante $P$ é associado a um handle fracionário $\ell \mapsto_q \text{rmutex}(\gamma, P)$.
   • Crucialmente, cada thread $t$ que interage com o mutex possui seu próprio predicado: $\text{holds}(\gamma, t, n, P)$. Aqui, $n$ representa o número de vezes que o thread $t$ adquiriu o mutex.
   • A exclusão mútua é aplicada pela regra de que, se dois threads detêm o mutex, pelo menos um deve ter uma contagem de zero ($n_1 = 0 \lor n_2 = 0$).
   • Para evitar que um único thread realize a "contagem dupla" de recursos, a lógica impõe que um thread não pode deter dois predicados $\text{holds}$ simultaneamente; assim, $\text{holds}(\gamma, t, n_1, P) * \text{holds}(\gamma, t, n_2, P) \vdash \text{False}$.

2. Transições de Estado e Empréstimo (Borrowing):

   • Lock/Unlock: Adquirir o lock incrementa a contagem $n$ do thread ($n \to n+1$), e liberar o lock decrementa $n$ ($n \to n-1$).
   • Regra de Empréstimo (Borrowing Rule): Um thread pode acessar a invariante protegida $P$ se, e somente se, sua contagem $n > 0$. A regra permite que um thread troque $\text{holds}(\gamma, t, n, P)$ (onde $n>0$) pelos recursos reais $P$ mais um retentor $\text{held}(\gamma, t, n)$ que rastreia a contagem, mas não concede acesso a $P$.
   • Tratamento de Argumentos Quantificados: Para abordar problemas onde as invariantes de lock contêm variáveis existencialmente quantificadas (ex: $\exists v. x \mapsto v$), os autores introduzem uma tupla de argumentos $a$ passada ao predicado $\text{holds}$. Isso garante que, quando um thread toma emprestado $P$, ele retém conhecimento específico sobre os recursos (ex: valores específicos de variáveis) em vez de re-quantificar e perder essa informação ao retornar ao estado da invariante.

Principais Contribuições

• Especificação Unificada: O artigo fornece uma especificação que permite aos clientes determinar se detêm o mutex apenas verificando se sua contagem $n$ é maior que zero, sem a necessidade de distinguir entre a primeira aquisição e a aquisição recursiva.
• Raciocínio Idiomático: As especificações permitem provas para padrões de código onde funções chamam outras funções que também adquirem o mesmo lock, espelhando o uso padrão de C++ sem exigir variantes de funções "sem lock".
• Verificação Formal de Concorrência em C++: O trabalho demonstra a aplicação dessas especificações para verificar a biblioteca de concorrência do C++ (especificamente std::recursive_mutex) usando o framework BRiCk.

Resultos
Os autores aplicaram com sucesso essas especificações para verificar o exemplo na Figura 1, onde uma função transfer chama update_a e update_b enquanto detém o mesmo mutex recursivo. A verificação confirma que:

• A função transfer pode reutilizar com segurança update_a, embora ambos adquiram o mesmo mutex.
• A invariante (a soma de balance_a e balance_b) é preservada através da operação.
• A lógica lida corretamente com o estado da invariante, quer o thread detivesse o lock inicialmente ou não, preservando valores específicos de variáveis (como $a$ e $b$) através da pilha de chamadas.

Significância
O artigo afirma que estas especificações tornam o raciocínio sobre mutexes recursivos "mais transparente e melhor encapsulado" do que o uso de mutexes normais. Ao separar as operações de adquirir o lock (incrementar $n$) e tomar emprestado a invariante (acessar $P$ quando $n>0$), a abordagem suporta padrões comuns de engenharia de software encontrados em linguagens mainstream. Este trabalho é apresentado como um passo em direção ao objetivo mais amplo de verificar toda a biblioteca padrão do C++, visando destacar princípios de raciocínio que são práticos para a programação concorrente do mundo real. Os autores observam que suas especificações atuais também cobrem outros componentes da biblioteca padrão, como std::atomic e std::vector.