On Wed, Jan 24, 2024 at 6:13 PM Leonid Meyerovich
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,