Re: [seL4] Frame buffer

2016-07-07 Thread Alexander Boettcher
ork and PS/2 driver. Under [2] you may find the current working branch, which is still in flux. We hope to get all our remaining x86 driver running until our Genode 16.08 release (see roadmap [3]), e.g. Intel graphic, Intel wifi and audio driver on native x86 hardware. Cheers, Alexander Boettche

[seL4] 3.1.0 to 3.2.0 (x86) upgrade issue

2016-07-21 Thread Alexander Boettcher
Hello, after upgrading the seL4 kernel (x86) from 3.1.0 to 3.2.0 we get for the very first invocation of seL4_X86_Page_Map an errorcode of *3* (seL4_IllegalOperation). We bisected the commits between 3.1.0 and 3.2.0 and [0] is the first bad commit for us. If we use the 3.2.0 release with [0] reve

[seL4] Image lies outside of usable physical memory

2016-07-21 Thread Alexander Boettcher
Hi, I want to boot seL4 (x86) 3.2.0 on a native machine (Lenovo X201) and I get a message like: End of loaded userland image lies outside of usable physical memory seL4 called fail at sel4/src/arch/x86/kernel/boot_sys.c: in function boot_sys, saying "boot_sys failed for some reason :( (Full log

Re: [seL4] 3.1.0 to 3.2.0 (x86) upgrade issue

2016-07-21 Thread Alexander Boettcher
gt; > Adrian > > On Thu 21-Jul-2016 11:55 PM, Alexander Boettcher wrote: > > Hello, > > after upgrading the seL4 kernel (x86) from 3.1.0 to 3.2.0 we get for the > very first invocation of seL4_X86_Page_Map an errorcode of *3* > (seL4_IllegalOperation). > > We b

[seL4] x86: loosing edge triggered interrupts when using I/O APIC

2016-08-23 Thread Alexander Boettcher
crokernels using the I/O APIC and they don't mask edge level triggered I/O APIC interrupts. I wonder if anybody already stumbled about the issue on seL4/x86? If not, please take the patch or give advices to adapt the patch so that it may get upstream. Thanks, Alexander Boettcher. [0] http:

Re: [seL4] IA32 syscall bindings

2016-08-23 Thread Alexander Boettcher
e.g. There, depending on "__pic__", different L4_SAVE_REG/L4_RESTORE_REG defines are prepared and later on used by the assembler parts. Is this the way to go ? Thanks for any suggestions. Cheers, Alexander Boettcher. [0] https://github.com/genodelabs/genode/blob/master/repos/base-sel4/patche

Re: [seL4] IA32 syscall bindings

2016-08-25 Thread Alexander Boettcher
set when -fpic or -fPIC is used. Please have a look and give advices what should be adjusted. Thanks, Alex. [0] https://github.com/alex-ab/genode/blob/sel4_syscall/sel4.patch > > Adrian > > On Tue 23-Aug-2016 7:35 PM, Alexander Boettcher wrote: >> Hello, >> >&

Re: [seL4] IA32 syscall bindings

2016-08-26 Thread Alexander Boettcher
Ok, added a github issue (34) with the commit. Alex. On 26.08.2016 01:20, Adrian Danis wrote: > I cannot really see a nicer way to implement it, so I think it's fine if > you want to put it up as a PR. > > Adrian > > On Fri 26-Aug-2016 7:15 AM, Alexander Boettcher wrote:

[seL4] Genode 16.08 supports dynamic workloads on seL4

2016-08-31 Thread Alexander Boettcher
n the extensive release documentation: https://genode.org/documentation/release-notes/16.08 and, for the impatient, a life demo scenario of Genode on seL4 can be downloaded: https://www.genode.org/documentation/release-notes/16.08#Try_Genode_seL4_at_home Best regards, -- Alexander Boettcher G

[seL4] Compilation of seL4 kernel 5.2.0

2017-06-13 Thread Alexander Boettcher
ware_gen.h 32/mode/api/shared_types_gen.h src/arch/x86/32/machine_asm.s_pp src/arch/x86/32/traps.s_pp src/arch/x86/multiboot.s_pp arch/object/structures_gen.h src/arch/x86/32/head.s_pp -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsge

Re: [seL4] Compilation of seL4 kernel 5.2.0

2017-06-13 Thread Alexander Boettcher
On 13.06.2017 11:08, Alexander Boettcher wrote: > alex@max:~/sel4.git$ ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 make it seems a ia32 only issue, using x86_64 succeeds. release SEL4_ARCH=ia32/x86_64 --- 3.2.0 - ok/ok 4.0.0 - fails/ok 5.0.0 - fails/ok 5.1.0 - fails/ok 5.2.0 - fails

[seL4] seL4_Fault_t and friends seems to be missing in user libsel4

2017-06-13 Thread Alexander Boettcher
seL4_Fault_tag seL4_Fault_VMFault_new and a lot more. These structs and functions seems to be generated only for the kernel side, e.g. in kernel_final.c they show up, but there are no traces of them on the user level side. Do I just miss a configuration option ? Thanks, -- Alexander Boettcher

