Add notes about the budget and interrupts #36
Conversation
| } | ||
| ``` | ||
|
|
||
| On the other hand, if a PD has `budget` available, but receives no notification, it is not run at all. Returning from `notified()` function and calling `seL4_Yield()` during the PD execution has the same effect, and donates the remaining budget of the PD. |
There was a problem hiding this comment.
"Returning from notified() function and calling seL4_Yield() during the PD execution has the same effect, and donates the remaining budget of the PD." Has the same effect as what exactly? I'm not sure what you mean by calling seL4_Yield after returning from the notified entry point?
There was a problem hiding this comment.
This is based on the discussion here. In my understanding, you can either return from notified() or call seL4_Yield() somewhere in your notified() function, and that will end the execution of that particular PD in the given period. Is that accurate?
There was a problem hiding this comment.
While seL4CP doesn't stop anyone from doing this in their user-code, I am kind of hesitant to have this in the manual as I don't think there should be any need to call seL4_Yield and having a non-event driven PD seems to go against the principles of seL4CP.
docs/manual.md
Outdated
| @@ -263,6 +292,8 @@ sel4cp does not provides timers, nor any *sleep* API. | |||
| After initialisation, activity in the system is initiated by an interrupt causing a `notified` entry point to be invoked. | |||
| That notified function may in turn notify or call other protection domains that cause other system activity, but eventually all activity indirectly initiated from that interrupt will complete, at which point the system is inactive again until another interrupt occurs. | |||
|
|
|||
| An interrupt must be acknowledged with `sel4cp_irq_ack()` in the `notified()` function, otherwise it will not be fired again. | |||
There was a problem hiding this comment.
An interrupt doesn't necessarily have to be acknowledged in the notified() function. My understanding is that the interrupt will continue to be fired, it just won't be delivered to seL4. Perhaps it would be better to say "otherwise the interrupt will not be delivered again".
There was a problem hiding this comment.
Good point, I updated the wording.
|
Just a general question I have is how did you interpret seL4-specific terminology such as "scheduling context" which isn't really explained in the seL4CP manual? Did you refer to the seL4 manual or are you already familiar with the concepts from previous seL4 experience? |
I read the seL4 manual, and have some previous experience, but I am by no means an seL4 expert. |
Cool, was just wondering. We should probably link to the seL4 manual or explain what a scheduling context is in the seL4CP manual but that can be done in another PR. |
|
@Ivan-Velickovic I am happy to close this PR - the existing documentation and tutorial is IMHO pretty good, if there is a need to further explain scheduling, perhaps a separate dedicated chapter with examples is better. |
|
There are some useful changes here, I just think the code example is not necessary. You can close the PR and I can take your patch and adjust in a new PR, if that's okay with you. |
Clarifications.