Support reply objects in seL4_libs Only if CONFIG_KERNEL_RT is enabled will they work, but most of the code is compiled in order to make maintenance easier.
diff --git a/libsel4utils/include/sel4utils/process.h b/libsel4utils/include/sel4utils/process.h index ec3731c..89a903c 100644 --- a/libsel4utils/include/sel4utils/process.h +++ b/libsel4utils/include/sel4utils/process.h
@@ -89,8 +89,11 @@ /* the slot for this processes sc */ SEL4UTILS_SCHED_CONTEXT_SLOT = 6, + /* The slot for this processes reply object */ + SEL4UTILS_REPLY_SLOT = 7, + /* First free slot in the cspace configured by sel4utils */ - SEL4UTILS_FIRST_FREE = 7 + SEL4UTILS_FIRST_FREE = 8 }; /**
diff --git a/libsel4utils/include/sel4utils/thread.h b/libsel4utils/include/sel4utils/thread.h index e1128e5..2546b1f 100644 --- a/libsel4utils/include/sel4utils/thread.h +++ b/libsel4utils/include/sel4utils/thread.h
@@ -45,6 +45,8 @@ seL4_CPtr ipc_buffer; seL4_Word ipc_buffer_addr; bool own_sc; + bool own_reply; + vka_object_t reply; } sel4utils_thread_t; typedef struct sel4utils_checkpoint {
diff --git a/libsel4utils/include/sel4utils/thread_config.h b/libsel4utils/include/sel4utils/thread_config.h index 62adbef..67df9c5 100644 --- a/libsel4utils/include/sel4utils/thread_config.h +++ b/libsel4utils/include/sel4utils/thread_config.h
@@ -57,6 +57,10 @@ bool no_ipc_buffer; /* scheduling parameters */ sched_params_t sched_params; + /* true if sel4utils should create a reply */ + bool create_reply; + /* otherwise provide one */ + seL4_CPtr reply; } sel4utils_thread_config_t; static inline sched_params_t @@ -82,6 +86,21 @@ } static inline sel4utils_thread_config_t +thread_config_create_reply(sel4utils_thread_config_t config) +{ + config.create_reply = true; + return config; +} + +static inline sel4utils_thread_config_t +thread_config_reply(sel4utils_thread_config_t config, seL4_CPtr reply) +{ + config.create_reply = false; + config.reply = reply; + return config; +} + +static inline sel4utils_thread_config_t thread_config_sched_context(sel4utils_thread_config_t config, seL4_CPtr sched_context) { config.sched_params.create_sc = false;
diff --git a/libsel4utils/src/irq_server/irq_server.c b/libsel4utils/src/irq_server/irq_server.c index 8ff7b5b..04bd331 100644 --- a/libsel4utils/src/irq_server/irq_server.c +++ b/libsel4utils/src/irq_server/irq_server.c
@@ -267,6 +267,7 @@ struct irq_server { seL4_CPtr delivery_ep; + vka_object_t reply; seL4_Word label; int max_irqs; vspace_t* vspace; @@ -349,6 +350,13 @@ ZF_LOGE("malloc failed on irq server memory allocation"); return -1; } + + if (config_set(CONFIG_KERNEL_RT) && vka_alloc_reply(vka, &irq_server->reply) != 0) { + ZF_LOGE("Failed to allocate reply object"); + free(irq_server); + return -1; + } + irq_server->delivery_ep = sync_ep; irq_server->label = label; irq_server->max_irqs = nirqs; @@ -384,7 +392,11 @@ seL4_Word badge; /* Wait for an event */ +#ifdef CONFIG_KERNEL_RT + msginfo = seL4_Recv(irq_server->delivery_ep, &badge, irq_server->reply.cptr); +#else msginfo = seL4_Recv(irq_server->delivery_ep, &badge); +#endif if (badge_ret) { *badge_ret = badge; }
diff --git a/libsel4utils/src/process.c b/libsel4utils/src/process.c index 4e5d4f4..cff1eb3 100644 --- a/libsel4utils/src/process.c +++ b/libsel4utils/src/process.c
@@ -619,6 +619,7 @@ thread_config = thread_config_cspace(thread_config, process->cspace.cptr, cspace_root_data); thread_config = thread_config_fault_endpoint(thread_config, SEL4UTILS_ENDPOINT_SLOT); thread_config.sched_params = config.sched_params; + thread_config.create_reply = config.create_cspace; error = sel4utils_configure_thread_config(vka, spawner_vspace, &process->vspace, thread_config, &process->thread); if (error) { @@ -642,9 +643,13 @@ if (config.create_cspace && config_set(CONFIG_KERNEL_RT)) { slot = sel4utils_copy_cap_to_process(process, vka, process->thread.sched_context.cptr); assert(slot == SEL4UTILS_SCHED_CONTEXT_SLOT); + slot = sel4utils_copy_cap_to_process(process, vka, process->thread.reply.cptr); + assert(slot == SEL4UTILS_REPLY_SLOT); } else { /* skip the sc slot */ allocate_next_slot(process); + /* skip the reply object slot */ + allocate_next_slot(process); } return 0;
diff --git a/libsel4utils/src/serial_server/parentapi.c b/libsel4utils/src/serial_server/parentapi.c index 195f069..216b5a9 100644 --- a/libsel4utils/src/serial_server/parentapi.c +++ b/libsel4utils/src/serial_server/parentapi.c
@@ -58,6 +58,11 @@ return error; } + /* Allocate a reply object that the server will track replies in */ + if (config_set(CONFIG_KERNEL_RT) && !vka_alloc_reply(parent_vka, &get_serial_server()->reply)) { + ZF_LOGE(SERSERVP"spawn_thread: failed to allocate reply"); + goto out; + } /* And also allocate a badged copy of the Server's endpoint that the Parent * can use to send to the Server. This is used to allow the Server to report * back to the Parent on whether or not the Server successfully bound to a @@ -178,6 +183,9 @@ if (get_serial_server()->parent_badge_value != SERIAL_SERVER_BADGE_VALUE_EMPTY) { serial_server_badge_value_free(get_serial_server()->parent_badge_value); } + if (get_serial_server()->reply.cptr != 0) { + vka_free_object(parent_vka, &get_serial_server()->reply); + } vka_free_object(parent_vka, &get_serial_server()->server_ep_obj); return error; }
diff --git a/libsel4utils/src/serial_server/serial_server.h b/libsel4utils/src/serial_server/serial_server.h index 93ecb2b..e2a12c3 100644 --- a/libsel4utils/src/serial_server/serial_server.h +++ b/libsel4utils/src/serial_server/serial_server.h
@@ -131,6 +131,7 @@ seL4_Word parent_badge_value; cspacepath_t _badged_server_ep_cspath; + vka_object_t reply; } serial_server_context_t; /* Global server instance accessor functions. */
diff --git a/libsel4utils/src/serial_server/server.c b/libsel4utils/src/serial_server/server.c index f9c56b4..23d3a3b 100644 --- a/libsel4utils/src/serial_server/server.c +++ b/libsel4utils/src/serial_server/server.c
@@ -34,6 +34,24 @@ return &serial_server; } +static inline seL4_MessageInfo_t recv(seL4_Word *sender_badge) +{ +#ifdef CONFIG_KERNEL_RT + return seL4_Recv(get_serial_server()->server_ep_obj.cptr, sender_badge, get_serial_server()->reply.cptr); +#else + return seL4_Recv(get_serial_server()->server_ep_obj.cptr, sender_badge); +#endif +} + +static inline void reply(seL4_MessageInfo_t tag) +{ +#ifdef CONFIG_KERNEL_RT + seL4_Send(get_serial_server()->reply.cptr, tag); +#else + seL4_Reply(tag); +#endif +} + serial_server_registry_entry_t * serial_server_registry_get_entry_by_badge(seL4_Word badge_value) { @@ -425,11 +443,11 @@ * First call seL4_Recv() to get the Reply cap back to the Parent, and then * seL4_Reply to report our status. */ - seL4_Recv(get_serial_server()->server_ep_obj.cptr, &sender_badge); + recv(&sender_badge); seL4_SetMR(SSMSGREG_FUNC, FUNC_SERVER_SPAWN_SYNC_ACK); tag = seL4_MessageInfo_new(error, 0, 0, SSMSGREG_SPAWN_SYNC_ACK_END); - seL4_Reply(tag); + reply(tag); /* If the bind failed, this thread has essentially failed its mandate, so * there is no reason to leave it scheduled. Kill it (to whatever extent @@ -444,7 +462,7 @@ /* Set the CNode slots where caps from clients will go */ serial_server_set_frame_recv_path(); - tag = seL4_Recv(get_serial_server()->server_ep_obj.cptr, &sender_badge); + tag = recv(&sender_badge); ZF_LOGD(SERSERVS "main: Got message from %x", sender_badge); func = seL4_GetMR(SSMSGREG_FUNC); @@ -476,7 +494,7 @@ seL4_SetMR(SSMSGREG_CONNECT_ACK_MAX_SHMEM_SIZE, get_serial_server()->shmem_max_size); tag = seL4_MessageInfo_new(error, 0, 0, SSMSGREG_CONNECT_ACK_END); - seL4_Reply(tag); + reply(tag); break; case FUNC_WRITE_REQ: @@ -507,7 +525,7 @@ seL4_SetMR(SSMSGREG_FUNC, FUNC_WRITE_ACK); seL4_SetMR(SSMSGREG_WRITE_ACK_N_BYTES_WRITTEN, bytes_written); tag = seL4_MessageInfo_new(error, 0, 0, SSMSGREG_WRITE_ACK_END); - seL4_Reply(tag); + reply(tag); break; case FUNC_DISCONNECT_REQ: @@ -517,7 +535,7 @@ seL4_SetMR(SSMSGREG_FUNC, FUNC_DISCONNECT_ACK); tag = seL4_MessageInfo_new(error, 0, 0, SSMSGREG_DISCONNECT_ACK_END); - seL4_Reply(tag); + reply(tag); break; case FUNC_KILL_REQ: @@ -526,7 +544,7 @@ /* The actual contents of the Reply don't matter here. */ seL4_SetMR(SSMSGREG_FUNC, FUNC_KILL_ACK); tag = seL4_MessageInfo_new(0, 0, 0, SSMSGREG_KILL_ACK_END); - seL4_Reply(tag); + reply(tag); /* Break out of the loop */ keep_going = 0; break;
diff --git a/libsel4utils/src/thread.c b/libsel4utils/src/thread.c index e568663..05041a9 100644 --- a/libsel4utils/src/thread.c +++ b/libsel4utils/src/thread.c
@@ -48,6 +48,7 @@ sel4utils_thread_config_t config = {0}; config = thread_config_fault_endpoint(config, fault_endpoint); config = thread_config_cspace(config, cspace, cspace_root_data); + config = thread_config_create_reply(config); return sel4utils_configure_thread_config(vka, parent, alloc, config, res); } @@ -78,6 +79,17 @@ } } + if (config_set(CONFIG_KERNEL_RT) && config.create_reply) { + if (vka_alloc_reply(vka, &res->reply)) { + ZF_LOGE("Failed to allocate reply"); + sel4utils_clean_up_thread(vka, alloc, res); + return -1; + } + res->own_reply = true; + } else { + res->reply.cptr = config.reply; + } + if (config_set(CONFIG_KERNEL_RT) && config.sched_params.create_sc) { /* allocate a scheduling context */ if (vka_alloc_sched_context(vka, &res->sched_context)) { @@ -177,6 +189,10 @@ vka_free_object(vka, &thread->sched_context); } + if (thread->own_reply && thread->reply.cptr != 0) { + vka_free_object(vka, &thread->reply); + } + memset(thread, 0, sizeof(sel4utils_thread_t)); } @@ -239,16 +255,16 @@ static int fault_handler(char *name, seL4_CPtr endpoint) { - seL4_Word badge; - seL4_MessageInfo_t info = seL4_Recv(endpoint, &badge); - + seL4_MessageInfo_t info; while (1) { + /* sleep so other things can run */ +#ifdef CONFIG_KERNEL_RT + info = seL4_Wait(endpoint, NULL); +#else + info = seL4_Recv(endpoint, NULL); +#endif sel4utils_print_fault_message(info, name); - - /* go back to sleep so other things can run */ - seL4_Recv(endpoint, &badge); } - return 0; }
diff --git a/libsel4vka/include/vka/capops.h b/libsel4vka/include/vka/capops.h index b222543..edca088 100644 --- a/libsel4vka/include/vka/capops.h +++ b/libsel4vka/include/vka/capops.h
@@ -23,6 +23,7 @@ #include <vka/cspacepath_t.h> #include <vka/object.h> +#ifndef CONFIG_KERNEL_RT inline static int vka_cnode_saveCaller(const cspacepath_t* src) { @@ -32,6 +33,7 @@ /* depth */ src->capDepth ); } +#endif inline static int vka_cnode_copy(const cspacepath_t* dest, const cspacepath_t* src, seL4_CapRights_t rights)
diff --git a/libsel4vka/include/vka/kobject_t.h b/libsel4vka/include/vka/kobject_t.h index aa82f7e..de932d4 100644 --- a/libsel4vka/include/vka/kobject_t.h +++ b/libsel4vka/include/vka/kobject_t.h
@@ -28,6 +28,7 @@ KOBJECT_UNTYPED, KOBJECT_ENDPOINT, KOBJECT_NOTIFICATION, + KOBJECT_REPLY, KOBJECT_SCHED_CONTEXT, #ifdef CONFIG_CACHE_COLORING KOBJECT_KERNEL_IMAGE, @@ -65,6 +66,8 @@ case KOBJECT_PAGE_TABLE: return seL4_PageTableBits; #ifdef CONFIG_KERNEL_RT + case KOBJECT_REPLY: + return seL4_ReplyBits; case KOBJECT_SCHED_CONTEXT: return objectSize > seL4_MinSchedContextBits ? objectSize : seL4_MinSchedContextBits; #endif @@ -97,6 +100,8 @@ #ifdef CONFIG_KERNEL_RT case KOBJECT_SCHED_CONTEXT: return seL4_SchedContextObject; + case KOBJECT_REPLY: + return seL4_ReplyObject; #endif #ifdef CONFIG_CACHE_COLORING case KOBJECT_KERNEL_IMAGE:
diff --git a/libsel4vka/include/vka/object.h b/libsel4vka/include/vka/object.h index d18019f..22fac3d 100644 --- a/libsel4vka/include/vka/object.h +++ b/libsel4vka/include/vka/object.h
@@ -185,6 +185,17 @@ { return vka_alloc_notification(vka, result); } + +static inline int vka_alloc_reply(UNUSED vka_t *vka, UNUSED vka_object_t *result) +{ +#ifdef CONFIG_KERNEL_RT + return vka_alloc_object(vka, seL4_ReplyObject, seL4_ReplyBits, result); +#else + ZF_LOGW("Allocating reply on non RT kernel"); + return ENOSYS; +#endif +} + static inline int vka_alloc_cnode_object(vka_t *vka, uint32_t slot_bits, vka_object_t *result) { return vka_alloc_object(vka, seL4_CapTableObject, slot_bits, result); @@ -255,6 +266,7 @@ LEAKY(page_directory) LEAKY(page_table) LEAKY(sched_context) +LEAKY(reply) static inline DEPRECATED("use vka_alloc_notification_leaky") seL4_CPtr vka_alloc_async_endpoint_leaky(vka_t *vka)