Formal proof of ACK temporal collision in Shared subscription with TLA+ and chaos cross-validation

[illyar80]

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:

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?