The outermost if statement can be removed in reply_pop
because reply_pop is called only in reply_remove, which
includes an explicit check for this condition.
The new inline function setThreadStateBlockedOnReply is
used within reply_push.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The clock sync test at boot keeps failing for the hifive board with time
deltas as high as 5. We think this is because mmode might be taking a
big lock for reading the time.
Add a macro for allowed delta and set it to a higher value for RISC-V.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Previously, a refill would be ready if its head time
was at most getKernelWcetTicks after the current time.
This would mean that refill_unblock_check could
bring a refill's time forward, which violates an
invariant (namely that the time of the last refill
is at most the period from the time of the head refill).
Moreover, since the time to exit the kernel is always
less than the WCET, this might result in us running
a thread whose refill time is in the future, which
seems to violate the timing model.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
It is an invariant in the MCS kernel that scSporadic implies sc_active.
Make use of that invariant by avoiding an explicit check for sc_active,
but assert the invariant in debug mode so it fails quickly when new
code breaks the invariant.
Essentially reverts 56098195f2 now that the invariant is preserved,
but adjusts the assertion from 17109eb8c9 to actually express
the invariant.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add helper functions to get kernel image location. This removes any
dependencies from the rest of the code on symbols and defines. It
also avoid passing a parameter though various functions.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Remove the return value from configure_sched_context(), because it never
fails. As a consequence, create_idle_thread() also never fails and does
not need a return value.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
Because ksCurTime is compared cross-node now, time across
nodes must be the same. Check this once during boot.
Replace __atomic_signal_fence with the more correct
__atomic_thread_fence, as ksNumCPUs will be changed
cross-node.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
Remove the now unused core argument from refill_new and replace all
REFILL_NEW calls with direct calls.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
The code using ksCurTime assumes that ksCurTime is up-to-date,
but this assumption is wrong for ksCurTime of other CPU cores.
Those can be quite some time in the past.
The implications of using NODE_STATE(ksCurTime) is that clocks
on all cores must be synchronous:
- Riscv is okay: The specification states: "The real-time clocks
of all hardware threads in a single user application should be
synchronized to within one tick of the real-time clock."
- x86 okay if not ancient when Invariant TSC is supported.
- aarch64 is okay.
- arm32: arm_global.h is okay. Exynos timer seems okay. am335x and
omap3430 are single-core.
See also #854.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
- explicitly mention the parameter to make macro less obscure.
- add brackets to make the expression an atom.
Signed-off-by: Axel Heider <axel.heider@hensoldt.net>
Explicitly include the config header file as the first thing, don't rely
on other headers doing this eventually.
Signed-off-by: Axel Heider <axelheider@gmx.de>
When calling chargeBudget or commitTime, only consume time within the SC
refills if the SC does not belong to the idle thread. This is to make it
easier to prove that the idle thread is always runable, even if it has
just consumed its SC's current timeslice.
Signed-off-by: Kent McLeod <kent@kry10.com>
Defined to be equal to CONFIG_NUM_DOMAINS. seL4 makes control-flow
decisions based on whether the number of domains is greater than 1. To
perform refinement proofs independent of the number of domains, we need
to follow both branches of these if statements, pretending we don't know
which branch will be taken. This is made significantly harder when
preprocessed C code ends up with comparisons like `if (16 > 1)`.
By adding a numDomains that appears in the C code, we obtain a name we
can point to and link up to higher level specifications.
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
- The field 'slot_pos_max' from 'ndks_boot' is not needed, the value
stored there is the constant BIT(CONFIG_ROOT_CNODE_SIZE_BITS).
- Improve the error message if the limit has been reached
Signed-off-by: Axel Heider <axelheider@gmx.de>
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>
Turns out the invariant 17109eb8c9 refers to is hard to prove
because it is not true, and the runtime check is necessary. This
assertion fails in sel4test SCHED_CONTEXT_0003 (Basic
api_sc_bind/UnbindObject testing).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The functions insert_region() and create_rootserver_objects() are not
used outside of boot.c, so there is no reason to make it publicly
available.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Also merge create_device_untypeds() and create_kernel_untypeds() into
create_untypeds() to simplify the code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Also make the output more verbose in case of errors, which is
helpful when porting the kernel to new platforms.
Signed-off-by: Axel Heider <axelheider@gmx.de>
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>
