Resumo Técnico: Um Framework de Datalog para Tipos de Dados Replicados Livres de Conflitos

Declaração do Problema

Aplicações distribuídas dependem cada vez mais de colaboração local-first, permitindo que múltiplos usuários atualizem dados compartilhados concorrentemente sem coordenação global. Embora os Tipos de Dados Replicados Livres de Conflitos (CRDTs) forneçam um mecanismo para convergência determinística e Consistência Eventual Forte (SEC), construir aplicações complexas a partir deles permanece um desafio. Desenvolvedores frequentemente compõem múltiplos CRDTs básicos (ex: conjuntos, mapas, sequências) para alcançar comportamentos mais ricos. No entanto, as políticas de resolução de conflitos não se compõem de forma previsível; padrões de concorrência sutis podem fazer com que CRDTs compostos convirjam para estados que violam a semântica pretendida da aplicação.

Atualmente, há uma falta de especificações explícitas e analisáveis que expliquem por que um determinado resultado concorrente surge. Desenvolvedores lutam para verificar se uma composição específica de CRDT atende fielmente à lógica pretendida da aplicação, particularmente ao lidar com invariantes como a ausência de arestas pendentes em grafos colaborativos. A verificação formal é frequentemente muito custosa e de nível especialista, enquanto testes ad-hoc podem perder casos de borda de concorrência complexos.

Metodologia

Os autores propõem o CRDTLog, um framework declarativo implementado em Datalog (especificamente usando o motor Soufflé) para especificar, prototipar e analisar a semântica de CRDTs. A metodologia central envolve a modelagem da semântica de CRDT como programas de lógica executáveis sobre contextos de operação.

1. Contextos de Operação

O framework adota e generaliza o modelo de tipos de dados replicados de Burckhardt. Um contexto de operação $C = (E, op, vis, ar)$ é definido como um grafo de eventos finito onde:

• $E$ é um conjunto de eventos.
• $op$ mapeia eventos para conjuntos de operações (permitindo a execução atômica de múltiplas operações por evento).
• $vis$ é uma relação de visibilidade acíclica (acontece-antes).
• $ar$ é uma ordem de arbitragem total (usada apenas quando a semântica exige, ex: o último escritor vence/last-writer-wins).

Um tipo de dado replicado $F_X$ é uma função determinística que mapeia uma operação e um contexto para um valor de retorno. Em Datalog, esses contextos são codificados como relações de entrada (setEvent, vis, ar), e o estado resultante é derivado como relações de saída.

2. Fluxo de Trabalho de Especificação

O framework suporta um fluxo de trabalho de duas camadas para desenvolvedores:

• Semântica de Nível de Especificação (SLS): Uma definição declarativa de alto nível do comportamento pretendido da aplicação, independente de qualquer design específico de CRDT. Isso é escrito diretamente em regras Datalog sobre o contexto de operação.
• Semântica Composicional de Nível de Implementação (ICS): Uma realização da aplicação usando uma composição de CRDTs básicos ou aninhados. Isso envolve a definição de regras de transformação que mapeiam operações de nível de aplicação para operações de nível de componente.

O framework permite o teste baseado em propriedades: dados um conjunto de execuções concorrentes geradas (contextos de operação), o sistema verifica se o ICS converge para o mesmo estado que o SLS. Se eles divergirem, a decomposição é revisada.

3. Lidando com CRDTs Aninhados e Compostos

O framework suporta:

• CRDTs Aninhados: Como Map⟨Set⟩. Como motores Datalog como o Soufflé não suportam instanciação dinâmica de módulos, o framework codifica estruturas aninhadas usando conjuntos indexados onde a chave atua como um discriminador de escopo.
• CRDTs Compostos: Aplicações complexas (ex: grafos colaborativos) são modeladas pela decomposição em CRDTs mais simples (ex: um Conjunto para nós e um Mapa para arestas) e pela definição de regras de transformação que lidam com a indução de conflitos (ex: garantir que uma adição de aresta vença uma remoção de nó concorrente).

