Modern real-time systems require accurate characterization of task timing behavior to ensure predictable performance, particularly on complex hardware architectures. Existing methods, such as worst-case execution time analysis, often fail to capture the fine-grained timing behaviors of a task under varying resource contexts (e.g., an allocation of cache, memory bandwidth, and CPU frequency), which is necessary to achieve efficient resource utilization. In this paper, we introduce a novel generative profiling approach that synthesizes context-dependent, fine-grained timing profiles for real-time tasks, including those for unmeasured resource allocations. Our approach leverages a nonparametric, conditional multi-marginal Schrödinger Bridge (MSB) formulation to generate accurate execution profiles for unseen resource contexts, with maximum likelihood guarantees. We demonstrate the efficiency and effectiveness of our approach through real-world benchmarks, and showcase its practical utility in a representative case study of adaptive multicore resource allocation for real-time systems.
Figures & tables
Fig. 1 : Effect of CPU frequency, cache, and memory bandwidth on the instruction retirement rate of fft [ 74 ] . The benchmark shows distinct phases, with varying relationships (no effect, linear, nonlinear) between instruction rate and CPU frequency, depending on resource allocation (middle phase).
Fig. 2 : Distributions of microarchitectural execution states (rates of instructions, cache requests and cache misses) of fft at three time points under two different resource contexts.
Fig. 3 : Our proposed generative profiling algorithm scheme with maximum-likelihood guarantee. From empirical profiles of a task’s microarchitectural execution states, conditioned on a sparse set of resource allocations B′ , we generate ‘synthetic’ profiles for the unknown resource allocations.
Fig. 4 : The relationship between a transport plan M , its projections, and the transport cost C for ns=3 empirical distributions {μσ}σ∈[[ns]] . Unimarginal projections equal the distributions, and for the three arbitrary colored points, [Mi1,i2,i3] encodes the total probability mass transported, and [Ci1,i2,i3] the per-unit cost thereof, along the grey-colored path therebetween. Similarly, the bimarginal projections of M and the pairwise cost c pertain to the pairwise sections of the path.
Fig. 5 : Maximum-likelihood synthetic profile ( blue ), mean synthetic profile ( red ), and all empirical profiles ( grey ) for the benchmarks fft and canneal when β=(7,12,2.1)⊤ on our default experimental platform.
Fig. 6 : Maximum-likelihood synthetic profile ( blue ), mean synthetic profile ( red ), and all empirical profiles ( grey ) for the benchmarks fft and canneal when β=(13,11,2.1)⊤ on PlatformLarge .
Fig. 7 : Accuracy and relative profiling time vs. % of resource contexts used for training (workload canneal ).
Baseline
Generative
Improvement
blackscholes
0.0429
0.0343
20.0%
bodytrack
0.0437
0.0375
14.2%
canneal
0.0227
0.0027
88.1%
dedup
0.0321
0.0191
40.5%
fft
0.0508
0.0478
5.9%
fluidanimate
0.0357
0.0275
23.0%
TABLE I : Per-benchmark accuracy (normalized DTW) of baseline vs. generated profiles, both trained on ≈6% of resource contexts, averaged over all β∈B. Smaller DTW indicates better accuracy. Improvement % is computed via 100×(baseline DTW−generative DTW)/ baseline DTW .
Count
Mean
90th
95th
99th
Max
28347
1.068
1.536
2.008
6.204
10.727
TABLE II : Runtime Overhead of DNA in μ s
Fig. 8 : Taskset Schedulability
Total Time (hrs)
# Empirical Profiles
Empirical
231
456,000
Baseline
0.64
1,250
Generative
1.14
1,250
TABLE III : Avg. End-to-end Measurement & Generation Time
Fig. 9 : DNA Performance Comparison using Generative vs. Baseline vs. Empirical Profiles.
Schedulability analysis is essential for certifying real-time systems, but existing tests are often developed through pen-and-paper proofs that are difficult to scale, validate, and maintain. Mechanized verification in PROSA/ROCQ offers a rigorous alternative, yet manually constructing such proofs requires substantial domain expertise and proof-engineering effort. Recent successes of large language models (LLMs) across a wide range of tasks make them promising candidates for generating PROSA/ROCQ scripts for mechanized theorem provers. However, state-of-the-art LLMs often lack the PROSA-specific knowledge required to correctly use its modeling abstractions and proof patterns. This paper introduces PROVE-RT, an LLM-assisted framework for generating PROSA/ROCQ scripts to mechanize schedulability analyses in real-time systems literature. PROVE-RT guides generation through dependency-aware informal sketches, retrieval from processed PROSA documentation, staged skeleton generation, and proof completion. We construct a mechanization-oriented corpus from 1, 191 real-time systems papers, containing 13, 134 informal sketches with dependency information. On a curated evaluation set, direct prompting of state-of-the-art LLMs fails to reliably generate valid PROSA mechanizations, whereas PROVE-RT achieves a success rate of 44.7%. These results show that retrieval-guided and staged LLM assistance can improve automated mechanization of schedulability analysis in PROSA/ROCQ.
Sadat Shahriyar, Shareef Ahmed, Abdullah Al Arafat
Florida International University · University of South Florida
FPGA-GPP heterogeneous systems combine software flexibility with the performance and energy efficiency of reconfigurable hardware. However, determining which application tasks should execute on the GPP or FPGA requires extensive expertise and design-space exploration, particularly when user objectives vary across latency, communication, resource utilisation, and power. This paper proposes Gen-TAS, a knowledge-grounded LLM framework for user-specific FPGA-GPP task allocation. By combining task-graph analysis with RAG, Gen-TAS grounds LLM reasoning in historical implementation knowledge and generates multiple explainable strategies tailored to the specified objectives. Human-in-the-loop selection and a deterministic backend connect LLM-generated decisions to reproducible FPGA SoC implementations. Experiments on CNN and SDR workloads across multiple LLMs demonstrate stable, requirement-driven allocation. Under latency-oriented objectives, implementations following the selected strategies achieve speedups of up to 2.45× and 92.53×, respectively, relative to the corresponding all-GPP baselines while other objectives select strategies that trade some acceleration performance for FPGA-GPP communication, resource utilisation, or FPGA power.
Mary Kong, Yuqin Zhao, Semih Vazgecen +2
Centre for Electronics Frontiers, Institute for Integrated Micro and Nano Systems, School of Engineering, University of Edinburgh, UK
Rigorous schedulability analysis is essential for the design of hard real-time systems, yet errors in pen-and-paper proofs threaten the safety of critical applications. The Prosa initiative addresses this by offering a foundation for building machine-checkable schedulability analysis proofs in the Rocq proof assistant. However, the substantial time and expertise required to construct such proofs remain a major barrier for wider adoption of Prosa. This work presents ProsaBuddy, an LLM?based agent system designed to lower the effort needed to develop mechanized real-time schedulability proofs. ProsaBuddy employs a ReAct loop with retrieval over the Prosa codebase, access to Rocq tools and optional human-written hints. It uses a subgoal?delegation architecture, decomposing a lemma into subgoals and dispatches them to subagents for proof. We evaluate ProsaBuddy on a mini benchmark drawn from real-time scheduling literature. Experiment results show that ProsaBuddy significantly outper?forms state-of-the-art LLM-based Rocq automated proving agent systems and a general coding agent OpenCode
Junyi Liu, Tianchi Ren, Fei Guan +4
City University of Hong Kong · Northeastern University (China) · Northeast Forestry University +3