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 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>
The RISC-V calling convention specifies that when a C function takes an
argument by value, the binary function should take the argument by
reference, if the value is larger than 2 pointer words.
For binary verification, we avoid implementing this aspect of the RISC-V
calling convention, by eliminating all such function arguments for
functions which are not inlined.
In this commit, we remove the `slot_range_t` structure altogether. For
the small number of functions which previously used this type, we unpack
the structure into three separate arguments.
Even though we are primarily concerned with RISC-V, we remove
`slot_range_t` arguments across all architectures.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The RISC-V calling convention specifies that when a C function takes an
argument by value, the binary function should take the argument by
reference, if the value is larger than 2 pointer words.
For binary verification, we avoid implementing this aspect of the RISC-V
calling convention, by eliminating all such function arguments for
functions which are not inlined.
In this commit, we remove `extra_caps_t` function arguments. This
primarily concerns invocation decode functions. Since `loookupExtraCaps`
already stores extra caps in a global `current_extra_caps`, this
essentially amounts to eliminating many redundant structure copy
operations.
On some execution paths involving IPC, the extra caps lookup may happen
twice: first in the invocation decode, and then for cap transfer in the
performance phase of the IPC operation. Because the two phases are
entirely distinct, there is no interference in the use of a common
global variable.
Even though we are primarily concerned with RISC-V, we remove
`extra_caps_t` arguments across all architectures.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Most of the uses of these are in functions where the cap type is
statically known and the correct branch could be used directly, but the
compiler does not know this so having these as inlines causes a large
number of accesses to bitfields of unrelated cap types in functions that
manipulate caps.
Moving this out of line makes the results of changing cap bitfields less
noisy.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
reply_unlink takes a reply and remove the link between that reply
and its tcb. This link always exists at the call site and the tcb
information is always avaialble, or can be made available.
This commit adds this tcb as an extra argument to aid varification.
Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
The base pointer is wrong, and it creates some nasty corruption down the
line (only affects debug builds).
Signed-off-by: Sylvain Gauthier <sylvain.gauthier@data61.csiro.au>
The current state of MCS seL4 verification makes use of an invariant
that whenever the scheduler action is set to "resume current thread"
the current thread and the current sc are bound together. Since
maybeReturnSchedContext may unbind a thread from a scheduling context,
it should perform a check on whether it is unbinding from the current
thread, and in that case call rescheduleRequired which will (among
other things) change the scheduler action.
Signed-off-by: Mitchell Buckley <mitchell.buckley@data61.csiro.au>
If a thread is running on the SchedContext of it's bound notification,
when it next does a blocking recv/wait operation on an ep the SC is
removed. This allows the thread to return to being a passive thread to
receive the next notification or ep message.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
Special debug variables that were previously stored at the end of the
tcb_t struct often cause the struct to get too large for the power-of-2
sized untyped object definition. This change moves these variables into
a new structure named debug_tcb_t that is located between the TCB CNode
and the tcb_t struct within a tcb kernel object. Because tcb_t needs to
be stored on a power-of-2 aligned boundary and the TCB CNode only
contains < 5 slots, there is easily > 512 bytes of unused data in every
tcb object. The kernel verification needs to be sure that objects don't
overlap in memory and so this space can't be easily used in a release
build at the moment, but for debug configurations using it shouldn't be
an issue.
Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
The thread_control_flag enum which defines which arguments should be
used to reconfigure the TCB should also be split into two sets of flags
as they are now applied to two different functions.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This ensures that verification are not required to prove problematic
combinations of updates to a TCB that aren't even permitted by the API.
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.
Explicitly create a struct definition for irq_t on SMP Arm
configurations. This makes it a lot harder to mistakenly use the wrong
irq encoding when moving an irq between a cnode index and hardware irq
number / core. A couple areas where this was being handled incorrectly
was fixed as part of the refactor. When performing an ipi for masking
PPI interrupts, the idx encoding is used as it fits into a single word.
Some invocations contain two phases, and certain operations cannot be
allowed to run in the first phase as it could effect the currently
running thread and result in an invalid system state for the second
phase. This change filters those invocations, preventing them from being
used in the first phase of a two-phase, blocking system call.
Before this change, we set the replyObject in the thread state on recv
with no back pointer such that stray pointers would be left in the
thread state when a reply object was completed.
The new semantics are clearer and fix this problem by doing the
following:
- tcb->tcbReply is removed and the thread state field is always used,
this was unneccessary duplication previously
- the thread state value is set to the reply object only when the thread
is in BlockedOnReply or BlockedOnRecv
- the reply contains a back pointer, replyTCB, which points to that
thread
- if a thread has its reply removed, it must be set to
ThreadState_Inactive.
- deletion is easy in the blockedOnRecv case, we just unlink the reply
and the tcb.
- deletion is complicated for blockedOnReply. If we are deleing a tcb,
we remove the actual reply object and the call chain is broken. If we
are deleting a reply, we maintain the call chain by moving the tcb to
the next reply.
- we refactor the reply object interface to solve the above.
* reply_clear: removes the reply from any connections (tcb, sc)
* reply_unlink: just unlinks the tcb and reply, and sets the thread
state to inactive
* reply_remove: removes the reply from the call chain
* reply_remove_tcb: removes the exact reply that a tcb is bound to,
as we are removing that tcb. Breaks the call chain.
- 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 commit allows scheduling contexts to be bound
to notification objects. When a passive server
receives a notification it will receive the scheduling
context from the notification. When the server
blocks the scheduling context is returned.
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.
Correctly defined the macros to translate between virtual and hardware
IRQs such that PPIs can be properly handled on gic_v2. It is now
possible to create a per-core handler for PPIs on platforms using this
GIC.
irq_t is now a "virtual" interrupt type that encapsulates the
information of the core in case of a private interrupt. There is a
couple of macros that need to be defined on the interrupt controller
level to translate between virtual and hardware IRQs.
This removes the assumption that each platform sotres the IPC buffer
address in a platform-specific register. The IPC buffer address is
instead stored in a thread-local variable in libsel4 which must be
initialised by the runtime.
This changes the comments regarding the size of the TCB to be more
generally accurate to help manually determine the size of the TCB for
different configurations.
These files can be included normally using libsel4 include paths. This
removes situations where the same file is available under different
include paths due to symlinking into different directory structures.
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.
Revocability of a cap, with respect to its parent, is a general property on caps and
makes sense to be abstracted. This allows for the addition of an arch case without
further complicating the cteInsert function itself.
A TCB object has two objects inside it, the cnode object and the 'actual tcb object'.
For simplicity of verification we would like the tcb_t portion of the object to also
be size aligned instead of just just being offset by the size of the cnode.
This definition is used as the size of the cnode portion of the TCB object (and not the tcb_t)
portion and so this provides a much less confusing name.
