[seL4] Re: seL4 fault processing
Which architecture are you on and are you using the hardware debug API? I think 4 is for debug exceptions. - Alwin ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: seL4 fault processing
On Wed, Jan 24, 2024 at 6:13 PM Leonid Meyerovich 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/libsel4/arch_include/arm/sel4/arch/shared_types.bf#L16
I wouldn't think though it has `CONFIG_HARDWARE_DEBUG_API` configured
otherwise shouldn't `DebugExpetion` show up in that tag enum.
> Thanks,
___
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: seL4 fault processing
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 wrote: > Which architecture are you on and are you using the hardware debug API? I > think 4 is for debug exceptions. > > - Alwin > ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: seL4 fault processing
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 ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
[seL4] Re: seL4 fault processing
Thank you On Thu, Jan 25, 2024 at 7:09 AM Indan Zupancic 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 > ___ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