Re: [seL4] seL4_Fault_t and friends seems to be missing in user libsel4

2017-06-14 Thread Alexander Boettcher
d 14-Jun-2017 1:32 AM, Alexander Boettcher wrote: > > Hello, > > if I compile and link seL4 5.2.0 > > ARCH=x86 PLAT=pc99 SEL4_ARCH=x86_64 make > > and I finally try to use the generated syscall/libsel4 headers, the > compiler complains about missing seL4_Fault types

Re: [seL4] seL4_Fault_t and friends seems to be missing in user libsel4

2017-06-14 Thread Alexander Boettcher
just send us a note. Alex. -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth ___ Devel mailing lis

[seL4] x86_64 kernel crash

2017-08-24 Thread Alexander Boettcher
rnel_vanilla/autoconfig.patch [1] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/image_bomb.elf [2] https://github.com/alex-ab/genode/raw/crash_sel4_kernel_vanilla/sel4 [3] https://genode.org/download/tool-chain [4] https://sourceforge.net/projects/genode/files/genode-toolchain/17.0

[seL4] benchmark - idle utilization

2017-08-25 Thread Alexander Boettcher
y for seL4 to handle this minor case. Could this possibly be changed (easily) ? Thanks, Alex. -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-

Re: [seL4] UEFI support for x86

2017-08-25 Thread Alexander Boettcher
n > Skipping table RSCI,, unknown > Skipping table WDAT^D^A, unknown > Warning: skipping table ACPI XSDT > > Maybe one or more of those tables needs to be loaded to handle > interrupts properly. The LPIT table is conspicuous in the case of the > timer test but I think other tests are likely to depend on the other tables. >

Re: [seL4] UEFI support for x86

2017-08-29 Thread Alexander Boettcher
ypes.h#L83). > Aside from that, as you say the code needs some deduplication etc, but I'm > happy to continue on github and get this in. ok, created a github issue at https://github.com/seL4/seL4/issues/67 -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://ww

Re: [seL4] benchmark - idle utilization

2017-08-29 Thread Alexander Boettcher
st needs to initialize the information properly. Currently I > believe the initialization is somewhat 'not done' under the assumption that > benchmark_utilisation_switch / benchmark_track_reset_utilisation will get > called. > > Adrian > > On Fri 25-Aug-2017 10:37

[seL4] Genode OS Framework 17.08 with extended seL4 support

2017-08-30 Thread Alexander Boettcher
notes/17.08 All the best, -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth ___ Devel mailing

Re: [seL4] x86_64 kernel crash

2017-08-30 Thread Alexander Boettcher
for reporting this. > > Adrian > > On Fri 25-Aug-2017 6:49 AM, Alexander Boettcher wrote: > > Hello, > > we're are in progress of extending our Genode/seL4 support, namely > adding x86_64 and ARM support. > > During this work I encountered on x86_64 some

Re: [seL4] UEFI support for x86

2017-10-02 Thread Alexander Boettcher
arning: VBE Bios not present > [init -> fb_drv] Warning: Could not set vesa mode 0x0@16 > [init -> ps2_drv] Error: no data available > [init -> nitpicker] Error: Framebuffer-session creation failed > (ram_quota=8192, cap_quota=3) > [init -> nitpicker] Error: __cxa_guard

Re: [seL4] UEFI support for x86

2017-11-30 Thread Alexander Boettcher
Hello, On 02.10.2017 11:05, Alexander Boettcher wrote: > The fb_boot_drv component could work with seL4 in UEFI mode (it does > with Genode/NOVA), but unfortunately the information about the > framebuffer location, size, color depth etc. are not propagated through > the seL4 k

Re: [seL4] UEFI support for x86

2017-12-04 Thread Alexander Boettcher
sical memory region 0x0-0x1f80 I'm not sure, whether here the Multiboot 2 information is incorrect or the parsing by the kernel is too strict. Here one would require some more investigation in the Multiboot 2 spec (overlapping regions are valid or not?) and on the target machine in grub2

Re: [seL4] UEFI support for x86

2017-12-11 Thread Alexander Boettcher
(Or at best use both drivers and add a input multiplexer, e.g. [0], which takes both drivers as input sources). Beforehand you may just try the usb_hid [1] scenario to actual test whether usb in general work on your machine(s). [0] repos/os/src/server/input_merger/README [1] repos/dde_linux/run/usb_

Re: [seL4] Memory Region overlap error

2018-07-09 Thread Alexander Boettcher
oot/sel4 ...". Use some simple scenario for testing, like log.run If the issue persists, you may try to boot Genode/seL4 the Multiboot 1 way instead of Multiboot 2, which however will solely work for BIOS legacy boots (no UEFI). Replace the "multiboot2" and "module2" in

Re: [seL4] Memory Region overlap error

