From 553f3667a0b71e5264a3e5950ee800f5a88d5a50 Mon Sep 17 00:00:00 2001 From: Nick Spinale Date: Fri, 12 Mar 2021 22:36:09 +0000 Subject: [PATCH] capDL-tool, capdl-loader-app: support bound nfns Add support for binding notifications to TCBs. Signed-off-by: Nick Spinale Signed-off-by: Gerwin Klein --- CHANGES.md | 1 + capDL-tool/CapDL/Model.hs | 5 ++++- capDL-tool/CapDL/ParserUtils.hs | 1 + capDL-tool/CapDL/State.hs | 1 + capDL-tool/tools/capdl.vim | 2 +- capdl-loader-app/include/capdl.h | 3 ++- capdl-loader-app/src/main.c | 9 +++++++++ 7 files changed, 19 insertions(+), 3 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 47896e3d..5327445e 100644 --- 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 index c57412d1..7d29265d 100644 --- 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 index 5ebcfa63..500aa981 100644 --- 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 index 7da1a830..6d4caa48 100644 --- 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 index 75253585..8f727393 100644 --- 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 index 32d46253..6aa0ea4f 100644 --- 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 index e3a5c380..b464e419 100644 --- 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