[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Temporal collisions in at-least-once message brokers — formal verification with TLA+ templates
Hi everyone,
I'd like to share a project I've been working on that uses TLA+ to detect a specific class of bugs in distributed message brokers.
The problem: In systems with at-least-once delivery (Kafka, RabbitMQ, NATS JetStream, Pulsar), there's a temporal collision window between storing a result and committing the offset/ack. If a consumer crashes in this window, the message is redelivered and the result is executed twice. This is well-known in practice but rarely formalized.
The approach: I built a toolchain that generates TLA+ specifications from parameterized YAML configurations. The key insight is that the crash window follows a repeatable pattern across brokers — the protocol is the same, only the variable names change. So instead of writing TLA+ from scratch for each broker, I use templates with placeholders:
- Kafka: offset, topic, partition → Process, StoreResult, CommitOffset
- NATS: stream, seqno → Process, StoreResult, SendAck
- RabbitMQ: taskState, deliveryTag → Process, StoreResult, AckMessage
- Pulsar: batchId, cursor → Process, StoreResult, CommitCursor
Each template models 4 modes: faulty (crash window), idempotent (dedup guard), two-phase async (split commit), and firefly (pulse-coupled sync).
Results: 16 templates verified by TLC, ~14k total states explored in ~14s. One negative finding: pulse-coupled synchronization (firefly mode) does NOT eliminate the crash window — the gap between StoreResult and CommitOffset exists regardless of commit timing.
I also built chaos cross-validation: Docker fault injection confirms TLC's predictions by injecting the exact crash timing the model predicts.
Code: Currently private, but I'm preparing it for release.
I haven't seen this specific pattern (temporal collisions in at-least-once brokers) discussed on this list. Has anyone here formalized similar consumer offset timing issues? I'd be curious to hear how others model the commit window.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/fd4a721a-5050-406b-8de6-cf20bf8b5f6bn%40googlegroups.com.