Pith. sign in

REVIEW 2 major objections 5 minor 42 references

Deductive Verification for Earliest Deadline First Scheduler Implementations

T0 review · 2 major / 5 minor · reviewed 2026-07-30 · grok-4.5

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read EDF correctness in real RTOS kernels reduces to three local properties that deductive verification can check without rewriting the scheduler.

desk verdict Solid, scoped Frama-C verification of real EDF paths in RTEMS and FreeRTOS—useful and honest about its boundaries, not a full end-to-end kernel proof. read the letter →

arxiv 2607.26927 v1 pith:7DZCL25I submitted 2026-07-29 cs.OS

Daniel Kuhse , Junjie Shi , Jan Duy Thien Pham , Kay Heider , Marcus Völker , Kuan-Hsun Chen , Jian-Jia Chen This is my paper · ORCID
classification cs.OS
keywords EDFschedulingformalverificationreal-timeoperatingsystemsdeductivereadyqueueschedulercorrectnessdeadline-drivenpriorities
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Abstract scheduling theory is not enough for safety-critical systems: the concrete Earliest Deadline First code must keep deadline-derived priorities consistent through job release, ready-queue updates, and dispatch. This paper defines three properties every correct EDF implementation must satisfy—deadline-to-priority mapping, ready-queue management, and scheduler decisions—and shows they jointly guarantee that, at every observable point outside the scheduler, the running job has the earliest absolute deadline or a context switch is already scheduled. It turns those properties into a modular deductive-verification framework with contracts and invariants at the scheduler boundary, treating generic kernel primitives and data-structure interfaces as assumptions. The framework is applied to three structurally different uniprocessor EDF realizations, including two generations of one production RTOS and an EDF retrofit of another, confirming the properties under the stated assumptions and exposing an overrun path where a deadline update without reinsertion would break ready-list order.

What carries the argument

The three EDF correctness properties (P1–P3) plus modular function contracts and state invariants in a deductive verifier: P1 ties each job’s priority to its absolute deadline, P2 keeps the ready queue ordered with the earliest-deadline job at the head, and P3 ensures every scheduler entry re-establishes earliest-deadline selection or a pending context switch.

What would settle it

Exhibit a uniprocessor trace in one of the checked kernels where, after a verified scheduler entry returns, a ready job with an earlier deadline executes without a pending dispatch, or show a ready-queue mutation between selection and the deferred context switch on the paths the paper claims to cover.

Watch

Extended reading notes

Core claim

Any correct EDF scheduler implementation must satisfy three local properties—deadline priorities, ready-queue management, and scheduler decisions—that together establish externally observable EDF behavior. Under explicit assumptions on kernel infrastructure and ready-queue interfaces, the uniprocessor EDF code in two RTEMS versions and a FreeRTOS EDF extension meets those properties, so the running job has the earliest absolute deadline among eligible jobs or a dispatch is already pending.

Load-bearing premise

A requested context switch must actually run before the next observable moment outside the scheduler, with no ready-queue updates in the gap—an assumption left outside full interrupt and OS coverage.

Editorial extensions

If this is right

  • EDF logic built on legacy fixed-priority infrastructure can be verified without a clean-slate kernel rewrite.
  • The same three properties and abstract ready-queue contracts transfer across structurally different RTOS designs.
  • Overrun paths harmless under fixed priorities can break EDF ready-list order and must be rechecked when deadlines become the sort key.
  • Verified replacements for the abstract queue and tree interfaces could be swapped in without redoing the EDF proofs.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same three-property split is a natural template for other dynamic-priority policies that reuse fixed-priority queues and caches.
  • Closing the context-switch timing gap would force verification of interrupt disable/enable discipline across the whole kernel, not only the scheduler module.
  • Ready-queue cache shortcuts that skip re-sorting after deadline changes are prime next targets for the same contract pattern.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper argues that EDF correctness in real RTOS kernels cannot be reduced to the abstract election rule alone, because deadline-derived priorities must be consistently maintained across release, ready-queue, and dispatch paths that often reuse fixed-priority infrastructure. It defines three local properties—P1 (deadline-to-priority mapping), P2 (ready-queue management), and P3 (scheduler decisions)—that together establish an externally observable EDF property (Definition 1) under an explicit context-switch timing assumption. It then presents a modular Frama-C/ACSL deductive framework with abstract ready-queue contracts and applies it to the uniprocessor EDF paths in RTEMS 5, RTEMS 6, and an author-modified FreeRTOS V11.1.0, discharging large sets of proof obligations and, in FreeRTOS, exposing and fixing an overrun reinsertion bug that breaks ready-list ordering.

