diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8ee2b9b..2177e4b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,7 +26,7 @@ jobs: strategy: fail-fast: false matrix: - preset: [native-gcc, native-clang, native-release, native-tiny, native-periodic, native-asan, native-tsan, native-coverage] + preset: [native-gcc, native-clang, native-release, native-tiny, native-periodic, native-timeslice, native-timeslice-tickless, native-asan, native-tsan, native-coverage] steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 - name: Install tools diff --git a/CHANGELOG.md b/CHANGELOG.md index 5e3479c..c5fe5a4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,8 @@ User-visible changes are recorded here. There are no released versions or releas ### Added +- Round-robin time slicing (`CONFIG_EMB_TIME_SLICING`, off by default): a thread at or below `CONFIG_EMB_TIMESLICE_PRIORITY` that runs for `CONFIG_EMB_TIMESLICE_TICKS` without blocking moves behind its READY equal-priority peers; without a peer its quantum is renewed (KRN-SCH-007, 026, 037; A63). The quantum is a deadline in the tickless computation and a comparison in the periodic tick. The reference model implements it, the new `native-timeslice` preset checks it through the differential bridge, and `native-timeslice-tickless` runs the conformance cases with the tickless clock. List scheduler only. + - The M2 contract decisions are accepted: amendments A29 to A61 and ADR-045 to ADR-048 and ADR-050 (project-owner review, 2026-10-31). - The M2 exit review (`docs/engineering/m2-exit-review.md`): every checklist item with its pull requests and evidence, the reconciliation of APIs, configuration, model and requirements, the defects found, and the remaining M3a hardware work. diff --git a/CMakePresets.json b/CMakePresets.json index 412cab4..ec290c8 100644 --- a/CMakePresets.json +++ b/CMakePresets.json @@ -37,6 +37,24 @@ "EMB_CONF": "configs/native-periodic.conf" } }, + { + "name": "native-timeslice", + "displayName": "native, GCC, base profile, checked, round-robin time slicing", + "inherits": "native-gcc", + "binaryDir": "${sourceDir}/build/native-timeslice", + "cacheVariables": { + "EMB_CONF": "configs/native-timeslice.conf" + } + }, + { + "name": "native-timeslice-tickless", + "displayName": "native, GCC, base profile, checked, time slicing with the tickless clock", + "inherits": "native-gcc", + "binaryDir": "${sourceDir}/build/native-timeslice-tickless", + "cacheVariables": { + "EMB_CONF": "configs/native-timeslice-tickless.conf" + } + }, { "name": "native-release", "displayName": "native, GCC, base profile, release build kind", @@ -270,6 +288,14 @@ "name": "native-periodic", "configurePreset": "native-periodic" }, + { + "name": "native-timeslice", + "configurePreset": "native-timeslice" + }, + { + "name": "native-timeslice-tickless", + "configurePreset": "native-timeslice-tickless" + }, { "name": "native-gcc", "configurePreset": "native-gcc" @@ -375,6 +401,20 @@ "outputOnFailure": true } }, + { + "name": "native-timeslice", + "configurePreset": "native-timeslice", + "output": { + "outputOnFailure": true + } + }, + { + "name": "native-timeslice-tickless", + "configurePreset": "native-timeslice-tickless", + "output": { + "outputOnFailure": true + } + }, { "name": "native-gcc", "configurePreset": "native-gcc", diff --git a/configs/native-timeslice-tickless.conf b/configs/native-timeslice-tickless.conf new file mode 100644 index 0000000..2b0c0ac --- /dev/null +++ b/configs/native-timeslice-tickless.conf @@ -0,0 +1,8 @@ +# SPDX-License-Identifier: Apache-2.0 +# Copyright 2026 Junior Deogracias +# Time slicing with the tickless clock: the quantum is one more programmed deadline +# (SPEC-003 §8). Conformance only; the differential bridge needs the periodic clock +# (configs/native-timeslice.conf). +CONFIG_EMB_TIME_SLICING=y +CONFIG_EMB_TIMESLICE_TICKS=2 +CONFIG_EMB_TIMESLICE_PRIORITY=20 diff --git a/configs/native-timeslice.conf b/configs/native-timeslice.conf new file mode 100644 index 0000000..855e623 --- /dev/null +++ b/configs/native-timeslice.conf @@ -0,0 +1,10 @@ +# SPDX-License-Identifier: Apache-2.0 +# Copyright 2026 Junior Deogracias +# Round-robin time slicing on the deterministic native test port (KRN-SCH-007, 026, 037): +# a short quantum so a few ticks rotate, and a threshold so levels above 20 are not sliced. +CONFIG_EMB_TIME_SLICING=y +CONFIG_EMB_TIMESLICE_TICKS=2 +CONFIG_EMB_TIMESLICE_PRIORITY=20 +# Periodic clock: the quantum then counts delivered ticks exactly, as the model does. In +# tickless builds it starts from the free-running counter, which the model cannot see. +# CONFIG_EMB_TICKLESS is not set diff --git a/docs/STATUS.md b/docs/STATUS.md index 8f788c5..1be11b0 100644 --- a/docs/STATUS.md +++ b/docs/STATUS.md @@ -8,7 +8,7 @@ This page is the authoritative inventory of implementation and available evidenc | Area | Current implementation | Evidence and limits | |---|---|---| -| Execution and scheduling | UP fixed priority, base bitmap/FIFO scheduler, tiny thread table, scheduler lock, thread lifecycle; idle context unreachable through handles, and slim (control-block prefix only) on tiny without an idle thread (ADR-050) | Common conformance cases; tiny has unique base priorities and restricted scheduling semantics | +| Execution and scheduling | UP fixed priority, base bitmap/FIFO scheduler, tiny thread table, scheduler lock, thread lifecycle; idle context unreachable through handles, and slim (control-block prefix only) on tiny without an idle thread (ADR-050); optional round-robin time slicing below a threshold level (A63, off by default) | Common conformance cases; tiny has unique base priorities and restricted scheduling semantics; slicing is list-scheduler only, bridge-checked with the periodic clock and conformance-tested in both clock modes on native, not measured on hardware | | Waiting and time | Shared wait protocol, sleep, deadlines, cancellation, suspend overlay, ordered timeouts | Native virtual time exercises periodic and tickless modes; embedded ports currently reject tickless | | Synchronization | Semaphores, mutexes with inheritance, ceiling, recursion and owner-death policy; event flags with ANY/ALL/CLEAR waits and binding (M2-05); condition variables with the mandatory relock (M2-06) | Conformance and native differential bridge; inheritance and deadlock detection have a configured depth limit | | Communication | Copy-by-value message queues: direct hand-off to a waiting receiver, slot hand-off from a waiting sender, send to front, peek, `EMB_NO_WAIT` calls from ISRs and a receive-side binding (M2-07) | Conformance and native differential bridge; no pipes, buffer pools or zero-copy ownership queues; the masked copy time is bounded by configuration, not measured on hardware | diff --git a/docs/requirements/KRN-SCH.md b/docs/requirements/KRN-SCH.md index 4ae7214..7cdff99 100644 --- a/docs/requirements/KRN-SCH.md +++ b/docs/requirements/KRN-SCH.md @@ -39,8 +39,8 @@ KRN-SCH-036 to 043 originate in 03 §2 and are restated verbatim. KRN-SCH-001 to ### KRN-SCH-007 Optional round robin **Statement.** Round-robin time slicing among threads of equal effective priority shall be optional, selected by `CONFIG_EMB_TIME_SLICING`. **Rationale.** 03 §2.1 ("optional round-robin"); KRN-SCH-037 restricts where it applies. -**Status.** Accepted 2026-10-31 (restated); not implemented. -**Verification.** Test: planned round-robin rotation and quantum cases. +**Status.** Accepted 2026-10-31 (restated); implemented (A63), list scheduler only. +**Verification.** Test: `sched_quantum_expiry_rotates_behind_all_peers`, `sched_two_spinners_share_their_level` on `native-timeslice` and `native-timeslice-tickless`; model: the TIMESLICE scenarios, explored and checked by the differential bridge on `native-timeslice`. **Trace.** 03 §2.1; SPEC-003 §8; KRN-TIM-029; v0.1 §4 ### KRN-SCH-008 Yield never to lower priority @@ -102,8 +102,8 @@ KRN-SCH-036 to 043 originate in 03 §2 and are restated verbatim. KRN-SCH-001 to ### KRN-SCH-026 Quantum expiry rotates only among peers **Statement.** When a running thread's quantum expires, it shall move behind its equal-priority peers only if one is READY; otherwise its quantum shall be renewed. **Rationale.** SPEC-003 §8 (v0.1 §5.8). -**Status.** Accepted 2026-10-31 (restated); not implemented. -**Verification.** Test: planned quantum expiry cases with and without a peer. +**Status.** Accepted 2026-10-31 (restated); implemented (A63). +**Verification.** Test: `sched_quantum_expiry_rotates_behind_all_peers`, `sched_quantum_expiry_without_a_peer_renews`; model: `timeslice_rotates_equal_priority`, `timeslice_no_peer_renews_the_quantum`. **Trace.** SPEC-003 §8; KRN-TIM-029; v0.1 §5.8 ### KRN-SCH-036 Configurable priority count @@ -116,8 +116,8 @@ KRN-SCH-036 to 043 originate in 03 §2 and are restated verbatim. KRN-SCH-001 to ### KRN-SCH-037 Time slicing below a threshold **Statement.** Time slicing shall apply only to threads at or below a configured threshold priority level (`CONFIG_EMB_TIMESLICE_PRIORITY`), with one configurable quantum, so that round robin can be enabled for background levels only without a per-level table. **Rationale.** Revised per R-003 §3.1; answers 08 Q8. -**Status.** Accepted (03 §2.1); not implemented. -**Verification.** Test: planned quantum cases above and below the threshold. +**Status.** Accepted (03 §2.1); implemented with `CONFIG_EMB_TIMESLICE_PRIORITY` (A63). +**Verification.** Test: `sched_levels_above_the_threshold_are_not_sliced` and the cases at level 3 below the threshold; model: `timeslice_threshold_exempts_higher_levels`. **Trace.** 03 §2.1; R-003 §3.1 ### KRN-SCH-038 Class interface for the ready structure @@ -145,7 +145,7 @@ KRN-SCH-036 to 043 originate in 03 §2 and are restated verbatim. KRN-SCH-001 to **Statement.** A thread preempted by a higher-priority thread shall be placed ahead of its equal-priority peers when it becomes eligible again, because its quantum is unspent; a thread that yields or exhausts its quantum shall be placed behind them. **Rationale.** 03 §2.1. **Status.** Accepted (03 §2.1); implemented. -**Verification.** Test: `sched_preempted_thread_goes_ahead_of_its_peers`; model. +**Verification.** Test: `sched_preempted_thread_goes_ahead_of_its_peers`, `sched_quantum_expiry_rotates_behind_all_peers`; model: `timeslice_preempted_thread_keeps_its_place`. **Trace.** 03 §2.1 ### KRN-SCH-042 Tiny thread table diff --git a/docs/requirements/KRN-TIM.md b/docs/requirements/KRN-TIM.md index 7f43ee4..9fa75ef 100644 --- a/docs/requirements/KRN-TIM.md +++ b/docs/requirements/KRN-TIM.md @@ -209,8 +209,8 @@ KRN-TIM-001 to 007 originate in the v0.1 specification (§7.5); KRN-TIM-008 to 0 ### KRN-TIM-029 Time slicing quantum as a deadline **Statement.** When time slicing is enabled for the running thread's priority level, the kernel shall track its quantum expiry as a per-CPU deadline included in the next-deadline computation, and at expiry shall move the thread to the tail of its class only if another READY thread exists at the same effective priority. **Rationale.** Round-robin without a timer object per thread, and v0.1 §5.8's rule that an uncontested quantum does not rotate. -**Status.** Accepted 2026-10-07 -**Verification.** Test: round-robin ordering tests in both clock modes; uncontested quantum does not cause a switch. +**Status.** Accepted 2026-10-07; implemented (A63): the quantum is a per-CPU deadline in the tickless next-deadline computation and a comparison in the periodic tick. +**Verification.** Test: the time-slicing cases of `tests/conformance/test_sched.c` on `native-timeslice` (periodic) and `native-timeslice-tickless`; uncontested expiry: `sched_quantum_expiry_without_a_peer_renews`. **Trace.** SPEC-003 §8; KRN-SCH-007, KRN-SCH-026, KRN-SCH-037 ### KRN-TIM-030 Cycle counter API diff --git a/docs/specs/AMENDMENTS-M2.md b/docs/specs/AMENDMENTS-M2.md index dbcce84..08b3bf1 100644 --- a/docs/specs/AMENDMENTS-M2.md +++ b/docs/specs/AMENDMENTS-M2.md @@ -40,3 +40,4 @@ Corrections found while preparing the M2 primitives, where an accepted specifica | A60 | SPEC-003 §14, §15 | The reference model covers timers (ISR-context callbacks running model operations, work-queue callbacks through the embedded work item); the differential bridge follows timer starts, stops, expiries and handler runs as events. An exploration horizon stops time from advancing while a thread could run once a periodic timer has run long enough, as the runner does. The tiny profile has no timers in M2 (maintainer decision, 2026-10-27). | `tools/model/embmodel/kernel.py` | | A61 | SPEC-006 §4.1, §4.2, §4.3, KRN-WQ-007 | `emb_dwork_t` is a public `emb_work_t` (the handler's argument) followed by opaque storage for an internal ISR_CONTEXT timer. The queue is named at schedule time and holds a timer reference while the delay runs, so it cannot be destroyed. `schedule` returns `EMB_EEXIST` while the delay runs or the item is queued, `EMB_EBUSY` while its handler runs on another queue; `reschedule` replaces a running delay and returns `EMB_EEXIST` for a queued item. Cancel reports `EMB_WORK_PENDING` for a stopped delay or a removed item. The trace record is `EMB_TRACE_DWORK_SCHEDULE`; the delay's own start and expiry are the timer records. | `kernel/work/dwork.c`, `include/emb/work.h` | | A62 | KRN-SCH-036, 03 §2.1 | The priority count's lower bound is 2, as `CONFIG_EMB_PRIORITY_COUNT` has always allowed, not 4: idle plus one application level is a valid tiny configuration. Accepted by the project owner 2026-10-31. | `kernel/Kconfig` | +| A63 | SPEC-003 §8, KRN-SCH-007, KRN-SCH-026, KRN-SCH-037, KRN-SCH-041, KRN-TIM-029 | Time slicing is implemented with one quantum (`CONFIG_EMB_TIMESLICE_TICKS`) and one threshold (`CONFIG_EMB_TIMESLICE_PRIORITY`, 255 for every level). It requires the list scheduler: `CONFIG_EMB_TIME_SLICING` depends on `!CONFIG_EMB_SCHED_TABLE`, since a table level holds one thread. The quantum restarts at every dispatch, also for a preempted thread resuming ahead of its peers, and a yield without a peer keeps it running. Expiry renews the quantum and, with a READY peer, sets a per-CPU rotation flag that makes the next decision place the thread behind its peers. A thread raised above the threshold stops being sliced at its next expiry; one lowered below it starts at its next dispatch. The reference model implements the same rules; the differential bridge checks them with the periodic clock only (`native-timeslice`), because a tickless quantum starts from the free-running counter, which can run ahead of the ticks the model counts. Implemented 2026-10-31 at the project owner's request; the details await review. | `kernel/time/time.c`, `kernel/sched/sched.c`, `kernel/Kconfig` | diff --git a/docs/specs/SPEC-003-time-timeouts-and-timers.md b/docs/specs/SPEC-003-time-timeouts-and-timers.md index b8a8d08..1294848 100644 --- a/docs/specs/SPEC-003-time-timeouts-and-timers.md +++ b/docs/specs/SPEC-003-time-timeouts-and-timers.md @@ -237,7 +237,9 @@ Overruns are therefore counted in two cases: whole periods missed because the de ## 8. Time slicing hook -When `CONFIG_EMB_TIME_SLICING=y` and the running thread's priority level has a nonzero quantum (KRN-SCH-037), the per-CPU state holds `quantum_deadline`, set at dispatch to `now + quantum`. It is not a timer object: it is one more input to the next-deadline computation (tickless) or one more comparison in the tick ISR (periodic). At expiry, if another READY thread exists at the same effective priority, the running thread is moved to the tail of its class and `reschedule_pending` is set (v0.1 §5.8); otherwise the quantum is simply renewed. Temporal-protection budgets (03 §2.3) will plug into the same place when their specification lands. +When `CONFIG_EMB_TIME_SLICING=y` and the running thread's effective priority is at or below `CONFIG_EMB_TIMESLICE_PRIORITY` (KRN-SCH-037), the per-CPU state holds `quantum_deadline`, set at dispatch to `now + CONFIG_EMB_TIMESLICE_TICKS`. It is not a timer object: it is one more input to the next-deadline computation (tickless) or one more comparison in the tick ISR (periodic). At expiry, after the pass that expires timeouts and timers, the quantum is renewed; if another READY thread exists at the same effective priority, the scheduler also marks the running thread for rotation and sets `reschedule_pending`, and the decision at the outermost interrupt exit moves it to the tail of its class (v0.1 §5.8). With the scheduler locked, the rotation waits for the unlock. + +Details (A63): a thread gets a fresh quantum each time it is dispatched, including after a preemption, where it resumes ahead of its peers (KRN-SCH-041); a yield that finds no peer does not restart it. A thread raised above the threshold while running stops being sliced at its next expiry; one lowered below it is sliced from its next dispatch. In tickless mode `now` is the free-running counter, which may be ahead of the last tick the interrupt delivered. The table scheduler has one thread per level, so slicing requires the list scheduler. Temporal-protection budgets (03 §2.3) will plug into the same place when their specification lands. ## 9. Cycle counter diff --git a/docs/user/configuration.md b/docs/user/configuration.md index 8dc046b..aeea325 100644 --- a/docs/user/configuration.md +++ b/docs/user/configuration.md @@ -13,6 +13,8 @@ The configuration pipeline resolves Kconfig defaults seeded by a port manifest, | `native-clang` | Clang compiler coverage; requires Clang | | `native-asan` / `native-tsan` | Sanitizer configurations; require supported compiler runtimes | | `native-coverage` | GCC `--coverage` build; after CTest, `tools/coverage/report.py` prints kernel statement and branch coverage | +| `native-timeslice` | GCC, checked base with round-robin time slicing (quantum 2 ticks, levels up to 20) and a periodic clock, so the differential bridge checks rotation | +| `native-timeslice-tickless` | The same slicing with the tickless clock; conformance only | Use the same preset name for configure, build and CTest. A tiny result does not verify base-only features; a release result does not exercise checked-build faults. Embedded presets additionally require their cross-compiler, libc and emulator; do not interpret a build with no registered tests as conformance. @@ -33,6 +35,14 @@ The later [timer-delivery validation](../engineering/m2-01-timer-correction.md) | `CONFIG_EMB_TIMER` | y | software timers; not available with the table scheduler | | `CONFIG_EMB_OBJ_LIST` | y (n on tiny) | exact refusal of init on live storage | +## Scheduler options + +| Option | Default | Notes | +|---|---|---| +| `CONFIG_EMB_TIME_SLICING` | n | round robin among equal effective priorities; not available with the table scheduler | +| `CONFIG_EMB_TIMESLICE_TICKS` | 10 | the quantum, started at each dispatch | +| `CONFIG_EMB_TIMESLICE_PRIORITY` | 255 | the highest sliced level; higher levels run until they block or yield | + The tiny `footprint_t1` reference configuration turns event flags and message queues off. ## Add diagnostic options without changing the reference preset diff --git a/docs/user/tasks.md b/docs/user/tasks.md index 6c45602..1feb438 100644 --- a/docs/user/tasks.md +++ b/docs/user/tasks.md @@ -78,7 +78,7 @@ Expected output is `periodic: 5 iterations, exit=7`, followed by process exit st ## Choose priorities and deadlines deliberately -Application priorities are `1 .. EMB_PRIORITY_MAX`; larger is more urgent. A high-priority thread must block when it has no work. Yield rotates equal-priority peers and cannot let a lower-priority thread run. Tiny uses unique base-priority slots, so these two priorities also avoid a slot collision there. +Application priorities are `1 .. EMB_PRIORITY_MAX`; larger is more urgent. A high-priority thread must block when it has no work. Yield rotates equal-priority peers and cannot let a lower-priority thread run. With `CONFIG_EMB_TIME_SLICING`, a thread at or below `CONFIG_EMB_TIMESLICE_PRIORITY` that runs for a whole quantum without blocking also moves behind its READY equal-priority peers; it never lets a lower priority run either. Tiny uses unique base-priority slots, so these two priorities also avoid a slot collision there. Advancing `next` from the previous deadline keeps the schedule anchored. Sleeping for a relative period after each iteration adds the work time to the period. If work overruns an absolute deadline, `sleep_until()` yields and the next iteration catches up; it does not count misses, skip periods or impose an execution budget. Define an application policy for overruns. In a 32-bit time configuration, compare instants using `emb_instant_before()` and keep scheduled deadlines within `EMB_TIMEOUT_MAX_TICKS` ahead. Avoid the maximum tick value as a finite object-wait deadline: it is the current forever sentinel. diff --git a/kernel/Kconfig b/kernel/Kconfig index b32aa95..6e20c4f 100644 --- a/kernel/Kconfig +++ b/kernel/Kconfig @@ -46,15 +46,30 @@ config EMB_PRIORITY_COUNT With the table scheduler the count is bounded by the architecture word width. config EMB_TIME_SLICING - bool "Round-robin time slicing among equal priorities (KRN-SCH-037)" + bool "Round-robin time slicing among equal priorities (KRN-SCH-007, KRN-SCH-037)" + depends on !EMB_SCHED_TABLE default n + help + A thread at or below EMB_TIMESLICE_PRIORITY that runs for EMB_TIMESLICE_TICKS + without blocking, yielding or being preempted moves behind its equal-priority + peers (KRN-SCH-026). The quantum starts at dispatch. The table scheduler has one + thread per level, so it has no peers to rotate among. config EMB_TIMESLICE_TICKS - int "Default quantum in ticks" + int "Quantum in ticks" depends on EMB_TIME_SLICING default 10 range 1 65535 +config EMB_TIMESLICE_PRIORITY + int "Highest priority level that is time sliced" + depends on EMB_TIME_SLICING + default 255 + range 1 255 + help + KRN-SCH-037: slicing applies to threads whose effective priority is at or below + this level; 255 slices every level. Higher levels run until they block or yield. + config EMB_IDLE_THREAD bool "Dedicated idle thread (off: inline idle context, ADR-036)" default n if EMB_PROFILE_TINY diff --git a/kernel/exec/exec.c b/kernel/exec/exec.c index b573b9b..3d00194 100644 --- a/kernel/exec/exec.c +++ b/kernel/exec/exec.c @@ -70,6 +70,10 @@ void emb_kernel_start(void) embk_cpu.current = first; embk_cpu.reschedule_pending = 0u; embk_cpu.kernel_state = EMBK_KERNEL_RUNNING; +#if CONFIG_EMB_TIME_SLICING + embk_cpu.rotate = 0u; + embk_time_slice_start(first); +#endif #if CONFIG_EMB_CHECKED embk_cpu.irq_lock_depth = 0u; /* the first thread is a fresh context; the idle record is 0 too */ diff --git a/kernel/include/embk/kernel.h b/kernel/include/embk/kernel.h index 55cfd13..c5c8ed0 100644 --- a/kernel/include/embk/kernel.h +++ b/kernel/include/embk/kernel.h @@ -233,6 +233,9 @@ typedef struct embk_cpu { uint8_t sched_lock_depth; uint8_t reschedule_pending; uint8_t kernel_state; /* EMBK_KERNEL_* */ +#if CONFIG_EMB_TIME_SLICING + uint8_t rotate; /* the current thread's quantum expired: the next decision rotates it */ +#endif #if CONFIG_EMB_CHECKED uint8_t irq_lock_depth; /* critical-section nesting */ #endif diff --git a/kernel/include/embk/sched.h b/kernel/include/embk/sched.h index bc3a718..f5d506e 100644 --- a/kernel/include/embk/sched.h +++ b/kernel/include/embk/sched.h @@ -81,6 +81,12 @@ extern uint8_t embk_sched_raised_count; /* threads with eff_prio != base_prio; l #endif #endif +#if CONFIG_EMB_TIME_SLICING +/* The current thread's quantum expired, timer interrupt: with an equal-priority peer READY, + * the next decision moves it behind its peers (KRN-SCH-026). */ +void embk_sched_slice_expired(void); +#endif + /* A thread became runnable at priority @prio: should it preempt the current thread? */ bool embk_sched_should_preempt(uint8_t prio); diff --git a/kernel/include/embk/time.h b/kernel/include/embk/time.h index 24e120f..04dc6da 100644 --- a/kernel/include/embk/time.h +++ b/kernel/include/embk/time.h @@ -22,6 +22,12 @@ bool embk_timeout_next(emb_tick_t *out_deadline); /* Tickless: reprogram the hardware deadline from the next timeout, lock held. */ void embk_time_program(void); +#if CONFIG_EMB_TIME_SLICING +/* At dispatch, lock held: start the quantum of @t, or stop it for the idle context and + * levels above CONFIG_EMB_TIMESLICE_PRIORITY (SPEC-003 §8). */ +void embk_time_slice_start(const embk_thread_t *t); +#endif + #if CONFIG_EMB_TIMER /* The timer list (ADR-047), lock held: thread timeouts and timers expire together in * deadline order, threads first on equal deadlines. The arm records the current pass. */ diff --git a/kernel/sched/sched.c b/kernel/sched/sched.c index 2d366c0..f3d305b 100644 --- a/kernel/sched/sched.c +++ b/kernel/sched/sched.c @@ -17,6 +17,9 @@ #include #include #include +#if CONFIG_EMB_TIME_SLICING +#include +#endif #if !EMBK_IDLE_SLIM embk_thread_t embk_idle_thread; /* slim: sched/idle_context.c allocates the prefix only */ @@ -236,6 +239,10 @@ embk_thread_t *embk_sched_select(bool yield) bool runnable = cur != EMBK_IDLE && thread_runnable(cur); embk_cpu.reschedule_pending = 0u; +#if CONFIG_EMB_TIME_SLICING + yield = yield || embk_cpu.rotate != 0u; /* an exhausted quantum goes behind its peers */ + embk_cpu.rotate = 0u; +#endif if (runnable) { if (next == NULL || next->eff_prio < cur->eff_prio || (next->eff_prio == cur->eff_prio && !yield)) { @@ -260,6 +267,9 @@ embk_thread_t *embk_sched_select(bool yield) embk_cpu.irq_lock_depth = next->lock_depth; #endif embk_cpu.current = next; +#if CONFIG_EMB_TIME_SLICING + embk_time_slice_start(next); +#endif return next; } @@ -306,6 +316,21 @@ void embk_sched_yield_locked(void) } } +#if CONFIG_EMB_TIME_SLICING +void embk_sched_slice_expired(void) +{ + const embk_thread_t *cur = embk_cpu.current; + if (cur == EMBK_IDLE || !thread_runnable(cur) || + embk_list_is_empty(&ready_lists[cur->eff_prio])) { + return; /* no peer: the quantum is renewed */ + } + embk_cpu.rotate = 1u; + embk_cpu.reschedule_pending = 1u; + emb_arch_reschedule_pend(); /* SPEC-002 §6.2 step 2: decided at the outermost exit */ + EMBK_TRACE(EMB_TRACE_RESCHED_PEND, embk_thread_index(cur), 0u, 0u); +} +#endif + void embk_sched_prio_changed(embk_thread_t *t, uint8_t old_eff) { #if CONFIG_EMB_SCHED_TABLE diff --git a/kernel/time/time.c b/kernel/time/time.c index 2d9688f..f63f062 100644 --- a/kernel/time/time.c +++ b/kernel/time/time.c @@ -28,6 +28,10 @@ typedef struct embk_time_state { embk_list_t timers; /* software timers, ordered by deadline (ADR-047); lock: timeout domain */ uint8_t pass; /* counts expiry passes */ #endif +#if CONFIG_EMB_TIME_SLICING + emb_tick_t slice_deadline; /* the running thread's quantum end (SPEC-003 §8) */ + uint8_t slice_armed; +#endif #if CONFIG_EMB_TICKLESS emb_arch_timer_raw_t last_raw; /* counter value at which ticks was last exact */ uint32_t raw_per_tick; @@ -293,6 +297,62 @@ bool embk_timeout_next(emb_tick_t *out_deadline) return true; } +#if CONFIG_EMB_TIME_SLICING +/* KRN-SCH-037: is @t's level sliced? */ +#if CONFIG_EMB_TIMESLICE_PRIORITY >= 255 +#define SLICED(t) ((t) != EMBK_IDLE) +#else +#define SLICED(t) ((t) != EMBK_IDLE && (t)->eff_prio <= CONFIG_EMB_TIMESLICE_PRIORITY) +#endif + +void embk_time_slice_start(const embk_thread_t *t) +{ + uint8_t was = ts.slice_armed; + ts.slice_armed = SLICED(t) ? 1u : 0u; + if (ts.slice_armed != 0u) { + ts.slice_deadline = embk_time_ticks_locked() + (emb_tick_t)CONFIG_EMB_TIMESLICE_TICKS; + } +#if CONFIG_EMB_TICKLESS + if ((was | ts.slice_armed) != 0u) { + embk_time_program(); + } +#else + (void)was; +#endif +} + +/* After the expiry pass: an exhausted quantum is renewed, and the scheduler rotates the + * thread if it has a peer (KRN-SCH-026); a rotation starts the next thread's quantum. A + * thread raised above the threshold since its dispatch stops being sliced. */ +static void slice_check(emb_tick_t now) +{ + if (ts.slice_armed == 0u || embk_tick_before(now, ts.slice_deadline)) { + return; + } + if (!SLICED(embk_cpu.current)) { + ts.slice_armed = 0u; + return; + } + ts.slice_deadline = now + (emb_tick_t)CONFIG_EMB_TIMESLICE_TICKS; + embk_sched_slice_expired(); +} +#endif + +#if CONFIG_EMB_TICKLESS +/* The earliest deadline the hardware must wake for: a timeout, a timer or the quantum. */ +static bool next_deadline(emb_tick_t *out_deadline) +{ + bool armed = embk_timeout_next(out_deadline); +#if CONFIG_EMB_TIME_SLICING + if (ts.slice_armed != 0u && (!armed || embk_tick_before(ts.slice_deadline, *out_deadline))) { + *out_deadline = ts.slice_deadline; + armed = true; + } +#endif + return armed; +} +#endif + /* Expire every node whose deadline is at or before @now, in deadline order (§5.3): the * earlier of the two lists' heads first, a thread timeout first on equal deadlines, and * each timer at most once per pass (ADR-047). @key is the timeout lock, which an @@ -357,7 +417,7 @@ void embk_time_program(void) emb_tick_t next; emb_tick_t delta; emb_tick_t max = emb_arch_timer_max_ticks(); - if (!embk_timeout_next(&next)) { + if (!next_deadline(&next)) { emb_arch_timer_cancel(); return; } @@ -389,6 +449,9 @@ void embk_time_init(void) embk_list_init(&ts.timers); ts.pass = 0u; #endif +#if CONFIG_EMB_TIME_SLICING + ts.slice_armed = 0u; +#endif } void embk_time_start(void) @@ -420,6 +483,9 @@ void embk_time_timer_isr(void) EMBK_TRACE(EMB_TRACE_TICK, (uint32_t)ts.ticks, 0u, 0u); #endif expire(ts.ticks, &key); +#if CONFIG_EMB_TIME_SLICING + slice_check(ts.ticks); +#endif embk_time_program(); embk_unlock_timeout(key); } diff --git a/tests/conformance/test_sched.c b/tests/conformance/test_sched.c index 7733db7..def3037 100644 --- a/tests/conformance/test_sched.c +++ b/tests/conformance/test_sched.c @@ -1,6 +1,7 @@ /* SPDX-License-Identifier: Apache-2.0 */ /* Copyright 2026 Junior Deogracias */ -/* Scheduler conformance (03 §2, SPEC-002 §5, §6; KRN-SCH-001 to 008, 016 to 019, 041). */ +/* Scheduler conformance (03 §2, SPEC-002 §5, §6; KRN-SCH-001 to 008, 016 to 019, 026, 037, + * 041). */ #include static void mark_and_exit(void *arg) @@ -101,6 +102,70 @@ EMB_TEST(sched_preempted_thread_goes_ahead_of_its_peers) } #endif +#if CONFIG_EMB_TIME_SLICING +/* One quantum and a tick of margin: a sliced spinner is rotated before it finishes. */ +#define SLICE_SPIN ((uint32_t)CONFIG_EMB_TIMESLICE_TICKS + 1u) + +static void spinner(void *arg) +{ + int id = (int)(intptr_t)arg; + emb_test_mark(id); + emb_test_spin_ticks(SLICE_SPIN); + emb_test_mark(id + 10); +} + +EMB_TEST(sched_quantum_expiry_rotates_behind_all_peers) +{ + EMB_TEST_REQ("KRN-SCH-007", "KRN-SCH-026", "KRN-SCH-041"); + emb_sched_lock(); + (void)emb_test_thread(EMB_TEST_NAME("s1"), 3u, 0u, spinner, (void *)1); + (void)emb_test_thread(EMB_TEST_NAME("m2"), 3u, 0u, mark_and_exit, (void *)2); + (void)emb_test_thread(EMB_TEST_NAME("m3"), 3u, 0u, mark_and_exit, (void *)3); + emb_sched_unlock(); + emb_test_mark(9); + /* s1's quantum expires mid-spin: it goes behind both peers, which run first */ + EMB_ASSERT_MARKS(1, 2, 3, 11, 9); +} + +EMB_TEST(sched_quantum_expiry_without_a_peer_renews) +{ + EMB_TEST_REQ("KRN-SCH-026"); + emb_sched_lock(); + (void)emb_test_thread(EMB_TEST_NAME("s1"), 3u, 0u, spinner, (void *)1); + (void)emb_test_thread(EMB_TEST_NAME("m2"), 2u, 0u, mark_and_exit, (void *)2); + emb_sched_unlock(); + emb_test_mark(9); + /* expiry finds no READY thread at level 3: no switch, the lower thread waits */ + EMB_ASSERT_MARKS(1, 11, 2, 9); +} + +EMB_TEST(sched_two_spinners_share_their_level) +{ + EMB_TEST_REQ("KRN-SCH-007", "KRN-SCH-026"); + emb_sched_lock(); + (void)emb_test_thread(EMB_TEST_NAME("s1"), 3u, 0u, spinner, (void *)1); + (void)emb_test_thread(EMB_TEST_NAME("s2"), 3u, 0u, spinner, (void *)2); + emb_sched_unlock(); + emb_test_mark(9); + /* each spins past its quantum, so each is rotated once before it finishes */ + EMB_ASSERT_MARKS(1, 2, 11, 12, 9); +} + +#if CONFIG_EMB_TIMESLICE_PRIORITY < CONFIG_EMB_PRIORITY_COUNT - 1 +EMB_TEST(sched_levels_above_the_threshold_are_not_sliced) +{ + uint8_t p = (uint8_t)(CONFIG_EMB_TIMESLICE_PRIORITY + 1); + EMB_TEST_REQ("KRN-SCH-037"); + emb_sched_lock(); + (void)emb_test_thread(EMB_TEST_NAME("s1"), p, 0u, spinner, (void *)1); + (void)emb_test_thread(EMB_TEST_NAME("m2"), p, 0u, mark_and_exit, (void *)2); + emb_sched_unlock(); + emb_test_mark(9); + EMB_ASSERT_MARKS(1, 11, 2, 9); /* FIFO only: the spinner keeps the processor */ +} +#endif +#endif + EMB_TEST(sched_blocking_under_scheduler_lock_is_misuse) { EMB_TEST_REQ("KRN-SCH-019", "API-013"); diff --git a/tests/differential/CMakeLists.txt b/tests/differential/CMakeLists.txt index 2b958fb..41c1b7a 100644 --- a/tests/differential/CMakeLists.txt +++ b/tests/differential/CMakeLists.txt @@ -5,7 +5,9 @@ if(CONFIG_EMB_ARCH_NATIVE AND CONFIG_EMB_TRACE AND CONFIG_EMB_SEM AND CONFIG_EMB emb_add_executable(diff_runner diff_runner.c) target_link_libraries(diff_runner PRIVATE emb_kernel_private) # periodic idle timeout peek find_package(Python3 COMPONENTS Interpreter QUIET) - if(Python3_Interpreter_FOUND) + # The model counts delivered ticks; a tickless quantum starts from the counter, so the + # bridge skips every scenario there (bridge.applicable) and the checks are not registered. + if(Python3_Interpreter_FOUND AND NOT (CONFIG_EMB_TIME_SLICING AND CONFIG_EMB_TICKLESS)) add_test(NAME differential_bridge COMMAND "${Python3_EXECUTABLE}" -I "${CMAKE_SOURCE_DIR}/tools/model/bridge.py" --runner "$" --runs 6 --seed 1) diff --git a/tests/differential/diff_runner.c b/tests/differential/diff_runner.c index 03584b6..372a554 100644 --- a/tests/differential/diff_runner.c +++ b/tests/differential/diff_runner.c @@ -1212,6 +1212,17 @@ static void isr_body(void *arg) /* ---- the dump ------------------------------------------------------------------------ */ +/* Only time-slicing builds print the fields, so other captures stay byte-identical. */ +#if CONFIG_EMB_TIME_SLICING +#define TIMESLICE_STR_(x) #x +#define TIMESLICE_STR(x) TIMESLICE_STR_(x) +#define TIMESLICE_CONFIG \ + " timeslice=" TIMESLICE_STR(CONFIG_EMB_TIMESLICE_TICKS) " timeslice_prio=" TIMESLICE_STR( \ + CONFIG_EMB_TIMESLICE_PRIORITY) +#else +#define TIMESLICE_CONFIG "" +#endif + static void dump(const char *end, unsigned long e0, unsigned long e1) { unsigned i; @@ -1221,7 +1232,7 @@ static void dump(const char *end, unsigned long e0, unsigned long e1) } dumped = 1u; (void)printf("config profile=%s owner_death=%s checked=%d tickless=%d idle_index=254 events=%d " - "conds=%d msgqs=%d workqs=%d timers=%d\n", + "conds=%d msgqs=%d workqs=%d timers=%d%s\n", CONFIG_EMB_PROFILE, #if CONFIG_EMB_MUTEX_OWNER_DEATH_FAULT && CONFIG_EMB_CHECKED "fault", @@ -1230,7 +1241,7 @@ static void dump(const char *end, unsigned long e0, unsigned long e1) #endif (int)CONFIG_EMB_CHECKED, (int)CONFIG_EMB_TICKLESS, (int)CONFIG_EMB_EVENT, (int)CONFIG_EMB_COND, (int)CONFIG_EMB_MSGQ, (int)CONFIG_EMB_WORKQ, - (int)CONFIG_EMB_TIMER); + (int)CONFIG_EMB_TIMER, TIMESLICE_CONFIG); n = event_count; for (i = 0u; i < n; i++) { (void)printf("ev %u %u %lu %lu %lu %lu\n", (unsigned)events[i].id, diff --git a/tests/framework/emb_test.c b/tests/framework/emb_test.c index a1584ce..81394af 100644 --- a/tests/framework/emb_test.c +++ b/tests/framework/emb_test.c @@ -5,6 +5,9 @@ #include #include +#if CONFIG_EMB_ARCH_NATIVE +#include +#endif EMB_TABLE_BOUNDS(const emb_test_case_t, emb_test_table); @@ -87,6 +90,17 @@ void emb_test_check_elapsed(unsigned line, uint32_t elapsed, uint32_t expected) } } +void emb_test_spin_ticks(uint32_t n) +{ + uint32_t t0 = EMB_TEST_NOW(); + /* bounded by @n ticks of the kernel clock */ + while ((uint32_t)(EMB_TEST_NOW() - t0) < n) { +#if CONFIG_EMB_ARCH_NATIVE + emb_native_tick(); +#endif + } +} + /* ---- marks ------------------------------------------------------------------------ */ static int marks[EMB_TEST_MARKS_MAX]; /* lock: pushed from any context; the runner reads when all diff --git a/tests/framework/emb_test.h b/tests/framework/emb_test.h index 7558856..f1466f0 100644 --- a/tests/framework/emb_test.h +++ b/tests/framework/emb_test.h @@ -135,6 +135,11 @@ void emb_test_check_elapsed(unsigned line, uint32_t elapsed, uint32_t expected); #define EMB_ASSERT_ELAPSED(t0, n) \ emb_test_check_elapsed(__LINE__, (uint32_t)(EMB_TEST_NOW() - (uint32_t)(t0)), (uint32_t)(n)) +/* Run without blocking until @n ticks have passed since the call: a busy thread that a + * time slice can rotate. Native time is virtual and advances only in idle, so there the + * helper raises the ticks itself. */ +void emb_test_spin_ticks(uint32_t n); + /* Software interrupts for the tests: a handler bound to a slot, raised on demand. * Delivery follows the port's rules: at once when unmasked, at the unlock when masked, * held while the slot is disabled. */ diff --git a/tools/evidence/configurations.json b/tools/evidence/configurations.json index 9492e4e..fe9325b 100644 --- a/tools/evidence/configurations.json +++ b/tools/evidence/configurations.json @@ -6,6 +6,8 @@ "native-release": {"target": "native", "scope": "host", "profile": "base", "checked": false}, "native-tiny": {"target": "native", "scope": "host", "profile": "tiny", "checked": true}, "native-periodic": {"target": "native", "scope": "host", "profile": "base", "checked": true}, + "native-timeslice": {"target": "native", "scope": "host", "profile": "base", "checked": true}, + "native-timeslice-tickless": {"target": "native", "scope": "host", "profile": "base", "checked": true}, "native-asan": {"target": "native", "scope": "host", "profile": "base", "checked": true}, "native-tsan": {"target": "native", "scope": "host", "profile": "base", "checked": true}, "native-coverage": {"target": "native", "scope": "host", "profile": "base", "checked": true}, diff --git a/tools/model/bridge.py b/tools/model/bridge.py index 4af5bb6..83c36a5 100644 --- a/tools/model/bridge.py +++ b/tools/model/bridge.py @@ -761,6 +761,10 @@ def applicable(sc: Scenario, config: dict) -> tuple: return False, "work queues are not configured in this build" if sc.timers and config.get("timers", "0") != "1": return False, "software timers are not configured in this build" + if config.get("timeslice", "0") != "0" and config.get("tickless", "1") == "1": + # A tickless quantum starts from the free-running counter, which can run ahead of the + # delivered ticks the model counts; native-timeslice checks slicing with a periodic clock. + return False, "time slicing is modeled with a periodic clock only" if profile == "tiny": if len(set(prios)) != len(prios): return False, "shared priorities need the base profile" @@ -782,8 +786,11 @@ def adapt(sc: Scenario, config: dict) -> Scenario: msgqs = {qid: dict(cfg, policy=Policy.BITMAP) for qid, cfg in sc.msgqs.items()} sc = replace(sc, sems=sems, events=events, conds=conds, msgqs=msgqs) # Historical native captures predate the clock-mode field and used tickless builds. + # Time slicing follows the build too; captures without the field had none. + quantum = int(config.get("timeslice", "0")) return replace(sc, owner_death=config.get("owner_death", "release"), - tickless=config.get("tickless", "1") == "1") + tickless=config.get("tickless", "1") == "1", + quantum=quantum or None, slice_prio=int(config.get("timeslice_prio", "255"))) def timer_regressions() -> list: diff --git a/tools/model/embmodel/kernel.py b/tools/model/embmodel/kernel.py index 3e0445f..684cb86 100644 --- a/tools/model/embmodel/kernel.py +++ b/tools/model/embmodel/kernel.py @@ -593,11 +593,14 @@ class Scenario: inactive: tuple = () # tids created INACTIVE (must be started by another thread or an ISR) name: str = "" tickless: bool = True # already-due compares request a timer interrupt + quantum: Optional[int] = None # CONFIG_EMB_TIMESLICE_TICKS; None: no time slicing + slice_prio: int = 255 # CONFIG_EMB_TIMESLICE_PRIORITY (KRN-SCH-037) def build(sc: Scenario) -> "Kernel": k = Kernel(programs={tid: tuple(p) for tid, (_, p) in sc.threads.items()}, isr_bodies=tuple(sc.isrs), - owner_death=sc.owner_death, tickless=sc.tickless, horizon=sc.horizon) + owner_death=sc.owner_death, tickless=sc.tickless, horizon=sc.horizon, + quantum=sc.quantum, slice_prio=sc.slice_prio) for tid, (prio, _) in sc.threads.items(): k.threads[tid] = Thread(tid=tid, prio=prio, base_prio=prio, inactive=(tid in sc.inactive)) k.queues[-(tid + 1)] = WaitQueue(qid=-(tid + 1), policy=Policy.FIFO) # SLEEP / NOTIFY / START @@ -707,6 +710,10 @@ class Kernel: trace: list = field(default_factory=list) in_expiry: bool = False # transient: inside a timer's expiry, not part of the key horizon: Optional[int] = None # static: the scenario's tick bound for periodic timers + quantum: Optional[int] = None # static: the time-slice quantum, None when off + slice_prio: int = 255 # static: the highest sliced level + slice_deadline: Optional[int] = None # the running thread's quantum end (SPEC-003 §8) + rotate: bool = False # the quantum expired: the next decision rotates # ------------------------------------------------------------------ state identity def key(self): @@ -723,7 +730,8 @@ def key(self): tuple((p, tuple(v)) for p, v in sorted(self.ready.items()) if v), self.current, self.now, self.irq_nesting, self.sched_lock_depth, self.reschedule_pending, tuple(self.timeouts), self.timer_pending, self.dequeued, - self.stale_timeouts, self.isr_fired, self.pi_depth_max) + self.stale_timeouts, self.isr_fired, self.pi_depth_max) + \ + (((self.slice_deadline, self.rotate),) if self.quantum else ()) def clone(self) -> "Kernel": k = copy.copy(self) @@ -783,19 +791,42 @@ def _best_ready(self) -> Optional[int]: def dispatch(self): cur = self.threads.get(self.current) if self.current is not None else None best_tid = self._best_ready() + rotate, self.rotate = self.rotate, False # an exhausted quantum goes behind its peers if cur is not None and self.runnable(cur): - if best_tid is None or self.threads[best_tid].prio <= cur.prio: + best = self.threads[best_tid] if best_tid is not None else None + if best is None or best.prio < cur.prio or (best.prio == cur.prio and not rotate): self.reschedule_pending = False return - self._make_ready(cur, preempted=True) + self._make_ready(cur, preempted=not rotate) if best_tid is None: self.current = None else: self.ready[self.threads[best_tid].prio].pop(0) self.current = best_tid self.reschedule_pending = False + self._slice_start() self._event("switch", self.current) + def _slice_start(self): + """At dispatch: the quantum of a thread at or below the threshold (KRN-SCH-037).""" + cur = self.threads.get(self.current) if self.current is not None else None + sliced = self.quantum and cur is not None and cur.prio <= self.slice_prio + self.slice_deadline = self.now + self.quantum if sliced else None + + def _slice_check(self): + """After the expiry pass: renew an exhausted quantum, and rotate with a READY peer + (KRN-SCH-026); a thread raised above the threshold since dispatch stops being sliced.""" + if self.slice_deadline is None or self.now < self.slice_deadline: + return + cur = self.threads.get(self.current) if self.current is not None else None + if cur is None or cur.prio > self.slice_prio: + self.slice_deadline = None + return + self.slice_deadline = self.now + self.quantum + if self.runnable(cur) and self.ready.get(cur.prio): + self.rotate = True + self.reschedule_pending = True + def reschedule_if_needed(self): if self.reschedule_pending and self.sched_lock_depth == 0: self.dispatch() @@ -1277,9 +1308,12 @@ def _op_sleep(self, t: Thread, op: Sleep) -> bool: return self._block_section(t, q, Reason.SLEEP, op.ticks, lambda: False, lambda: 0) def _op_yield(self, t: Thread): + deadline = self.slice_deadline self._make_ready(t, preempted=False) self.current = None self.dispatch() + if self.current == t.tid: + self.slice_deadline = deadline # no peer: no switch, the quantum runs on self._advance(t) def _op_setprio(self, op: SetPrio): @@ -1965,6 +1999,7 @@ def _expire_due(self): self.wake_timeout(th[2], th[3]) for t in self.timers.values(): t.armed_in_pass = False + self._slice_check() self.irq_nesting -= 1 self._p1() @@ -2221,9 +2256,12 @@ def enabled(self) -> list: # A periodic timer keeps a tick enabled forever. The runner advances time only when # idle or by one of its few scheduled ticks, so past the scenario's horizon the model # ticks only while idle. + # A running quantum does the same. periodic = any(t.deadline is not None and t.period for t in self.timers.values()) - past = periodic and self.horizon is not None and self.now >= self.horizon - if (self.timeouts or any(t.deadline is not None for t in self.timers.values())) and \ + unbounded = periodic or self.slice_deadline is not None + past = unbounded and self.horizon is not None and self.now >= self.horizon + if (self.timeouts or self.slice_deadline is not None or + any(t.deadline is not None for t in self.timers.values())) and \ not (past and self.current is not None): acts.append(("tick",)) return acts diff --git a/tools/model/evidence.py b/tools/model/evidence.py index ebb12af..9edacb7 100644 --- a/tools/model/evidence.py +++ b/tools/model/evidence.py @@ -55,6 +55,8 @@ def program(ops): body=program(cfg.get("body", ())))) for t, cfg in sc.timers.items()] if sc.horizon is not None: data["horizon"] = sc.horizon + if sc.quantum is not None: # and time slicing + data["timeslice"] = dict(quantum=sc.quantum, priority=sc.slice_prio) return data @@ -92,6 +94,11 @@ def objects(items, enum_field=None, enum_type=None): if not threads: raise ValueError("a scenario needs at least one thread") from embmodel import Protocol + timeslice = raw.get("timeslice", {"quantum": None, "priority": 255}) + if set(timeslice) != {"quantum", "priority"} or \ + (timeslice["quantum"] is not None and type(timeslice["quantum"]) is not int) or \ + type(timeslice["priority"]) is not int: + raise ValueError("invalid time-slicing configuration") return bridge.Scenario(name=raw["name"], threads=threads, sems=objects(raw["sems"], "policy", bridge.Policy), mutexes=objects(raw["mutexes"], "protocol", Protocol), @@ -105,7 +112,8 @@ def objects(items, enum_field=None, enum_type=None): horizon=raw.get("horizon"), isrs=tuple(program(ops) for ops in raw["isrs"]), inactive=tuple(raw["inactive"]), owner_death=raw["owner_death"], - tickless=raw["tickless"]) + tickless=raw["tickless"], quantum=timeslice["quantum"], + slice_prio=timeslice["priority"]) def sha256(path): diff --git a/tools/model/tests/scenarios.py b/tools/model/tests/scenarios.py index 81b08da..2239e4a 100644 --- a/tools/model/tests/scenarios.py +++ b/tools/model/tests/scenarios.py @@ -849,3 +849,55 @@ def combined_dwork_cancel_races_expiry(): combined_destroy_timeout_and_isr_give, combined_bindings_two_sources, combined_timer_feeds_handler_queue, combined_dwork_cancel_races_expiry] ALL = ALL + COMBINED + + +# --------------------------------------------------------------------------------------- +# M2 leftover: round-robin time slicing (KRN-SCH-007, KRN-SCH-026, KRN-SCH-037, SPEC-003 §8). +# The quantum and the threshold are the scenario's static configuration; the bridge replaces +# them with the build's, so on builds without slicing these run unsliced. +# --------------------------------------------------------------------------------------- +from dataclasses import replace # noqa: E402 + + +def timeslice_rotates_equal_priority(): + """Two threads at one level: once the first's quantum expires the second may run before + the first has given, so its no-wait take can fail; without ticks it never does.""" + return Scenario(name="timeslice_rotates_equal_priority", + threads={1: (2, (Give(0), Give(0), Give(0))), 2: (2, (Take(0, NO_WAIT),))}, + sems={0: dict(count=0)}, quantum=1, horizon=4) + + +def timeslice_threshold_exempts_higher_levels(): + """The same threads above the threshold level are never sliced (KRN-SCH-037).""" + return replace(timeslice_rotates_equal_priority(), name="timeslice_threshold_exempts_higher_levels", + slice_prio=1) + + +def timeslice_no_peer_renews_the_quantum(): + """Expiry without an equal-priority peer renews the quantum: the lower thread waits.""" + return Scenario(name="timeslice_no_peer_renews_the_quantum", + threads={1: (2, (Give(0), Give(0), Give(0))), 2: (1, (Take(0, NO_WAIT),))}, + sems={0: dict(count=0)}, quantum=1, horizon=4) + + +def timeslice_preempted_thread_keeps_its_place(): + """A sliced thread preempted by a sleeper's wake goes back ahead of its peer (KRN-SCH-041); + a fresh quantum starts when it runs again.""" + return Scenario(name="timeslice_preempted_thread_keeps_its_place", + threads={1: (2, (Give(0), Give(0))), 2: (2, (Take(0, NO_WAIT), Take(0, NO_WAIT))), + 3: (3, (Sleep(1), Give(1)))}, + sems={0: dict(count=0), 1: dict(count=0)}, quantum=2, horizon=4) + + +def timeslice_yield_and_isr_wake_at_expiry(): + """A yield, an ISR-made-ready peer and an expiring quantum at the same instants.""" + return Scenario(name="timeslice_yield_and_isr_wake_at_expiry", + threads={1: (2, (Give(0), Yield(), Give(0))), 2: (2, (Take(0), Take(0, 2)))}, + sems={0: dict(count=0)}, quantum=1, horizon=3, + isrs=((Give(0),),)) + + +TIMESLICE = [timeslice_rotates_equal_priority, timeslice_threshold_exempts_higher_levels, + timeslice_no_peer_renews_the_quantum, timeslice_preempted_thread_keeps_its_place, + timeslice_yield_and_isr_wake_at_expiry] +ALL = ALL + TIMESLICE diff --git a/tools/model/tests/test_explore.py b/tools/model/tests/test_explore.py index 815eff0..5608237 100644 --- a/tools/model/tests/test_explore.py +++ b/tools/model/tests/test_explore.py @@ -1,5 +1,6 @@ """Exhaustive exploration of every scenario (KRN-WAIT-007, KRN-WAIT-022) and outcome checks.""" import unittest +from dataclasses import replace from embmodel import Result, build, explore from tests import scenarios as S @@ -647,3 +648,51 @@ def test_dwork_cancel_racing_expiry_runs_at_most_once(self): if w[0] == 0: self.assertNotEqual(d[1][1][1], Result.SATISFIED) # canceled: nothing gave self.assertEqual(seen, {0, 1}) + + +class TimeSlicing(unittest.TestCase): + """Round-robin time slicing (KRN-SCH-007, KRN-SCH-026, KRN-SCH-037, KRN-SCH-041).""" + + @staticmethod + def takes(make): + return {dict(dict(o)["threads"])[2][0][1] for o in explore(make()).outcomes} + + def test_every_timeslice_scenario_holds_invariants(self): + for make in S.TIMESLICE: + sc = make() + with self.subTest(scenario=sc.name): + self.assertGreater(explore(sc).terminals, 0) + + def test_expiry_rotates_to_an_equal_priority_peer(self): + self.assertEqual(self.takes(S.timeslice_rotates_equal_priority), {Result.SATISFIED, Result.TIMEOUT}) + + def test_levels_above_the_threshold_are_not_sliced(self): + self.assertEqual(self.takes(S.timeslice_threshold_exempts_higher_levels), {Result.SATISFIED}) + + def test_expiry_without_a_peer_renews(self): + self.assertEqual(self.takes(S.timeslice_no_peer_renews_the_quantum), {Result.SATISFIED}) + + def test_without_slicing_the_first_thread_runs_to_completion(self): + sc = S.timeslice_rotates_equal_priority() + self.assertEqual({dict(dict(o)["threads"])[2][0][1] for o in explore(replace(sc, quantum=None)).outcomes}, + {Result.SATISFIED}) + + def test_rotation_goes_behind_peers_and_preemption_ahead(self): + k = build(S.timeslice_preempted_thread_keeps_its_place()) + while k.current == 3: # 3 sleeps; 1 runs + k.apply(("run",)) + self.assertEqual((k.current, k.slice_deadline, k.ready[2]), (1, k.now + 2, [2])) + k.apply(("tick",)) # 3 wakes and preempts 1 + self.assertEqual((k.current, k.ready[2]), (3, [1, 2])) # 1 ahead of its peer + while k.current == 3: # 3 gives and exits + k.apply(("run",)) + self.assertEqual((k.current, k.slice_deadline), (1, k.now + 2)) # a fresh quantum + k.apply(("tick",)) + k.apply(("tick",)) # expiry: behind 2 + self.assertEqual((k.current, k.ready[2]), (2, [1])) + + def test_yield_without_a_peer_keeps_the_quantum(self): + k = build(S.timeslice_no_peer_renews_the_quantum()) + k.slice_deadline = 5 + k._op_yield(k.threads[1]) + self.assertEqual((k.current, k.slice_deadline), (1, 5))