seL4/include
Gerwin Klein 90dafb2e71 yieldTo: respect kernel reply protocol
Before:

- invokeSchedContext_Consumed and invokeSchedContext_YieldTo clobber
  the message info field in the reply from kernel, which results in a
  length 0 message.

- invokeSchedContext_Consumed and invokeSchedContext_YieldTo may crash
  the kernel for read-only IPC buffers

- invokeSchedContext_Consumed and invokeSchedContext_YieldTo generate
  a reply from kernel for syscalls that should not generate replies

- completeYieldTo does not set the badge register, which will contain
  whatever that previous syscall returned and not correctly indicate
  success/failure.

- completeYieldTo sets registers of the current thread, combined with
  IPC buffer message registers of potentially another thread.

Instead:

- pass the thread to setConsumed instead of the IPC buffer, so we can
  write to the correct registers

- look up the IPC buffer again and check for write authority

- follow the kernel reply protocol, which includes only generating a
  message for `call`. This means, we need to pass the flag through from
  higher-level decode functions.

- set thread state to Running if a reply message from the kernel was
  created, leave on Restart for default empty success message.

- set the badge register

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
2025-06-04 15:54:45 +02:00
..
32/mode Bump minimum CMake version 2025-02-26 17:11:57 +11:00
64/mode Bump minimum CMake version 2025-02-26 17:11:57 +11:00
api treewide: typo fixes 2025-04-14 12:05:16 +10:00
arch cleanup: remove obselete pageType and asidMax 2025-05-02 12:39:23 +01:00
benchmark benchmark: config opt. name to enable log buffer 2022-03-31 08:56:06 +11:00
drivers Add support for SiFive Premier P550 platform 2025-04-02 13:51:53 +11:00
fastpath reply: do not assume replyObject NULL invariant 2025-02-10 15:53:08 +11:00
kernel treewide: typo fixes 2025-04-14 12:05:16 +10:00
machine treewide: typo fixes 2025-04-14 12:05:16 +10:00
model statedata: only define tlbLockCount when needed 2025-03-12 13:36:10 +11:00
object yieldTo: respect kernel reply protocol 2025-06-04 15:54:45 +02:00
plat treewide: typo fixes 2025-04-14 12:05:16 +10:00
smp SMP: Fix IPI Race 2025-02-27 09:29:48 +11:00
api.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
assert.h debug: use c99 standard instead of gcc extensions 2023-11-16 12:09:52 +00:00
basic_types.h boot: document region types 2023-04-12 15:07:02 +10:00
bootinfo.h boot: Remove constant BI_FRAME_SIZE_BITS 2023-08-23 15:10:32 +02:00
compound_types.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
config.h libsel4: Fix name for AARCH64_VSPACE_S2_START_L1 2021-09-06 08:08:54 +10:00
hardware.h boot: simplify boot code recycling 2023-08-13 09:04:26 +10:00
linker.h replacing all ifndef with pargma once 2020-03-23 11:04:46 +11:00
machine.h re-use existing functions to avoid redundancy 2022-09-15 11:25:04 +02:00
object.h trivial: remove duplicate headers 2022-02-05 15:30:25 +11:00
stdarg.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
stdint.h print 64-bit integers on 32-bits systems fully 2021-11-26 06:01:11 +01:00
string.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
types.h trivial: remove superfluous empty lines 2021-09-27 23:09:09 +10:00
util.h utils: wrap config_set for verification 2025-03-28 10:53:48 +11:00