The scheduler cannot correctly schedule once the timestamp exceeds
MAX_RELEASE_TIME as releases beyond this point may be subject to
overflow. For most systems this should still allow a great many years if
the timestamp starts from 0 at system boot.
Some systems currently start with a random initial timestamp and my
begin with a timestamp that prvents correct budgeting. This assert helps
to catch cases where scheduling becomes invalid due to the timestamp
exceeding the give bound.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The proofs currently only guarantee that the system scheduler is correct
while the current time is less than INT64_MAX - 3 * MAX_PERIOD ticks.
With the MAX_PERIOD configured to almost INT64_MAX, this would imply
that the system scheduler is never correct.
To ensure that we get a large duration where the system is correct, we
take 1/8th of the TOTAL representable time as the MAX_PERIOD, ensuring
that 3 * MAX_PERIOD is still less than half of all representable time.
For a system with a 1MHz scheduling clock, this produces a valid
execution time on the order of 2^19 years.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This re-introduces the overrun handling but bounds charging of budget
such that we never calculate a refill with a start using an integer
overflow.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
A refill can still be charged if the refill list is full. This means
that we only require sufficient capacity to continue a timeslice.
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This replaces the refill_split_check and refill_budget_check with a
single function that chanrges the provided usage to an SC and updates
the refills.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
When ksDomainTime reaches 0 the current domain expires and the next
domain is switched to. This change performs the domain time accounting
in one place, in updateTimestamp, and avoids situations where ksConsumed
is reset without also updating ksDomainTime such as in chargeBudget.
Calling rescheduleRequired in the domain expires ensures that a new
thread will be chosen in the scheduler after the domain has been
advanced. Any remaining ksConsumed will be charged to the outgoing
scheduling context when it is switched away from.
Signed-off-by: Kent McLeod <kent@kry10.com>
Rather than charge consumed time to the current thread at the point
where it is exhausted in a long-running syscall, we only check whether
checkBudget would fail and raise an exception if it would. We then
always charge after handleInvocation rather than avoid-double charging.
This is done as it is easier to add the exhaustion case in the abstract
spec in this manner (without also adding changes to the current SC).
Signed-off-by: Curtis Millar <curtis@curtism.me>
As this variable bounds both the period and the budget and the period
itself bounds the budget, the name for this variable would be more
appropriately named 'MAX_PERIOD'
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This adds a flags parameter to SchedControl_Configure to enable
configuration of a sporadic SC.
This also allows flags to be added in the future as needed without
breaking the API.
This allows the user to configure an SC either to be constrained as a
sporadic task where accumulated time is only delayed to when a task has
become runnable (implementing the sporadic server algorithm) or
whenever the task becomes the current executing task (implementing the
sliding-window constraint as in constant-bandwidth servers).
This can be used to prevent non-realtime tasks from exceeding bandwidth
under any circumstances, even in an over-committed configuration, whilst
also allowing work-conserving tasks to be configured in the same system.
To implement sporadic servers, we need to ensure that the suspension of
a task cannot be used as a mechanism to amplify budget of a task by
granting that task access to effectively multiple periods worth of
replenishments within a single period.
To align the implementation of SCs with the model of sporadic servers we
must delay available time until the release of a task. Within seL4, a
release would be any time where an SC changes from not being associated
with a Running, RunningVM, or Restart thread to one that is.
This can occur when an SC is bound to a new thread in such a state or
when a thread changes to such a state from any non-running states.
Critically, replenishments should not be delayed at the point when an SC
becomes the current SC (as was the case prior to this commit). This has
the effect of enforcing a continuous, constant bandwidth which is a
restriction that is incompatible with standard scheduling logic.
Accounting for this requires inserting a new refill_unblock_check
call whenever a sporadic SC is unblocked and removing the
refill_unblock_check call from when said SC is scheduled.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
A 'released' SC is one that has been configured with its head refill in
the past.
An 'active' checking function checks for whether an SC has been
configured.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This removes the explicit CMake configuration for the kernel log buffer
and replaces it with a #define that is enabled for the required
configurations.
Signed-off-by: Curtis Millar <curtis@curtism.me>
A previous commit produced some build errors, since it converted the
`REFILL_HEAD` and `REFILL_TAIL` macros to functions returning
`refill_t`, and the results were used as lvalues. This commit returns
pointers instead, and also converts `REFILL_INDEX` to a function.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
SimplExportAndRefine can't handle the level of pointer arithmetic being
performed by `REFILL_INDEX` if it's literally inlined into a function,
however it *can* handle that arithmetic if it's in a separate function.
Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
The capacity does not need to be passed as an argument to
refill_check_budget as all information that it was being used for can be
dertermined from the usage directly.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
We need to bound the time the user provides to configure scheduling
contexts to avoid malicious or erraneous overflows of the scheduling
math. Make the max period/budget 1 hour.
1 hour is sufficiently small that it will fit in a 32-bit error message.
1 week is sufficiently small for 64-bit platforms.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
For each thread also track number of times scheduled, number of kernel
entries and amount of cycles spent inside the kernel. Also add
core-wide totals for each.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
This changes the semantics if `isBlocked` to not include the 'inactive'
state when it returns true. The old semantics for isBlocked are provided
by `isStopped`.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
All time for an SC should be relative to its assigned core. Any
operations which may occur on an SC on a remote core must explicitly
refer to that core.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The starting and ready times for any SC should be relative to the core
on which the SC is running rather than the current core.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
All the kernel header files now use pargma once rather than the ifndef,
as the pre-processed C files do not change while header files
are protected with pargma once. This will also solve any naming issues
caused by ifndef.
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
Currently on x86 device untypeds are generated by passing the entire
address space minus any parts that are reserved by the kernel or that
are "real" memory (e.g. kernel image, physical RAM).
On ARM and RISC-V, device untypeds were generated at compile-time from
a device tree. This patch moves ARM and RISC-V to use the same approach
as x86, and moves the code from x86 into a common location that's
shared between the three architectures.
Co-Authored-By: Anna Lyons <anna@gh.st>
ChargeBudget can be called after a preemption, but the preemption may
have deleted the scheduling context. Do not charge scheduling contexts
that have been deleted (check scRefillMax).
Preemption can be via the timer interrupt. In this case we need to
update the timestamp so we can reprogram the timer for the next timeout
and guarantee it is in the future, otherwise we will end up setting a
timeout in the past.
- seL4_TCB_Configure no longer takes a fault endpoint.
- seL4_TCB_SetSpace takes a cap in the callers cspace for the
fault endpoint, not the target tcbs.
- seL4_TCB_SetSchedParams now also takes a fault endpoint as above.
This change installs the fault endpoint cap into the tcb cnode
first validating it.
This means either of the functions that set it will now return an error
if the cap is not either a null cap or an endpoint with send and
grant rights.
Significantly, the cap passed to the function should be in the callers
cspace, not the target tcbs.
This allows users to define custom amounts of refills without
increasing the scheduling context size system wide.
also add libsel4 functions for refill size
This is a list of fixes that came up while working on the verification
spec for the mcs changes.
- trigger a timer tick if we are unable to split a refill
due to the refill list being full.
- make refill_ordered more useful
- pull the thread out of the scheduler before updating it
- simplify refill logic at verifications request
- Add unused to refill_sum
- Don't refill_split_check if consumed is empty
- sched_control: fix double increment bug
- sched-control: charge before reconfiguring ksCurSC
- Charge round robin threads differently
Sporadic server refill rules do not behave correctly for round robin
threads, instead, change the logic. Round robin threads have 2 refills:
current and next.
This changes the budget/remaining fields in scheduling contexts
to contain timer ticks, not number of abstract sel4ticks.
seL4_SchedControl_Configure now takes microseconds, not ticks.
This commit is plat-independant - the platform and arch specific
timer code follows in later commits.
This is the first part of the seL4 MCS. This commit:
* adds a scheduling context object. Threads without scheduling
context objects cannot be scheduled.
* replaces tcbTimeSlice with the scheduling context object
* adds seL4_SchedControl caps for each core
* adds seL4_SchedControl_Configure which allows users to configure
amount of ticks a scheduling context has, and set a core for the
scheduling context.
* adds seL4_SchedContext_Bind, Unbind and UnbindObject, which allows
a tcb to be bound to a scheduling context.
This change allows us to know, from just the kernel and dtb, where user
level untyped objects start being allocated from.
- allocate rootserver objects from last available freemem region.
- move create_rootserver_objects call into init_freemem.
Previously, the boot allocator would do dynamic calculations to
minimise fragmentation, then throw away the smallest regions.
With the new boot allocator, we can reasonably predict that
fragmentation will create at most one extra region, so this commit
adds one freemem slot for ARM.
Prior to this change, the boot process would dynamically allocate
memory for root server objects based on the order of initialisation.
Allocation was a best-fit algorithm.
This change preallocates all memory for root server objects to an
aligned untyped just after the user image. By allocating the objects in
order of size, allocation is greatly simplified and the ability to
reproduce the allocation offline based on the kernel and user image
sizes is increased.
Fixes a case where a thread can go from Running->Inactive->Restart and use a restart PC
that is out of date. An out of date restart PC occurs when a thread was transitioned to
running after being in a blocked state, but was never scheduled and so did not execute
the traps code that updates the restart PC.
A 'more correct' fix would be to update the restart PC when a thread is first transitioned
to Running, but this results in lots of unnecessary update as
* Frequently immediately schedule a thread after it is transitioned to running, making
the update to restart PC completely redundant as it gets immediately overwritten
* Rarely suspend threads making all the updates a 'high' cost for fixing an infrequent
operation
As a result this solution lazily fixes the restart PC only when we enter a state where
we might need a correct restart PC, which currently in the kernel is only when we
go from Running->Inactive, which can only happen in `suspend`
init_freemem sets up available regions of memory for the hardware that
seL4 is booting on. Previously this function was duplicated across
architectures, with minor duplication.
This change provides a top-level init_freemem suitable for all
architectures.
- arm/riscv: change get_avail_p_reg to return whole p_reg array
- update all architectures to use new init_freemem.
- wrap init_freemem calls with arch_init_freemem for each arch, where
arch_init_freemem sets up the available and reserved regions of memory
which are passed to init_freemem.
The memory used for the irq cnode is never available to the user. As a
result this memory can be allocated statically, simplifying the
bootcode.
- remove allocation of irq cnode
- add static init
- generate irq cnode size from cmake for arm
- add static constants for riscv, x86 as there is no variability at the
moment.
