THE CONTEXT SWITCH MECHANISM IN L4LINUX (Lin's expectation...)

+----------------------------------------------+
| * : L4 thread scheduled by Fiasco scheduler  |
| # : task_struct scheduled by Linux scheduler |
+----------------------------------------------+

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(1) Starting state
 - L4 thread "A" is active.
 - The context of Linux server is the task_struct corresponds to "A".
 - L4 thread "B" is waiting IPC from Linux server.

+-------------------+
| Linux server      |
|+-----------------+|
|| task_struct(A)# ||
|+-----------------+|
|+-----------------+|
|| task_struct(B)  ||
|+-----------------+|
|         :         | +-----------------+ +-----------------+
|         :         | |  L4 thread (A)* | |  L4 thread (B)  |
+-------------------+ +-----------------+ +-----------------+
    (Waiting IPC)          (Running)         (Waiting IPC)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(2) Switch to Linux server
 - Linux server is scheduled by Fiasco scheduler (how to ?).
 - "A" and "B" are waiting IPC from Linux server.

+-------------------+
| Linux server *    |
|+-----------------+|
|| task_struct(A)# <-----------+
|+-----------------+|          | [?]
|+-----------------+|          |
|| task_struct(B)  ||          |
|+-----------------+|          |
|         :         | +-----------------+ +-----------------+
|         :         | |  L4 thread (A)  | |  L4 thread (B)  |
+-------------------+ +-----------------+ +-----------------+
      (Running)          (Waiting IPC)       (Waiting IPC)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(3) Linux server internal context switch
 - schedule() is called in Linux server, and then task_struct of "B"
   becomes the context of it.

+-------------------+
| Linux server *    |
|+-----------------+|
|| task_struct(A)  ||
|+--------l--------+|
|+--------V--------+|
|| task_struct(B)# ||
|+-----------------+|
|         :         | +-----------------+ +-----------------+
|         :         | |  L4 thread (A)  | |  L4 thread (B)  |
+-------------------+ +-----------------+ +-----------------+
      (Running)          (Waiting IPC)       (Waiting IPC)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(4) Switch to "B"
 - Linux server replies IPC to "B" and wait again.
 - "B" is only ready, so it is scheduled.

+-------------------+
| Linux server      |
|+-----------------+|
|| task_struct(A)  ||
|+-----------------+|
|+-----------------+|        [IPC reply ?]
|| task_struct(B)# |-------------------------------+
|+-----------------+|                              V
|         :         | +-----------------+ +-----------------+
|         :         | |  L4 thread (A)  | |  L4 thread (B)  |
+-------------------+ +-----------------+ +-----------------+
    (Waiting IPC)        (Waiting IPC)         (Running)