This eases verification by using a local variable
which remains unchanged during execution of the
function.
This preserves semantics since tcbSchedDequeue
will not modify the scTcb field of the given sc.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
On aarch32, single stepping is configured by setting an instruction
breakpoint to mismatch mode. The way that it is checked whether a
given breakpoint is being used as a normal breakpoint or for
single-stepping is by checking if it has been configured to mismatch.
This works because the HW debug API does not currently provide a way
to otherwise configure mismatch breakpoints, but seems like an
unsatisfactory solution. Whether single-stepping is enabled, and
the breakpoint that is being used for it is already stored in the
TCB of a thread, and this commit changes checks related to
single-stepping to use this information instead.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Changing the debug register fields to what they are referred to
as in the ARMv7 and ARMv8 manuals. Mostly a cosmetic change,
but improves clarity.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
This is most likely an artifact from the change of the IPC buffer
handling before v11.0.0, where a thread-local register (tp on RISC-V)
was reserved by the kernel for storing the pointer to the thread's
IPC buffer. Architectures such as aarch64 would set the register
inside Arch_switchToThread() and then not touch the register in
restore_user_context(). When the RISC-V port was up-streamed, it
didn't restore the register with the other registers, but also
didn't restore it in Arch_switchToThread() and so ended up restoring
it right at the end of the restore process.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Axel Heider <axel.heider@codasip.com>
This removes the tcb parameter from schedContext_unbindTCB, which
is unnecessary, since it is always the scTcb of the given sc.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This refactors awaken, providing an inline function for the
while loop condition, and modifying tcbReleaseDequeue to now
perform the entire loop body.
Since tcbReleaseDequeue will perform tcbReleaseRemove on the
head of the release queue, the variable ksReprogram will be set
to true within tcbReleaseRemove, and therefore, we do not need
to set this variable separately within the loop body of awaken.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
The version bump should be stable in code layout and fixes crashes on
more recent python code.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- tweak SMP/multikernel text to make clear that SMP is not deprecated
- rephrase old VSpace reuse section hopefully be clearer
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- MCS WCET settings are just defaults without much basis
- stale page cap data also allows cache ops to proceed
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Frame caps should be checked for stale mapping info before authorising
any operation on them. In this particular case, the mapping may have
become invalid.
See also #1281
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When performing data cache invalidate by virtual address, the mapping
must have write permissions, otherwise a fault will be generated by the
hardware. Therefore, when the kernel performs this operation during
cache maintenance invocations it must first check that the mapping has
write rights in the decode phase of the operation.
Co-authored-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit's parent renames the interface XML files.
The symlinks added in this commit serve to ease the transition to the
new names for downstream projects.
These links are added:
- include/interfaces/{sel4.xml -> object-api.xml}
- arch_include/*/interfaces/{sel4arch.xml -> object-api-arch.xml}
- sel4_arch_include/*/interfaces/{
sel4arch.xml -> object-api-sel4-arch.xml
}
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The ELF loader may well be satisfied with a smaller alignment, but the
compile time assert in the kernel requires super section alignment for
physBase.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The page no longer exists on the doc site, and the site does not
actually have more info, because the change log is generated from here.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