Significance. If the scoped claim holds, this is a genuine advance for verification of production-style RTOS schedulers: it targets existing (or lightly adapted) kernels rather than clean-slate reimplementations, supplies machine-checked ACSL contracts and discharged WP/Alt-Ergo goals with reproducible artifact and tables of proof effort, and demonstrates portability across two RTEMS generations plus a structurally different FreeRTOS list-based design. The FreeRTOS overrun finding is concrete evidence that the specifications are not tautological. The work is limited to uniprocessor EDF under stated infrastructure assumptions, but within that envelope it fills a clear gap left by seL4/CertiKOS-style kernels, model-checking of abstracted schedulers, and prior FreeRTOS API or cooperative-application verification.

major comments (2)
  1. [Section II-C, IV-C] Sec. II-C and IV-C: Definition 1 is established from P1–P3 only under the assumption that a requested context switch executes before the next observable point outside the scheduler, with no intervening ready-queue updates. The paper correctly flags this and notes RTEMS deferred dispatch until the thread-dispatch disable level returns to zero. Because this assumption is load-bearing for the external claim, the manuscript should state more sharply, for each case study, which concrete kernel paths are relied upon to discharge it (e.g., FreeRTOS immediate switch after the scheduler vs. RTEMS disable-level return) and what would falsify it, rather than leaving the gap only as “out of scope.”
  2. [Section VI, Abstract] Sec. VI and Abstract/Contributions: The FreeRTOS result verifies an author-constructed EDF retrofit of V11.1.0 (deadline field replacing static priority, sorted ready-list insertion, MSP430 port kept in C), not a shipping FreeRTOS EDF configuration. That is still valuable—especially given the overrun fix—but the framing that the framework applies to “existing RTOS” EDF realizations is accurate for RTEMS 5/6 and only partly accurate for FreeRTOS. The contribution statement and evaluation should separate “verification of production EDF code” (RTEMS) from “verification-guided construction and check of an EDF extension” (FreeRTOS) so the central portability claim is not overstated.
minor comments (5)
  1. [Figure 1, Figure 3, Section VI-D] Figure 1’s gray “verification target” region is helpful; a short explicit mapping from P1–P3 to the yellow/blue function groups in Figure 3 (and the FreeRTOS entry points in Sec. VI-D) would make the property-to-code correspondence easier to audit.
  2. [Section VII-B, Table I, Table II] Tables I–II report Qed/Alt-Ergo goal counts and wall times but not annotation LOC, number of predicates/invariants, or which goals required manual contract iteration. A brief effort breakdown would strengthen the reusability discussion in Sec. VII-B.
  3. [Section II-B, II-C] Tie-breaking for equal absolute deadlines is stated as implementation-defined (FIFO in RTEMS). P2/P3 should explicitly say whether equal-deadline order is part of the verified invariant or left unconstrained, to avoid ambiguity when reading the ready-queue model.
  4. Minor prose/typo issues: “V ¨olker”, “UA V”, and occasional doubled spaces; also “edf-verification” artifact URL appears twice with slightly different access dates—normalize.
  5. [Section I, VIII] Related work cites Vanhems et al. and FreeRTOS/RTEMS verification efforts appropriately; a one-sentence contrast with Zephyr’s ready_q.cache issue (mentioned in the introduction) would connect the motivating bug report to whether the framework’s P2 would have caught an analogous cache invariant.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: EDF properties are independent specs checked against code, not defined by the implementations.

full rationale

This is a deductive-verification paper. Definition 1 and properties P1–P3 are stated as external EDF semantics (deadline-to-priority mapping, ready-queue ordering, heir/dispatch decisions). The Frama-C/ACSL contracts check RTEMS 5/6 and a FreeRTOS EDF retrofit against those specs under explicitly declared modular assumptions (RB-tree/list interface contracts, kernel primitives, context-switch gap). Success is not defined as whatever the code already does; the FreeRTOS overrun case was found and fixed precisely because the specs were independent of the initial implementation. There are no fitted parameters, no self-definitional equations, no load-bearing uniqueness theorems imported from overlapping authors, and no renaming of a known empirical pattern. Self-citations (e.g., prior Frama-C RTOS work) are background, not the derivation of the central claim. Residual trust is the usual declared verification boundary, which is not circularity by construction.

Assumptions & free parameters 0 free parameters · 8 assumptions · 1 invented entities

