From 7a8e0e59af3146b9f82139d748bda49e17b13388 Mon Sep 17 00:00:00 2001 From: Alexander Boettcher Date: Mon, 7 Aug 2017 17:55:15 +0200 Subject: [PATCH] sel4: enable smp for x86 Issue #2451 --- .../lib/mk/spec/wand_quad/core-sel4.mk | 2 +- .../base-sel4/lib/mk/spec/x86_32/core-sel4.mk | 2 +- .../base-sel4/lib/mk/spec/x86_64/core-sel4.mk | 2 +- repos/base-sel4/patches/autoconf_32.config | 6 +++-- repos/base-sel4/patches/autoconf_64.config | 14 ++++++++++-- repos/base-sel4/src/core/include/platform.h | 7 ++++++ .../src/core/include/platform_thread.h | 6 +++-- .../base-sel4/src/core/include/thread_sel4.h | 5 +++-- repos/base-sel4/src/core/platform_thread.cc | 7 +++--- .../src/core/spec/arm/platform_thread.cc | 22 +++++++++++++++++++ repos/base-sel4/src/core/spec/arm/thread.cc | 6 ++++- .../src/core/spec/x86/platform_thread.cc | 20 +++++++++++++++++ .../base-sel4/src/core/spec/x86_32/thread.cc | 5 ++++- .../src/core/spec/x86_64/platform.cc | 2 -- .../base-sel4/src/core/spec/x86_64/thread.cc | 5 ++++- repos/base-sel4/src/core/thread_start.cc | 2 +- repos/base/run/affinity.run | 3 ++- repos/base/run/mp_server.run | 1 - 18 files changed, 95 insertions(+), 22 deletions(-) create mode 100644 repos/base-sel4/src/core/spec/arm/platform_thread.cc create mode 100644 repos/base-sel4/src/core/spec/x86/platform_thread.cc diff --git a/repos/base-sel4/lib/mk/spec/wand_quad/core-sel4.mk b/repos/base-sel4/lib/mk/spec/wand_quad/core-sel4.mk index dfe049005..344dfc3a3 100644 --- a/repos/base-sel4/lib/mk/spec/wand_quad/core-sel4.mk +++ b/repos/base-sel4/lib/mk/spec/wand_quad/core-sel4.mk @@ -1,5 +1,5 @@ SRC_CC += $(addprefix spec/arm/, boot_info.cc thread.cc platform.cc irq.cc \ - vm_space.cc) + vm_space.cc platform_thread.cc) INC_DIR += $(REP_DIR)/src/core/spec/arm diff --git a/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk b/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk index 378580ed1..a14fff0fc 100644 --- a/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk +++ b/repos/base-sel4/lib/mk/spec/x86_32/core-sel4.mk @@ -1,6 +1,6 @@ SRC_CC += $(addprefix spec/x86_32/, boot_info.cc thread.cc platform.cc \ platform_pd.cc vm_space.cc) -SRC_CC += $(addprefix spec/x86/, irq.cc vm_space.cc) +SRC_CC += $(addprefix spec/x86/, irq.cc vm_space.cc platform_thread.cc) SRC_CC += io_port_session_component.cc SRC_CC += io_port_session_support.cc diff --git a/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk b/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk index 002efd809..75eb756c8 100644 --- a/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk +++ b/repos/base-sel4/lib/mk/spec/x86_64/core-sel4.mk @@ -1,6 +1,6 @@ SRC_CC += $(addprefix spec/x86_64/, boot_info.cc thread.cc platform.cc \ platform_pd.cc vm_space.cc) -SRC_CC += $(addprefix spec/x86/, irq.cc vm_space.cc) +SRC_CC += $(addprefix spec/x86/, irq.cc vm_space.cc platform_thread.cc) SRC_CC += io_port_session_component.cc SRC_CC += io_port_session_support.cc diff --git a/repos/base-sel4/patches/autoconf_32.config b/repos/base-sel4/patches/autoconf_32.config index f2dfbbb3d..a94218e59 100644 --- a/repos/base-sel4/patches/autoconf_32.config +++ b/repos/base-sel4/patches/autoconf_32.config @@ -27,14 +27,16 @@ #define CONFIG_LIB_PLATSUPPORT 1 #define CONFIG_LIB_SEL4_ALLOCMAN 1 #define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 -@@ -49,7 +48,6 @@ +@@ -49,8 +49,7 @@ #define CONFIG_HAVE_LIB_SEL4_VSPACE 1 #define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 230 #define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 -#define CONFIG_SYSCALL 1 - #define CONFIG_MAX_NUM_NODES 1 +-#define CONFIG_MAX_NUM_NODES 1 ++#define CONFIG_MAX_NUM_NODES 16 #define CONFIG_CROSS_COMPILER_PREFIX "" #define CONFIG_MAX_RMRR_ENTRIES 32 + #define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1 @@ -66,7 +64,9 @@ #define CONFIG_OPTIMISATION_O2 1 #define CONFIG_HAVE_LIB_CPIO 1 diff --git a/repos/base-sel4/patches/autoconf_64.config b/repos/base-sel4/patches/autoconf_64.config index 82eb458d3..0bddc7930 100644 --- a/repos/base-sel4/patches/autoconf_64.config +++ b/repos/base-sel4/patches/autoconf_64.config @@ -25,6 +25,15 @@ #define CONFIG_LIB_PLATSUPPORT 1 #define CONFIG_LIB_SEL4_ALLOCMAN 1 #define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1 +@@ -50,7 +50,7 @@ + #define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 230 + #define CONFIG_LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ 0 + #define CONFIG_SYSCALL 1 +-#define CONFIG_MAX_NUM_NODES 1 ++#define CONFIG_MAX_NUM_NODES 16 + #define CONFIG_CROSS_COMPILER_PREFIX "" + #define CONFIG_MAX_RMRR_ENTRIES 32 + #define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1 @@ -66,14 +68,13 @@ #define CONFIG_OPTIMISATION_O2 1 #define CONFIG_HAVE_LIB_CPIO 1 @@ -41,11 +50,12 @@ #define CONFIG_HAVE_LIB_PLATSUPPORT 1 #define CONFIG_NUM_DOMAINS 1 #define CONFIG_HAVE_LIB_UTILS 1 -@@ -93,7 +94,6 @@ +@@ -93,8 +93,6 @@ #define CONFIG_LIBSEL4DEBUG_ALLOC_BUFFER_ENTRIES 128 #define CONFIG_CACHE_LN_SZ 64 #define CONFIG_ARCH_X86_64 1 -#define CONFIG_HUGE_PAGE 1 #define CONFIG_LIB_SEL4_MUSLC_SYS_MORECORE_BYTES 1048576 #define CONFIG_BUILDSYS_USE_CCACHE 1 - #define CONFIG_MAX_NUM_NODES 1 +-#define CONFIG_MAX_NUM_NODES 1 + #define CONFIG_KERNEL_STACK_BITS 12 diff --git a/repos/base-sel4/src/core/include/platform.h b/repos/base-sel4/src/core/include/platform.h index 3bc98efec..30d96db5b 100644 --- a/repos/base-sel4/src/core/include/platform.h +++ b/repos/base-sel4/src/core/include/platform.h @@ -247,6 +247,13 @@ class Genode::Platform : public Platform_generic size_t vm_size() const { return _vm_size; } Rom_fs *rom_fs() { return &_rom_fs; } + Affinity::Space affinity_space() const override { + return sel4_boot_info().numNodes; } + + /******************* + ** seL4 specific ** + *******************/ + Cnode &phys_cnode() { return _phys_cnode; } Cnode &top_cnode() { return _top_cnode; } Cnode &core_cnode() { return _core_cnode; } diff --git a/repos/base-sel4/src/core/include/platform_thread.h b/repos/base-sel4/src/core/include/platform_thread.h index 11b3acc74..a8db2ff3d 100644 --- a/repos/base-sel4/src/core/include/platform_thread.h +++ b/repos/base-sel4/src/core/include/platform_thread.h @@ -67,6 +67,8 @@ class Genode::Platform_thread : public List::Element enum { INITIAL_IPC_BUFFER_VIRT = 0x1000 }; + Affinity::Location _location; + public: /** @@ -156,12 +158,12 @@ class Genode::Platform_thread : public List::Element /** * Set the executing CPU for this thread */ - void affinity(Affinity::Location) { } + void affinity(Affinity::Location location); /** * Get the executing CPU for this thread */ - Affinity::Location affinity() const { return Affinity::Location(); } + Affinity::Location affinity() const { return _location; } /** * Set CPU quota of the thread diff --git a/repos/base-sel4/src/core/include/thread_sel4.h b/repos/base-sel4/src/core/include/thread_sel4.h index 1ddee5aba..9f3db874b 100644 --- a/repos/base-sel4/src/core/include/thread_sel4.h +++ b/repos/base-sel4/src/core/include/thread_sel4.h @@ -48,7 +48,7 @@ namespace Genode { * Set register values for the instruction pointer and stack pointer and * start the seL4 thread */ - void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp); + void start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, unsigned cpu); }; @@ -129,6 +129,7 @@ void Genode::Thread_info::destruct() } -void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp); +void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, + unsigned cpu); #endif /* _CORE__INCLUDE__THREAD_SEL4_H_ */ diff --git a/repos/base-sel4/src/core/platform_thread.cc b/repos/base-sel4/src/core/platform_thread.cc index 34aae8df1..8a690646a 100644 --- a/repos/base-sel4/src/core/platform_thread.cc +++ b/repos/base-sel4/src/core/platform_thread.cc @@ -167,7 +167,7 @@ int Platform_thread::start(void *ip, void *sp, unsigned int cpu_no) _pd->page_directory_sel().value(), no_cap_data); ASSERT(ret == 0); - start_sel4_thread(_info.tcb_sel, (addr_t)ip, (addr_t)(sp)); + start_sel4_thread(_info.tcb_sel, (addr_t)ip, (addr_t)(sp), _location.xpos()); return 0; } @@ -215,11 +215,12 @@ bool Platform_thread::install_mapping(Mapping const &mapping) Platform_thread::Platform_thread(size_t, const char *name, unsigned priority, - Affinity::Location, addr_t utcb) + Affinity::Location location, addr_t utcb) : _name(name), _utcb(utcb), - _pager_obj_sel(platform_specific()->core_sel_alloc().alloc()) + _pager_obj_sel(platform_specific()->core_sel_alloc().alloc()), + _location(location) { _info.init(_utcb ? _utcb : INITIAL_IPC_BUFFER_VIRT); diff --git a/repos/base-sel4/src/core/spec/arm/platform_thread.cc b/repos/base-sel4/src/core/spec/arm/platform_thread.cc new file mode 100644 index 000000000..97e5810d3 --- /dev/null +++ b/repos/base-sel4/src/core/spec/arm/platform_thread.cc @@ -0,0 +1,22 @@ +/* + * \brief Platform thread interface implementation - arm specific + * \author Alexander Boettcher + * \date 2017-08-08 + */ + +/* + * Copyright (C) 2017 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU Affero General Public License version 3. + */ + +#include + +void Genode::Platform_thread::affinity(Affinity::Location location) +{ + _location = location; + + Genode::error("could not set affinity"); + //seL4_TCB_SetAffinity(tcb_sel().value(), location.xpos()); +} diff --git a/repos/base-sel4/src/core/spec/arm/thread.cc b/repos/base-sel4/src/core/spec/arm/thread.cc index 8db331b48..e45bd3759 100644 --- a/repos/base-sel4/src/core/spec/arm/thread.cc +++ b/repos/base-sel4/src/core/spec/arm/thread.cc @@ -21,7 +21,8 @@ #include #include -void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp) +void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, + unsigned cpu) { /* set register values for the instruction pointer and stack pointer */ seL4_UserContext regs; @@ -35,6 +36,9 @@ void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp) num_regs, ®s); ASSERT(ret == 0); + if (cpu != 0) + error("could not set affinity of thread"); + seL4_TCB_Resume(tcb_sel.value()); } diff --git a/repos/base-sel4/src/core/spec/x86/platform_thread.cc b/repos/base-sel4/src/core/spec/x86/platform_thread.cc new file mode 100644 index 000000000..0cb80b7b3 --- /dev/null +++ b/repos/base-sel4/src/core/spec/x86/platform_thread.cc @@ -0,0 +1,20 @@ +/* + * \brief Platform thread interface implementation - x86 specific + * \author Alexander Boettcher + * \date 2017-08-08 + */ + +/* + * Copyright (C) 2017 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU Affero General Public License version 3. + */ + +#include + +void Genode::Platform_thread::affinity(Affinity::Location location) +{ + _location = location; + seL4_TCB_SetAffinity(tcb_sel().value(), location.xpos()); +} diff --git a/repos/base-sel4/src/core/spec/x86_32/thread.cc b/repos/base-sel4/src/core/spec/x86_32/thread.cc index ae1c40a92..f0ce8ecba 100644 --- a/repos/base-sel4/src/core/spec/x86_32/thread.cc +++ b/repos/base-sel4/src/core/spec/x86_32/thread.cc @@ -21,7 +21,8 @@ #include #include -void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp) +void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, + unsigned cpu) { /* set register values for the instruction pointer and stack pointer */ seL4_UserContext regs; @@ -36,6 +37,8 @@ void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp) num_regs, ®s); ASSERT(ret == 0); + seL4_TCB_SetAffinity(tcb_sel.value(), cpu); + seL4_TCB_Resume(tcb_sel.value()); } diff --git a/repos/base-sel4/src/core/spec/x86_64/platform.cc b/repos/base-sel4/src/core/spec/x86_64/platform.cc index 01941024b..0db4b4440 100644 --- a/repos/base-sel4/src/core/spec/x86_64/platform.cc +++ b/repos/base-sel4/src/core/spec/x86_64/platform.cc @@ -79,5 +79,3 @@ void Genode::Platform::_init_core_page_table_registry() } #endif } - - diff --git a/repos/base-sel4/src/core/spec/x86_64/thread.cc b/repos/base-sel4/src/core/spec/x86_64/thread.cc index 9555fde58..25af07cd8 100644 --- a/repos/base-sel4/src/core/spec/x86_64/thread.cc +++ b/repos/base-sel4/src/core/spec/x86_64/thread.cc @@ -21,7 +21,8 @@ #include #include -void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp) +void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp, + unsigned cpu) { /* set register values for the instruction pointer and stack pointer */ seL4_UserContext regs; @@ -35,6 +36,8 @@ void Genode::start_sel4_thread(Cap_sel tcb_sel, addr_t ip, addr_t sp) num_regs, ®s); ASSERT(ret == 0); + seL4_TCB_SetAffinity(tcb_sel.value(), cpu); + seL4_TCB_Resume(tcb_sel.value()); } diff --git a/repos/base-sel4/src/core/thread_start.cc b/repos/base-sel4/src/core/thread_start.cc index 901796741..04099d6d1 100644 --- a/repos/base-sel4/src/core/thread_start.cc +++ b/repos/base-sel4/src/core/thread_start.cc @@ -100,7 +100,7 @@ void Thread::_thread_start() void Thread::start() { start_sel4_thread(Cap_sel(native_thread().tcb_sel), (addr_t)&_thread_start, - (addr_t)stack_top()); + (addr_t)stack_top(), _affinity.xpos()); } diff --git a/repos/base/run/affinity.run b/repos/base/run/affinity.run index d6f86bfeb..cc662dc18 100644 --- a/repos/base/run/affinity.run +++ b/repos/base/run/affinity.run @@ -10,7 +10,8 @@ if { ![have_spec panda] && ![expr [have_spec x86_32] && [have_spec foc] ] && ![expr [have_spec x86_64] && [have_spec foc] ] && - ![have_spec nova] + ![have_spec nova] && + ![have_spec sel4] } { puts "Platform is unsupported." exit 0 diff --git a/repos/base/run/mp_server.run b/repos/base/run/mp_server.run index 2264f311e..ef7cf987b 100644 --- a/repos/base/run/mp_server.run +++ b/repos/base/run/mp_server.run @@ -42,7 +42,6 @@ if {[have_include "power_on/qemu"]} { if {[have_spec fiasco]} { set want_cpus 1 } if {([have_spec x86_64] && [have_spec hw])} { set want_cpus 1 } if {[have_spec zynq]} { set want_cpus 1 } - if {[have_spec sel4]} { set want_cpus 1 } append qemu_args " -nographic -smp $want_cpus,cores=$want_cpus " }