Hi,
I'm Erik Schierboom and I study at the Radboud University Nijmegen. Right now, I'm writing my master thesis, under supervision of Hendrik Tews, on the formal verification of a part of Fiasco's IPC implementation. I studied the thesis by René Reusner but I don't fully grasp the lazy-scheduling details. I have the following questions.
For one, the description says that the sender is not removed from the ready-list when the switch is made to the receiver (even though it is now in waiting status). However, as the sender is the active thread it is not part of the ready-list by definition (at least that is how I interpreted the system), so how could it be removed anyway?
Secondly, the switching from sender to receiver is simply an execution context switch. If the receiver finishes before the sender's time is up, does the receiver switch the execution context back to that of the sender?
With regards,
Erik