The central claim is conditional verification under a modular boundary. Almost all load-bearing content outside the annotated EDF paths is assumed: uniprocessor entry points, data-structure interface contracts, context-switch timing, and Frama-C memory/volatile modeling. No numeric parameters are fitted. The three properties are definitional formalizations of standard EDF intent, not new physical entities.

assumptions (8)
  • domain assumption Requested context switch runs before the next observable external point, with no ready-queue mutation in between (Sec. II-C, IV-C).
    Needed to lift local P3 postconditions to Definition 1's externally observable EDF behavior; full interrupt coverage is declared out of scope.
  • domain assumption Underlying kernel primitives (dispatch, memory, tick, non-EDF infrastructure) are correct.
    Sec. IV-C verification boundary; EDF proofs compose with these black boxes.
  • domain assumption Ready-queue and priority-aggregation data structures obey abstract set/membership/min contracts (OpenBSD RB-tree in RTEMS; doubly-linked lists in FreeRTOS).
    Sec. IV-C; concrete tree/list implementations are not verified, only interface assumptions.
  • domain assumption Uniprocessor scheduler entry points have no concurrent modification of volatile scheduler state during the verified operations; Volatile ghost mirroring is sound.
    Sec. IV-B; required for stable reasoning about dispatch flags and current-TCB pointers.
  • domain assumption Pointer casts and structural-inheritance representations in RTEMS/FreeRTOS preserve the intended object layout (trusted under Typed+Cast memory model).
    Sec. IV-B and VII-C; Frama-C does not prove cast intent.
  • standard math Hoare-logic / ACSL contract modularity: callees may be replaced by their contracts.
    Standard deductive-verification foundation used throughout Sec. IV.
  • domain assumption Implicit deadlines (D_i = T_i) in the default RTEMS rate-monotonic/EDF path and in the FreeRTOS xTaskDelayUntil retrofit.
    Sec. V-A and VI-C; shapes how deadline updates are modeled in the case studies.
  • ad hoc to paper EDF correctness is captured by P1–P3 implying Definition 1 under the context-switch assumption.
    Sec. II-C formalization choice; reasonable but specific packaging of EDF intent for modular proofs.
invented entities (1)
  • Three EDF correctness properties P1–P3 (deadline priorities, ready queue management, scheduler decisions) independent evidence
    purpose: Provide a portable specification target for any EDF realization inside existing RTOS kernels.
    They are a structured restatement of classical EDF semantics for verification boundaries, not new runtime mechanisms; independent evidence is the standard scheduling literature plus the case-study proofs.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Deductive Verification for Earliest Deadline First Scheduler Implementations." pith.science (2026). https://pith.science/paper/7DZCL25I

@misc{pith2026260726927,
  author       = {Pith},
  title        = {Pith review of: Deductive Verification for Earliest Deadline First Scheduler Implementations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7DZCL25I}},
  note         = {Machine review of arXiv:2607.26927}
}
read the original abstract

Real-Time Operating Systems (RTOSes) rely on scheduler implementations to provide predictable task execution. For safety-critical systems, it is therefore not sufficient to reason only about the abstract scheduling policy; the concrete implementation must also preserve the intended scheduling semantics. This is particularly challenging for Earliest Deadline First (EDF) scheduling, because EDF introduces dynamic, deadline-derived priorities that are often realized by reusing kernel infrastructure originally designed for fixed-priority scheduling. In this work, we formalize EDF correctness through three essential properties that any implementation of the Earliest Deadline First (EDF) scheduler must satisfy. Based on these properties, we propose a framework utilizing deductive verification, that applies to any EDF-based scheduler realization. We instantiate the framework in Frama-C/ACSL and apply it to three structurally different EDF scheduler realizations: RTEMS 5, RTEMS 6, and an EDF extension of FreeRTOS.

Figures

Figures reproduced from arXiv: 2607.26927 by the authors.

