diff --git a/src/kernel/boot.c b/src/kernel/boot.c index 549e8a22a14e1e0dab1f6a8d356a0d0eb93054ca..a7700c8f56f353f8cb4be84bf9a4ec2dc7b25a8c 100644 --- a/src/kernel/boot.c +++ b/src/kernel/boot.c @@ -370,6 +370,7 @@ create_initial_thread( pptr_t pptr; cap_t cap; tcb_t* tcb; + deriveCap_ret_t dc_ret; /* allocate TCB */ pptr = alloc_region(TCB_BLOCK_SIZE_BITS); @@ -382,6 +383,13 @@ create_initial_thread( tcb->tcbTimeSlice = CONFIG_TIME_SLICE; Arch_initContext(&tcb->tcbContext); + /* derive a copy of the IPC buffer cap for inserting */ + dc_ret = deriveCap(SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), ipcbuf_cap); + if (dc_ret.status != EXCEPTION_NONE) { + printf("Failed to derive copy of IPC Buffer\n"); + return false; + } + /* initialise TCB (corresponds directly to abstract specification) */ cteInsert( root_cnode_cap, @@ -394,7 +402,7 @@ create_initial_thread( SLOT_PTR(pptr, tcbVTable) ); cteInsert( - ipcbuf_cap, + dc_ret.cap, SLOT_PTR(pptr_of_cap(root_cnode_cap), BI_CAP_IT_IPCBUF), SLOT_PTR(pptr, tcbBuffer) );