From 33c2bc3bf2c45a96c42d78e8f23ab31f17d4b5de Mon Sep 17 00:00:00 2001
From: Norman Feske <norman.feske@genode-labs.com>
Date: Tue, 10 Feb 2015 15:33:45 +0100
Subject: [PATCH] sel4: capability delegation test

---
 repos/base-sel4/doc/ipc_and_virt_mem.txt | 45 ++++++++++++++++++++++++
 repos/base-sel4/src/test/sel4/main.cc    | 21 ++++++++++-
 2 files changed, 65 insertions(+), 1 deletion(-)

diff --git a/repos/base-sel4/doc/ipc_and_virt_mem.txt b/repos/base-sel4/doc/ipc_and_virt_mem.txt
index b4c62f2e1..5af612c26 100644
--- a/repos/base-sel4/doc/ipc_and_virt_mem.txt
+++ b/repos/base-sel4/doc/ipc_and_virt_mem.txt
@@ -140,6 +140,51 @@ desired output:
 ! void second_thread_entry(): returned from seL4_Reply
 
 
+Delegation of capabilities via IPC
+==================================
+
+The seL4 kernel supports the delegation of capabilities across address-space
+boundaries by the means of synchronous IPC. As Genode fundamentally relies
+on such a mechanism, I decide to give it a try by extending the simple IPC
+test. Instead of letting the main thread call the second thread without any
+arguments, the main thread will pass the thread capability of the second
+thread as argument. Upon reception of the call, the second thread will find
+a capability in its IPC buffer. To validate that the received capability
+corresponds to the thread cap, the second thread issues a 'seL4_TCB_Suspend'
+operation on the received cap. It is supposed to stop it execution right
+there. This experiment requires the following steps:
+
+# At the caller side, we need to supply a capability as argument to the
+  'seL4_Call' operation by specifying the number of capabilities to transfer
+  at the 'extraCaps' field of the 'seL4_MessageInfo', and marshalling the
+  index of the capability via the 'seL4_SetCap' function (specifying
+  SECOND_THREAD_CAP as argument).
+
+# At the callee side, we need to define where to receive an incoming
+  capability. First, we have to reserve a CNode slot designated for the
+  new capability. For the test, a known-free index will do:
+
+  ! enum { RECV_CAP = 0x102 };
+
+  Second, we have to configure the IPC buffer of the second thread to
+  point to the RECV_CAP:
+
+  ! seL4_SetCapReceivePath(seL4_CapInitThreadCNode, RECV_CAP, 32);
+
+  We specify 32 as receive depth because the CNode of the initial thread has a
+  size of 2^12 and a guard of 20.
+
+At this point I am wondering that there is apparently no way to specify a
+*receive window* rather than an individual CNode for receiving capabilities.
+After revisiting Section 4.2.2 of the manual, I came to the realization that
+*seL4 does not support delegating* *more than one capability in a single IPC*.
+From Genode's perspective, this could become an issue because Genode's RPC
+framework generally allows for the delegation of multiple capabilities via a
+single RPC call.
+
+That said, the simple capability-delegation test works as expected.
+
+
 
 
 
diff --git a/repos/base-sel4/src/test/sel4/main.cc b/repos/base-sel4/src/test/sel4/main.cc
index 35a35bd51..7a5b96444 100644
--- a/repos/base-sel4/src/test/sel4/main.cc
+++ b/repos/base-sel4/src/test/sel4/main.cc
@@ -82,14 +82,30 @@ enum { SECOND_THREAD_CAP = 0x100 };
  */
 enum { EP_CAP = 0x101 };
 
+/*
+ * Capability slot used by the second thread to receive a capability via IPC.
+ */
+enum { RECV_CAP = 0x102 };
+
 
 void second_thread_entry()
 {
 	init_ipc_buffer();
 
+	seL4_SetCapReceivePath(seL4_CapInitThreadCNode, RECV_CAP, 32);
+
 	PDBG("call seL4_Wait");
 	seL4_MessageInfo_t msg_info = seL4_Wait(EP_CAP, nullptr);
 	PDBG("returned from seL4_Wait, call seL4_Reply");
+
+	PDBG("msg_info: got unwrapped  %d", seL4_MessageInfo_get_capsUnwrapped(msg_info));
+	PDBG("          got extra caps %d", seL4_MessageInfo_get_extraCaps(msg_info));
+	PDBG("          label          %d", seL4_MessageInfo_get_label(msg_info));
+
+	seL4_TCB_Suspend(RECV_CAP);
+
+	PDBG("this message should not appear");
+
 	seL4_Reply(msg_info);
 	PDBG("returned from seL4_Reply");
 
@@ -211,7 +227,10 @@ int main()
 
 	PDBG("call seL4_Call");
 
-	seL4_MessageInfo_t msg_info = seL4_MessageInfo_new(0, 0, 0, 0);
+	seL4_MessageInfo_t msg_info = seL4_MessageInfo_new(13, 0, 1, 0);
+
+	seL4_SetCap(0, SECOND_THREAD_CAP);
+
 	seL4_Call(EP_CAP, msg_info);
 
 	PDBG("returned from seL4_Call");