seL4/include
Ben Leslie 0c6229d598 Add support for GICv3 virtualization
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>
2021-09-03 10:23:06 +10:00
..
32/mode replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
64/mode replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
api prefer macro CURRENT_CPU_INDEX() 2021-08-17 18:19:37 +10:00
arch Add support for GICv3 virtualization 2021-09-03 10:23:06 +10:00
benchmark KernelBenchmarksTrackUtilisation: Add more stats 2020-07-15 15:15:27 +10:00
drivers debug: restructure kernel console handling 2021-05-14 13:13:36 +10:00
fastpath replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
kernel boot: remove ndks_boot.slot_pos_max 2021-09-02 08:44:24 +10:00
machine debug: restructure kernel console handling 2021-05-14 13:13:36 +10:00
model define macro SEL4_WORD_CONST() 2021-08-17 18:19:37 +10:00
object mcs: Only unbind extant donated ntfn sc 2021-04-29 12:07:07 +10:00
plat risc-v: remove obsolete file 2021-07-05 09:17:33 +10:00
smp Repair barriers in clh_lock_acquire 2020-06-22 11:53:08 +10:00
api.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
assert.h ensure assert() macro is an atom 2021-08-19 08:28:27 +10:00
basic_types.h define macro SEL4_WORD_CONST() 2021-08-17 18:19:37 +10:00
bootinfo.h trivial: improve style for code and comments 2021-08-31 10:53:31 +10:00
compound_types.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
config.h trivial: remove empty lines 2021-04-01 10:33:41 +10:00
hardware.h boot: make linker definitions generic 2021-07-01 11:30:19 +10:00
linker.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
machine.h use const qualifier 2021-07-01 10:48:47 +10:00
object.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
stdarg.h Revised kernel printf implementation 2020-05-19 13:16:20 +10:00
stdint.h support PRIu64 and SEL4_PRIu_word in kernel 2021-05-14 13:34:38 +10:00
string.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
types.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
util.h trivial: improve style for code and comments 2021-08-31 10:53:31 +10:00