Interprocess Communication & the L4 Microkernel

Figure 2: Definition of the IPC system call.

IPC(To, FromSpecifier, Timeouts) 

Arguments:                   Returns:
----------------------       -------------
ThreadId To
ThreadId FromSpecifier   ->  ThreadId From 
Word	 Timeouts


Argument Semantics:
---------------------
To == nilthread 
	-> IPC includes no send phase

To != nilthread 
	-> Destination thread and IPC includes a send phase	

FromSpecifier == nilthread 
	-> IPC includes no receive phase

FromSpecifier == anythread 
	-> Incoming messages are accepted from any thread or hardware interrupts and IPC includes a receive phase

FromSpecifier == anylocalthread 
	-> Incoming messages are accepted from any thread in the current address space and IPC includes a receive phase

FromSpecifier != (nilthread OR anythread OR anylocalthread)
	-> Incoming messages are only accepted from the specified thread and IPC includes a receive phase

Timeouts == RcvTimeout
	-> Receive phase waits until either a message transfer starts or the RcvTimeout expires. Ignored for send-only IPC.

Timeouts == SndTimeout
	-> If the send timeout expires before the message transfer could start then the IPC operation fails.

Return Semantics:
------------------
From <- Thread ID of the sender. The delivered thread IDs are always local unless they identify a thread running in a 			different address space.