This removes the operations that trigger a reschedule or reprogram the
timer from `preemptionPoint` to ensure the relevant state updates in
the proof occur where they are easier to verify.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
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>
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>
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>
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>
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 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.
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.
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.
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`
GrantReply is a new access right added to endpoint capabilities, which
allows seL4_Call to be used on those capabilities (specifically, it
allows reply caps *only* to be granted across endpoints).
Prior to the addition of GrantReply, endpoint capabilities required the
Grant access right, which allowed any arbitrary capabilitiy to be
transferred over an endpoint. Using GrantReply, systems can now be
constructed where threads using seL4_Call over an endpoint do not need to be in the same
security subsystem.
Instead of switching to the thread contained in `ksSchedulerAction` on a `schedule` we
instead decide between the 'candidate' contained in `ksSchedulerAction`, the current thread
or potentially neither if the candidate is deemed invalid and the current thread is blocked.
A consequence of this change is that it is no longer meaningful to have a distinction between
`switchIfRequiredTo` and `attemptSwitchTo`. Now both these cases simply identify a candidate,
which may or may not be picked in `schedule`. Part of the distinction of `switchIfRequiredTo`
was to not avoid switching if possible when performing notifications. This is now handled by
prefering the current thread over the candidate if the current thread has not blocked.
This change is largely semantic preserving overall, with the exception of non-blocking
synchronous sends now acting like notifications and also preferring to resume running the
current thread.
The motivation for this change was to make it much easier for verification to show
correspondence between the fastpath changes introduced in the previous commit and the
slowpath scheduler.
This commit does the following:
* invert the bit field scheduler for better cache performance for high priority threads
* peeks into the bitfield scheduler to allow fastpath to be leveraged when IPC occurs from lo --> hi priority threads if correct
Where MCP = Maximum Controlled Priority
This commit adds:
* seL4_TCB_SetMCPriority
and changes the arguments to
* seL4_TCB_Configure
As of this commit, a thread cannot create or set a threads
priority (including itself) above its mcp. Previously the kernel
did this check against a threads priority, which prevented a thread
from setting it's own priority down and then up again.
Diminish rights were to prevent a user from sending a writeable
cap over a read only endpoint. It turns out this 'security' can
be worked around without difficulty (by putting caps in a cnode
and sending the cnode) making the current diminish rights
implementation functionally useless.
Removing diminish rights has the benefit of simplifying all the
IPC paths.
This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely,
and changes the return type of seL4_Wait to void (seL4_Wait should be
used for notification objects, and seL4_Recv should be used where
seL4_Wait was used previously for endpoints).
Background
seL4 organizes threads into ready queues, of which there is one for each
domain, for each priority level. The ready queue for a given
domain/priority combination can be found by indexing the array
`ksReadyQueues` with "domain*num_priorities + priority".
Current scheduler implementation
To find the non-empty ready queue with the maximum priority for the current domain,
seL4 iterates through `ksReadyQueues`, starting with the element
corresponding to the current domain and maximum possible priority, and
decrementing the priority until a non-empty queue is found. This is
problematic in cases where the only ready threads have low priorities,
as iterating through many elements of an array effectively flushes the
cache.
Changes in this patch
This patch replaces the iteration with a lookup into a table of
bitfields per domain. Using bitfields allows the kernel to determine the
highest priority level with a non-empty ready queue for the current
domain by counting the leading zeroes in bitfields. This removes the
negative cache effects of iterating through an array.
Implementation details
For each domain, a multilevel table of bitfields is maintained which
stores the priority levels within that domain for which there exist
ready threads. On a 32-bit architecture, the top level of the table is a 32-bit bitfield where if
the ith bit is set, there is at least 1 priority level in
[i*32..i*32+31] with a non-empty ready queue. The positions of bits in
this bitfield are used as indices into the second level table, which is
an array of 32-bit bitfields. The ith bit of the jth bitfield in this
array set to 1, indicates that priority level j*32+i has a non-empty
ready queue.
