PaperlayerView exact revision on arXiv

Source-linked AI summary

Formal Reasoning about Performance Models

Moussa Labbadi, Rupak Majumdar, V. R. Sathiyanarayana, Sadegh Soudjani

arXiv:2609.37728v1cs.LOcs.PFcs.PL

TL;DR

Performance reasoning for discrete-event systems lacks a sound and complete logical foundation. The paper defines a calculus and proof rules for reachability and expected reaching time, then demonstrates proofs for server systems and a routing protocol. The rules cover cases beyond analytic queueing solutions and formally establish almost-sure synchronization in the protocol.

  • Problem

    Performance properties of discrete-event systems are typically assessed through repeated simulation and statistical estimation, without a sound and complete proof system for such systems.

    Source: §1 · pp. 1–2

  • Method

    The paper formalizes discrete-event systems with a calculus for event scheduling and continuous sampling, then develops proof rules for almost-sure reachability and expected reaching time.

    Source: §1 · p. 2, §3.1 · p. 5

  • Results

    The rules prove almost-sure reachability and expected reaching time, including queue-clearance properties in client–server models and almost-sure synchronization in a routing protocol.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The framework supports formal performance analysis of discrete-event models beyond analytically tractable queueing cases and establishes a formal synchronization result for a routing protocol.

    Source: §1 · p. 2

    The routing synchronization certificate assumes small jitter, Tr < Tc/2; the large-jitter case is left for future work.

    Source: §5.3 · p. 22

Abstract

from arXiv · show

Discrete-event simulation is a standard technique for modelling and analysing the performance of computer systems, networks, and services. Although simulation tools are widely used, reasoning about the correctness and performance guarantees of the models they implement remains largely ad hoc: simulation outputs are interpreted statistically, but there is no logical foundation for deductive reasoning about their behaviour. We present a core imperative calculus that captures the essential constructs common to discrete-event simulators: asynchronous execution, continuous and discrete sampling from distributions, and time-based event scheduling through a global event queue. On top of this calculus, we develop a proof system for reasoning about almost-sure reachability and expected reaching time properties. Our main result is a sound and complete proof rule for these properties. Our framework generalizes deductive reasoning for discrete-time probabilistic programs to the setting of performance models, in which continuous time and continuous probability distributions are central. We have implemented the proof rules in a tool embedded in Lean. We demonstrate the applicability of our proof rule by deriving proofs of almost-sure reachability and expected reaching time for a number of case studies, including client-server examples that go beyond analytic solutions from queueing theory as well as convergence behaviours in network routing protocols. Establishing the soundness and completeness of our proof rules requires significantly more complex arguments than in the discrete-time setting. This is due to the fundamentally discontinuous nature of the operational semantics and the measure-theoretic challenges of continuous time and probability distributions.

1 Introduction

The introduction addresses the lack of a sound and complete logical framework for performance reasoning about discrete-event systems. It presents a calculus and proof rules for reachability and expected reaching time, mechanized in Lean and applied to server and routing models.

1 Introduction

  • The proof rules address a gap left by existing logics, which do not jointly handle event-driven scheduling and continuous-time events.Discrete-event systems can have uncountable state spaces and successors, and their dynamics need not satisfy the weak Feller assumption used by some stability techniques.Source: §1 · pp. 1–2
  • The framework provides sound and complete proof rules for almost-sure reachability and expected reaching time in discrete-event systems.The reachability rule uses drift and variant functions; the expected-time rule uses a supermartingale that dominates the hitting time.Source: §1 · p. 2
  • Completeness requires new topological arguments, including petite-set properties and Egorov’s theorem.The introduction attributes this difficulty to uncountable state and non-continuous dynamics.Source: §1 · p. 2
  • The case studies include a routing protocol whose distributed nodes synchronize almost surely despite jitter intended to prevent synchronization.The paper presents this as the first formal proof of the protocol’s synchronization and reports that its models include cases beyond closed-form queueing solutions.Source: §1 · p. 2
  • A discrete-event calculus models asynchronous procedures, probabilistic choice, continuous sampling, continuous-time evolution, and time-based scheduling.Its operational semantics model interaction with a global event scheduler and produce Markov processes.Source: §1 · p. 3
  • Leonides, embedded in Lean, mechanizes the semantics and proof-system soundness and provides tactics for proving the target properties.The introduction reports proofs for performance models of server systems and network routing protocols.Source: §1 · p. 3

2 Reasoning about Discrete Event Simulation Models

This section explains how DES models discrete-event execution and illustrates its reasoning rules with a client–server queue. Under λ < μ, the rules establish almost-sure queue clearance and finite expected backlog-clearing time.

