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>
With this change, even architectures which do not use a distinct region
to map the kernel ELF will use the `kpptr_to_addr` to translate any
address from the kernel region.
This ensures that these accesses are correctly checked for bounds when
used and will make it easier to move the ELF mapping into a distinct
region of virtual address space.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Move all of the virtual to physical translation functions into a single
common file and use the updated constants.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Like SCTLR, CNTV_CTL is switched to/from hardware when we enable/disable
the VCPU, so it must be read from a saved VCPU context when that VCPU
isn't active.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
The scheduler cannot correctly schedule once the timestamp exceeds
MAX_RELEASE_TIME as releases beyond this point may be subject to
overflow. For most systems this should still allow a great many years if
the timestamp starts from 0 at system boot.
Some systems currently start with a random initial timestamp and my
begin with a timestamp that prvents correct budgeting. This assert helps
to catch cases where scheduling becomes invalid due to the timestamp
exceeding the give bound.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
The proofs currently only guarantee that the system scheduler is correct
while the current time is less than INT64_MAX - 3 * MAX_PERIOD ticks.
With the MAX_PERIOD configured to almost INT64_MAX, this would imply
that the system scheduler is never correct.
To ensure that we get a large duration where the system is correct, we
take 1/8th of the TOTAL representable time as the MAX_PERIOD, ensuring
that 3 * MAX_PERIOD is still less than half of all representable time.
For a system with a 1MHz scheduling clock, this produces a valid
execution time on the order of 2^19 years.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This re-introduces the overrun handling but bounds charging of budget
such that we never calculate a refill with a start using an integer
overflow.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
A refill can still be charged if the refill list is full. This means
that we only require sufficient capacity to continue a timeslice.
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
This replaces the refill_split_check and refill_budget_check with a
single function that chanrges the provided usage to an SC and updates
the refills.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
Remove the UART handling details from the top level I/O handling that
implements printf(). The architecture's I/O handling must define how
the debug channel is implemented and what special handling is
required. This allows separating UART and SBI debug output handling.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Replace capDL() by a generic debug_capDL() where all architectures are
supposed to provide an implementation or print an error.
Signed-off-by: Axel Heider <axelheider@gmx.de>
