Performance¶

The timing-sensitive settings in VeriLib are few but interlocking. Getting one wrong usually shows up as a job that "disappears" rather than an error, so it is worth understanding how they relate.

The timeout chain¶

A single atomize job passes through four independent time limits:

EventBridge (1 min)  →  autoscaler reaction
        RabbitMQ consumer_timeout   ─┐
                CLI_TIMEOUT (4800s) ─┤ probe subprocess must finish inside both
                    retry TTL (50s)  ┘ delay before a failed message returns

Setting	Default	What it bounds
`CLI_TIMEOUT`	`4800` (80 min)	The probe subprocess
RabbitMQ `consumer_timeout`	broker config	How long a consumer may hold an unacked message
Retry queue `x-message-ttl`	`50000` ms	How long a transiently-failed message waits before redelivery
`RABBITMQ_HEARTBEAT`	`60`	Connection liveness
`LAMBDA_SCHEDULE_RATE`	`1 minute`	Autoscaling metric resolution

CLI_TIMEOUT must stay ≤ the broker's consumer_timeout

If a probe runs longer than consumer_timeout, RabbitMQ closes the channel while the worker is still working. The worker finishes, tries to ack a message on a dead channel, and the broker redelivers the job to another consumer — which repeats the same expensive probe run.

The symptom is a job that appears to run forever and burns capacity, with no error message. When raising CLI_TIMEOUT for slow projects, raise consumer_timeout first.

Concurrency model¶

Throughput comes from more workers, not more in-flight messages per worker.

RABBITMQ_PREFETCH=1 is deliberate: with prefetch > 1, a consumer that grabs several long probe jobs blocks them all behind the first, while sibling consumers sit idle. One message per consumer keeps the queue as the scheduler.

Knob	Effect
`ATOMIZE_MIN_TASKS` / `MAX_TASKS`	Real concurrency
`RABBITMQ_PREFETCH`	Leave at `1`
`MAX_WORKERS`	Legacy poll mode only — the thread pool in `main.py`. Not used by queue workers.

See Scalability.

Where time actually goes¶

Phase	Cost driver
Clone	`--depth 1`, so repo size not history. Sparse `--filter=tree:0` clone when the URL names a subfolder.
S3 mirror	File count more than total bytes; `S3_MAX_CONCURRENCY` defaults to `8`.
Probe extract	Dominant cost. A Verus or Lean run over a large crate is minutes to tens of minutes.
Parse + persist	Proportional to atom count; a write burst on MySQL. Because MySQL is a managed RDS instance reached over the network, statement count matters as much as instance size here.

The livelog stream carries duration_seconds per step, so per-phase timing is observable per job without extra instrumentation — see Message contracts.

Retry timing¶

A transient failure costs at least 50 seconds before the message is retried, and that hop is invisible on the response queue. With ATOMIZE_MAX_RETRIES=5, a message can spend over four minutes cycling before a permanent error is published.

When diagnosing "nothing happened", check the depth of <queue>_retry_queue before concluding the message was lost.

Frontend¶

Setting	Effect
`MODE=production`	Enables asset fingerprinting; hashed bundles become long-cacheable
`USE_NEW_UI_TOOLS=1`	Serves bundled Gulp output from `public/assets/dist/` instead of unbundled legacy files
`SHOW_ERRORS` / `DEBUG_MODE`	Must be off in production

React assets are built in CI and swapped in atomically, so a deploy does not serve a half-updated asset directory. See React rewrite.

Unknowns

There is no published latency budget, no APM integration documented, and no load-test results in any repo. The numbers above are limits and defaults, not measured performance.