sel4: enable smp for x86

Issue #2451
This commit is contained in:
Alexander Boettcher 2017-08-07 17:55:15 +02:00 committed by Christian Helmuth
parent 0dd9c6a018
commit 7a8e0e59af
18 changed files with 95 additions and 22 deletions

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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; }

View File

@ -67,6 +67,8 @@ class Genode::Platform_thread : public List<Platform_thread>::Element
enum { INITIAL_IPC_BUFFER_VIRT = 0x1000 };
Affinity::Location _location;
public:
/**
@ -156,12 +158,12 @@ class Genode::Platform_thread : public List<Platform_thread>::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

View File

@ -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_ */

View File

@ -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);

View File

@ -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 <platform_thread.h>
void Genode::Platform_thread::affinity(Affinity::Location location)
{
_location = location;
Genode::error("could not set affinity");
//seL4_TCB_SetAffinity(tcb_sel().value(), location.xpos());
}

View File

@ -21,7 +21,8 @@
#include <thread_sel4.h>
#include <platform_thread.h>
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, &regs);
ASSERT(ret == 0);
if (cpu != 0)
error("could not set affinity of thread");
seL4_TCB_Resume(tcb_sel.value());
}

View File

@ -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 <platform_thread.h>
void Genode::Platform_thread::affinity(Affinity::Location location)
{
_location = location;
seL4_TCB_SetAffinity(tcb_sel().value(), location.xpos());
}

View File

@ -21,7 +21,8 @@
#include <thread_sel4.h>
#include <platform_thread.h>
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, &regs);
ASSERT(ret == 0);
seL4_TCB_SetAffinity(tcb_sel.value(), cpu);
seL4_TCB_Resume(tcb_sel.value());
}

View File

@ -79,5 +79,3 @@ void Genode::Platform::_init_core_page_table_registry()
}
#endif
}

View File

@ -21,7 +21,8 @@
#include <thread_sel4.h>
#include <platform_thread.h>
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, &regs);
ASSERT(ret == 0);
seL4_TCB_SetAffinity(tcb_sel.value(), cpu);
seL4_TCB_Resume(tcb_sel.value());
}

View File

@ -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());
}

View File

@ -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

View File

@ -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 "
}