seL4/include/api
Kent McLeod 9d9bb994e5 debug: create debug_tcb_t struct
Special debug variables that were previously stored at the end of the
tcb_t struct often cause the struct to get too large for the power-of-2
sized untyped object definition. This change moves these variables into
a new structure named debug_tcb_t that is located between the TCB CNode
and the tcb_t struct within a tcb kernel object. Because tcb_t needs to
be stored on a power-of-2 aligned boundary and the TCB CNode only
contains < 5 slots, there is easily > 512 bytes of unused data in every
tcb object. The kernel verification needs to be sure that objects don't
overlap in memory and so this space can't be easily used in a release
build at the moment, but for debug configurations using it shouldn't be
an issue.

Signed-off-by: Kent McLeod <Kent.Mcleod@data61.csiro.au>
2020-07-22 00:31:18 +10:00
..
debug.h debug: create debug_tcb_t struct 2020-07-22 00:31:18 +10:00
failures.h Enabled IPC debug features under new config 2020-04-06 14:21:46 +10:00
faults.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
syscall.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
types.h debug: create debug_tcb_t struct 2020-07-22 00:31:18 +10:00