- Use SMP_TERNARY() macro.
- Rename get_hart_id() to plic_get_current_hart_id(), as this is just a
helper function for the other PLIC code in this file.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
RISC-V defines the concept of a PLIC, but leaves the details open. The
driver is for the PLIC of the SiFive U54/U74 SOC, which is used on
the HiFive Unleashed/Unmatched and Polarfire board.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- describe PLIC behavior and corner cases.
- provide a common header file for the API.
- add a dummy PLIC driver for spike.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
- Move CSR SIE access wrappers to generic code.
- Move CSR SIE/SIP bit constants to header file.
- Rename CSR SIE/SIP bit constants to use the names from the RISC-V
specification.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
MODE_RESERVED is unused on RISC-V, so remove it from the code base. It
can be brought back when needed based on the state of the ARM
implementation, which has been clean up to remove global dependencies.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- define NUM_RESERVED_REGIONS to align ARM and RSIC-V code
- add runtime checks to catch errors. These checks can't be static or
use assert(), as the parameters are passed by a kernel loader. They
must be considered dynamic and can potentially change any time out
of the kernel's control.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Update GIC_VCPU_MAX_NUM_LR constant to reflect that only 16 list
registers are supported on GICv3. The kernel still reads the actual
number of supported list registers out of the GICH_VTR register so the
kernel would still do the right thing before this change.
Signed-off-by: Kent McLeod <kent@kry10.com>
This adds sufficient kernel support for the GICv3 interrupt controller
to be used in a virtualization context on aarch64.
This set of changes has some limitations, however it is still an
improvement on the status quo.
Limitations:
1: This only provides support for aarch64. Anyone wanting support
for aarch32 + GICv3 + virtualization would need to add additional
code.
2: This code only supports 32 priority levels. Support for more
than 32 priority requires changing the get/set_gic_vcpu_ctrl_apr
interface. This is feasible, but requires a more invasive set of
changes. 32 priority levels has been shown to be sufficient in
practise.
Impacts on verification:
This set of changes should only impact Aarch64 Hypervisor
configurations. This is not yet verified so should not have
an impact on verification.
Level of testing:
This has been tested on an iMX8QXP based board. Testing
has at this point in time been limited to a single virtual
machine.
Note: support for this board is not yet upstrea, but is
currently being prepared.
Explanation of changes:
Ideally a new config item would not be required and this
could be driven purely by DTS and hardware.yml configuration.
However, the structures.bf requires changes. This can only
deal with config.h header files, not other more complex
header files. As such it was necessary to introduce a config
item which can be used for this purpose.
The appropriate platforms (as determined by examination of
DTS files) have been updated with the appropriate config
setting. This config setting only has any relevance if
hypervisor mode is already enabled, so should not cause
any difficulty for existing code or configuration.
Note: No testing has been performed on the updated
platforms.
There may be alternative factorings of this, which could
be considered in future work.
Signed-off-by: Ben Leslie <benno@brkawy.com>
- The field 'slot_pos_max' from 'ndks_boot' is not needed, the value
stored there is the constant BIT(CONFIG_ROOT_CNODE_SIZE_BITS).
- Improve the error message if the limit has been reached
Signed-off-by: Axel Heider <axelheider@gmx.de>
The structure actually describes kernel frames and not kernel devices.
In most of the cases a peripherals will fit into one page, but some can
need more pages. On some platform there are no kernel devices at all.
Provides the macro NUM_KERNEL_DEVICE_FRAMES as simple way to find out if
there are mapping that hides the corner cases. This eventually allows
implementing a generic handling even on RISC-V without much overhead, so
the hack for HiFive/Spike can be removed.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This removes the operations that trigger a reschedule or reprogram the
timer from `preemptionPoint` to ensure the relevant state updates in
the proof occur where they are easier to verify.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The L2 cache handling functions were copied from the ARM code in the
initial port, but they are not used on RISC-V. Remove them from the
code base, they can be brought back if a platform has an L2 cache that
needs to be maintained.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
Turns out the invariant 17109eb8c9 refers to is hard to prove
because it is not true, and the runtime check is necessary. This
assertion fails in sel4test SCHED_CONTEXT_0003 (Basic
api_sc_bind/UnbindObject testing).
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a comment to clearly state the functions are empty on purpose, but
they still need to be provided to support the generic code flow.
Signed-off-by: Axel Heider <axelheider@gmx.de>
The functions insert_region() and create_rootserver_objects() are not
used outside of boot.c, so there is no reason to make it publicly
available.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Replace the macro SMP_TERNARY(getCurrentCPUIndex(), 0) by the much
simpler macro CURRENT_CPU_INDEX() that does the same.
Signed-off-by: Axel Heider <axelheider@gmx.de>
CURRENT_CPU_INDEX() is supported to return a word_t. The C parser from
the verification toolchain requires declaring word_t constants without
casting integer values to word_t.
Signed-off-by: Axel Heider <axelheider@gmx.de>
This fixes a correctness and security issue where uncached user
mappings might see old data from before the clearMemory operation.
See also the discussion on GitHub issue #481
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Also merge create_device_untypeds() and create_kernel_untypeds() into
create_untypeds() to simplify the code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Make the definition for NULL generic, so it can be used in constants
that are shared by C and assembly code.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Provide the macro ULL_CONST() for 'unsigned long long' constants, and
use it where applicable.
- Add a verbose explanation why the 'unsigned long long' type is used
for time constants.
Signed-off-by: Axel Heider <axelheider@gmx.de>
- Reorder the macro definitions to ensure things are define before they
are used.
- provide a verbose explanation why the UL_CONST() macro is needed.
- make BIT() macro is defined generic by using UL_CONST().
Signed-off-by: Axel Heider <axelheider@gmx.de>
Also make the output more verbose in case of errors, which is
helpful when porting the kernel to new platforms.
Signed-off-by: Axel Heider <axelheider@gmx.de>
