GitLab

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

Fix issues where scheduling context is dereferenced after it is removed
from the associated TCB.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

While the new check is technically redundant, it is consistent with how
schedContext_completeYieldTo is called elsewhere and eases verification.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

This makes it have the same structure as reply_remove and is easier to
verify.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

This should have the same control flow and will be much easier to
verify.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

This should make verification of this function easier.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

Deleting a reply object that is linked to a BlockedOnReceive thread is
unusual behaviour and it's not clear what the expected behaviour
should be. Previously, finaliseCap called replyUnlink but this sets the
thread to Inactive while leaving it in the endpoint's queue, which
breaks the invariants. Calling cancelIPC at least guarantees that the
system ends up in a consistent state.
Signed-off-by: Corey Lewis <Corey.Lewis@data61.csiro.au>

When a revoke operation clears the current SC, that SC can't continue
operation past the subsequent preemption point. Presumably, that SC had
sufficient budget for each iteration up to the last and could have been
charged for the last iteration.

Simply setting the consumed time to 0 at the point where the SC would
have been charged is equivalent to charging the time to that SC priori
to its being cleared, including any accounting for overrun.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

Call updateTimestamp unconditionally whenever ksWorkUnitsCompleted
exceeds the preemption level. This is necessary such that future calls
to checkBudget and chargeBudget occur with the correct time consumed.
Signed-off-by: Kent McLeod <kent@kry10.com>

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>

At a preemption point the current SC may have been revoked and cleared
and would thus no longer be configured. In this case, it woudl be
invalid to perform a checkBudget and so we just treat it as a preemption
and don't charge any budget.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

We must ensure that the current thread is not already yielding to
another thread when it makes a YieldTo invocation. This should never
happen as we should always cancel any YieldTo before returning to
user-level, however we cannot prove this invariant at this time.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

When determining whether a SC donated from the notification should be
returned, we must ensure not to try and return a NULL SC to a
notification with not bound SC.

This could occur when a passive server performs a NBSendWait/NBSendRecv
with a notification in the receive phase, where the SC for the receiver
was returned in the send phase and the notification has no bound SC.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

This should not change the behavior of this function in any way but
makes the order of operations more similar to other locaitons in the
code in a manner that eases verification.
Signed-off-by: Michael McInerney <Michael.McInerney@data61.csiro.au>
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

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>

See: https://sel4.atlassian.net/browse/SELFOUR-2830

 for details.

On SMP configuration the `ic ialluis` instruction must be used
to ensure the I-cache on all cores is invalidated.
Signed-off-by: Ben Leslie <benno@brkawy.com>

Signed-off-by: Axel Heider <axelheider@gmx.de>

See: https://github.com/seL4/seL4/issues/346

 for details.

VPPIEvent and VGICMaintenance handling is updated to first
check that the current thread has budget. If it does not
have budget the interrupts are ignored. As interrupts are
level-triggered this effectively just delays the interrupts.

The check for budget is based on determining if the current
thread is enqueued. This occurs if (and only if) the current
thread has had a budget check that is expired.
Signed-off-by: Ben Leslie <benno@brkawy.com>

The current version of the proofs does not track whether the current SC
is bound to the current thread or any thread at all in the proof state.
As a short-term workaround, we add explicit checks in the kernel to
guarantee that we don't treat the current SC as having been unblocked
rather than relying on static knowledge that this doesn't occur.

The proofs should be updated in the future with all of the checks
introduced in this PR removed.
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...

refill_unblock_check is called in switchSchedContext whenever an SC is
switched to. Any other calls would have no effect:
- If the SC was already running then it would have had
  refill_unblock_check already called on it,
- If the SC was not already running, then it would have
  refill_unblock_check called when it was next switched to which would
  override the previous call.
Signed-off-by: Kent McLeod <kent@kry10.com>

The `refill_order` assertion is only applicable when the scheduling
context is not round-robin.

Assertions are changed such that `refill_order` is only asserted
when the the scheduling context is *not* a round-robin scheduling
context.

When performing `maybe_add_empty_tail` the `rTime` attribute
is updated to the existing time. This smplifies as compared
to existing code. Another option could be to set to zero, however
this brreaks invariants relied on for verification.

See: https://github.com/seL4/seL4/issues/262

Signed-off-by: Ben Leslie <benno@brkawy.com>

If one thread replies on behalf of the a thread to which an SC is
donated and that thread is in the release queue, that thread must be
removed from the release queue when the SC is returned.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

Move syscall and fastpath checks after interrupt and exceptions.
Exceptions were being interpreted as null-syscalls.
Remove duplication for return address.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

Inline fastpath functions and call out to them from traps.S.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

Signed-off-by: Axel Heider <axelheider@gmx.de>

Actually divide by KHz frequency when on a platform that uses a clock
that does not have an integer MHz frequency for aarch64.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

the function is not always passed the TIMER_PRECISION argument. If it is
not, we should not set the global varaible.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

This is makes it easier to avoid undefined behaviour in the proofs.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>

define KernelPlatformZCU102 and KernelPlatformUltra96 that both
use KernelPlatformZynqmp then.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>

We need to check if the name of the variable has been defined, not if
its value as a variable name has been defined, when determining whether
to set a default value.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>

We must store the consumed time in us rather than in ticks into message
registers. In the overflow case, the time being stored was the maximum
US time in ticks, this fix converts it to US before being stored.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>