Ultra-low-latency trading systems demand runtime verification (RV) that is both expressive and fast, with processing budgets measured in hundreds of nanoseconds. We present ChronosRV, a framework that compiles specifications written in a bounded fragment of Metric Temporal Logic (MTL) extended with a SERE-style (regular sequence) subset and lightweight aggregations, into highly optimized C++ monitors integrated in a zero-copy, lock-free, NUMA-aware event engine. We formalize a discrete-time, three-valued prefix semantics that supports bounded memory and robust verdicts in the presence of bounded out-of-order (OOO) arrivals via watermarks. Our synthesis pipeline maps logic to an operator network of bounded timers, counters, and small DFAs, with per-key sharding to exploit data parallelism. On synthetic workloads reflecting equity trading pipelines, ChronosRV sustains >1–4M events/s with median per-event processing in the sub-microsecond range, and detects injected violations with high accuracy under bounded OOO jitter. We provide a proof sketch of soundness and bounded completeness under watermarking, and report detailed ablations for property complexity, sharding, and OOO robustness.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

ChronosRV: Online Runtime Monitoring and Code Generation for Bounded Temporal Specifications in Low-Latency C++ Trading Systems

  • Pengfei Qiu,
  • Jun Zhang,
  • Weiguo Song

摘要

Ultra-low-latency trading systems demand runtime verification (RV) that is both expressive and fast, with processing budgets measured in hundreds of nanoseconds. We present ChronosRV, a framework that compiles specifications written in a bounded fragment of Metric Temporal Logic (MTL) extended with a SERE-style (regular sequence) subset and lightweight aggregations, into highly optimized C++ monitors integrated in a zero-copy, lock-free, NUMA-aware event engine. We formalize a discrete-time, three-valued prefix semantics that supports bounded memory and robust verdicts in the presence of bounded out-of-order (OOO) arrivals via watermarks. Our synthesis pipeline maps logic to an operator network of bounded timers, counters, and small DFAs, with per-key sharding to exploit data parallelism. On synthetic workloads reflecting equity trading pipelines, ChronosRV sustains >1–4M events/s with median per-event processing in the sub-microsecond range, and detects injected violations with high accuracy under bounded OOO jitter. We provide a proof sketch of soundness and bounded completeness under watermarking, and report detailed ablations for property complexity, sharding, and OOO robustness.