2 Reasoning about Discrete Event Simulation Models

  • DES executes procedures atomically in logical zero time and uses a global event queue to run the earliest scheduled event, advancing global time to that event.The client schedules requests after exponentially distributed delays, while service times are independently exponentially distributed.Source: §2 · p. 3
  • The client–server example is an infinite-state model with an unbounded request queue and captures imperative computation, asynchronous invocation, real-time evolution, and probabilistic choice.The model encodes an M/M/1 queue.Source: §2 · pp. 3–4
  • Under λ < μ, the client–server queue empties almost surely, and a supermartingale upper-bounds the expected time until it first becomes empty.The queue size serves as both the drift and variant candidate because it drifts toward zero and is more likely to shrink at each event.Source: §2 · p. 4
  • The approach can prove similar performance properties when added features such as throttling, retries, or exponential backoff leave closed-form queueing solutions unavailable.The passage contrasts these cases with bounds derivable by classical queueing theory.Source: §2 · p. 4

3 The DES Language

DES is a core imperative language for discrete-event systems, combining probabilistic commands with asynchronous, time-based scheduling. Its operational semantics assigns distributions to configurations and induces a discrete-time Markov process.

3.1 Syntax

  • DES procedures use real-valued variables and imperative control, with ⊕p for discrete choice and ∼ for continuous sampling; event-queue posts can simulate loops.The language has no while construct, but loops can be simulated by posting a continuation with delay 0.Source: §3.1 · p. 5
  • The post command schedules a procedure with arguments at the current time plus a sampled nonnegative delay, while now() and peek() expose current and next-event times.The event queue executes the procedure with the earliest scheduled time; zero-delay posts can continue a loop.Source: §3.1 · p. 5

3.2 Markov Processes as Operational Semantics

  • Execution alternates between procedure-body steps and scheduler dequeues, which select the pending event with the least scheduled time and identifier.The scheduler advances time to the selected event’s timestamp before executing its procedure.Source: §3.2 · p. 6
  • Each procedure is loop-free and terminates; configurations with skip and an empty queue are terminal.A DES step compiles the small steps of a procedure command into a single transition to a skip command.Source: §3.2 · pp. 6, 8
  • A post samples a delay, creates a fresh event identifier, and probabilistically enqueues exactly one event with the resulting scheduled time and arguments.The fresh identifier provides deterministic tie-breaking among events with equal timestamps.Source: §3.2 · p. 7
  • DES operational semantics assigns a probability measure over configurations to each step, inducing a discrete-time Markov process over configuration traces.Terminal configurations transition to themselves in the induced process.Source: §3.2 · p. 8

4 Almost-Sure Reachability and Expected Reach Time for DES

This section develops sound and complete proof rules for almost-sure reachability and expected reach time in DES, using invariants, supermartingales, variants, and procedure-specific witnesses for Markov processes and compositional verification. It extends the reasoning to exponential rate-based event sources and shows how the M/M/1 queue’s certificate depends on their representation.

4 Almost-Sure Reachability and Expected Reach Time for DES

  • DES reach time is the expected DES timestamp at the first goal configuration, not the expected number of Markov-process steps to reach the goal.Time is part of each DES configuration and therefore is subsumed into the Markov-process state.Source: §4 · p. 9

4.1 Proof Rules for Almost-Sure Reachability: Overview

  • The proof strategy first establishes sound and complete reachability rules for general Markov processes, then gives a compositional rule for DES procedures.The general-process result must handle DES semantics that do not satisfy continuity assumptions imposed by existing results.Source: §4.1 · p. 9

4.2 Proof Rules for Almost-Sure Reachability: Markov Processes

  • Rule 4.1 uses an invariant, an exempt set, a supermartingale, and a variant with assistant functions as certificates for almost-sure reachability.The supermartingale controls progress across its sublevel sets, while the variant is bounded on those sets and decreases with positive probability bounded away from zero within each of its own sublevel sets.Source: §4.1 · p. 10, §4.2 · p. 10

4.3 Almost-Sure Reachability: Proof Rule for DES

  • The DES rule replaces global certificates with supermartingales and variants for each procedure, using dequeue witnesses to compare successive procedure certificates.Theorem 4 establishes soundness and completeness by translating certificates between the DES rule and the rule for its associated Markov process.Source: §4.3 · pp. 13–14
  • The cited theorems establish that Rule 4.2 and Rule 4.1 are each sound and complete, with Theorem 4 covering Rule 4.2 and Theorem 2 covering Rule 4.1.Source: §4.2 · p. 10, §4.3 · p. 14
  • To bound expected DES reach time, the rule first requires almost-sure reachability and then a procedure-specific supermartingale bounding expected time to the goal.The expected-time witnesses include a dequeue witness formed from the relevant procedure witness.Source: §4.3 · p. 15
  • Completeness of Rule 4.1 implies completeness of Rule 4.2.Source: §4.3 · p. 15

