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 .
- Jun 20, 2019
-
-
Anna Lyons authored
Add a device tree overlay such that all memory on the exynos4 fits in the kernel window. It's unknown if the memory past 0x50000000 is valid, when the elf-loader attempts to write to it it hangs.
-
Matthew Brecknell authored
This is workaround for part of binary verification, which currently cannot handle some modes of array access.
-
Anna Lyons authored
If we place the user image at the end of memory, the user image can be beyond the kernel window. Handle this in arch_init_freemem by comparing to paddr's not pptrs.
-
Anna Lyons authored
This change allows us to know, from just the kernel and dtb, where user level untyped objects start being allocated from. - allocate rootserver objects from last available freemem region. - move create_rootserver_objects call into init_freemem.
-
Anna Lyons authored
The user image could be on either side of mode_reserved_region. Fix this by assuming there is 1 or 0 mode_reserved_regions, and checking if the user image is either side.
-
Japheth Lim authored
This fails early if the build process failed to calculate a suitable MAX_NUM_FREEMEM_REG.
-
Japheth Lim authored
Previously, the boot allocator would do dynamic calculations to minimise fragmentation, then throw away the smallest regions. With the new boot allocator, we can reasonably predict that fragmentation will create at most one extra region, so this commit adds one freemem slot for ARM.
-
Anna Lyons authored
-
Anna Lyons authored
Prior to this change, the boot process would dynamically allocate memory for root server objects based on the order of initialisation. Allocation was a best-fit algorithm. This change preallocates all memory for root server objects to an aligned untyped just after the user image. By allocating the objects in order of size, allocation is greatly simplified and the ability to reproduce the allocation offline based on the kernel and user image sizes is increased.
-
Anna Lyons authored
Prior to this change, seL4_MappingFailedLookupLevel() would retrun '22' after any failed EPT mapping operation. This change fixes this to return the correct amount of unresolved bits in the address.
-
- Jun 19, 2019
-
-
G. Branden Robinson authored
Cache `platform_yaml` so we can reference it from `elfloader-tool` CMake logic.
-
Anna Lyons authored
- read PMUSERENR_ENABLE first before updating. On the cortex-a8 (specifically omap3) not doing this would result in the kernel aborting. - do not read DBGDSCR_ext on cortex-a8, read DBGDSCR_int. This is only implemented in armv7.1, not armv7, and also causes the kernel to abort.
-
- Jun 18, 2019
-
-
Kent McLeod authored
These tools sometimes style differently across different versions.
-
Anna Lyons authored
With the increased faults on various configurations (hyp, mcs) we need more bits to identify faults.
-
Kent McLeod authored
While masking and unmasking IRQs seems to work for some IRQ sources, there are IRQ sources where masking an IRQ during a claim causes no more IRQs to be raised after the IRQ is unmasked. This change explicitly follows the claim->acknowledgement procedure that the PLIC expects.
-
Kent McLeod authored
We add support for seL4_IRQControlGet and seL4_IRQControlGetTrigger. If a platform doesn't support setting the trigger, then seL4_IRQControlGetTrigger will return an error. If the platform doesn't have a PLIC driver, then it won't have any IRQs that can be requested. Also authored by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
-
Kent McLeod authored
Previously we only handled IRQs generated by the BBL running in machine mode via changes to supervisor interrupt pending (SIP) bits. Now that we need to support shared global interrupts through the PLIC we need to modify the way interrupts are processed. We additionally remove many DONT_TRANSLATE annotations on functions that the CParser is able to parse. Also authored by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
-
Kent McLeod authored
We assume the PLIC is currently the only global interrupt controller that RISC-V platforms are going to use. Each platform may have a different programmers model for interracting with the hardware controller. We provide a common interface for PLIC drivers to implement that the kernel will use to manage IRQs. Also authored by: Siwei Zhuang <siwei.zhuang@data61.csiro.au>
-
Siwei Zhuang authored
- Create device untypeds for platform devices that can be passed to user space. - Create kernel device mapping for devices required by the kernel. Note that the current kernel device mapping is simply a 1GiB of page physical memory as that contains all devices for all RISC-V platforms that are currently supported.
-
- Jun 17, 2019
-
-
Kent McLeod authored
For now we keep the RISC-V platforms under the spike kernel platform name. Splitting the different platform definitions into different header files will help maintainability as we add different device layouts and kernel device drivers.
-
Kent McLeod authored
PPTR_USER_TOP represents the first inaccessible user address which is usually ((2^(38-12))-1)*0x1000 on SV39. This corresponds to the first address of the last page in the lower half of the top level page table.
-
Kent McLeod authored
Add a comment and diagram explaining the current structure of the SV39 kernel address space. The top half of the virtual address space is reserved for the kernel and consists of the Kernel window of all accessible physical memory, the kernel ELF mapping and the Kernel device mapping region.
-
Kent McLeod authored
There is a 1GiB region reserved at the top of the Kernel virtual address space to map devices used by the kernel into. The start of this range is referred to by PPTR_KDEV. This also represents the end of the Kernel ELF window mapping.
-
Siwei Zhuang authored
Verification requires the KERNEL_BASE to be 1GB aligned at the start of the kernel elf window. It was also the location where the kernel elf was mapped. As we have to include SBI memory in the kernel elf window, the KERNEL_ELF_BASE is introduced for the real kernel elf mapping. Keeping KERNEL_BASE unchanged.
-
Anna Lyons authored
Include padding to round up to a page boundary.
-
Anna Lyons authored
-
Anna Lyons authored
The previous minimum (4) was actually too small to fit more than 1 capability, which would not allow the kernel to boot. A 4K minimum means on 32-bit, an 8 size is the minimum (256 slots) and on 64-bit, 7 (128 slots). In addition to being a more practical minimum, this also allows for simplification of the boot code for future commits.
-
Anna Lyons authored
This constant represents the size of the root page table.
-
Anna Lyons authored
This is because future work needs to access the rmrr_list globally.
-
Anna Lyons authored
In order to enable user-level access to the PMU, which is required by the benchmarks.
-
Damon Lee authored
-
Anna Lyons authored
plat/machine/timer.h is unused on arm, so remove it and fix up the includes.
-
- Jun 14, 2019
-
-
Anna Lyons authored
-
Anna Lyons authored
Remove benchmark_utilisation_kentry_stamp.
-
Anna Lyons authored
-
Anna Lyons authored
This code did not compile...
-
Anna Lyons authored
- consolidate armv_init_ccnt into arm_init_ccnt, which is general - move armv_handleOverflowIRQ definition to benchmark.h (no need for extra header) - clean up definition of armv_handleOverflowIRQ
-
Anna Lyons authored
-
Anna Lyons authored
-
Anna Lyons authored
Both CONFIG_ENABLE_BENCHMARKS and CONFIG_EXPORT_PMU_USER configured the PMU on armv7 and armv8 to be accessible with different code. Use the same code.
-