Figure 1
Figure 1. The workflow of EDF scheduler. The gray area is the verification [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. The ready queue management workflow within EDF scheduler node [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Overview of verified EDF scheduler and thread priority functions, with [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figures from the paper (1 more)
Figure 5
Figure 5. Figure 5: Control flow of executing priority update. Pending updates come from [PITH_FULL_IMAGE:figures/full_fig_p008_5.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

42 extracted references

  1. [1]

    Potential Issues with the EDF Sched- uler in Zephyr, 2024

    Alexander Pinheiro Paschoaletto. Potential Issues with the EDF Sched- uler in Zephyr, 2024. https://github.com/zephyrproject-rtos/zephyr/ issues/79361, Last accessed on 2026-05-06

    2024

  2. [2]

    FreeRTOS: Real-time operating system for microcontrollers

    Amazon. FreeRTOS: Real-time operating system for microcontrollers. https://www.freertos.org/, Last accessed on 2026-05-18

    2026

  3. [3]

    Baier and J.-P

    C. Baier and J.-P. Katoen.Principles of model checking. MIT press, 2008

    2008

  4. [4]

    Bertot and P

    Y . Bertot and P. Cast ´eran.Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004

    2004

  5. [5]

    Blom and M

    S. Blom and M. Huisman. The vercors tool for verification of concurrent programs. InFM: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, pages 127–131, 2014

    2014

  6. [6]

    Bobot, J.-C

    F. Bobot, J.-C. Filli ˆatre, C. March ´e, and A. Paskevich. Why3: Shepherd your herd of provers.Boogie 2011: First International Workshop on Intermediate Verification Languages, 2011

    2011

  7. [7]

    Boukir, J

    K. Boukir, J. B ´echennec, and A. D ´eplanche. Requirement specification and model-checking of a real-time scheduler implementation. In28th International Conference on Real Time Networks and Systems, RTNS, pages 89–99. ACM, 2020

    2020

  8. [8]

    Bozhko and B

    S. Bozhko and B. B. Brandenburg. Abstract response-time analysis: A formal foundation for the busy-window principle. In M. V ¨olp, editor, 32nd Euromicro Conference on Real-Time Systems, ECRTS, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f ¨ur Informatik, 2020

    2020

Show all 42 references
  1. [9]

    Chong and B

    N. Chong and B. Jacobs. Formally verifying freertos’ interprocess com- munication mechanism. InEmbedded World Exhibition & Conference, 2021

    2021

  2. [10]

    Cohen, M

    E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. InTheorem Proving in Higher Order Logics, 22nd International Conference, Proceedings. Springer, 2009

    2009

  3. [11]

    P. Cuoq, F. Kirchner, N. Kosmatov, V . Prevosto, J. Signoles, and B. Yakobowski. Frama-c: A software analysis perspective. InSoftware Engineering and Formal Methods SEFM. Springer, 2012

    2012

  4. [12]

    ESP-IDF Programming Guide

    Espressif Systems. ESP-IDF Programming Guide. https://docs.espressif. com/projects/esp-idf/en/v6.0.1/esp32/index.html, Last accessed on 2026- 05-20

    2026

  5. [13]

    R. W. Floyd. Assigning meanings to programs.Proceedings of Symposium on Applied Mathematics, 19:19–32, 1967

    1967

  6. [14]

    Frama-C Software Analyzers

    FRAMA-C. Frama-C Software Analyzers. https://frama-c.com/, Last accessed on 2026-05-06

    2026

  7. [15]

    ANSI/ISO C Specification Language, 2007

    FRAMA-C. ANSI/ISO C Specification Language, 2007. https://frama-c. com/html/acsl.html, Last accessed on 2026-05-15

    2007

  8. [16]

    WP Plugin, 2007

    FRAMA-C. WP Plugin, 2007. https://frama-c.com/fc-plugins/wp.html, Last accessed on 2026-05-15

    2007

  9. [17]

    Gadia, C

    S. Gadia, C. Artho, and G. Bloom. Verifying nested lock priority inheritance in RTEMS with java pathfinder. In18th International Conference on Formal Engineering Methods, Proceedings, 2016

    2016

  10. [18]

    Garion, G

    C. Garion, G. Hattenberger, B. Pollien, P. Roux, and X. Thirioux. A gentle introduction to c code verification using the frama-c platform, 2022

    2022

  11. [19]

    R. Gu, Z. Shao, H. Chen, X. N. Wu, J. Kim, V . Sj¨oberg, and D. Costanzo. Certikos: An extensible architecture for building certified concurrent OS kernels. In12th OSDI, 2016

    2016

  12. [20]

    X. Guo, M. Lesourd, M. Liu, L. Rieg, and Z. Shao. Integrating formal schedulability analysis into a verified OS kernel. InComputer Aided Verification - 31st International Conference, CAV. Springer, 2019

    2019

  13. [21]

    X. Guo, L. Rieg, and P. Torrini. A generic approach for the certified schedulability analysis of software systems. InEmbedded and Real-Time Computing Systems and Applications (RTCSA). IEEE, 2021

    2021

  14. [22]

    C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, 1969

    1969

  15. [23]

    Jomaa, P

    N. Jomaa, P. Torrini, D. Nowak, G. Grimaud, and S. Hym. Proof- oriented design of a separation kernel with minimal trusted computing base.Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 76, 2018

    2018

  16. [24]

    Klein, K

    G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al. sel4: Formal verification of an os kernel. InOperating systems principles, 2009

    2009

  17. [25]

    Kuhse, J

    D. Kuhse, J. Shi, J. D. T. Pham, K. Heider, M. V ¨olker, K.-H. Chen, and J.-J. Chen. Deployment Instructions and Function Contracts for Deduc- tive Verification of Earliest Deadline First Scheduler Implementations,

  18. [26]

    Lammich and T

    P. Lammich and T. Nipkow. Priority search trees.Arch. Formal Proofs, 2019

    2019

  19. [27]

    Leinenbach and T

    D. Leinenbach and T. Santen. Verifying the microsoft hyper-v hypervisor with vcc. InFM 2009: Formal Methods, pages 806–809, 2009

    2009

  20. [28]

    Liang, D

    H. Liang, D. Zhang, X. Pei, X. Jia, G. Li, and J. Xu. A correctness verification method for c programs based on vcc. InInternational Conference on Cyber Security and Cloud Computing. IEEE, 2016

    2016

  21. [29]

    Lin and B

    C. Lin and B. Wang. Formal analysis of freertos scheduler on ARM cortex-m4 cores. InInternational Conference on Formal Engineering Methods, pages 199–215, 2024

    2024

  22. [30]

    Zephyr project

    Linux Foundation. Zephyr project. https://zephyrproject.org/, 2016. Last accessed on 2026-05-26

    2016

  23. [31]

    Mousavi, A

    H. Mousavi, A. Ebnenasir, and E. Mahmoudzadeh. Formal specification, verification and repair of contiki’s scheduler.ACM Trans. Cyber Phys. Syst., 7(4):22:1–22:28, 2023

    2023

  24. [32]

    Nicole, M

    O. Nicole, M. Lemerre, S. Bardin, and X. Rival. No crash, no exploit: Automated verification of embedded kernels. In27th IEEE Real-Time and Embedded Technology and Applications Symposium, 2021

    2021

  25. [33]

    An SMT Solver For Software Verification

    OCamlPro SAS. An SMT Solver For Software Verification. https: //alt-ergo.ocamlpro.com/, Last accessed on 2026-05-20

    2026

  26. [34]

    Pollien, C

    B. Pollien, C. Garion, G. Hattenberger, P. Roux, and X. Thirioux. Verifying the mathematical library of an uav autopilot with frama-c. In26th International Conference FMICS. Springer, 2021

    2021

  27. [35]

    J. Shi, C. von Egidy, K. Chen, and J. Chen. Formal verification of resource synchronization protocol implementations: A case study in RTEMS.IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 2022

    2022

  28. [36]

    Singh, M

    A. Singh, M. D’Souza, and A. Ebrahim. Conformance testing of ARINC 653 compliance for a safety critical RTOS using UPPAAL model checker. InSAC: The 36th ACM/SIGAPP Symposium on Applied Computing, pages 1807–1814. ACM, 2021. 12

    2021

  29. [37]

    Staroletov

    S. Staroletov. A formal model of a partitioned real-time operating system in promela.Proceedings of the Institute for System Programming of RAS, 32:49–66, 12 2020

    2020

  30. [38]

    Tasche, P

    P. Tasche, P. Herber, and M. Huisman. Deductive verification of cooperative RTOS applications.ACM Trans. Embed. Comput. Syst., 24(5s):131:1–131:25, 2025

    2025

  31. [39]

    Texas Instruments Incorporated.MSP430FR599x, MSP430FR596x Mixed-Signal Microcontrollers, 2021

    2021

  32. [40]

    Real-Time Executive for Multiprocessor Systems (RTEMS), 2014

    The RTEMS Project. Real-Time Executive for Multiprocessor Systems (RTEMS), 2014. http://www.rtems.org/, Last accessed on 2026-05-27

    2014

  33. [41]

    Vanhems, V

    F. Vanhems, V . Rusu, D. Nowak, and G. Grimaud. A formal correctness proof for an EDF scheduler implementation. In28th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS, 2022. 13

    2022

  34. [2026]

    https://github.com/TU-Dortmund-CS-LS12-DAES-teaching/ edf-verification, Last accessed on 2026-07-27

    2026

Pith tools

Reviewed July 30, 2026 · model on record in the stance chip above.