TLA+ per la Verifica Formale: Trovare Bug nei Sistemi Distribuiti Prima di Scrivere una Singola Riga di Codice

Fondamenti di TLA+

TLA+ (Temporal Logic of Actions) è il linguaggio di specifica formale di Leslie Lamport. Non scrivi codice in TLA+ — scrivi un modello matematico del tuo sistema come macchina a stati. Poi esegui il model checker TLC, che esplora esaustivamente ogni possibile stato che il tuo sistema può raggiungere e verifica che i tuoi invarianti valgano in tutti.

L'insight chiave: i bug dei sistemi distribuiti non sono nel codice. Sono nel design. Se il tuo protocollo è sbagliato, nessuna quantità di codice accurato o testing ti salverà. TLA+ trova bug di design prima che tu scriva una singola riga di codice di implementazione.

Una specifica TLA+ minimale:

---- MODULE SimpleCounter ----
EXTENDS Integers

VARIABLE count

Init == count = 0

Increment == count < 10 /\ count' = count + 1

Next == Increment

Spec == Init /\ [][Next]_count

CountInvariant == count >= 0 /\ count <= 10

====

PlusCal: TLA+ per Esseri Umani

TLA+ grezzo è notazione matematica. PlusCal è un linguaggio algoritmico che transpila in TLA+ e si legge più come pseudocodice:

---- MODULE MutualExclusion ----
EXTENDS Integers, TLC

CONSTANT NumProcesses

(*--algorithm mutex
variables
 lock = "free";

process proc \in 1..NumProcesses
variables hasLock = FALSE;
begin
 AcquireLock:
 await lock = "free";
 lock := self;
 hasLock := TRUE;

 CriticalSection:
 skip;

 ReleaseLock:
 lock := "free";
 hasLock := FALSE;

 goto AcquireLock;
end process;
end algorithm; *)

MutualExclusion ==
 \A p1, p2 \in 1..NumProcesses :
 (p1 /= p2) =>
 ~(pc[p1] = "CriticalSection" /\ pc[p2] = "CriticalSection")

====

Esegui TLC con NumProcesses = 3 e esplorerà ogni possibile interleaving dei tre processi. Se due processi possono mai essere nella sezione critica simultaneamente, TLC produce un controesempio.

L'Esempio Reale di Kafka

La seguente specifica ha trovato un bug reale. Modella una versione semplificata del protocollo di ribilanciamento dei consumer group di Kafka:

---- MODULE KafkaRebalance ----
EXTENDS Integers, Sequences, FiniteSets, TLC

CONSTANTS
 Consumers,
 Partitions,
 MaxGenerations

VARIABLES
 groupState,
 generation,
 members,
 leader,
 assignment,
 consumerState,
 pendingJoins,
 pendingSync

vars == <<groupState, generation, members, leader, assignment,
 consumerState, pendingJoins, pendingSync>>

TypeInvariant ==
 /\ groupState \in {"empty", "rebalancing", "stable"}
 /\ generation \in 0..MaxGenerations
 /\ members \subseteq Consumers
 /\ leader \in Consumers \union {"none"}
 /\ \A p \in Partitions : assignment[p] \in Consumers \union {"unassigned"}
 /\ \A c \in Consumers : consumerState[c] \in
 {"idle", "joining", "active", "failed"}

Init ==
 /\ groupState = "empty"
 /\ generation = 0
 /\ members = {}
 /\ leader = "none"
 /\ assignment = [p \in Partitions |-> "unassigned"]
 /\ consumerState = [c \in Consumers |-> "idle"]
 /\ pendingJoins = {}
 /\ pendingSync = {}

\* Un consumer fallisce (crash)
ConsumerFail(c) ==
 /\ consumerState[c] \in {"joining", "active"}
 /\ consumerState' = [consumerState EXCEPT ![c] = "failed"]
 /\ members' = members \ {c}
 \* IL BUG ERA QUI: assignment non veniva pulito immediatamente
 \* Originale (buggato): UNCHANGED <<assignment>>
 \* Fix: pulire gli assignment del consumer fallito
 /\ assignment' = [p \in Partitions |->
 IF assignment[p] = c THEN "unassigned" ELSE assignment[p]]
 /\ IF leader = c
 THEN leader' = IF members' /= {} THEN CHOOSE m \in members' : TRUE
 ELSE "none"
 ELSE UNCHANGED leader
 /\ UNCHANGED <<groupState, generation, pendingJoins, pendingSync>>

\* SAFETY: Nessuna partizione assegnata a un consumer fallito
NoFailedAssignment ==
 \A p \in Partitions :
 assignment[p] /= "unassigned" =>
 consumerState[assignment[p]] /= "failed"

\* SAFETY: Tutti i consumer assegnati sono membri del gruppo
AssignedAreMembers ==
 \A p \in Partitions :
 assignment[p] /= "unassigned" => assignment[p] \in members

====

Il Bug che TLC Ha Trovato

Eseguendo questo con l'originale UNCHANGED <<assignment>> nell'azione ConsumerFail, TLC trova una violazione di NoFailedAssignment in 6 stati:

Error: Invariant NoFailedAssignment is violated.

Error trace:
1: <Init>
 groupState = "empty", generation = 0

