seL4系統呼叫主要有以下八個：

1. seL4 Send()：
   通過已被命名的cap傳遞訊息，然後允許程式繼續，如果呼叫這個cap的是endpoint，且沒有receiver接收訊息，sender將會被阻塞到有receiver接收。Reciver和核心物件不會返回錯誤。

2. seL4 NBSend()：
   不會阻塞的send，在沒有receiver時，將訊息丟棄，Reciver和核心物件不會返回錯誤。

3. seL4 Call()：
   和seL4_Send()一樣，但是會在訊息上附加回復sender的cap，該cap將存在receiver的TCB中一個特殊的slot中。通過cap呼叫核心服務時，使用seL4_Send()使核心服務可以返回錯誤程式碼或者其他相應。

4. seL4 Wait() ：
   用來通過endpoint接收訊息，如果沒有訊息可接收，則該執行緒被阻塞，直到有訊息可接收。該系統呼叫只能通過endpoint的cap呼叫，否則會導致錯誤。

5. seL4 Reply()：
   用來響應seL4_Call()，將訊息回覆給sender，並將其喚醒。因TCB中僅有一個槽儲存回覆cap，所以seL4_Reply()只能給最近的一個seL4_Call()回覆。

6. seL4 ReplyWait()：
   是seL4_Reply()+seL4_Wait()。能用一次核心系統呼叫同時回覆訊息，並等待下一條訊息。

7. seL4 Poll()：
   將會無阻塞地通過endpoint傳送訊息。該系統呼叫只能被擁有asynchronous endpoint cap的程序呼叫，負責產生錯誤。

8. seL4 Yield()：
   唯一不需要 Capability的系統呼叫。會將呼叫者剩餘的時間片交給同等優先度的可執行執行緒。如果沒有這樣的執行緒，則會重新換新呼叫的執行緒，即該系統呼叫無任何作用。

小小的總結：前7個系統呼叫都是和IPC有關的，而最後一個和排程有關，具體的函式還會在之後的博文中發出來。