capDL-tool, capdl-loader-app: support bound nfns

Add support for binding notifications to TCBs. Signed-off-by: Nick Spinale <nick@nickspinale.com> Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4 · Jul 1, 2024 · 60d1c3c · 60d1c3c
1 parent e3ff513
commit 60d1c3c
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 3 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -15,6 +15,7 @@
 ### Changes
 
 * add support for SMC capability
+* add support for binding notifications to TCBs
 * enable MCS build; use `seL4_TCB_SetAffinity` only for non-MCS kernels
 * allow `SchedControlCap` to refer to a secondary core
 * minimal update for seL4 AArch64 VSpace API change, removing `seL4_ARM_PageGlobalDirectoryObject`

diff --git a/capDL-tool/CapDL/Model.hs b/capDL-tool/CapDL/Model.hs
@@ -369,8 +369,11 @@ tcbSCSlot = 6
 tcbTempFaultEPSlot :: Word
 tcbTempFaultEPSlot = 7
 
+tcbBoundNotificationSlot :: Word
+tcbBoundNotificationSlot = 8
+
 tcbBoundVCPUSlot :: Word
-tcbBoundVCPUSlot = 8
+tcbBoundVCPUSlot = 9
 
 --
 -- The string used when defining an IOSpaceMasterCap, an ASIDControlCap,

diff --git a/capDL-tool/CapDL/ParserUtils.hs b/capDL-tool/CapDL/ParserUtils.hs
@@ -475,6 +475,7 @@ symbolic_slot =
     <|> keyw "fault_ep_slot" tcbFaultEPSlot
     <|> keyw "sc_slot" tcbSCSlot
     <|> keyw "temp_fault_ep_slot" tcbTempFaultEPSlot
+    <|> keyw "bound_notification" tcbBoundNotificationSlot
     <|> keyw "bound_vcpu" tcbBoundVCPUSlot
 
 parse_slot :: MapParser Word

diff --git a/capDL-tool/CapDL/State.hs b/capDL-tool/CapDL/State.hs
@@ -497,6 +497,7 @@ validTCBSlotCap arch slot cap
     | slot == tcbFaultEPSlot = is _EndpointCap cap
     | slot == tcbSCSlot = is _SCCap cap
     | slot == tcbTempFaultEPSlot = is _EndpointCap cap
+    | slot == tcbBoundNotificationSlot = is _NotificationCap cap
     | slot == tcbBoundVCPUSlot = arch /= RISCV && is _VCPUCap cap
     | otherwise = cap == NullCap
 

diff --git a/capDL-tool/tools/capdl.vim b/capDL-tool/tools/capdl.vim
@@ -24,7 +24,7 @@ syn keyword CapDLAttribute addr affinity badge dom fault_ep G guard guard_size i
 syn match CapDLCPP "[ \t]*#.*$"
 syn match CapDLLiteral "\<\(0x\)\?[0-9]\+\(k\|M\)\?\( bits\)\?\>"
 syn match CapDLLiteral "\<0x[0-f]\+\>"
-syn keyword CapDLSymbolicSlot cspace vspace reply_slot caller_slot ipc_buffer_slot fault_ep_slot sc_slot temp_fault_ep_slot bound_vcpu
+syn keyword CapDLSymbolicSlot cspace vspace reply_slot caller_slot ipc_buffer_slot fault_ep_slot sc_slot temp_fault_ep_slot bound_notification bound_vcpu
 
 syn region Foldable start="{" end="}" fold transparent
 

diff --git a/capdl-loader-app/include/capdl.h b/capdl-loader-app/include/capdl.h
@@ -417,9 +417,10 @@ typedef struct {
 #define CDL_TCB_FaultEP_Slot        5
 #define CDL_TCB_SC_Slot             6
 #define CDL_TCB_TemporalFaultEP_Slot   7
+#define CDL_TCB_Notification_Slot   8
 
 #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
-#define CDL_TCB_VCPU_SLOT           8
+#define CDL_TCB_VCPU_SLOT           9
 #endif
 
 #define CDL_CapData_MakeGuard(x, y) \

diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c
@@ -1013,6 +1013,8 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb)
     if (cdl_ipcbuffer == NULL) {
         ZF_LOGD("  Warning: TCB has no IPC buffer");
     }
+    CDL_Cap *cdl_notification = get_cap_at(cdl_tcb, CDL_TCB_Notification_Slot);
+
 #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
     CDL_Cap *cdl_vcpu = get_cap_at(cdl_tcb, CDL_TCB_VCPU_SLOT);
 #endif
@@ -1030,6 +1032,7 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb)
     seL4_CPtr sel4_vspace_root = cdl_vspace_root ? orig_caps(CDL_Cap_ObjID(cdl_vspace_root)) : 0;
     seL4_CPtr sel4_ipcbuffer   = cdl_ipcbuffer ? orig_caps(CDL_Cap_ObjID(cdl_ipcbuffer)) : 0;
     seL4_CPtr UNUSED sel4_sc   = cdl_sc ? orig_caps(CDL_Cap_ObjID(cdl_sc)) : 0;
+    seL4_CPtr sel4_notification = cdl_notification ? orig_caps(CDL_Cap_ObjID(cdl_notification)) : 0;
 #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
     seL4_CPtr sel4_vcpu        = cdl_vcpu ? orig_caps(CDL_Cap_ObjID(cdl_vcpu)) : 0;
 #endif
@@ -1145,6 +1148,12 @@ static void init_tcb(CDL_Model *spec, CDL_ObjID tcb)
 
     ZF_LOGF_IFERR(error, "");
 
+    if (sel4_notification) {
+        int error = seL4_TCB_BindNotification(sel4_tcb, sel4_notification);
+        ZF_LOGF_IFERR(error, "Failed to bind Notification %s to TCB %s",
+                      CDL_Obj_Name(get_spec_object(spec, CDL_Cap_ObjID(cdl_notification))), CDL_Obj_Name(cdl_tcb));
+    }
+
 #if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) || defined(CONFIG_VTX)
     if (sel4_vcpu) {
 #ifdef CONFIG_ARM_HYPERVISOR_SUPPORT