4.4 Bounding the Expected Reach Time

  • Expected reach time measures the global clock at the first goal configuration, not the number of steps to the goal.A system can have infinite expected hitting steps yet reach its goal at expected logical time zero if infinitely many steps occur at the same timestep.Source: §4.4 · pp. 15–16
  • Rule 4.3 for bounding expected reach time in DES is sound and complete.It uses a supermartingale that dominates the clock at goal configurations; its soundness requires Rule 4.2 because failure to reach the goal almost surely makes the true expected reach time infinite.Source: §4.4 · pp. 15–16

4.5 Exponential Distributions and Rate-Based Event Sources

  • The post_rate primitive represents exponential-rate sources by compiling them into a global source set and a tick procedure that runs an exponential race.Tick samples an aggregate rate and selects a source proportionally to its rate; when several rate sources compete, only the winner is inserted into the event queue.Source: Figure 7 · p. 17, §4.5 · p. 18
  • Using the compiled transition kernel, sound and complete reachability and expected-reach-time rules also apply to programs using post_rate.The kernel sequences tick after each step, so rate-based sources compete with queued events when selecting the next procedure.Source: §4.5 · p. 18
  • When λ≤μ, the post_rate M/M/1 model makes V=U=n a certificate, because arrivals and service completions race with probabilities λ/(λ+μ) and μ/(λ+μ).In ordinary DES, queue length alone is not a supermartingale; for λ<μ, the certificate depends on time and procedure phase, while at λ=μ the supermartingale has no simple closed form.Source: §4.5 · pp. 17, 19

5 Implementation and Case Studies

Leonides mechanizes the DES calculus and proof rules in Lean and applies them to client-server models and a routing protocol. The case studies establish queue reachability under stated stability conditions and almost-sure synchronization in the protocol's small-jitter regime.

5.1 Mechanization in Lean

  • Leonides mechanizes the DES calculus and proof rules in Lean, emitting proof obligations that its flauto tactic can discharge, though some system-specific lemmas may be needed.The completed development has no sorry and depends only on Lean's standard classical axioms.Source: §5.1 · p. 19

5.2 Benchmarks: Variations on Client-Server Systems

  • The Basic M/M/1 queue and its feedback variation use V = U = n; the basic queue drains at rate μ−λ, while feedback slightly lowers the variant's descent probability.Feedback re-enqueues a completed request with probability p.Source: §5.2 · p. 19
  • The client-server variations use distinct certificates: priority queues weight levels to order descent, while series servers require a quadratic supermartingale and an upstream-first variant.For k servers in series, the diagonal quadratic form requires λ < μ1 < ··· < μk; cross terms cover the stable region λ < μi.Source: §5.2 · p. 20
  • The timeout-and-retry model tracks queued copies, remaining retry budget, and pending deadlines; its paired witnesses certify reachability and finite expected time when λ(1 + R) < μ.Retries can leave duplicate request copies in the queue, and the certificate adds a phase term for the imminent timeout.Source: §5.2 · p. 20

5.3 Case Study: Almost Sure Synchronization of Routing Protocols

  • The routing case models periodic messages without the time-distance assumptions used in Floyd and Jacobson's discrete-time Markov model, and assumes small jitter Tr < Tc/2 for its synchronization certificate.The model's routers cannot send and receive simultaneously, and pending reads are handled before a router resets its timer.Source: §5.3 · pp. 21–22

5.3.1 Certifying Synchronization.

  • The synchronization certificate uses per-procedure supermartingales for inter-router time distance and variants that descend by Tr/8 with probability at least 1/4, proving synchronization almost surely.The certificate handles the synchronized and collision states with a bounded deterministic dispatch sequence; its stated result is for the small-jitter regime.Source: §5.3.1 · pp. 23–24

6 Related Work

Prior probabilistic program logics and stochastic-system verification frameworks address important termination or quantitative-analysis problems, but the cited approaches do not provide sound and complete reasoning for general event-driven DES performance properties. The paper situates its certificates among ranking, drift, and barrier methods.

Probabilistic program reasoning

  • Probabilistic program logics provide ranking-supermartingale, stochastic-invariant, and Hoare-style termination reasoning, but address untimed programs rather than continuous time, event scheduling, or timed performance properties [9] [64] [49].The cited work also includes supermartingale-based rules for almost-sure and quantitative termination [34].Source: §6 · p. 24