2: JoinGroup("c1")
 consumerState["c1"] = "joining"

3: JoinGroup("c2")
 consumerState["c2"] = "joining"

4: TriggerRebalance
 generation = 1, members = {"c1", "c2"}, leader = "c1"

5: LeaderAssign
 assignment = [1 |-> "c1", 2 |-> "c2", 3 |-> "c1", 4 |-> "c2"]

6: ConsumerFail("c2")
 consumerState["c2"] = "failed", members = {"c1"}
 assignment = [1 |-> "c1", 2 |-> "c2", 3 |-> "c1", 4 |-> "c2"]
 ^^^^^^^^^^^^^^^^^^^^^^^^ c2 è failed ma ha ancora le partizioni 2 e 4!

Il fix è ovvio una volta che lo vedi: quando un consumer fallisce, pulire immediatamente le sue assegnazioni di partizione. Ma nell'implementazione reale, la pulizia degli assignment avveniva durante il prossimo ribilanciamento, non al momento del rilevamento del fallimento. Questo significava che c'era una finestra dove un nuovo consumer poteva unirsi, innescare un ribilanciamento, e l'algoritmo di assegnazione del leader poteva vedere l'assegnazione vecchia e prendere decisioni conflittuali.

Questo tipo di finestra può esistere in sistemi di produzione per mesi. TLC la trova in 0,3 secondi.

Eseguire il Model Checker

cat > KafkaRebalance.cfg << 'EOF'
CONSTANTS
 Consumers = {"c1", "c2", "c3"}
 Partitions = {1, 2, 3, 4}
 MaxGenerations = 3

INIT Init
NEXT Next

INVARIANTS
 TypeInvariant
 NoFailedAssignment
 AssignedAreMembers
EOF

java -jar tla2tools.jar -config KafkaRebalance.cfg KafkaRebalance.tla

# Output:
# Model checking completed. No errors found.
# 847.293 states generated, 234.521 distinct states found.
# Finished in 00:00:04 (4 secondi)

847.293 stati. Ogni singolo possibile interleaving di join, fallimenti, ribilanciamenti e assegnazioni del leader con 3 consumer, 4 partizioni e fino a 3 generazioni. Esplorato esaustivamente in 4 secondi. Nessuna randomness, nessun "speriamo di beccare il bug" — certezza matematica che gli invarianti valgono.

Proprietà Temporali: Liveness

Le proprietà di safety ("le cose brutte non succedono mai") trovano molti bug, ma le proprietà di liveness ("le cose buone alla fine succedono") trovano una classe diversa:

\* LIVENESS: Ogni partizione è alla fine assegnata a un consumer attivo
EventuallyAssigned ==
 \A p \in Partitions :
 <>(assignment[p] /= "unassigned" /\
 consumerState[assignment[p]] = "active")

\* LIVENESS: Il gruppo alla fine diventa stabile dopo un ribilanciamento
EventuallyStable ==
 groupState = "rebalancing" ~> groupState = "stable"

L'operatore <> significa "alla fine" (a un certo punto nel futuro). L'operatore ~> significa "porta a" (ogni volta che il lato sinistro è vero, il lato destro è alla fine vero).

Pattern Pratici Riutilizzabili

Modellare Partizioni di Rete

VARIABLE connected

NetworkPartition(n1, n2) ==
 /\ connected' = [connected EXCEPT ![{n1, n2}] = FALSE]
 /\ UNCHANGED <<otherVars>>

SendMessage(from, to, msg) ==
 /\ connected[{from, to}]
 /\ \* ... resto della logica di invio

Modellare Perdita e Riordinamento dei Messaggi

VARIABLE messages \* Insieme di messaggi in volo (disordinato by design)

Send(msg) ==
 /\ messages' = messages \union {msg}

Receive(msg) ==
 /\ msg \in messages
 /\ messages' = messages \ {msg}

LoseMessage(msg) ==
 /\ msg \in messages
 /\ messages' = messages \ {msg}
 /\ UNCHANGED <<otherVars>>

Quando Non Usare TLA+

TLA+ è overkill per la maggior parte del software. Usalo quando:

1. La correttezza è critica e il testing è insufficiente. Protocolli di consenso distribuito, strutture dati lock-free, livelli di isolamento delle transazioni.
2. Lo spazio di interazione è troppo grande per il testing. 5 nodi, ciascuno con 4 stati, 3 tipi di messaggi, fallimento in qualsiasi punto — sono miliardi di interleaving.
3. Il costo di un bug è alto. Corruzione dati, perdita finanziaria, sistemi safety-critical.

Non usarlo per:

• Applicazioni CRUD
• Servizi request-response semplici
• Qualsiasi cosa dove la parte difficile è la UI o la logica di business piuttosto che il protocollo di concorrenza

La curva di apprendimento è reale — circa 3 settimane di studio dedicato per andare da zero a produttivo. Ma dato il track record di TLC nel trovare bug in protocolli che sembravano ovviamente corretti, modellare ogni protocollo distribuito non banale prima dell'implementazione è un investimento solido. La spec di solito richiede 2-3 giorni. Trovare e fixare un bug di concorrenza in produzione richiede 2-3 settimane. La matematica è accessibile.