Principais Contribuições

1. Framework Declarativo: Um framework estendido para especificar semânticas de CRdt e de aplicações colaborativas baseadas em contextos de operação, implementado em Datalog.
2. Implementação CRDTLog: Um sistema construído sobre o Soufflé que fornece uma biblioteca de especificações para CRDTs básicos, aninhados e compostos, juntamente com ferramentas para gerar contextos de operação e comparar resultados semânticos.
3. Estudo de Caso sobre Grafos Colaborativos: Uma análise detalhada de duas variantes de grafos:
   • Isolate-Delete (ID): Nós só podem ser removidos se estiverem isolados.
   • Detach-Delete (DD): Remover um nó remove todas as arestas incidentes.
     O estudo demonstra como o framework expõe comportamentos de concorrência não óbvios, como o modo como uma decomposição ingênua de um grafo DD usando Map⟨Set⟩ pode levar a arestas pendentes devido às semânticas de conflito de "vitória da atualização", exigindo uma estratégia de transformação específica (usando um conjunto plano de tuplas de aresta) para satisfazer a invariante.
4. Avaliação Empírica: Uma avaliação sistemática da equivalência semântica entre especificações abstratas e realizações compostas, juntamente com benchmarks de escalabilidade.

Resultados Experimentais

Os autores avaliaram o framework usando teste baseado em propriedades nas aplicações de grafos ID e DD:

• Equivalência Semântica (RQ1): Através de 1.000 execuções independentes para oito configurações diferentes (variando réplicas e contagens de eventos), o ICS e o SLS produziram estados observáveis idênticos, validando a correção das composições de CRDT.
• Escalabilidade:
  • Tamanho do Grafo: À medida que o número de nós e arestas aumentava, a implementação ICS tornava-se significativamente mais rápida que a SLS (até uma ordem de magnitude para grafos grandes), pois a decomposição reduz a complexidade das regras e o tamanho dos joins.
  • Concorrência: O aumento no número de réplicas (de 2 para 16) teve apenas um impacto modesto no tempo de execução, pois afeta primariamente a estrutura da relação de visibilidade, não a complexidade de avaliação de regras.
  • Volume de Eventos: O custo de avaliação escala principalmente com o número de eventos no contexto de operação.
• Incrementalidade: Quando instanciado com o DDlog (um motor Datalog incremental), o framework suportou verificação interativa, passo a passo. Embora mais lento que o Soufflé para processamento em lote, permaneceu prático para contextos de pequeno a médio porte adequados para design exploratório.

Significância e Alegações

O artigo afirma ser o primeiro trabalho a usar sistematicamente o Datalog como base para prototipar e analisar CRDTs complexos e suas composições.

A significância reside na mudança do foco da verificação da correção de CRDTs individuais (como feito em trabalhos como o Peepul) para a verificação de semânticas de nível de aplicação através de composições. Ao tornar os desajustes semânticos entre o comportamento pretendido e as composições de CRDT explícitos, executáveis e falsificáveis, o framework permite que desenvolvedores:

• Explorem alternativas de decomposição de CRDT antes de se comprometerem com uma implementação distribuída.
• Testem sistematicamente casos de borda em interações concorrentes.
• Isolem o núcleo semântico da resolução de conflitos das escolhas de protocolo e engenharia.

Os autores mantêm uma postura modesta, observando que, embora seu protótipo use Soufflé, a abordagem depende de recursos padrão de Datalog (recursão, negação estratificada, agregados) disponíveis em muitos motores. Eles reconhecem que a verificação formal de aplicações distribuídas permanece de nível especialista e que seu trabalho fornece uma alternativa de teste sistemático e leve durante a fase de design. O trabalho futuro inclui a formalização do CRDTLog em um provador de teoremas para provas verificadas por máquina.