My root task (root thread created by kernel) checks for fault from the other threads, which are created in root thread with badged fault_ep
seL4_Word badge; seL4_MessageInfo_t messageInfo = seL4_NBRecv(init_objects.fault_cap, &badge); if (seL4_MessageInfo_get_label(messageInfo) != seL4_Fault_NullFault ) { process_fault(messageInfo, badge); }
Normally I don't have any faults, but every time I have seL4_MessageInfo_get_label(messageInfo) == 4, which is not in seL4_Fault_tag enumeration type
enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 };
Could somebody explain?
Thanks,
Which architecture are you on and are you using the hardware debug API? I think 4 is for debug exceptions.
- Alwin
I don't have any faults if I use seL4_Recv instead (in a separate thread). It happens only if I use seL4_NBRecv and check the tag after it returns. I use AARCH64
On Wed, Jan 24, 2024 at 3:59 PM Alwin Joshy alwin.joshy@unsw.edu.au wrote:
Which architecture are you on and are you using the hardware debug API? I think 4 is for debug exceptions.
- Alwin
Hello Leonid,
On 2024-01-24 21:16, Leonid Meyerovich wrote:
I don't have any faults if I use seL4_Recv instead (in a separate thread). It happens only if I use seL4_NBRecv and check the tag after it returns.
If there is no message or fault pending, seL4_NBRecv() will return immediately. When that happens, the badge value will be zero and no messageInfo will be returned. That is, whatever was in register X1 at the time of the call will be returned.
You have to use non-zero badges and check the badge value for non-blocking system calls, assuming you actually want non-blocking behaviour, which is unlikely.
The only way to find this out is by reading the code, it's not documented in the manual as it should have been.
Greetings,
Indan
Thank you
On Thu, Jan 25, 2024 at 7:09 AM Indan Zupancic indan@nul.nu wrote:
Hello Leonid,
On 2024-01-24 21:16, Leonid Meyerovich wrote:
I don't have any faults if I use seL4_Recv instead (in a separate thread). It happens only if I use seL4_NBRecv and check the tag after it returns.
If there is no message or fault pending, seL4_NBRecv() will return immediately. When that happens, the badge value will be zero and no messageInfo will be returned. That is, whatever was in register X1 at the time of the call will be returned.
You have to use non-zero badges and check the badge value for non-blocking system calls, assuming you actually want non-blocking behaviour, which is unlikely.
The only way to find this out is by reading the code, it's not documented in the manual as it should have been.
Greetings,
Indan
On Wed, Jan 24, 2024 at 6:13 PM Leonid Meyerovich leonid@trustedst.com wrote:
My root task (root thread created by kernel) checks for fault from the other threads, which are created in root thread with badged fault_ep
seL4_Word badge; seL4_MessageInfo_t messageInfo = seL4_NBRecv(init_objects.fault_cap,&badge); if (seL4_MessageInfo_get_label(messageInfo) != seL4_Fault_NullFault ) { process_fault(messageInfo, badge); }
Normally I don't have any faults, but every time I have seL4_MessageInfo_get_label(messageInfo) == 4, which is not in seL4_Fault_tag enumeration type
enum seL4_Fault_tag { seL4_Fault_NullFault = 0, seL4_Fault_CapFault = 1, seL4_Fault_UnknownSyscall = 2, seL4_Fault_UserException = 3, seL4_Fault_VMFault = 5, seL4_Fault_VGICMaintenance = 6, seL4_Fault_VCPUFault = 7, seL4_Fault_VPPIEvent = 8 };
Could somebody explain?
I can't really explain it, but I wanted to note the DebugException appears to typically have tag 4, IIUC the above `enum seL4_Fault_tag` appears to be generated by the following with non-mcs + arm hypervisor support, https://github.com/seL4/seL4/blob/5df69647820f4517378f0e3d4af7347560f8c791/l... I wouldn't think though it has `CONFIG_HARDWARE_DEBUG_API` configured otherwise shouldn't `DebugExpetion` show up in that tag enum.
Thanks,
-
Alwin Joshy -
Indan Zupancic -
Leonid Meyerovich -
Matt Rice