Handling of periodic components

[podhrmic]

The guide mentions budget and period as thread attributes for each protection domain. My understanding is that:

• budget means how long the PD can run after it gets notified
• period means how often the notify function of PD will be called by the kernel only if there is a pending notification

Is that accurate?

And if so, what is the recommended way for handling a PD that performs some periodic task? For example blinking an LED. I understand that I can set a memory mapped timer, and wait for timer interrupts. But in cases where no MM timer is available to the user space (see seL4/microkit#27), can the kernel be used to provide notifications?

[abrandnewusername]

The budget and period bound the fraction of CPU time that a PD can consume. Briefly, budget is the total amount of time the PD can run during a period of time. For a comprehensive explanation of this model, please check the seL4CP Manual as well as seL4 Manual Chapter 6.1.6.

I will add more explanation to the Guide, thanks for pointing this out.

The seL4 kernel is not responsible for sending periodic notifications. For your case, the potential workaround I can think of is to configure the PD to have the period of the periodic task, and the budget of the amount of time that it needs for execution. You might want it to have a higher priority so the task doesn't often get preempted/blocked by other threads. You might also want to do a seL4_Yield to donate the remaining budget. With this implementation, your task will behave more like a sporadic task.

It might be easier to use a board that has usable timers instead of using QEMU :).