sel4: core-local thread creation

repos/base-sel4/include/base/native_types.h

@@ -33,7 +33,7 @@ namespace Genode {
 
 	struct Native_thread
 	{
-		int id;
+		unsigned tcb_sel = 0;
 
 		/**
 		 * Only used in core
@@ -42,12 +42,23 @@ namespace Genode {
 		 * the physical thread object, which is going to be destroyed
 		 * on destruction of the 'Thread'.
 		 */
-		Platform_thread *pt;
+		Platform_thread *pt = nullptr;
 	};
 
 	typedef Native_capability_tpl<Cap_dst_policy> Native_capability;
 
-	typedef struct { } Native_utcb;
+	class Native_utcb
+	{
+		private:
+
+			/**
+			 * On seL4 the UTCB is called IPC buffer. We use one page
+			 * for each IPC buffer.
+			 */
+			enum { IPC_BUFFER_SIZE = 4096 };
+
+			addr_t _utcb[IPC_BUFFER_SIZE/sizeof(addr_t)];
+	};
 
 	struct Native_config
 	{

repos/base-sel4/src/core/include/core_cspace.h

@@ -38,6 +38,7 @@ class Genode::Core_cspace
 			PHYS_CNODE_SEL        = 0x203,
 			CORE_VM_PAD_CNODE_SEL = 0x204,
 			CORE_VM_CNODE_SEL     = 0x205,
+			CORE_STATIC_SEL_END,
 		};
 
 		/* indices within top-level CNode */

repos/base-sel4/src/core/include/platform.h

@@ -81,6 +81,13 @@ class Genode::Platform : public Platform_generic
 		Cnode _phys_cnode { seL4_CapInitThreadCNode, Core_cspace::PHYS_CNODE_SEL,
 		                    Core_cspace::NUM_PHYS_SEL_LOG2, _phys_alloc };
 
+		struct Core_sel_alloc : Bit_allocator<1 << Core_cspace::NUM_PHYS_SEL_LOG2>
+		{
+			Core_sel_alloc() { _reserve(0, Core_cspace::CORE_STATIC_SEL_END); }
+		} _core_sel_alloc;
+
+		Lock _core_sel_alloc_lock;
+
 		/**
 		 * Replace initial CSpace with custom CSpace layout
 		 */
@@ -125,9 +132,12 @@ class Genode::Platform : public Platform_generic
 
 		Cnode &phys_cnode() { return _phys_cnode; }
 		Cnode &top_cnode()  { return _top_cnode; }
+		Cnode &core_cnode() { return _core_cnode; }
 
 		Vm_space &core_vm_space() { return _core_vm_space; }
 
+		unsigned alloc_core_sel();
+
 		void wait_for_exit();
 };
 

repos/base-sel4/src/core/platform.cc