2018-07-11 Thread Alexander Boettcher
ultiboot 2 Memory region overlap Thanks for testing. May you please apply the seL4 kernel patch and test, whether this solves your issue ? [0] http://usr.sysret.de/jws/genode/hcl.html -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amt

Re: [seL4] Memory Region overlap error

2018-07-11 Thread Alexander Boettcher
I would guess that now something is wrong with the ACPI tables (content provided by the BIOS/UEFI of your machine or the parsing in the kernel). Cheers, -- Alexander Boettcher Genode Labs http://www.genode-labs.com - http://www.genode.org Genode Labs GmbH - Amtsgericht Dresden

[seL4] x86 seL4 kernel bug - kernel page faults on seL4_VMEnter

2018-09-25 Thread Alexander Boettcher
/0dd40b6c43a290173ea7782b97afbbbddfa23b36/src/arch/x86/object/vcpu.c#L1543 [1] https://sel4.systems/Info/Roadmap/home.pml -- Alexander Boettcher Genode Labs https://www.genode-labs.com - https://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske

Re: [seL4] x86 seL4 kernel bug - kernel page faults on seL4_VMEnter

2018-09-26 Thread Alexander Boettcher
ification, > NODE_STATE(ksCurThread)); > > I'll create a task to investigate deeper and add a test for this to our test > suite and confirm that the fix works. We won't have time to do this in the > next week though. It would be great if you can let me know if the patch

Re: [seL4] Problem in Installing Genode OS

2018-10-02 Thread Alexander Boettcher
rds any other operating system which > is built using the seL4 microkernel. Camkes is another option. Cheers, -- Alexander Boettcher Genode Labs https://www.genode-labs.com - https://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing

[seL4] FOSDEM 2019 - Microkernels developer room - CfP

2018-10-12 Thread Alexander Boettcher
FYI Forwarded Message Subject: FOSDEM 2019 - Microkernels developer room - CfP Date: Thu, 11 Oct 2018 11:48:24 +0200 From: Sebastian Sumpf Reply-To: Genode users mailing list To: us...@lists.genode.org FOSDEM 2019 - Microkernels and Component-based OSes devroom CALL FOR PARTIC

[seL4] Scheduling of vCPUs on x86

2018-11-08 Thread Alexander Boettcher
scheduler thread states to be different between hardware architectures in seL4. Cheers, -- Alexander Boettcher Genode Labs https://www.genode-labs.com - https://www.genode.org Genode Labs GmbH - Amtsgericht Dresden - HRB 28424 - Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian He

Re: [seL4] Scheduling of vCPUs on x86

2018-11-08 Thread Alexander Boettcher
On 08.11.18 09:30, Alexander Boettcher wrote: > vCPUs) on the same timeslice are not considered to be scheduled again, Sorry, "on the same timeslice" must be replaced by "on the same priority level" Cheers, -- Alexander Boettcher Genode Labs https://www.genode-labs.com -

Re: [seL4] Scheduling of vCPUs on x86

2018-11-08 Thread Alexander Boettcher
interest, what's the reason for the different approaches? >> ___ >> Devel mailing list >> Devel@sel4.systems >> https://sel4.systems/lists/listinfo/devel >> > > > ___ &g

Re: [seL4] Scheduling of vCPUs on x86

2018-11-08 Thread Alexander Boettcher
't see an obvious way to keep the original if statement and add a || and a ifdef CONFIG_VTX ... without changing the original code. Since the type of switch style and the ifdef was used already in the same file, I supposed it such be fine. But let's see how you change it ;-) Thanks,

Re: [seL4] TLB issue

2018-11-15 Thread Alexander Boettcher
CPUs still successfully > access the corresponding memory instead of triggering a fault. > > To be able to reproduce the problem, you might investigate the simple > test case here: > > > https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7da50 >

Re: [seL4] TLB issue

2018-12-18 Thread Alexander Boettcher
://github.com/seL4/seL4/pull/107 On 15.11.18 14:39, Alexander Boettcher wrote: > Hello, > > On 15.11.18 13:20, Stefan Kalkowski wrote: >> yesterday I've started to develop a low-level platform test to stress several >> multi-processor aspects on top of the Genode API. Thereby,

Re: [seL4] Rust ports on Genode/seL4

2019-11-04 Thread Alexander Boettcher
ch you don't need in the beginning. Try to adhere to the https://genode.org/documentation/developer-resources/getting_started example and set as kernel seL4 to build and start a graphical demo. Cheers, Alex. -- Alexander Boettcher Genode Labs https://www.genode-labs.com - https://www

[seL4] CfP: Microkernel and Component-based OS Devroom at FOSDEM 2022

2021-12-07 Thread Alexander Boettcher
Hello seL4 community, FOSDEM 2022 will be an online event (again) with the traditional Microkernel devroom as part of it. Thanks to Martin Decky & my colleague Sebastian Sumpf for engagement! The original Call for Papers follows. Best regards, Alexander. -- Alexander Boettcher Genode