Teoria Formal & Fundamentação Matemática

1. Modelo Formal de Transações e Histórias de Execução

O ChaosSQL fundamenta sua análise na teoria formal clássica de banco de dados estabelecida por Bernstein, Goodman, Papadimitriou e Adya.

Definição Formal de Transação

Uma transação T_i é definida matematicamente como uma tupla ordenada:

T_i = (O_i, <_i)

Onde:

• O_i é um conjunto finito de operações atômicas de leitura r_i[x], escrita w_i[x], commit c_i ou abort a_i, acessando entidades de dados x ∈ D.
• <_i é uma ordem estrita parcial sobre O_i que reflete o fluxo determinístico do programa da transação.
• Existe exatamente uma operação terminal t_i ∈ {a_i, c_i}, que é o elemento maximal sob <_i.

Definição Formal de História (Schedule)

Uma história de execução concorrente S sobre um conjunto finito de transações T = {T₁, T₂, …, T_n} é uma ordem parcial S = (bigcup_i=1ⁿ O_i, <_S) que satisfaz:

1. bigcup_i=1ⁿ <_i  ⊆  <_S (preserva a ordem interna de instruções de cada transação).
2. Para quaisquer duas operações conflitantes o_i, o_j ∈ S (onde i ≠ j), ou o_i <_S o_j ou o_j <_S o_i.

2. Condições de Conflito de Bernstein & Teorema CSR

Condição de Conflito de Bernstein (1966)

Duas operações o_i, o_j ∈ S pertencentes a transações distintas (i ≠ j) estão em conflito direto se e somente se acessam a mesma entidade de dados x ∈ D e pelo menos uma delas é uma operação de mutação (w):

Conflict(o_i, o_j) ⟺ (target(o_i) = target(o_j) = x)  ∧  (o_i is w  ∨  o_j is w)

Grafo de Serialização Direta (Adya Dependency Graph)

Dado um schedule de execução S, o Grafo de Serialização SG(S) = (V, E) é um dígrafo onde:

• Os vértices V = T correspondem ao conjunto de transações comitadas.
• Existe uma aresta direcionada (T_i → T_j) ∈ E se e somente se existe o_i ∈ T_i e o_j ∈ T_j tais que o_i <_S o_j e Conflict(o_i, o_j).

As Três Relações Fundamentais de Dependência (Atul Adya, 1999)

1. Dependência de Leitura (wr - Read Dependency): T_i  —^wr→  T_j se T_i grava uma versão de x e T_j subsequentemente lê essa mesma versão.
2. Dependência de Sobrescrita (ww - Overwrite Dependency): T_i  —^ww→  T_j se T_i grava uma versão de x e T_j subsequentemente sobrescreve x.
3. Anti-Dependência (rw - Anti-Dependency): T_i  —^rw→  T_j se T_i lê uma versão de x e T_j subsequentemente grava uma nova versão de x, tornando a leitura de T_i desatualizada.

Teorema Fundamental da Serializabilidade por Conflito (CSR)

A presença de qualquer ciclo direcionado (T₁ → T₂ → … → T₁) prova que a execução é semanticamente inconsistente e não possui equivalente serial.

3. Agendamento Probabilístico PCT-SQL (Burckhardt & Musuvathi)

Testes de concorrência ingênuos falham devido à explosão combinatória. Para n transações executando m passos cada, o número de intercalações possíveis Ω cresce fatorialmente:

|Ω| = ((n · m)!)⁄(m!)ⁿ

Para apenas 5 transações de 3 passos, existem 168.168.000 intercalações possíveis. A chance de acertar a troca de contexto exata por pura aleatoriedade é inferior a 10^-6.

Teorema do Limite Inferior de Burckhardt (ASPLOS 2010)

Burckhardt e Musuvathi provaram que, se um bug de concorrência requer uma profundidade de agendamento d (número de restrições de prioridade ou trocas de contexto críticas para disparar), o algoritmo Probabilistic Concurrency Testing (PCT) o encontra em uma única rodada com pelo menos esta probabilidade:

ℙ(Detecção) ≥ 1⁄(n · k^d-1)

Onde n é o número de threads concorrentes e k é o total de passos executados.

Aplicação Prática em Bancos de Dados Relacionais

• Estudos empíricos seminais (Lu et al., ASPLOS) demonstram que ~96% dos bugs de concorrência reais possuem profundidade d = 1 ou d = 2 (Lost Update requer d=1; Write Skew requer d=2).
• Para d = 2, a probabilidade de detecção por execução é ℙ ≥ 1⁄(n · k). Em um teste com 4 workers e 25 passos (n=4, k=25), ℙ ≥ 1⁄100 = 1%.
• Em uma bateria curta de R = 300 rodadas:

ℙ(Encontrar o Bug em R Rodadas) = 1 - (1 - 1⁄100)³⁰⁰ ≈ 1 - e^-3 ≈ 95.02%

4. Minimização com Andreas Zeller Delta-Debugging (ddmin)

Definição Formal de 1-Minimalidade

Seja C = ⟨ op₁, op₂, …, op_N ⟩ a sequência ordenada de operações agendadas que dispara uma falha de invariante test(C) = FAIL.

Uma subsequência C^* ⊆ C é dita 1-Minimal se e somente se:

test(C^*) = FAIL   ∧   ∀ op ∈ C^*: test(C^* ∖ {op}) = PASS

A Implementação do ddmin no ChaosSQL

O ChaosSQL executa cada subsequência candidata contra um banco recém-reinicializado e só a mantém quando ela reproduz a mesma assinatura de falha: status violation na mesma invariante. Um candidato que termina com outro status, como um erro de execução por FOREIGN KEY constraint failed causado pela remoção da operação que criou o registro pai, não conta como reprodução e é descartado.

1. Os replays são memoizados, então uma subsequência já testada nunca é executada duas vezes.
2. Depois que o ddmin converge, uma auditoria final remove cada operação restante uma vez e confirma que a falha desaparece, o que estabelece a 1-minimalidade.
3. O shrinker não calcula dependências de dados entre operações; ele depende da checagem de assinatura para rejeitar candidatos que quebram a integridade referencial.

5. Linearizabilidade e Observações de Caixa-Preta (Elle)

Inspirado na metodologia de Kyle Kingsbury (Jepsen) e Peter Alvaro (VLDB 2020), o ChaosSQL infere anomalias estritamente a partir do histórico observável de operações do cliente (leituras, escritas e retornos). Não há necessidade de instrumentação interna no código fonte do banco de dados, tornando o ChaosSQL universalmente compatível com qualquer motor relacional compatível com SQL.