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>
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>
- 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.
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.
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.
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.
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.
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.
- 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
- Move identical definitions from armv6 and armv7 to common arm code.
- Remove excessive #ifdef guards - let the compiler throw it away if
it isn't used
Always handle overflow irqs from the cycle counter if overflow irqs are
enabled, not just when we are updating the log. Otherwise if logging
isn't enabled but the counter overflows the kernel will be stuck in a
interrupt handling loop.
Fixes a case where a thread can go from Running->Inactive->Restart and use a restart PC
that is out of date. An out of date restart PC occurs when a thread was transitioned to
running after being in a blocked state, but was never scheduled and so did not execute
the traps code that updates the restart PC.
A 'more correct' fix would be to update the restart PC when a thread is first transitioned
to Running, but this results in lots of unnecessary update as
* Frequently immediately schedule a thread after it is transitioned to running, making
the update to restart PC completely redundant as it gets immediately overwritten
* Rarely suspend threads making all the updates a 'high' cost for fixing an infrequent
operation
As a result this solution lazily fixes the restart PC only when we enter a state where
we might need a correct restart PC, which currently in the kernel is only when we
go from Running->Inactive, which can only happen in `suspend`
hardware.c was defined for both 32 and 64 bit arm kernels. However, the
only difference in the file is the register used in setNextPC. Add this
register as a #define in registerset.h, move hardware.c to be common for
both 32- and 64-bit arm.
init_freemem sets up available regions of memory for the hardware that
seL4 is booting on. Previously this function was duplicated across
architectures, with minor duplication.
This change provides a top-level init_freemem suitable for all
architectures.
- arm/riscv: change get_avail_p_reg to return whole p_reg array
- update all architectures to use new init_freemem.
- wrap init_freemem calls with arch_init_freemem for each arch, where
arch_init_freemem sets up the available and reserved regions of memory
which are passed to init_freemem.
The idle thread is not managed at user-level and so it can instead be
statically allocated. This simplifies the boot code and increments
towards being easier to formally verify.
Persuant to the fact that userspace cannot save and restore the debug coprocessor,
there is no point in delivering a fault message to userspace when CP14 is accessed.
The debug coprocessor must be entirely handled by the kernel, and a new hardware
accessor and manipulation capability must be designed and implemented now.
The memory used for the irq cnode is never available to the user. As a
result this memory can be allocated statically, simplifying the
bootcode.
- remove allocation of irq cnode
- add static init
- generate irq cnode size from cmake for arm
- add static constants for riscv, x86 as there is no variability at the
moment.
We now support receiving a DTB from the ELF loader and passing it on
to userspace in extra bootinfo. We still support booting without a DTB,
though - the device tree address is set to zero in the boot code and no
extra bootinfo region is provided.
