PD 1 running ready stopped PD 2 Notification running ready Read 'A' stopped seL4 running stopped Write 'A' Write 'B' Buffer A B 0 5 10 15 20 When PD 1 sends a notification to the higher priority PD 2, it gets immediately preempted, until when PD 2 finishes. The data written to the buffer can be consumed by PD 2, provided that it takes less time than the remaining budget in the current period of PD 2.