This project is mirrored from https://github.com/seL4/seL4.git.
Pull mirroring failed .
Repository mirroring has been paused due to too many failed attempts. It can be resumed by a project maintainer or owner.
Last successful update .
Repository mirroring has been paused due to too many failed attempts. It can be resumed by a project maintainer or owner.
Last successful update .
- Jan 16, 2024
-
-
Gerwin Klein authored
Type invLabel consistently as word_t, not sometimes as unsigned int. This makes verification easier because it avoids unnecessary casts. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
Type and ghost state annotations for verification. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
The highest defined interrupt in the data sheet is 543 - 32 = 511. This is important, because the code expects all IRQ numbers to fit into 9 bits (which 511 does, but 512 would not). Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
The rest of the code uses 9-bit irq width. Keep in sync here to ease verification. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
Refactor getMapRefForASID for verification into separate parts, because the returned pointer doesn't exist as a concept in the executable spec. Also avoid ptr_set functions to simplify heap reasoning. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
- Jan 13, 2024
-
-
Axel Heider authored
This is missing in commit e6fbbbb0 Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Jan 12, 2024
-
-
Axel Heider authored
Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
Axel Heider authored
Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Jan 02, 2024
-
-
Axel Heider authored
Since commit cf8be663 this is no longer needed. Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Dec 28, 2023
-
-
Cindy Liu authored
Signed-off-by:
Cindy Liu <hcindyl@google.com>
-
Cindy Liu authored
Signed-off-by:
Cindy Liu <hcindyl@google.com>
-
Cindy Liu authored
Use importlib.metadata to check the jinja2 version Signed-off-by:
Cindy Liu <hcindyl@google.com>
-
- Dec 12, 2023
-
-
Gerwin Klein authored
The kernel.elf file is occasionally more useful for debugging than the final board image. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
- Dec 06, 2023
-
-
Birg authored
Signed-off-by:
Birg <bbrcknl@github.com>
-
Rafal Kolanski authored
lr_num is assigned to from word_t, so should also be word_t rather than unsigned int. Signed-off-by:
Rafal Kolanski <rafal.kolanski@proofcraft.systems>
-
Rafal Kolanski authored
On AArch64, if this is int, we encounter a situation where we can't prove equivalence with the abstract spec without an extra invariant that the number of these registers isn't zero (to satisfy 32<->64 bit casts). Sticking with word size will make sense on both 32 and 64 bit. Signed-off-by:
Rafal Kolanski <rafal.kolanski@proofcraft.systems>
-
Rafal Kolanski authored
Arch_decodeInvocation takes a word_t length and then passes it to functions that take an unsigned int length. This was OK on 32-bit where these types are the same, but on 64-bit this is a downcast without a range check. It isn't clear why this doesn't trip a compiler warning. Signed-off-by:
Rafal Kolanski <rafal.kolanski@proofcraft.systems>
-
- Nov 29, 2023
-
-
Birg authored
Signed-off-by:
Birg <bbrcknl@github.com>
-
- Nov 27, 2023
-
-
Axel Heider authored
Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Nov 24, 2023
-
-
Axel Heider authored
Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
Axel Heider authored
Avoid the annoying style checker complaints. Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Nov 23, 2023
-
-
Axel Heider authored
Support multiple architectures as parameter. Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Nov 16, 2023
-
-
Axel Heider authored
Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
Axel Heider authored
The default value is zero anyway. Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Nov 15, 2023
-
-
Corey Lewis authored
This insertion is not required, as the slot has just been cleared by cteDelete. Avoiding the insertion simplifies verification. Signed-off-by:
Corey Lewis <corey.lewis@proofcraft.systems>
-
Corey Lewis authored
This changes it to be a pure function, which eases verification Signed-off-by:
Corey Lewis <corey.lewis@proofcraft.systems>
-
- Nov 10, 2023
-
-
Axel Heider authored
The assert() condition is checked two lines above Signed-off-by:
Axel Heider <axelheider@gmx.de>
-
- Nov 08, 2023
-
-
Ivan-Velickovic authored
Signed-off-by:
Ivan-Velickovic <i.velickovic@unsw.edu.au>
-
Ivan-Velickovic authored
Similarly to the U54-MC, the U74-MC has a S-core that does not run in supervisor mode. Signed-off-by:
Ivan-Velickovic <i.velickovic@unsw.edu.au>
-
Ivan-Velickovic authored
Signed-off-by:
Ivan-Velickovic <i.velickovic@unsw.edu.au>
-
Gerwin Klein authored
The comment that PRECISION is too low when the assert fails was wrong. PRECISION should have no influence on it. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
- make sure the tick count does not underflow - make sure the tick count does not become 0 in the division, because a value of 0 stops the timer. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
Move the ksCurTime assertions out of setDeadline, because they are not necessarily true there. Assert ksCurTime in setNextInterrupt instead. We only know that the deadline being set is at least ksCurTime - getTimerPrecision(), which can be slightly in the past (ksCurTime is already slightly in the past, at kernel entry). Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Michael McInerney authored
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>
-
- Nov 07, 2023
-
-
Gerwin Klein authored
Put MCS-only invocations into their own groups and files. This solves the problem that doxygen gets confused by duplicate function names with the same parameters. MCS/non-MCS is distinguished by evaluating the <condition> field in the API XML definition. If the condition evaluates to true when CONFIG_KERNEL_MCS is set, it is an MCS-only method, otherwise it is assumed to be non-MCS or present in both configs. Fixes #558 Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
Disambiguate (for the reader) between normal and mcs versions of SetSpace in the manual. This does not yet solve doxygen confusion. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
HTML_TIMESTAMP and LATEX_TIMESTAMP have been removed in more recent doxygen versions. Since we are using the defaults, they are safe to remove in our config file. Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
Different API groups may contain the same function name, for instance IRQ_Control GetTrigger for RISC-V vs the same for ARM. Duplicate function names with identical parameter lists confuse doxygen, leading it to generate a single merged xml entry for both, which means one of the entires will be missing and the other will be potentially wrong. When the functions are placed in different files and different groups at the same time, doxygen no longer is confused in all cases. Therefore: - generate a separate file for each API group - generate a separate file group_defs.h that contains group definitions and declares group nesting Unfortunately, this does not seem to always work (e.g. the toplevel MCS/non-MCS syscalls), so manual inspection is still necessary when adding new calls and separate doxygen runs for duplicate function names may be necessary. Generating separate files as above enables this option, should it become necessary in the future. Fixes #530 Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-
Gerwin Klein authored
Signed-off-by:
Gerwin Klein <gerwin.klein@proofcraft.systems>
-