{"id":"826bab6c-db8b-4573-8c6b-a5e70b36eee9","arxiv_id":"2607.26927","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.5,"correctness_risk":"low","formal_verification":"partial","parameter_count":0,"one_line_summary":"A Frama-C/ACSL framework verifies three EDF correctness properties on RTEMS 5, RTEMS 6, and a FreeRTOS EDF extension under explicit kernel assumptions.","lead":"The authors define three correctness properties for Earliest Deadline First schedulers and verify them with Frama-C on RTEMS 5/6 and a FreeRTOS EDF port. This matters because safety-critical systems need the concrete kernel code, not just the abstract policy, to preserve deadline ordering.","discovery_kind":"new_method","skeptic_critique":{"model":"grok-4.5","headline":"No significant objection identified beyond the paper's own scoped assumptions.","rationale":"The central claim is scoped and modular: under explicit assumptions on data-structure interfaces and that a requested context switch occurs before the next external observable point with no intervening ready-queue mutation, the three implementations satisfy P1–P3 and thereby Definition 1. The reader already isolates the strongest remaining gap (the context-switch timing assumption, especially RTEMS deferred dispatch). That gap is real for end-to-end external EDF behavior but is not a flaw internal to the verified scheduler logic; covering it would require interrupt handlers and broader OS infrastructure the paper correctly places out of scope. No stronger load-bearing concern (e.g., an unstated aliasing hole that would invalidate the Typed+Cast model, or a missing entry point that breaks the invariant chain) is evident from the manuscript, tables, and boundary discussion. Hence the CONDITIONAL verdict and the identified weakest assumption stand; no adjustment is warranted.","tokens_in":18584,"tokens_out":450,"duration_ms":8242,"concrete_test":"Re-run the artifact's Frama-C/WP scripts on the released ACSL-annotated RTEMS 5/6 and FreeRTOS sources; confirm Tables I–II goal counts and that the edf_running_earliest / ready-queue invariants are proved for every listed entry point. Any undischarged obligation on an EDF entry point would weaken the claim.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader's weakest assumption (context-switch gap / deferred dispatch in RTEMS, Sec. II-C and IV-C) is correctly identified and is already treated by the paper as out of scope. Under the stated modular boundary—abstract ready-queue contracts, assumed kernel primitives, and the uniprocessor entry-point restriction—P1–P3 do establish Definition 1 at observable points. No internal inconsistency, missing case in the three codebases, or hidden circularity in the Frama-C argument appears load-bearing beyond what the authors flag. The FreeRTOS overrun fix and discharged goal counts further support the scoped claim.","agreement_with_reader":"agree"},"referee_report":{"model":"grok-4.5","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.","tokens_in":18723,"tokens_out":1224,"duration_ms":33448,"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":[{"comment":"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.”","section":"Section II-C, IV-C"},{"comment":"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.","section":"Section VI, Abstract"}],"minor_comments":[{"comment":"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.","section":"Figure 1, Figure 3, Section VI-D"},{"comment":"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.","section":"Section VII-B, Table I, Table II"},{"comment":"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.","section":"Section II-B, II-C"},{"comment":"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.","section":null},{"comment":"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.","section":"Section I, VIII"}],"recommendation":"minor_revision","confidential_remarks":"The paper is a solid systems-verification contribution appropriate for a serious OS/real-time venue. The FreeRTOS case is slightly weaker novelty-wise than RTEMS because the EDF code is the authors’, but the bug find and cross-infrastructure methodology compensate. I do not see a reject-level soundness problem; minor revision to tighten the context-switch assumption presentation and the FreeRTOS framing should suffice."},"author_rebuttal":null,"desk_editor":{"model":"grok-4.5","letter":"Punchline: this is the first practical deductive framework aimed at EDF as it actually sits inside existing RTOS kernels, not a clean-slate reimplementation. They define three local properties (deadline→priority, ready-queue maintenance, scheduler decision), discharge large Frama-C/WP goal sets on RTEMS 5, RTEMS 6, and a FreeRTOS EDF retrofit, ship an artifact, and catch a real overrun reinsertion bug in the FreeRTOS path. That combination is the real contribution.\n\nWhat works: the properties are independent of any one codebase and map cleanly onto how EDF is bolted onto fixed-priority infrastructure. The modular boundary (abstract ready-queue contracts, assumed tick/dispatch/context-switch primitives) is stated up front rather than smuggled in. Tables of Qed/Alt-Ergo goals and the FreeRTOS fix give concrete evidence the specs bite. Related work is fair: Vanhems et al., seL4/CertiKOS, API-level FreeRTOS work, and application-level encodings are positioned correctly without overclaiming.\n\nSoft spots, in proportion: the load-bearing assumption is that a requested context switch runs before the next observable point with no intervening ready-queue update. RTEMS deferred dispatch makes that gap real; the paper marks full interrupt/OS coverage out of scope. Data-structure interfaces (OpenBSD RB-trees, FreeRTOS lists) and cast/representation assumptions sit on the trusted boundary too. None of that breaks the internal argument under the stated uniprocessor entry-point restriction—P1–P3 do establish their Definition 1 at observable points—but external “the running job is always earliest-deadline” still rests on infrastructure they did not verify. That is a limitation of scope, not a hidden contradiction.\n\nMath and citation pattern look fine; no circular success criterion. Who cares: people doing RTOS verification, certification-adjacent scheduling, or EDF ports on legacy kernels. I would bring it to reading group, cite the property split and the FreeRTOS finding, and send it to peer review. Expect referees to push on the dispatch gap and how much of “EDF correctness” is still assumed; the paper already owns that.","headline":"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.","tokens_in":19380,"tokens_out":563,"would_cite":true,"duration_ms":15098,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"grok-4.5","headline":"EDF correctness in real RTOS kernels reduces to three local properties that deductive verification can check without rewriting the scheduler.","keywords":["EDF scheduling","formal verification","real-time operating systems","deductive verification","ready queue","scheduler correctness","deadline-driven priorities"],"falsifier":"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.","tokens_in":19459,"feed_emoji":"⏱️","tokens_out":851,"duration_ms":39098,"temperature":0.7,"pith_summary":"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.","feed_headline":"Three properties verify EDF schedulers in real RTOS code","feed_subtitle":"Deductive checks on production kernels show deadline order holds under stated infrastructure assumptions","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Three local properties prove EDF schedulers correct in real RTOS code","Deductive framework checks EDF deadline order in RTEMS and FreeRTOS","Any EDF implementation must satisfy three properties for correct dispatch","Frama-C verifies EDF semantics hold in three production scheduler ports","Formal checks confirm earliest-deadline dispatch under kernel assumptions"],"cache_read_input_tokens":128,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Three local properties prove EDF schedulers correct in real RTOS code","Deductive framework checks EDF deadline order in RTEMS and FreeRTOS","Any EDF implementation must satisfy three properties for correct dispatch","Frama-C verifies EDF semantics hold in three production scheduler ports","Formal checks confirm earliest-deadline dispatch under kernel assumptions"]},"model":"grok-4.5","effort":"low","cost_usd":0.001565,"raw_usage":{"total_tokens":814,"prompt_tokens":721,"num_sources_used":0,"completion_tokens":73,"cost_in_usd_ticks":15648000,"prompt_tokens_details":{"text_tokens":721,"audio_tokens":0,"image_tokens":0,"cached_tokens":256},"completion_tokens_details":{"audio_tokens":0,"reasoning_tokens":20,"accepted_prediction_tokens":0,"rejected_prediction_tokens":0}},"tokens_in":721,"tokens_out":73,"duration_ms":2251,"temperature":1.0,"reasoning_tokens":20,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-30T16:45:20.070376+00:00","model_set":{"reader":"grok-4.5"},"falsifier":"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.","supporting_citations":[],"review_version":1}