Fiasco lazy-scheduling question

[eschierb at sci.kun.nl]

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