This was removed in 2016 289bf92bf0.
Additionally, 5fac9e8198 removed the
section of the comment regarding having enough room for all the
untyped caps; because otherwise "enough space for 12 caps" is
somewhat uninteresting (most of the cspace is taken up by untypeds).
Signed-off-by: julia <git.ts@trainwit.ch>
As decided at the most recent TSC meeting, bump cmake format to the
latest version. This will change/break style in many of the existing
cmake files, but pinning pyyaml to < 6 is not a long-term option.
Also bump patch version of autopep8, which should not lead to style
changes.
Bump overall sel4-deps version because the cmake-format change is
incompatible. Version 0.6.0 was not published because of the pyyaml
pinning/downgrade.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Migrate documentation of the API docs generation process here from the
docsite where it is too much out of view. Here it is closer to where it
is needed an more likely to get updated when things change.
Compared to the docsite version, this has applied:
- standard wrap column
- markdown lints
- adjusted headings
- `object-api-sel4-arch.xml` etc renames
- include RISC-V in structure
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove manual table of contents for rendering on the docsite, which will
provide an automatic TOC.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
When evaluating XML condition expressions, properly treat undefined
values as undefined, not as False. Otherwise, the negation of an
undefined value may make an entire expression true and incorrectly
label some methods as MCS methods.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- introduce arch interface for IRQControlCap dependencies as well as for
isMDBParentOf (Arch_isIRQControlDescendant, Arch_isMDBParentOf). This
mirrors the corresponding interface in the proofs and Haskell and
avoids #ifdef proliferation in generic code.
- Arch_isIRQControlDescendant is currently only used for SGISignalCaps
- Arch_isMDBParentOf is used for SGISignalCaps and SMCCaps
- fix argument checking in Arch_decodeIRQControlInvocation (+ style
tweak)
- Arch_sameObjectAs must return false for SGISignalCaps to align with
finality definition of caps, i.e. SGISignalCaps are always final. This
has no behaviour change, because finality doesn't matter for behaviour
for SGISignalCaps, but we require for the proofs that the concept of
finality aligns with the spec.
- simplify checks for IRQControlCap in sameObjectAs: sameObjectAs can
never be true for IRQControlCap.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Fix a bug in VGIC Maintenance/VPPI logic that allowed a thread to be
simultaneously BlockedOnReply and in the release queue.
Co-authored-by: Alwin Joshy <joshyalwin@gmail.com>
Signed-off-by: Krishnan Winter <krishnanwinter1@gmail.com>
set ts-2025 for master branch l4v and leave on ts-2024 for MCS until MCS
is updated to Isabelle2025 as well.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Non-functional change. This will probably affect verification,
so definitely not expecting this to be merged anytime soon.
But it was very weird we had this rootSlot argument mark as UNUSED,
and it took me a bit to realise exactly what excaprefs[0] was
supposed to be.
Signed-off-by: julia <git.ts@trainwit.ch>
We're currently using AWS Arm VMs, and vanilla Isabelle2024 ships a Z3
version that does not work on Arm. Using the ts-2024 branch fixes this
until we have upgraded everything to Isabelle2025.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This fixes the error message in decodeSetTimeoutEndpoint
and correctly updates current_syscall_error.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
We no longer need to check this as the previous commit changed
decodeSetSchedParams to only pass the thread_control_sched_update_sc
flag if these conditions are true.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
The implementation of TCB_SetSchedParams did not follow the API
reference, as it would fail if:
a. The TCB already had a scheduling context, even if this was the same
as the one being passed in.
b. The scheduling context was bound to a TCB, even if this was the TCB
that was invoked.
Signed-off-by: Alwin Joshy <joshyalwin@gmail.com>
Before:
- invokeSchedContext_Consumed and invokeSchedContext_YieldTo clobber
the message info field in the reply from kernel, which results in a
length 0 message.
- invokeSchedContext_Consumed and invokeSchedContext_YieldTo may crash
the kernel for read-only IPC buffers
- invokeSchedContext_Consumed and invokeSchedContext_YieldTo generate
a reply from kernel for syscalls that should not generate replies
- completeYieldTo does not set the badge register, which will contain
whatever that previous syscall returned and not correctly indicate
success/failure.
- completeYieldTo sets registers of the current thread, combined with
IPC buffer message registers of potentially another thread.
Instead:
- pass the thread to setConsumed instead of the IPC buffer, so we can
write to the correct registers
- look up the IPC buffer again and check for write authority
- follow the kernel reply protocol, which includes only generating a
message for `call`. This means, we need to pass the flag through from
higher-level decode functions.
- set thread state to Running if a reply message from the kernel was
created, leave on Restart for default empty success message.
- set the badge register
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
I originally made the config before
6f2fe4626d so this patch gets rid
of the warning for the eswin config.cmake.
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Take advantage of the new --skip-unchanged option added to the
config_gen.py header generator to skip regenerating unchanged header
files which forced a rebuild of the entire project whenever CMake was
reconfigured.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
Currently, whenever CMake is reconfigured, config_gen.py will always
regenerate the output config header and json, forcing a timestamp
update and a rebuild. This change adds a --skip-unchanged option which
skips writing to the output file if the write would not change the
file's contents. The default is off to avoid breaking builds that rely
on the existing behavior of always overwriting.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
Previously, config_gen.py required the generated header and json to be
either written to a file or sent to stdout. This meant that there was
no way to avoid writing to a file, as the header and json data would be
merged into the same stdout stream. This change makes it so that the
header or json generation can be suppressed entirely by omitting the
corresponding --write-c or --write-json options.
Signed-off-by: James Martin <fennelfoxxo@gmail.com>
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 SiFive Premier P550 [1] is a new development board from SiFive
that is based on the ESWIN EIC7700X SoC.
The platform is interesting to the seL4 community as it implements
the RISC-V hypervisor extension meaning we now have real hardware to
evaluate RISC-V hypervisor changes to seL4. It also implements the
Sscofpmf extension and so we'll be able to get more experiment with
proper profiling on RISC-V.
Unfortunately, it seems we still do not have proper ASID suppor
according to [2].
The board comes in two configurations, 16GB and 32GB of memory.
This adds support for the 16GB model.
The DTS comes from SiFive's fork of Linux [3].
No modifications were made, any extra things are in the overlay.
[1]: https://www.sifive.com/boards/hifive-premier-p550
[2]: https://forums.sifive.com/t/asid-vmid-support-in-p550-eic7700x/6887
[3]: https://github.com/sifive/riscv-linux/tree/dev/kernel/hifive-premier-p550
Signed-off-by: Ivan-Velickovic <i.velickovic@unsw.edu.au>
Deploy the MCS verification manifest for versions that have no MCS
preprocess differences. These may be different from non-MCS preprocess
outcomes, and since the MCS verification is on a branch, we can deploy
it separately.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Wrap config_set macro in a static inline function so that verification
automation does not simplify away dead code branches based on it, but
the compiler still does.
In most parts of the proofs we want to pretend that we don't know the
config value yet and consider both options. This makes the proofs more
independent on the config value that is selected.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This eases verification by using a local variable
which remains unchanged during execution of the
function.
This also makes use of the function sc_active.
Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
Save and restore the CNTKCTL register alongside other virtual timer
registers when switching VCPUs.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
This introduces two new constants to the vcpu reg enum, with the goal of
unifying reg range saves/restores and making explicit which registers
are affected.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
seL4_VCPUReg_CPACR was sometimes saved to an inactive current VCPU,
overwriting the previous value and erroneously enabling FPU access.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
In aarch64 kernel configurations, it is not possible to configure the
FPU to be disabled. This makes certain ifdefs redundant.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Moves it to the arm-specific arch data.
Adds an extra CONFIG_HAS_ARM_TLB_LOCK that defaults to ON when the
architecture is ARM_CORTEX_A8.
Again, variable was noticed in the objdump of a RISC-V build, despite
only being used for a specific ARM CortexA8 platform.
Signed-off-by: julia <git.ts@trainwit.ch>
