PD 1 running ready stopped PD 2 Notification running Read 'A' ready stopped seL4 running stopped Buffer Write 'A' Write 'B' A B When PD 1 sends a notification to the higher priority PD 2, it gets immediately preempted, until when PD 2 finishes. 0 5 10 15 20 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.