f9micro / f9-kernel

An efficient and secure microkernel built for ARM Cortex-M cores, inspired by L4
Other
679 stars 145 forks source link

L4 error message codes do not match documentation. #161

Open ab1aw opened 5 years ago

ab1aw commented 5 years ago

I am looking at the error codes on page 64 of the L4 eXperimental Kernel Reference Manual Version X.2 Document Revision 6 November 17, 2006

The error code values and descriptions in that document do not match the F9 implementation in the file user/include/l4/thread.h

I encountered this issue while debugging an IPC timeout failure when invoking L4_Receive_Timeout(). The error use case was that the sending thread did not call L4_Send() prior to the receiving thread timeout duration expiring. The error message in this case was ' ErrorCode = 0x3 l4_error_invalid_space'. In addition, the thread (app) crashed rather than continuing to process the error and recovering to retry the L4_Receive_Timeout().

My questions: 1 - Should the error codes and descriptions match the aforementioned document? 2 - Should a crash/dump occur upon a timeout when calling L4_Receive_Timeout()?

Thank you.