GitHub user illyar80 edited a discussion: Formal proof of ACK temporal
collision in Shared subscription with TLA+ and chaos cross-validation
## Summary
We independently proved and reproduced the ACK temporal collision in **Apache
Pulsar Shared subscription** — a race condition where a consumer crashes (or
fails to ack in time) after storing a result but before the acknowledgment
reaches the broker, causing the redelivered message to be processed twice.
This is **documented behavior** (Pulsar at-least-once delivery with
`unacked_messages_timeout_ms`), not an implementation bug. Our contribution is:
1. **Formal proof** via TLA+ model checking — exhaustively explores all
interleavings including batch delivery semantics
2. **Chaos cross-validation** via ack timeout + PostgreSQL — confirms the
mathematical prediction in a physical containerized environment
3. **Cross-broker reproduction** — identical scenario reproduced on RabbitMQ,
NATS JetStream, and Kafka, proving it is a fundamental distributed systems
problem
---
## The Scenario
```
Consumer Pulsar DB
| | |
| consume(msg, batch) | |
|<------------------------------| |
| process(msg) | |
| store_result(msg) | |
|---------------------------------------------------------->|
| | |
| *** ACK TIMEOUT *** | |
| (unacked_messages_timeout_ms)| |
| | |
| | redeliver(msg) |
|<------------------------------| |
| process(msg) AGAIN | |
| store_result(msg) | *** DOUBLE *** |
|---------------------------------------------------------->|
```
## Pulsar-Specific Details
Pulsar Shared subscription differs from Kafka (offset commit) and NATS
(AckWait) in two important ways:
1. **Batch delivery**: Pulsar delivers messages in batches. The crash window is
between `Process` (individual message within a batch) and `SendAck`
(batch-level acknowledgment). If the consumer crashes after processing one
message but before acknowledging the batch, the **entire batch is redelivered**
— including already-acked messages that lose their ack state.
2. **Ack timeout, not docker kill**: Pulsar does not redeliver messages on
connection drop in Shared subscription (the broker waits for consumer
reconnection). Redelivery is triggered by `unacked_messages_timeout_ms` — a
consumer-side timeout that must be shorter than the processing delay. We used
`ACK_TIMEOUT_MS=11000` with `PROCESSING_TIME_MS=15000`.
## Formal Proof (TLA+)
We modeled the system as a TLA+ specification with the following actions:
- `DeliverBatch` — broker delivers a batch of messages
- `Process` — consumer processes one message and stores the result
- `AckTimeout` — broker detects unacked messages after timeout
- `RedeliverBatch` — broker redelivers the unacked batch
- `SkipRedeliver` — idempotent guard detects already-executed messages
**Results:**
| Mode | States | Depth | Result |
|------|--------|-------|--------|
| Faulty | 21 | 4 | **VIOLATED** — `InvariantNoDoubleExecution` fails |
| Idempotent (with `db[id]==0` guard) | 386 | 12 | **PASS** — no
counterexamples anywhere |
## Chaos Cross-Validation
We built a pilot (`pilot_pulsar/`) that:
1. Starts Pulsar (standalone), PostgreSQL, and a Python consumer via Docker
Compose
2. Configures the consumer with `unacked_messages_timeout_ms=11000` and
`PROCESSING_TIME_MS=15000`
3. Publishes a single message
4. Consumer stores the result, then sleeps 15s (simulating work)
5. After 11s, Pulsar's `UnAckedMessageTracker` fires — redelivers the message
6. Consumer receives the duplicate, and (in faulty mode) stores it again
7. Counts DB rows
**Results:**
| Mode | Chaos Executions | Verdict |
|------|-----------------|---------|
| Faulty | **2** DB rows | COLLISION confirmed |
| Idempotent | **1** DB row | Guard works |
## Cross-Broker Validation
We adapted the same TLA+ model and chaos pilot for **RabbitMQ, NATS JetStream,
and Kafka**. All results match:
| Broker | Mode | TLC States | TLC Depth | TLC Result | Chaos Result |
|--------|------|-----------|-----------|------------|-------------|
| **Pulsar** | Faulty | 21 | 4 | **VIOLATED** | 2 executions |
| **Pulsar** | Idempotent | 386 | 12 | **PASS** | 1 execution |
| RabbitMQ | Faulty | 108 | 7 | **VIOLATED** | 2 executions |
| RabbitMQ | Idempotent | 277 | 11 | **PASS** | 1 execution |
| NATS JetStream | Faulty | 47 | 6 | **VIOLATED** | 2 executions |
| NATS JetStream | Idempotent | 105 | 9 | **PASS** | 1 execution |
| Kafka | Faulty | 47 | 6 | **VIOLATED** | 2 executions |
| Kafka | Idempotent | 105 | 9 | **PASS** | 1 execution |
**Verdict:** 8/8 TLC predictions matched 8/8 chaos experiments across 4 brokers.
## The Fix
The recommended consumer-side fix is the **idempotent consumer pattern**:
```python
consumer = client.subscribe(
topic='persistent://public/default/test-topic',
subscription_name='test-sub',
subscription_type=SubscriptionType.Shared,
unacked_messages_timeout_ms=11000, # must be < processing time
)
while True:
msg = consumer.receive()
# Idempotent guard: check before processing
if should_skip(int(msg.data().decode())):
consumer.acknowledge(msg)
continue
store_result(int(msg.data().decode())) # INSERT into DB
time.sleep(15000) # simulate work (must be > ack timeout)
consumer.acknowledge(msg)
```
The key insight: the `unacked_messages_timeout_ms` must be **shorter than the
processing delay** (Pulsar ignores values ≤ 10s), so redelivery happens while
the consumer is still alive.
## Discussion
We would love feedback from the Pulsar team and community:
- Are there any Pulsar-specific configurations (e.g., `ackTimeoutMillis`,
`acknowledgementGroupTime`) that could narrow the crash window at the broker
level?
- Does Pulsar's Key_Shared subscription eliminate this class of collisions, or
does the same fundamental issue apply?
GitHub link: https://github.com/apache/pulsar/discussions/26181
----
This is an automatically sent email for [email protected].
To unsubscribe, please send an email to: [email protected]
