Ivan Velickovic
Ivan Velickovic
Files generated from the kernel build system, such as `platform_gen.json` and `platform_gen.yaml` currently list the device regions used by the kernel, e.g for the ZCU102: ```yaml devices: - end: 0xf9010000...
The creation of write-only page mappings on RISC-V does not seem correct to me. I believe if I create a mapping with only write permissions, the value of `vmRights` becomes...
The commit that I made https://github.com/seL4/seL4/commit/69040396083959df9bb7cdc193cdf3f13af5bde8 recently seems to have caused a regression when booting seL4, as assertions such as: ``` Booting all finished, dropped to user space seL4 failed...
I'd be keen to have this section finished/fleshed out, but I'm only familiar with virtualising ARM guests on seL4 from a user-space perspective, which is probably not enough to do...
The libsel4 `seL4_GetMR` and `seL4_SetMR` wrappers over accessing the IPC buffer are not documented in the manual. I can understand not wanting to couple the manual to libsel4 since it's...
Why are seL4_TCB_WriteRegisters/seL4_TCB_ReadRegisters not taking into account the count parameter?
Below is the libsel4 definition of `seL4_TCB_WriteRegisters` for AArch64: ``` seL4_TCB_WriteRegisters(seL4_TCB _service, seL4_Bool resume_target, seL4_Uint8 arch_flags, seL4_Word count, seL4_UserContext *regs) { seL4_Error result; seL4_MessageInfo_t tag = seL4_MessageInfo_new(TCBWriteRegisters, 0, 0, 38);...
Given that the IPC fastpath is enabled by default, I was wondering whether it is worth documenting in the manual the conditions for the fastpath to actually be taken so...
Here is what I am confused about/occurred to me from reading the description of domains: * What kind of information flow is limited? To me just "information flow" is pretty...
When making systems that abstract over seL4 system calls/invocations (e.g. seL4 Core Platform) or have more build-time checks (e.g the seL4 Rust crate), it would be useful to be able...
Is there anything stopping the PLIC driver being automatically used on RISC-V platforms if the platform's DTS has the right compatible string (`riscv,plic0`)? Or is it more nuanced than that?