From 2b245937582deb74b45061f3a373f7ba63472b76 Mon Sep 17 00:00:00 2001 From: Norman Feske Date: Wed, 15 Oct 2014 14:48:45 +0200 Subject: [PATCH] sel4: minimalistic roottask --- repos/base-sel4/doc/notes.txt | 320 +++++++++++++++++- repos/base-sel4/include/base/ipc_msgbuf.h | 112 ++++++ repos/base-sel4/include/base/ipc_pager.h | 159 +++++++++ repos/base-sel4/include/base/native_types.h | 73 ++++ repos/base-sel4/lib/mk/base-common.inc | 34 ++ repos/base-sel4/lib/mk/x86_32/base-common.mk | 1 + repos/base-sel4/lib/mk/x86_32/kernel.mk | 2 +- repos/base-sel4/mk/spec-sel4.mk | 1 + repos/base-sel4/run/test.run | 4 +- .../base-sel4/src/base/console/core_console.h | 27 ++ repos/base-sel4/src/base/ipc/ipc.cc | 135 ++++++++ repos/base-sel4/src/base/ipc/pager.cc | 44 +++ repos/base-sel4/src/base/lock/lock_helper.h | 31 ++ .../src/base/thread/thread_bootstrap.cc | 32 ++ .../base-sel4/src/base/thread/thread_sel4.cc | 61 ++++ repos/base-sel4/src/test/sel4/context_area.cc | 23 ++ repos/base-sel4/src/test/sel4/main.cc | 19 ++ repos/base-sel4/src/test/sel4/mini_env.cc | 38 +++ repos/base-sel4/src/test/sel4/target.mk | 15 + repos/base-sel4/src/test/sel4/thread.cc | 58 ++++ 20 files changed, 1184 insertions(+), 5 deletions(-) create mode 100644 repos/base-sel4/include/base/ipc_msgbuf.h create mode 100644 repos/base-sel4/include/base/ipc_pager.h create mode 100644 repos/base-sel4/include/base/native_types.h create mode 100644 repos/base-sel4/lib/mk/base-common.inc create mode 100644 repos/base-sel4/lib/mk/x86_32/base-common.mk create mode 100644 repos/base-sel4/mk/spec-sel4.mk create mode 100644 repos/base-sel4/src/base/console/core_console.h create mode 100644 repos/base-sel4/src/base/ipc/ipc.cc create mode 100644 repos/base-sel4/src/base/ipc/pager.cc create mode 100644 repos/base-sel4/src/base/lock/lock_helper.h create mode 100644 repos/base-sel4/src/base/thread/thread_bootstrap.cc create mode 100644 repos/base-sel4/src/base/thread/thread_sel4.cc create mode 100644 repos/base-sel4/src/test/sel4/context_area.cc create mode 100644 repos/base-sel4/src/test/sel4/main.cc create mode 100644 repos/base-sel4/src/test/sel4/mini_env.cc create mode 100644 repos/base-sel4/src/test/sel4/target.mk create mode 100644 repos/base-sel4/src/test/sel4/thread.cc diff --git a/repos/base-sel4/doc/notes.txt b/repos/base-sel4/doc/notes.txt index b7ea36e3f..0f29aff7f 100644 --- a/repos/base-sel4/doc/notes.txt +++ b/repos/base-sel4/doc/notes.txt @@ -24,10 +24,10 @@ Following the convention to host each kernel in its dedicated _base-_ source repository, the seL4-specific code will go to _base-sel4_. This way, we can cleanly hold the seL4-specific code apart from generic Genode code. -For the start, the new repository will contain three things: This notes -document at _doc/_, the port-description file for downloading the seL4 +For the start, the new repository will contain two things: This notes +document at _doc/_ and the port-description file for downloading the seL4 kernel _(ports/sel4.port)_ accompanied with the corresponding hash file -_(ports/sel4.hash)_, and a bunch of small tests _(src/test/sel4/)_ +_(ports/sel4.hash)_. Since seL4 is hosted on GitHub, writing a port-description file is easy. We can simply use _base-nova/ports/nova.port_ as a template and adapt it: @@ -293,4 +293,318 @@ a root task to the system. A root task for exercising the kernel interface =============================================== +At this point, there are two options. We could either start with a very +minimalistic hello-world program that is completely unrelated to Genode. Such +a root-task from scratch could be used to explore the individual system calls +before jumping into Genode. The second option would be to go directly for +a Genode program, which includes a proper C++ runtime and Genode's generic +linker script. +I went for the latter option and created a simple test program at +_base-sel4/src/test/sel4/_. The _target.mk_ file looks as follows: + +! TARGET = test-sel4 +! SRC_CC = main.cc +! LIBS = cxx startup + +The 'main' function of the _main.cc_ file does no much except for writing +at an illegal (yet known) address: + +! int main() +! { +! *(int *)0x1122 = 0; +! return 0; +! } + +When attempting to build the program by issuing 'make test/sel4' from within +our build directory, the build system will attempt to compile the C++ runtime, +which, in turn, depends on a few Genode headers. Some headers are readily +provided by the _base/_ repository but others are expected to be supplied +by the _base-_ repository. The compile errors look like this: + +! COMPILE malloc_free.o +! In file included from repos/base/include/parent/capability.h:17:0, +! from repos/base/include/base/env.h:20, +! from repos/base/src/base/cxx/malloc_free.cc:17: +! repos/base/include/base/capability.h:21:31: +! fatal error: base/native_types.h: No such file or directory + +For now, we can supply a dummy version of this header, which contain +preliminary type definitions. To see, which types are expected from which +header file, we can take cues from the other _base-_ platforms. + +At link time, we will observe plenty of undefined references originating +from the startup code. Most of those references concern basic data +structures such as the AVL tree. Normally, those symbols are provided by +the so-called _base-common_ library, which is used both core and non-core +programs. We can take a copy of a _base-common.mk_ file from one of the +other base platforms as a starting point. I decided to go for the version +provided by _base-nova_. With the base-common library present, we can +replace the 'cxx' and 'startup' libs by the base-common library in the +'LIBS' declaration of our test-sel4 program. Because base-common already +depends on both 'cxx' and 'startup', there is no need to specify those +libraries twice. + +On the attempt to compile the base-common library, we will stumble over +further missing headers such as _ipc_msgbuf.h_. Here the _base-linux_ +version of this file becomes handy because it is free-standing. + +When compiling _lock.cc_, the compiler complaints about the missing +_lock_helper.h_ file. This platform-specific file that is internally used by +the lock implementation is normally expected +at _base-/src/base/lock/_. For now, just for getting the binary +linked, we provide empty dummies: + +! static inline void thread_yield() { } +! static inline void thread_switch_to(Genode::Thread_base *thread_base) { } +! static inline void thread_stop_myself() { } +! +! static inline bool thread_check_stopped_and_restart(Genode::Thread_base *) +! { +! return false; +! } + +The next missing piece is the platform-specific implementation of the IPC +API _(ipc/ipc.cc and ipc/pager.cc)_, which are expected to reside at +_base-sel4/src/base/ipc/_. We just take the simplest version of the other +base platforms (in this case _base-codezero/src/base/ipc/) and strip it down +to become mere dummy. + +By adding the base-common library, the number of unresolved references +decreased by a great amount. Some functions are still unresolved. +There are many references to 'printf', which is not part of the base-common +library because core uses a different back end (typically a kernel debugger) +than non-core processes (using a session to core's LOG service). Because +our test plays the role of a root task, we can include core's version by +adding 'base/src/base/console/core_printf.cc' as source to our target +description file. + +! SRC_CC += base/console/core_printf.cc +! vpath %.cc $(BASE_DIR)/src + +The back end of 'core_printf.cc' has to be provided by a header at +_base-sel4/src/base/console/core_console.h_. For now, we just provide +an empty implementation of '_out_char'. To let the compiler find the +header, we need to add the extend the include search path as follows: + +! INC_DIR += $(REP_DIR)/src/base/console + +For the unresolved references for 'env_context_area_ram_session' and +'env_context_area_rm_session', the following dummy will do: + +! #include +! #include +! +! namespace Genode { +! Rm_session *env_context_area_rm_session() { return nullptr; } +! Ram_session *env_context_area_ram_session() { return nullptr; } +! } + +The remaining pieces of the puzzle is the 'Genode::env()' function, which +is an accessor to the Genode environment. Because the Genode environment does +not exist yet, we provide a dummy 'env' called _mini_env_. Initially, this +implementation of the 'Genode::Env' interface merely returns dummy values +(null pointers and invalid capabilies). + +After this step, the test-sel4 target links successfully. To use it as +roottask, we have to modify our _test.run_ script by + +# Adding a build step + ! build { test/sel4 } +# Specifying the test-sel4 binary as boot module so that the our run + environment includes it in the boot image and appends the file as module + to the boot-loader configuration. + ! build_boot_image "test-sel4" + +When issuing 'make run/test' now, we get the following messages from the +kernel: + +! Detected 1 boot module(s): +! module #0: start=0x169000 end=0x186754 size=0x1d754 +! name='/genode/test-sel4' +! ELF-loading userland images from boot modules: +! module #0 for node #0: size=0x27000 v_entry=0x136cc +! v_start=0x0 v_end=0x27000 +! p_start=0x187000 p_end=0x1ae000 +! Moving loaded userland images to final location: +! from=0x187000 to=0x15e000 size=0x27000 +! +! Starting node #0 +! Caught cap fault in send phase at address 0x0 +! while trying to handle: +! vm fault on data at address 0x9090c3fb with status 0x4 +! in thread 0xe0189880 at address 0x314a + +Assuming that 'v_start' and 'v_end' stand for the virtual address range +if the loaded binary, those numbers look weird. Normally, Genode binaries +are linked at a much higher address, e.g., 0x1000000. By inspecting the +binary via the readelf commend, it turns out that we haven't yet declared the +link address for the seL4 platform. So its time to introduce a so-called spec +file for the "sel4" build-spec value. The new file _base-sel4/mk/spec-sel4.mk_ +will be incorporated into the build process whenever the 'SPEC' declaration of +the build directory has the value "sel4" listed. To define the default link +address for the platform, the file has the following content: + +! LD_TEXT_ADDR ?= 0x01000000 + +When issuing 'make test/sel4 VERBOSE=', we can see the link address specified +at the linker command line. Another look at the binary via readelf confirms +that the location of the text segment looks good now. Re-executing the run +script produces the same result as before though. But the last message is +quite helpful: + +! vm fault on data at address 0x0 with status 0x4 +! in thread 0xe0189880 at address 0x100312b + +The last address lies well within the text segment of our binary. It seems +that the kernel has kicked off the execution of our root task (presumably +at the entry point address as found in the ELF binary). At some point, our +"root task" de-references a null pointer. Given that several of the dummy +functions that we just created, return null pointers, this is hardly a +surprise. So let us have a look how far we have come by inspecting the +fault address 0x100312b using +! objdump -lSd bin/test-sel4 | less +In less, we search for the pattern "100312b". We see that the surrounding +code belongs to the heap implementation ('Heap::_allocate_dataspace'). It +seems that someone is trying to use 'Genode::env()->heap()'. To confirm +this assumption, we can use Qemu's GDB stub to obtain a backtrace. We have +to take the following steps: + +# We want to halt the execution at the point where the fault would happen + instead of triggering a page fault. The easiest way to accomplish that + is to insert an infinite loop at the right spot. The infinite loop serve + us as a poor man's break point. In our case, we add a 'for (;;);' statement + right at the beginning of the '_allocate_dataspace' function in + _repos/base/src/base/heap/heap.cc_. When re-executing the run script after + this change, we can see that the fault message won't appear. + +# We cancel the execution of the run script and start Qemu manually using + the command-line arguments that are found in the log output (the message + "spawn qemu ...". To enable Qemu's GDB stub, we have to append "-s" as + argument. + ! qemu-system-i386 -nographic -m 64 -cdrom var/run/test.iso -s + +# When qemu is running, we start GDB from another shell (changing to + our build directory) as follows: + ! gdb bin/test-sel4 -ex "target remote :1234" + +# Listing the backtrace via the 'bt' command is quite revealing (output + slightly edited for brevity): + + ! (gdb) bt + ! #0 Genode::Heap::_allocate_dataspace + ! at genode/repos/base/src/base/heap/heap.cc:57 + ! #1 0x010030b9 in Genode::Heap::_unsynchronized_alloc + ! at genode/repos/base/src/base/heap/heap.cc:181 + ! #2 0x01003155 in Genode::Heap::alloc + ! at genode/repos/base/src/base/heap/heap.cc:199 + ! #3 0x01010732 in malloc + ! #4 0x0100f539 in start_fde_sort + ! #5 init_object + ! at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde.c:768 + ! #6 search_object + ! at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde.c:958 + ! #7 0x01010375 in _Unwind_Find_registered_FDE + ! at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde.c:1022 + ! #8 _Unwind_Find_FDE + ! at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2-fde-dip.c:440 + ! #9 0x0100d4c3 in uw_frame_state_for + ! #10 0x0100dff8 in uw_init_context_1 + ! at ../../../../../../contrib/gcc-4.7.2/libgcc/unwind-dw2.c:1500 + ! #11 0x0100e3ea in _Unwind_RaiseException + ! #12 0x01011f51 in __cxa_throw () + ! #13 0x01013751 in init_main_thread () + ! at genode/repos/base/src/platform/init_main_thread.cc:119 + ! #14 0x010134fe in _start () + ! at genode/repos/base/src/platform/x86_32/crt0.s:47 + +We can see that Genode's startup code tries to throw the first C++ exception. +There is a lengthy comment at the corresponding code portion that explains +the rationale behind throwing an exception right from the startup code. +The exception handling, in particular the stack unwinding) is done by the +GCC support library, which eventually calls 'malloc' to allocate some +backing store for metadata. Genode has no 'malloc' function. But for making +the GCC support library happy (which expects a C runtime to be present), our +Genode-specific C++ support code in the form of the 'cxx' library comes with +a library-local version of malloc _(base/src/base/cxx/malloc_free.cc)_. This +malloc implementation uses a separate 'Genode::Heap' instance. The instance +has an initial capacity of 512 bytes. If the allocations exceed this capacity, +this heap will try to expand using 'env()->ram_session()' as backing store. +This is why the '_allocate_dataspace' function was called. At the current +stage, we don't have an implementation of 'env()->ram_session()'. To work +around this early allocation issue, we can simply increase the capacity of +the 'initial_block', let's say by factor 10. When re-executing the run script +now, '_allocate_dataspace' won't be called. Hence, we execution won't get +stuck in our infinite loop (we can remove the loop either way now). Instead, +we get another null-pointer dereference: + +! vm fault on data at address 0x0 with status 0x4 +! in thread 0xe0189880 at address 0x1003ab7 + +The procedure to investigate the reason for this page fault is exactly the +same as for the first one, using objdump, infinite loops, and Qemu's GDB stub. + +This time, the null-pointer dereference occurs in +_base/src/base/thread/thread.cc_ on the attempt to allocate so-called +thread context for the main thread. Such thread contexts contain the +stacks and meta data of threads. They are placed in a dedicated virtual +memory area that is manually managed by the process. + +For our minimalistic root task, we don't have Genode's address-space +management facilities at our disposal yet. So we have to side-step the +'_alloc_context' function somehow. This can be accomplished by using +custom version of _thread.cc_ instead of the one provided by the _base/_ +repository. So we remove _thread.cc_ from the base-common library for now +and add a new _thread.cc_ file to our test-sel4 target. The following +dummy stub will do for now: + +! static Thread_base::Context *main_context() +! { +! enum { STACK_SIZE = sizeof(long)*4*1024 }; +! +! static long buffer[STACK_SIZE/sizeof(long)]; +! +! /* the context is located beyond the top of the stack */ +! addr_t const context_addr = (addr_t)buffer + sizeof(buffer) +! - sizeof(Thread_base::Context); +! +! Thread_base::Context *context = (Thread_base::Context *)context_addr; +! context->stack_base = (addr_t)buffer; +! return context; +! } +! +! Thread_base *Thread_base::myself() { return nullptr; } +! +! Thread_base::Thread_base(const char *name, size_t stack_size, Type type, +! Cpu_session *cpu_session) +! : +! _cpu_session(cpu_session), _context(main_context()) +! { +! strncpy(_context->name, name, sizeof(_context->name)); +! _context->thread_base = this; +! +! _init_platform_thread(type); +! } +! +! Thread_base::Thread_base(const char *name, size_t stack_size, Type type) +! : Thread_base(name, stack_size, type, nullptr) { } +! +! Thread_base::~Thread_base() { _deinit_platform_thread(); } + +Genode's startup code will change the stack of the main thread prior calling +the main function. This way, the stack can be placed at a dedicated area of +the virtual address space (thread-context area). By not placing the stack +close to the program image, stack overflows won't silently corrupt data but +trigger a page fault. The code above, however, allocates a dummy context for +the main thread in the BSS segment (the 'buffer' used as backing store for the +context is a static variable). This code above is intended as an interim +solution for the initialization of the main thread only. + +When executing our run script again, we will get the following message: + +! vm fault on data at address 0x1122 with status 0x6 +! in thread 0xe0189880 at address 0x1000190 + +This message is caused by the main function of our test program! In this +function, we deliberately triggered a fault at the address 0x1122 via +the statement '*(int *)0x1122 = 0;' diff --git a/repos/base-sel4/include/base/ipc_msgbuf.h b/repos/base-sel4/include/base/ipc_msgbuf.h new file mode 100644 index 000000000..380b6d5e2 --- /dev/null +++ b/repos/base-sel4/include/base/ipc_msgbuf.h @@ -0,0 +1,112 @@ +/* + * \brief seL4-specific layout of IPC message buffer + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +#ifndef _INCLUDE__BASE__IPC_MSGBUF_H_ +#define _INCLUDE__BASE__IPC_MSGBUF_H_ + +namespace Genode { + + /** + * IPC message buffer layout + */ + class Msgbuf_base + { + public: + + enum { MAX_CAPS_PER_MSG = 8 }; + + protected: + + /* + * Capabilities to be transferred + */ + int _caps[MAX_CAPS_PER_MSG]; + Genode::size_t _used_caps; + Genode::size_t _read_cap_index; + + /** + * Maximum size of plain-data message payload + */ + Genode::size_t _size; + + /** + * Actual size of plain-data message payload + */ + Genode::size_t _used_size; + + char _msg_start[]; /* symbol marks start of message buffer data */ + + /* + * No member variables are allowed beyond this point! + */ + + public: + + char buf[]; + + Msgbuf_base() { reset_caps(); } + + /** + * Return size of message buffer + */ + inline Genode::size_t size() const { return _size; }; + + /** + * Return address of message buffer + */ + inline void *addr() { return &_msg_start[0]; }; + + void reset_caps() { _used_caps = 0; _read_cap_index = 0; } + + bool append_cap(int cap) + { + if (_used_caps == MAX_CAPS_PER_MSG) + return false; + + _caps[_used_caps++] = cap; + return true; + } + + int read_cap() + { + if (_read_cap_index == _used_caps) + return -1; + + return _caps[_read_cap_index++]; + } + + size_t used_caps() const { return _used_caps; } + + int cap(unsigned index) const + { + return index < _used_caps ? _caps[index] : -1; + } + }; + + + /** + * Pump up IPC message buffer to specified buffer size + */ + template + class Msgbuf : public Msgbuf_base + { + public: + + char buf[BUF_SIZE]; + + Msgbuf() { _size = BUF_SIZE; } + }; +} + + +#endif /* _INCLUDE__BASE__IPC_MSGBUF_H_ */ diff --git a/repos/base-sel4/include/base/ipc_pager.h b/repos/base-sel4/include/base/ipc_pager.h new file mode 100644 index 000000000..c72f3bfaf --- /dev/null +++ b/repos/base-sel4/include/base/ipc_pager.h @@ -0,0 +1,159 @@ +/* + * \brief Pager support for Genode on seL4 + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +#ifndef _INCLUDE__BASE__IPC_PAGER_H_ +#define _INCLUDE__BASE__IPC_PAGER_H_ + +#include +#include +#include +#include + +namespace Genode { + + class Mapping + { + private: + + addr_t _from_phys_addr; + addr_t _to_virt_addr; + size_t _num_pages; + bool _writeable; + + enum { PAGE_SIZE_LOG2 = 12 }; + + public: + + /** + * Constructor + */ + Mapping(addr_t dst_addr, addr_t src_addr, + Cache_attribute const cacheability, bool io_mem, + unsigned l2size = PAGE_SIZE_LOG2, + bool rw = true) + : + _from_phys_addr(src_addr), + _to_virt_addr(dst_addr), + _num_pages(1 << (l2size - PAGE_SIZE_LOG2)), + _writeable(rw) + { } + + /** + * Construct invalid mapping + */ + Mapping() : _num_pages(0) { } + + /** + * Prepare map operation + * + * No preparations are needed on Codezero because all mapping + * originate from the physical address space. + */ + void prepare_map_operation() { } + + addr_t from_phys() const { return _from_phys_addr; } + addr_t to_virt() const { return _to_virt_addr; } + size_t num_pages() const { return _num_pages; } + bool writeable() const { return _writeable; } + }; + + + /** + * Special paging server class + */ + class Ipc_pager : public Native_capability + { + private: + + Native_thread_id _last; /* faulted thread */ + addr_t _pf_addr; /* page-fault address */ + addr_t _pf_ip; /* instruction pointer of faulter */ + bool _pf_write; /* true on write fault */ + + Mapping _reply_mapping; + + public: + + /** + * Constructor + */ + Ipc_pager(); + + /** + * Wait for a new page fault received as short message IPC + */ + void wait_for_fault(); + + /** + * Reply current page-fault and wait for a new one + */ + void reply_and_wait_for_fault(); + + /** + * Request instruction pointer of current page fault + */ + addr_t fault_ip() { return _pf_ip; } + + /** + * Request fault address of current page fault + */ + addr_t fault_addr() { return _pf_addr; } + + /** + * Set parameters for next reply + */ + void set_reply_mapping(Mapping m) { _reply_mapping = m; } + + /** + * Set destination for next reply + */ + void set_reply_dst(Native_capability pager_object) { + _last = pager_object.local_name(); } + + /** + * Answer call without sending a mapping + * + * This function is used to acknowledge local calls from one of + * core's region-manager sessions. + */ + void acknowledge_wakeup(); + + /** + * Return thread ID of last faulter + */ + Native_thread_id last() const { return _last; } + + /** + * Return badge for faulting thread + */ + unsigned long badge() const { return _last; } + + /** + * Return true if page fault was a write fault + */ + bool is_write_fault() const { return _pf_write; } + + /** + * Return true if last fault was an exception + */ + bool is_exception() const + { + /* + * Reflection of exceptions is not supported on this platform. + */ + return false; + } + }; +} + +#endif /* _INCLUDE__BASE__IPC_PAGER_H_ */ diff --git a/repos/base-sel4/include/base/native_types.h b/repos/base-sel4/include/base/native_types.h new file mode 100644 index 000000000..e4478a511 --- /dev/null +++ b/repos/base-sel4/include/base/native_types.h @@ -0,0 +1,73 @@ +/* + * \brief Platform-specific type definitions + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2013 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +#ifndef _INCLUDE__BASE__NATIVE_TYPES_H_ +#define _INCLUDE__BASE__NATIVE_TYPES_H_ + +#include +#include + +namespace Genode { + + struct Cap_dst_policy + { + typedef int Dst; + static bool valid(Dst tid) { return false; } + static Dst invalid() { return true; } + static void copy(void* dst, Native_capability_tpl* src); + }; + + class Platform_thread; + + typedef int Native_thread_id; + + struct Native_thread + { + int id; + + /** + * Only used in core + * + * For 'Thread' objects created within core, 'pt' points to + * the physical thread object, which is going to be destroyed + * on destruction of the 'Thread'. + */ + Platform_thread *pt; + }; + + typedef Native_capability_tpl Native_capability; + + typedef struct { } Native_utcb; + + struct Native_config + { + /** + * Thread-context area configuration. + */ + static constexpr addr_t context_area_virtual_base() { + return 0x40000000UL; } + static constexpr addr_t context_area_virtual_size() { + return 0x10000000UL; } + + /** + * Size of virtual address region holding the context of one thread + */ + static constexpr addr_t context_virtual_size() { return 0x00100000UL; } + }; + + struct Native_pd_args { }; + + typedef int Native_connection_state; +} + +#endif /* _INCLUDE__BASE__NATIVE_TYPES_H_ */ diff --git a/repos/base-sel4/lib/mk/base-common.inc b/repos/base-sel4/lib/mk/base-common.inc new file mode 100644 index 000000000..fd4fa6f87 --- /dev/null +++ b/repos/base-sel4/lib/mk/base-common.inc @@ -0,0 +1,34 @@ +# +# \brief Portions of base library shared by core and non-core processes +# \author Norman Feske +# \date 2013-02-14 +# + +LIBS += cxx startup + +SRC_CC += ipc/ipc.cc ipc/pager.cc +SRC_CC += avl_tree/avl_tree.cc +SRC_CC += allocator/slab.cc +SRC_CC += allocator/allocator_avl.cc +SRC_CC += heap/heap.cc heap/sliced_heap.cc +SRC_CC += console/console.cc +SRC_CC += child/child.cc +SRC_CC += process/process.cc +SRC_CC += elf/elf_binary.cc +SRC_CC += lock/lock.cc +SRC_CC += signal/signal.cc signal/common.cc +SRC_CC += server/server.cc +#SRC_CC += thread/thread.cc +SRC_CC += thread/trace.cc +SRC_CC += thread/myself.cc +SRC_CC += thread/context_allocator.cc +#SRC_CC += env/cap_map.cc + +INC_DIR += $(REP_DIR)/src/base/lock +INC_DIR += $(BASE_DIR)/src/base/lock +INC_DIR += $(BASE_DIR)/src/base/thread + +vpath %.cc $(REP_DIR)/src/base +vpath %.cc $(BASE_DIR)/src/base + +# vi: set ft=make : diff --git a/repos/base-sel4/lib/mk/x86_32/base-common.mk b/repos/base-sel4/lib/mk/x86_32/base-common.mk new file mode 100644 index 000000000..7c6d23984 --- /dev/null +++ b/repos/base-sel4/lib/mk/x86_32/base-common.mk @@ -0,0 +1 @@ +include $(REP_DIR)/lib/mk/base-common.inc diff --git a/repos/base-sel4/lib/mk/x86_32/kernel.mk b/repos/base-sel4/lib/mk/x86_32/kernel.mk index df1e85b78..3cd30309e 100644 --- a/repos/base-sel4/lib/mk/x86_32/kernel.mk +++ b/repos/base-sel4/lib/mk/x86_32/kernel.mk @@ -16,7 +16,7 @@ LINKER_OPT_PREFIX := -Wl, build_kernel: $(VERBOSE)$(MAKE) \ TOOLPREFIX=$(CROSS_DEV_PREFIX) \ - ARCH=ia32 PLAT=pc99 DEBUG=1 V=1 \ + ARCH=ia32 PLAT=pc99 DEBUG=1 \ LDFLAGS+=-nostdlib LDFLAGS+=-Wl,-nostdlib \ $(addprefix LDFLAGS+=$(LINKER_OPT_PREFIX),$(LD_MARCH)) \ CFLAGS+=-fno-builtin-printf \ diff --git a/repos/base-sel4/mk/spec-sel4.mk b/repos/base-sel4/mk/spec-sel4.mk new file mode 100644 index 000000000..0197b1215 --- /dev/null +++ b/repos/base-sel4/mk/spec-sel4.mk @@ -0,0 +1 @@ +LD_TEXT_ADDR ?= 0x01000000 diff --git a/repos/base-sel4/run/test.run b/repos/base-sel4/run/test.run index ff08409cd..c7b924b7e 100644 --- a/repos/base-sel4/run/test.run +++ b/repos/base-sel4/run/test.run @@ -1,6 +1,8 @@ +build { test/sel4 } + create_boot_directory -build_boot_image "" +build_boot_image "test-sel4" append qemu_args " -nographic -m 64 " diff --git a/repos/base-sel4/src/base/console/core_console.h b/repos/base-sel4/src/base/console/core_console.h new file mode 100644 index 000000000..738acda03 --- /dev/null +++ b/repos/base-sel4/src/base/console/core_console.h @@ -0,0 +1,27 @@ +/* + * \brief Console backend for seL4 + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +#include + + +namespace Genode +{ + class Core_console : public Console + { + protected: + + void _out_char(char c) { } + }; +} + + diff --git a/repos/base-sel4/src/base/ipc/ipc.cc b/repos/base-sel4/src/base/ipc/ipc.cc new file mode 100644 index 000000000..b78a0a849 --- /dev/null +++ b/repos/base-sel4/src/base/ipc/ipc.cc @@ -0,0 +1,135 @@ +/* + * \brief seL4 implementation of the IPC API + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +/* Genode includes */ +#include +#include +#include +#include + +using namespace Genode; + + +/***************** + ** Ipc_ostream ** + *****************/ + +void Ipc_ostream::_send() +{ + PDBG("not implemented"); + + _write_offset = sizeof(umword_t); +} + + + +Ipc_ostream::Ipc_ostream(Native_capability dst, Msgbuf_base *snd_msg) +: + Ipc_marshaller((char *)snd_msg->addr(), snd_msg->size()), + _snd_msg(snd_msg), _dst(dst) +{ + _write_offset = sizeof(umword_t); +} + + +/***************** + ** Ipc_istream ** + *****************/ + +void Ipc_istream::_wait() +{ + PDBG("not implemented"); + + _read_offset = sizeof(umword_t); +} + + +Ipc_istream::Ipc_istream(Msgbuf_base *rcv_msg) +: + Ipc_unmarshaller((char *)rcv_msg->addr(), rcv_msg->size()), + _rcv_msg(rcv_msg) +{ + _read_offset = sizeof(umword_t); +} + + +Ipc_istream::~Ipc_istream() { } + + +/**************** + ** Ipc_client ** + ****************/ + +void Ipc_client::_call() +{ + PDBG("not implemented"); + + _write_offset = _read_offset = sizeof(umword_t); +} + + +Ipc_client::Ipc_client(Native_capability const &srv, Msgbuf_base *snd_msg, + Msgbuf_base *rcv_msg, unsigned short) +: Ipc_istream(rcv_msg), Ipc_ostream(srv, snd_msg), _result(0) +{ } + + +/**************** + ** Ipc_server ** + ****************/ + +void Ipc_server::_prepare_next_reply_wait() +{ + /* now we have a request to reply */ + _reply_needed = true; + + /* leave space for return value at the beginning of the msgbuf */ + _write_offset = 2*sizeof(umword_t); + + /* receive buffer offset */ + _read_offset = sizeof(umword_t); +} + + +void Ipc_server::_wait() +{ + /* wait for new server request */ + try { Ipc_istream::_wait(); } catch (Blocking_canceled) { } + + _prepare_next_reply_wait(); +} + + +void Ipc_server::_reply() +{ + try { _send(); } catch (Ipc_error) { } + + _prepare_next_reply_wait(); +} + + +void Ipc_server::_reply_wait() +{ + if (_reply_needed) + _reply(); + + _wait(); +} + + +Ipc_server::Ipc_server(Msgbuf_base *snd_msg, + Msgbuf_base *rcv_msg) +: + Ipc_istream(rcv_msg), Ipc_ostream(Native_capability(), snd_msg), + _reply_needed(false) +{ } diff --git a/repos/base-sel4/src/base/ipc/pager.cc b/repos/base-sel4/src/base/ipc/pager.cc new file mode 100644 index 000000000..3a07a4560 --- /dev/null +++ b/repos/base-sel4/src/base/ipc/pager.cc @@ -0,0 +1,44 @@ +/* + * \brief Pager support for seL4 + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +/* Genode includes */ +#include +#include + +using namespace Genode; + + +/*************** + ** IPC pager ** + ***************/ + +void Ipc_pager::wait_for_fault() +{ + PDBG("not implemented"); +} + + +void Ipc_pager::reply_and_wait_for_fault() +{ + PDBG("not implemented"); +} + + +void Ipc_pager::acknowledge_wakeup() +{ + PDBG("not implemented"); +} + + +Ipc_pager::Ipc_pager() { } + diff --git a/repos/base-sel4/src/base/lock/lock_helper.h b/repos/base-sel4/src/base/lock/lock_helper.h new file mode 100644 index 000000000..4d09ef2f8 --- /dev/null +++ b/repos/base-sel4/src/base/lock/lock_helper.h @@ -0,0 +1,31 @@ +/* + * \brief seL4-specific helper functions for the Lock implementation + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +/* Genode includes */ +#include +#include + + +static inline void thread_yield() { } + + +static inline bool thread_check_stopped_and_restart(Genode::Thread_base *) +{ + return false; +} + + +static inline void thread_switch_to(Genode::Thread_base *thread_base) { } + + +static inline void thread_stop_myself() { } diff --git a/repos/base-sel4/src/base/thread/thread_bootstrap.cc b/repos/base-sel4/src/base/thread/thread_bootstrap.cc new file mode 100644 index 000000000..531b81d0e --- /dev/null +++ b/repos/base-sel4/src/base/thread/thread_bootstrap.cc @@ -0,0 +1,32 @@ +/* + * \brief Thread bootstrap code + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +/* Genode includes */ +#include +#include + + +/***************************** + ** Startup library support ** + *****************************/ + +void prepare_init_main_thread() { } + +void prepare_reinit_main_thread() { prepare_init_main_thread(); } + + +/***************** + ** Thread_base ** + *****************/ + +void Genode::Thread_base::_thread_bootstrap() { } diff --git a/repos/base-sel4/src/base/thread/thread_sel4.cc b/repos/base-sel4/src/base/thread/thread_sel4.cc new file mode 100644 index 000000000..1cf78b872 --- /dev/null +++ b/repos/base-sel4/src/base/thread/thread_sel4.cc @@ -0,0 +1,61 @@ +/* + * \brief seL4-specific implementation of the Thread API + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +/* Genode includes */ +#include +#include +#include +#include + +#include +#include + + +using namespace Genode; + + +/** + * Entry point entered by new threads + */ +//void Thread_base::_thread_start() +//{ +// PDBG("not implemented"); +//} + + +/***************** + ** Thread base ** + *****************/ + +void Thread_base::_init_platform_thread(size_t, Type type) +{ + PDBG("not implemented"); +} + + +void Thread_base::_deinit_platform_thread() +{ + PDBG("not implemented"); +} + + +void Thread_base::start() +{ + PDBG("not implemented"); +} + + +void Thread_base::cancel_blocking() +{ + PDBG("not implemented"); +} diff --git a/repos/base-sel4/src/test/sel4/context_area.cc b/repos/base-sel4/src/test/sel4/context_area.cc new file mode 100644 index 000000000..e1a935f79 --- /dev/null +++ b/repos/base-sel4/src/test/sel4/context_area.cc @@ -0,0 +1,23 @@ +/* + * \brief Dummy context_area helper + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +#include +#include + +namespace Genode { + + Rm_session *env_context_area_rm_session() { return nullptr; } + + Ram_session *env_context_area_ram_session() { return nullptr; } +} + diff --git a/repos/base-sel4/src/test/sel4/main.cc b/repos/base-sel4/src/test/sel4/main.cc new file mode 100644 index 000000000..77e17df17 --- /dev/null +++ b/repos/base-sel4/src/test/sel4/main.cc @@ -0,0 +1,19 @@ +/* + * \brief Test for exercising the seL4 kernel interface + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + + +int main() +{ + *(int *)0x1122 = 0; + return 0; +} diff --git a/repos/base-sel4/src/test/sel4/mini_env.cc b/repos/base-sel4/src/test/sel4/mini_env.cc new file mode 100644 index 000000000..5e148f9e8 --- /dev/null +++ b/repos/base-sel4/src/test/sel4/mini_env.cc @@ -0,0 +1,38 @@ +/* + * \brief Minimalistic implementation of the Genode::env + * \author Norman Feske + * \date 2014-10-14 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +#include + + +namespace Genode { struct Mini_env; } + + +struct Genode::Mini_env : Env +{ + Parent *parent() { return nullptr; } + Ram_session *ram_session() { return nullptr; } + Ram_session_capability ram_session_cap() { return Ram_session_capability(); } + Cpu_session *cpu_session() { return nullptr; } + Cpu_session_capability cpu_session_cap() { return Cpu_session_capability(); } + Rm_session *rm_session() { return nullptr; } + Pd_session *pd_session() { return nullptr; } + Allocator *heap() { return nullptr; } +}; + +namespace Genode { + + Env *env() { + static Mini_env inst; + return &inst; + } +} diff --git a/repos/base-sel4/src/test/sel4/target.mk b/repos/base-sel4/src/test/sel4/target.mk new file mode 100644 index 000000000..08e191497 --- /dev/null +++ b/repos/base-sel4/src/test/sel4/target.mk @@ -0,0 +1,15 @@ +TARGET = test-sel4 +SRC_CC = main.cc context_area.cc mini_env.cc thread.cc + +LIBS = base-common + +SRC_CC += base/console/core_printf.cc +INC_DIR += $(REP_DIR)/src/base/console + +vpath %.cc $(BASE_DIR)/src + +SRC_CC += thread_sel4.cc +vpath thread_sel4.cc $(REP_DIR)/src/base/thread + +SRC_CC += thread_bootstrap.cc +vpath thread_bootstrap.cc $(REP_DIR)/src/base/thread diff --git a/repos/base-sel4/src/test/sel4/thread.cc b/repos/base-sel4/src/test/sel4/thread.cc new file mode 100644 index 000000000..1a8f7cb4b --- /dev/null +++ b/repos/base-sel4/src/test/sel4/thread.cc @@ -0,0 +1,58 @@ +/* + * \brief Implementation of the Thread API + * \author Norman Feske + * \date 2014-10-15 + */ + +/* + * Copyright (C) 2014 Genode Labs GmbH + * + * This file is part of the Genode OS framework, which is distributed + * under the terms of the GNU General Public License version 2. + */ + +#include +#include +#include +#include +#include + +using namespace Genode; + + +static Thread_base::Context *main_context() +{ + enum { STACK_SIZE = sizeof(long)*4*1024 }; + + static long buffer[STACK_SIZE/sizeof(long)]; + + /* the context is located beyond the top of the stack */ + addr_t const context_addr = (addr_t)buffer + sizeof(buffer) + - sizeof(Thread_base::Context); + + Thread_base::Context *context = (Thread_base::Context *)context_addr; + context->stack_base = (addr_t)buffer; + return context; +} + + +Thread_base *Thread_base::myself() { return nullptr; } + + +Thread_base::Thread_base(size_t, const char *name, size_t stack_size, Type type, + Cpu_session *cpu_session) +: + _cpu_session(cpu_session), _context(main_context()) +{ + strncpy(_context->name, name, sizeof(_context->name)); + _context->thread_base = this; + + _init_platform_thread(type); +} + + +Thread_base::Thread_base(size_t quota, const char *name, size_t stack_size, Type type) +: Thread_base(quota, name, stack_size, type, nullptr) { } + + +Thread_base::~Thread_base() { _deinit_platform_thread(); }