DES and performance modeling

  • Simulation frameworks typically assess performance empirically, while PEPA and Modest support quantitative analysis of abstract finite-state models and queueing theory treats idealized fixed stochastic structures [59].Probabilistic model checking and PCTL/CSL target finite-state Markov chains and decision processes.Source: §6 · p. 25

Certificates for stochastic systems

  • The framework combines ranking-supermartingale and variant certificates with classical drift conditions; prior barrier-certificate converse results are comparatively rare or rely on restrictive assumptions [43, 47, 49] [3] [42] [63].The passage also notes that synthesis approaches for linear systems can use linear matrix inequalities, while polynomial dynamics can use polynomial or SOS optimization [39] [40].Source: §6 · p. 25
  • Continuous-time certification remains relatively underexplored, and the cited sampling-based and neural-certificate approaches do not establish completeness; this work offers explicit drift/variant certificates for DES and continuous-time stochastic systems [7] [53].The paper describes its framework as bridging Markov-chain drift conditions with variant-based progress reasoning.Source: §6 · p. 25

7 Conclusion

The paper presents a deductive verification framework for performance models expressed in an expressive DES language. Its proof rules are sound and complete, and Leonides semi-automatically discharges obligations for examples including a stochastic routing protocol.

7 Conclusion

  • The paper provides sound and complete rules for almost-sure reachability and expected reaching time in a DES language with infinite state, continuous time, probabilistic choice, and event-driven execution.The conclusion characterizes this as an initial step in deductive verification for performance.Source: §7 · pp. 25–26
  • Leonides semi-automatically discharges proof obligations for examples including a formal analysis of a stochastic routing protocol.Source: §7 · p. 26

A.1 Soundness

The soundness argument combines supermartingale behavior outside an exempt set with a uniform positive chance of progress from sublevel sets. A counterexample explains why a descent condition that can leave the certified sublevel set does not suffice.

Soundness of Rule 4.1

  • A nonnegative supermartingale outside the exempt set forces trajectories to revisit some sublevel set infinitely often almost surely, while the variant condition gives a uniform positive chance of reaching Goal there.A zero-one law then yields almost-sure reachability.Source: §A.1 · pp. 28–30

Uniform progress from sublevel sets

  • From every state in a V sublevel set, the proof obtains a positive lower bound η(m) on reaching Goal within N(m) steps.It derives this by bounding U on the sublevel set and applying its positive-probability descent condition.Source: §A.1 · p. 30

Counterexample to the earlier rule

  • The symmetric random walk illustrates unsoundness when a certified U descent can leave the V sublevel set: subsequent certified decreases can shrink and sum to at most U(x0) = 1.The walk then never reaches Goal, despite the purported rule's certificate.Source: §A.1 · p. 32
  • The counterexample certificate does not satisfy Rule 4.1's V2 condition because no positive d(1) uniformly bounds its U decrease across the relevant states.Source: §A.1 · p. 32

A.2 Completeness

The completeness proof builds drift and variant certificates on a recurrent chain restricted to states that reach Goal almost surely. It then restricts the certificates to an invariant where the drift is finite, completing the construction required by Rule 4.1.

A.2 Completeness

  • Restricting to Inv, the states that reach Goal almost surely, yields a ψ-irreducible recurrent chain with Goal petite.Goal is petite because each goal state transitions to x0 in one step; recurrence follows since every state in Inv reaches Goal almost surely.Source: §A.2 · pp. 32–33
  • The proof constructs a drift function V, a variant U, and then restricts the invariant to states where V is finite to meet Rule 4.1’s certificate requirements.The construction uses Goal as the exempt set.Source: §A.2 · pp. 34, 38
  • An increasing petite-set exhaustion of Inv supplies the shared structure for constructing V and bounding U on V’s sublevel sets.The sets are built inductively, starting with C0 = Goal, and cover Inv.Source: §A.2 · p. 34
  • A subsequence sum of hitting probabilities builds V to satisfy the drift criterion and grow unbounded off petite sets while remaining finite ψ-almost everywhere.The subsequence is chosen using uniform bounds on early escape and late return probabilities.Source: §A.2 · pp. 36–37
  • U assigns increasing levels across the exhaustion, and transitions from each level have probability greater than 2^-n of descending at least one level, establishing V2.The construction also makes U zero exactly on Goal.Source: §A.2 · pp. 37–38
  • The invariant V<∞ contains x0 and Goal and is preserved by transitions, allowing finite-valued certificates to be extended to all states.Outside V<∞, the extended certificates take value 1.Source: §A.2 · p. 38
Loading 2609.37728v1…