@@ -244,8 +244,7 @@ Platform::Platform()
 	               Core_cspace::CORE_VM_ID,
 	               _core_page_table_registry)
 {
-
+	/* XXX add boot modules to ROM fs */
-	/* add boot modules to ROM fs */
 
 	/*
 	 * Print statistics about allocator initialization
@@ -261,6 +260,14 @@ Platform::Platform()
 }
 
 
+unsigned Platform::alloc_core_sel()
+{
+	Lock::Guard guard(_core_sel_alloc_lock);
+
+	return _core_sel_alloc.alloc();
+}
+
+
 void Platform::wait_for_exit()
 {
 	sleep_forever();

repos/base-sel4/src/core/thread_start.cc

@@ -19,13 +19,104 @@
 /* core includes */
 #include <platform.h>
 #include <platform_thread.h>
+#include <untyped_memory.h>
+#include <map_local.h>
 
 using namespace Genode;
 
 
+static Untyped_address create_and_map_ipc_buffer(Range_allocator &phys_alloc,
+                                                 addr_t virt_addr)
+{
+	/* create IPC buffer of one page */
+	size_t const ipc_buffer_size_log2 = get_page_size_log2();
+	Untyped_address const untyped_addr =
+		Untyped_memory::alloc_log2(phys_alloc, ipc_buffer_size_log2);
+
+	Untyped_memory::convert_to_page_frames(untyped_addr.phys(), 1);
+
+	if (!map_local(untyped_addr.phys(), virt_addr, 1)) {
+		PERR("could not map IPC buffer phys %lx at local %lx",
+		     untyped_addr.phys(), virt_addr);
+	}
+
+	return untyped_addr;
+}
+
+
+static void create_tcb(Cnode &core_cnode, Range_allocator &phys_alloc,
+                       unsigned dst_idx)
+{
+	/* create TCB */
+	size_t const tcb_size_log2 = get_page_size_log2();
+	Untyped_address const untyped_addr =
+		Untyped_memory::alloc_log2(phys_alloc, tcb_size_log2);
+
+	seL4_Untyped const service     = untyped_addr.sel();
+	int          const type        = seL4_TCBObject;
+	int          const offset      = untyped_addr.offset();
+	int          const size_bits   = 0;
+	seL4_CNode   const root        = core_cnode.sel();
+	int          const node_index  = 0;
+	int          const node_depth  = 0;
+	int          const node_offset = dst_idx;
+	int          const num_objects = 1;
+
+	int const ret = seL4_Untyped_RetypeAtOffset(service,
+	                                            type,
+	                                            offset,
+	                                            size_bits,
+	                                            root,
+	                                            node_index,
+	                                            node_depth,
+	                                            node_offset,
+	                                            num_objects);
+
+	if (ret != 0)
+		PDBG("seL4_Untyped_RetypeAtOffset (TCB) returned %d", ret);
+}
+
+
 void Thread_base::_init_platform_thread(size_t, Type type)
 {
-	PDBG("not implemented");
+	Platform &platform = *platform_specific();
+	Range_allocator &phys_alloc = *platform.ram_alloc();
+
+	addr_t const utcb_virt_addr = (addr_t)&_context->utcb;
+	Untyped_address const ipc_buffer =
+		create_and_map_ipc_buffer(phys_alloc, utcb_virt_addr);
+
+	/* allocate TCB selector within core's CNode */
+	unsigned const tcb_idx = platform.alloc_core_sel();
+
+	create_tcb(platform.core_cnode(), phys_alloc, tcb_idx);
+	unsigned const tcb_sel = tcb_idx;
+	_tid.tcb_sel = tcb_sel;
+
+	/* assign IPC buffer to thread */
+	{
+		/* determine page frame selector of the allocated IPC buffer */
+		unsigned ipc_buffer_sel = Untyped_memory::frame_sel(ipc_buffer.phys());
+
+		int const ret = seL4_TCB_SetIPCBuffer(tcb_sel, utcb_virt_addr, ipc_buffer_sel);
+		if (ret != 0)
+			PDBG("seL4_TCB_SetIPCBuffer returned %d", ret);
+	}
+
+	/* set scheduling priority */
+	enum { PRIORITY_MAX = 0xff };
+	seL4_TCB_SetPriority(tcb_sel, PRIORITY_MAX);
+
+	/* associate thread with core PD */
+	{
+		seL4_CapData_t no_cap_data = { { 0 } };
+		int const ret = seL4_TCB_SetSpace(tcb_sel, 0,
+		                  platform.top_cnode().sel(), no_cap_data,
+		                  seL4_CapInitThreadPD, no_cap_data);
+
+		if (ret != 0)
+			PDBG("seL4_TCB_SetSpace returned %d", ret);
+	}
 }
 
 
@@ -37,6 +128,10 @@ void Thread_base::_deinit_platform_thread()
 
 void Thread_base::_thread_start()
 {
+	int dummy;
+	PDBG("called, stack at 0x%p, spinning...", &dummy);
+	for (;;);
+
 	Thread_base::myself()->_thread_bootstrap();
 	Thread_base::myself()->entry();
 	sleep_forever();
@@ -45,7 +140,21 @@ void Thread_base::_thread_start()
 
 void Thread_base::start()
 {
-	PDBG("not implemented");
+	/* set register values for the instruction pointer and stack pointer */
+	seL4_UserContext regs;
+	Genode::memset(&regs, 0, sizeof(regs));
+
+	regs.eip = (uint32_t)&_thread_start;
+	regs.esp = (uint32_t)stack_top();
+	regs.gs  = IPCBUF_GDT_SELECTOR;
+	size_t const num_regs = sizeof(regs)/sizeof(seL4_Word);
+	int const ret = seL4_TCB_WriteRegisters(_tid.tcb_sel, false,
+	                                        0, num_regs, &regs);
+
+	if (ret != 0)
+		PDBG("seL4_TCB_WriteRegisters returned %d", ret);
+
+	seL4_TCB_Resume(_tid.tcb_sel);
 }