Execution trace-based model verification to analyze multicore and real-time systems

Problem and motivation

Large execution traces can reveal timing and scheduling failures, but interpreting millions of events is slow and requires deep operating-system knowledge. Model checking can identify a violated specification without explaining whether preemption, blocking, a system call, scheduling, or application code caused it.

Method and contribution

A developer-specified state-machine model contains states, transitions, metric variables, and quantitative constraints. The method extracts model instances from user-space and kernel traces, labels constraint occurrences valid/invalid/uncertain, excludes uncertain cases, and compares sampled valid and invalid instances. It uses 95% confidence, a 5% margin of error, and reservoir sampling. Elements such as RUNNING, BLOCKED, PREEMPTED, and SYSCALL are converted into duration sets and merged into interval sets; directional edit-distance-like comparisons, occurrence/distance weights, differential interval sets, and responsibility scores identify the most likely causes. Follow-up analyses include process state, critical path, priority inheritance, state-machine state, CPU-top, and CPU-frequency analysis. LTTng/LTTng-UST is selected as the primary low-impact kernel/user-space tracing stack, with CTF events and a common clock; the cyclictest case uses LTTng snapshot mode.

Findings and evidence

Four case studies diagnose low-priority JACK2, in-kernel wake-lock priority inversion, bad user-space code, and a preempted cyclictest waker. JACK2 analysis attributes 96.65% of excess time to WAKING and 96.51% to process preemption, identifying the higher-priority cpuburn process. The wakelock analysis identifies abnormal blocking on open, priority inheritance, and preemption by highprio1. The user-space case locates the excess time in step3. The cyclictest case on an NVIDIA Jetson TK1 traces a 7-ms outlier through rt_sigtimedwait, preempted ktimersoftd/3, and the irq/154-hpd HDMI hot-plug handler. The four traces contain 321/419,164, 42/194,997, 29/89,840, and 41,677/208,489 UST/kernel events. On an Intel Core i7-4790 at 3.6 GHz with 32 GiB DDR3, sampling preserves the highest responsibility within 0.1% in 100-run comparisons while reducing process-state analysis from 23,925.75 to 15,311.02 ms for JACK2 and from 103,119.10 to 7,124.76 ms for cyclictest.

Limitations and future directions

Limitations: The method depends on a developer-provided model and suitable tracepoints, and generated or selected valid baselines may not cover complex or changing behavior. Sampling is an approximation, missing snapshot data can cause instances to be dropped, and full analysis remains sensitive to the number of trace events, model instances, and variable changes. The evaluation uses four controlled/common real-time cases rather than a broad cross-platform workload study.

Future work: The paper proposes automatically setting constraint values from traces. It does not establish online learning, modern OpenTelemetry support, or automatic model generation for this publication. Supporting data are available from the corresponding author upon reasonable request.

Sources and identifiers

• Published version published

When to cite this paper

Cite this paper when using model-based quantitative constraints and user-space/kernel traces to diagnose real-time or multicore execution problems.

• LTTng/LTTng-UST and CTF-based correlation of kernel and user-space execution evidence.
• Reservoir-sampled valid/invalid model instances, interval-set comparison, and responsibility scoring for likely causes.
• JACK2, wake-lock priority inversion, bad user-space code, and cyclictest case studies with trace-size, runtime, and sampling results.

Citation

@article{ezzatiJivan2022executiontrace,
  author = {Raphaël Beamonte and Naser Ezzati-Jivan and Michel R. Dagenais},
  title = {Execution trace-based model verification to analyze multicore and real-time systems},
  year = {2022},
  journal = {Concurrency and Computation: Practice and Experience},
  volume = {34},
  number = {17},
  eid = {e6974},
  publisher = {Wiley},
  issn = {1532-0626, 1532-0634},
  doi = {10.1002/cpe.6974},
  url = {https://doi.org/10.1002/cpe.6974}
}

Beamonte, R., Ezzati-Jivan, N., & Dagenais, M. R. (2022). Execution trace-based model verification to analyze multicore and real-time systems. Concurrency and Computation: Practice and Experience, 34(17), e6974. https://doi.org/10.1002/cpe.6974

R. Beamonte, N. Ezzati-Jivan, and M. R. Dagenais, "Execution trace-based model verification to analyze multicore and real-time systems," Concurrency and Computation: Practice and Experience, vol. 34, no. 17, 2022, doi: 10.1002/cpe.6974