- when CONFIG_DEBUG is enabled, track all threads
- when CONFIG_PRINTING is enabled, provide seL4_DebugDumpScheduler which
allows the user to dump the state of the kernel scheduler.
The Arch_hasVCPU function instead of cheaking for whether a thread has a VCPU was
specifically checking for whether a thread on aarch32 had a VCPU, as that was the
condition needed to be passed into sanitiseRegister. This made the implementation
on x86 extremely confusing as Arch_hasVCPU was implemented to return false due to
there being no need for sanitiseRegister on x86 to know whether there was a vcpu.
This commit changes hasVCPU variables to be an abstract archInfo boolean that can
be used arbitrarily by an architecture. Arch_hasVCPU function was also changed to
become Arch_getSanitiseRegisterInfo whose result only passed to sanitiseRegister.
This version of compile_assert is not expanded during verification builds and
can be used in cases where you would like an assertion that contains syntax
that is not supported by the C parser
In the original slow path, armv_contextSwitch_HWASID shoots first.
Verification can't reorder machine operations on hardware state we don't
model. This puts the fastpath into the same order as the slow path.
invokeVCPUReadReg should not be setting message registers for the return message unless
the user performed a call. In doing so we must refactor the call to readVCPUReg to
outside the introduced `if` condition since, as it performs machine operations, it
should always happen
The fields in the multiboot_info structure have precise sizes and should not use pointers
types as these sizes change between ia32 and x86_64 builds. This commit changes such
fields to be the correct fixed size uint32_t
When performing non standalone builds a separate autoconf.h file is generated and defines
the configuration of the kernel. Currently the directory with that file as well as the
kernels include/plat/${PLAT} directory are both listed as include directories to the
compiler. Due to the directory with the generated autoconf.h being earlier in the -I
list the generated autoconf.h will be used in preference to the standalone autoconf.h.
Relying on the order of -I directives is too unstable and so this commit moves the
autoconf.h files to a dedicated configs directory, which is only added as a -I
directive if a standalone build is being performed.
Provides a configuration option for enabling HDCR.TD* traps, or saving and loading debug
state on VCPU switches. Currently verification only plans to support the trap setting.
As this option complicates all of the #ifdef's related to debug registers even further,
abstractions for enabling/disabling each individual piece of the debug code for different
configuration options are also implemented.
Part of these refactored #ifdef guards was to remove the guards completely from libsel4
around the definitions of the number of breakpoints and watchpoints.
We were previously using UNPREDICTABLE behaviour, because we were setting
HDCR.TDE without setting the other debug-related bits in HDCR.
Also, don't duplicate code: just call setHDCRTrapDebugExceptionState
within initHDCR().
A more efficient way of setting up threads' initial context is implemented
by this patch: essentially instead of reading the debug coprocessor everytime
we create a thread, we read the coprocessor once at boot and then assign
those pre-read values when initializing threads.
Previous implementation read a 64-bit value from two registers in one go
and implicitly cast down to paddr_t.
C Parser cannot handle an asm register read into anything other than a
word.
Workaround: perform two 32-bit reads instead, returning one of them.
struct vcpu { struct tcb* tcb; ...
struct arch_tcb { struct vcpu* vcpu; ...
and
struct tcb { struct arch_tcb tcbArch; ...
These conspire to generate a type error on verification side due to
assumptions about non-colliding names.
- Restart TCB from inside the lock if it is waiting for anything other than IRQ
- Only replace the TCB with idle thread if it is in ThreadState_RunningVM state
Also, this makes the design generic to be shared with arm.
This removes some duplicated constants and moves some constants into debug.h such that
they are visible without the user debugging API enabled. These constants are useful
for configuring other debugging/performance monitoring features.
This patch disables the debug register state save and restore on ARM-hyp,
such that Guest VMs can now interfere with one another and trigger
one another for certain limited scenarios. This will be undone later on.
