- Devel - lists.sel4.systems

Re: [seL4] seL4 website down
by Mike Clark 03 Oct '17

03 Oct '17

Yes, it appears to be down. Mike On Oct 2, 2017 12:39 PM, <keith(a)matellio.com> wrote: Is it just me or is everyone having trouble accessing the seL4 website? I’m getting the following: MOD_PYTHON ERROR ProcessId: 29222 Interpreter: 'sel4.systems.keg.ertos.in.nicta.com.au' ServerName: 'sel4.systems.keg.ertos.in.nicta.com.au' DocumentRoot: '/var/www/seL4/content' URI: '/Community/mailman/home.pml' Location: '/Community' Directory: None Filename: '/var/www/seL4/content/Community/mailman/home.pml' PathInfo: None Phase: 'PythonHandler' Handler: 'ertos' Traceback (most recent call last): File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch default=default_handler, arg=req, silent=hlist.silent) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target module = import_module(module_name, path=path) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module return __import__(module_name, {}, {}, ['*']) File "/var/www/seL4/code/ertos.py", line 9, in <module> from bib import html_bib, html_abstract, yearlist, get_bibtex File "/var/www/seL4/code/bib.py", line 11, in <module> rg = cfg.get('core', 'rg') File "/usr/lib/python2.7/ConfigParser.py", line 618, in get raise NoOptionError(option, section) NoOptionError: No option 'rg' in section: 'core' Keith _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

2 1

seL4 website down
by keith＠matellio.com 03 Oct '17

03 Oct '17

Is it just me or is everyone having trouble accessing the seL4 website? I'm getting the following: MOD_PYTHON ERROR ProcessId: 29222 Interpreter: 'sel4.systems.keg.ertos.in.nicta.com.au' ServerName: 'sel4.systems.keg.ertos.in.nicta.com.au' DocumentRoot: '/var/www/seL4/content' URI: '/Community/mailman/home.pml' Location: '/Community' Directory: None Filename: '/var/www/seL4/content/Community/mailman/home.pml' PathInfo: None Phase: 'PythonHandler' Handler: 'ertos' Traceback (most recent call last): File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch default=default_handler, arg=req, silent=hlist.silent) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target module = import_module(module_name, path=path) File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module return __import__(module_name, {}, {}, ['*']) File "/var/www/seL4/code/ertos.py", line 9, in <module> from bib import html_bib, html_abstract, yearlist, get_bibtex File "/var/www/seL4/code/bib.py", line 11, in <module> rg = cfg.get('core', 'rg') File "/usr/lib/python2.7/ConfigParser.py", line 618, in get raise NoOptionError(option, section) NoOptionError: No option 'rg' in section: 'core' Keith

1 0

Integer overflow bug in capdl-loader
by Jeff Kubascik 30 Sep '17

30 Sep '17

Hello, I am working with seL4 7.0.0 on the zynq7000 platform. I have come across a bug that occurs when a device physical memory region includes the highest address, i.e. where the memory region ends at 0xFFFFFFFF on 32 bit systems. When I create a CAmkES component that uses the highest address, I see the following error. ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0 paddr=[10000000..100ac81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'capdl-loader-experimental' paddr=[33000..1aefff] vaddr=[8000..183fff] virt_entry=befc Enabling MMU and paging Bootstrapping kernel Booting all finished, dropped to user space <<seL4(CPU 0) [decodeUntypedInvocation/210 T0xffdfd100 "rootserver" @8fa8]: Untyped Retype: Insufficient memory (1 * 4096 bytes needed, 0 bytes available).>> Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() [Err seL4_NotEnoughMemory]: I have traced this problem to an integer overflow bug in the capdl-loader. The patch below shows how I have addressed this error. >From 22c9dd76a31713c98710830c2ea865a4e5d8a078 Mon Sep 17 00:00:00 2001 From: Jeff Kubascik <jeff.kubascik(a)dornerworks.com> Date: Wed, 27 Sep 2017 13:52:36 -0400 Subject: [PATCH] Fixed integer overflow bug in capdl-loader that occurs when a device physical memory region ends at 0xFFFFFFFF --- capdl-loader-app/src/main.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c index 34eedb0..305da2a 100644 --- a/capdl-loader-app/src/main.c +++ b/capdl-loader-app/src/main.c @@ -554,7 +554,7 @@ static int find_device_object(void *paddr, seL4_Word type, int size_bits, seL4_C /* Assume we are allocating from a device untyped. Do a linear search for it */ for (unsigned int i = 0; i < bootinfo->untyped.end - bootinfo->untyped.start; i++) { if (bootinfo->untypedList[i].paddr <= (uintptr_t)paddr && - bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) >= (uintptr_t)paddr + BIT(size_bits)) { + bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) - 1 >= (uintptr_t)paddr + BIT(size_bits) - 1) { /* just allocate objects until we get the one we want. To do this * correctly we cannot just destroy the cap we allocate, since * if it's the only frame from the untyped this will reset the -- 2.7.4 I have added a -1 to the end address calculations to fix the edge case when bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) is equal to 0x100000000, an integer overflow. The current statement is comparing the address of the next byte past the end of the memory region. My change is comparing the address of the last byte in the memory region. I have tested this fix on the zynq7000 and it works. However, I am not too familiar with the capdl-loader. Are there any problems with this fix that I have not considered? Thanks, Jeff Kubascik

2 2

ARM 64-bit Support in seL4
by keith＠matellio.com 29 Sep '17

29 Sep '17

Not sure if this is the best place to post this question but I noticed on the seL4 roadmap page on the website that 64-bit support for ARM is due out at the end of 3Q2017. Is that correct, and if so, can someone give me some hints of where to look for it in the repository?

4 3

sel4 on QEMU
by ashokk＠spanidea.com 28 Sep '17

28 Sep '17

Hi, I am trying to run sel4 on QEMU, i am following this steps(https://wiki.sel4.systems/Hardware/Qemu) make clean make optiplex9020_defconfig make silentoldconfig make but while doing make i am getting following error.. /home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c: In function ‘get_breakpoint_format’:/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: error: ‘seL4_InstructionBreakpoint’ undeclared (first use in this function) *break_type = seL4_InstructionBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: note: each undeclared identifier is reported only once for each function it appears in/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:131:19: error: ‘seL4_BreakOnRead’ undeclared (first use in this function) *rw = seL4_BreakOnRead; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:135:27: error: ‘seL4_DataBreakpoint’ undeclared (first use in this function) *break_type = seL4_DataBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:136:19: error: ‘seL4_BreakOnWrite’ undeclared (first use in this function) *rw = seL4_BreakOnWrite; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:146:19: error: ‘seL4_BreakOnReadWrite’ undeclared (first use in this function) *rw = seL4_BreakOnReadWrite; ^make[1]: *** [src/gdb_server/gdb.o] Error 1make: *** [libsel4camkes] Error 2 can you please give any solution to solve these errors.. RegardsAshok

2 2

Sel4 compilation error for RasperryPi-3
by ashokk＠spanidea.com 27 Sep '17

27 Sep '17

Hi I am trying to cross-compile sel4 for rasperry-pi-3. i am executing following command on sel4 kernel source to cross-compile. TOOLPREFIX=arm-linux-gnueabi- ARCH=arm PLAT=bcm2837 ARMV=armv8-a CPU=cortex-a53 i am getting following error while doing make [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] 32/mode/api/shared_types_gen.h [CPP] src/arch/arm/armv/armv8-a/32/machine_asm.s_pp In file included from src/arch/arm/armv/armv8-a/32/machine_asm.S:11:0: ./include/config.h:17:22: fatal error: autoconf.h: No such file or directory compilation terminated. make: *** [src/arch/arm/armv/armv8-a/32/machine_asm.s_pp] Error 1 rm 32/mode/api/shared_types_gen.h plat/machine/hardware_gen.h arch/object/structures_gen.h is there any solution for this... RegardsAshok

2 1

General question about software
by Raymond Jennings 26 Sep '17

26 Sep '17

So, I know that at a basic level, a block device driver would probably need I/O permissions, and I'm guessing that it would be handling requests from a file system driver. Is that basically how the seL4 software ecosystem is laid out? What's typical for how "software in the wild" is actually organized and layered on top of the microkernel? I only know about seL4 from a theoretical standpoint, read the manual and stuff, and mostly familiar with the actual kernel, but I'm a complete noob when it comes to actual software.

3 2

Raspberry pi 3 compilation error
by Prathamesh Rahate 26 Sep '17

26 Sep '17

Hi, I am trying to cross-compile seL4 for rapsberry pi 3 using steps mentioned hereseL4 on the Raspberry Pi 3 | | | seL4 on the Raspberry Pi 3 | | | I am getting following error while compiling, are there any patches available to fix this error: [STAGE] libsel4sync.a[libs/libsel4sync] done.[apps/sel4test-tests] building... [HEADERS] [STAGE] test_init_data.h [STAGE] arch/* [STAGE] arch_frame_type.h [STAGE] autoconf.h [CC] src/helpers.o [CC] src/main.o [CC] src/tests/multicore.o [CC] src/tests/preempt.o [CC] src/tests/serial_server.o [CC] src/tests/breakpoints.o [CC] src/tests/scheduler.o [CC] src/tests/pagetables.o [CC] src/tests/inc_untyped.o [CC] src/tests/interrupt.o [CC] src/tests/sync.o [CC] src/tests/iopt.o [CC] src/tests/ioports.o [CC] src/tests/vspace.o [CC] src/tests/ipc.o [CC] src/tests/schedcontext.o [CC] src/tests/fpu.o [CC] src/tests/ept.o [CC] src/tests/trivial.o [CC] src/tests/binding.o [CC] src/tests/cnodeops.o [CC] src/tests/threads.o [CC] src/tests/cspace.o [CC] src/tests/regressions.o/tmp/cc7e2jo9.s: Assembler messages:/tmp/cc7e2jo9.s:120: Error: selected processor does not support ARM mode `ldrex r2,[r3]'/tmp/cc7e2jo9.s:154: Error: selected processor does not support ARM mode `strex r0,r3,[r2]'make[1]: *** [src/tests/regressions.o] Error 1make: *** [sel4test-tests] Error 2user@user-Lenovo:~/seL4test$ Thanks,Prathamesh

2 1

User-space drivers
by ashokk＠spanidea.com 25 Sep '17

25 Sep '17

Hi guys, This is Ashokkumar, i want to write a sample serial(UART) communication user-space driver in sel4,can i get any help from your side. I am just started sel4 i don't know how to build and execute the programs,if you have any documents or examples about user-space programs please share with me... RegardsAshok

2 1

Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches
by Austin Seipp 21 Sep '17

21 Sep '17

Hello *, I hope you're all doing well. I recently got seL4 running on my Raspberry Pi 3, and wanted to report some notes here and ask some questions regarding the port, and perhaps get some help working on a patch (or twelve, I'm sure.) Recently I followed the Data61 blog post here to get a recent copy of seL4 on my RPi, but hit a few errors along the way that burned some time. In particular I got burned by the U-Boot glitch and getting seL4 building due to a glitch in the 'repo' setup for sel4test: https://research.csiro.au/ tsblog/sel4-raspberry-pi-3/ I ended up writing my own blog post, with effectively "fully reproducible" instructions (e.g. one of the codepad.org links on the RPi3 wiki page was dead) for a recent build. This includes proper setup for uboot.env in order to `fatload` and `bootm` the seL4 ELF binary off disk, the right U-Boot version, and using Docker to build the seL4 image: https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html That's all fine, but... I got curious about this U-Boot glitch, as even a recent (git) copy of U-Boot still suffered from the issue reported in the original Data61 blog post. I found it strange this regression would exist for nearly 9 months, unless it was possibly something intentional (e.g. an intended behavioral change) or it went unreported. The glitch is this: after booting the seL4 binary, the system immediately hangs with no output after trying to start the sel4test application. This glitch did not occur in versions of U-Boot up-to v2017.01. Versions v2017.03 and later (to now) suffer. I decided to spend some time bisecting this problem and found the issue. Versions of U-Boot after v2017.01 include the following patch, which causes the data cache to be enabled prior to U-Boot loading and executing ELF binaries: https://github.com/thoughtpolice/u-boot/commit/ 995eab8b5b580b67394312b1621c60a71042cd18 This behavior previously existed as a workaround for QNX, which required that the dcache be disabled before execution. U-Boot, previously, disabled the dcache when booting *any* ELF binary at all (the binary can of course enable it or check to see if it isn't enabled already), as a simplistic workaround. This patch changes it to only disable the dcache on U-Boot images (uImages) marked as QNX ELF binaries, so that QNX systems boot properly still. It would seem then that seL4 -- or at least sel4test -- requires the dcache to be disabled upon entry for the RPi3. If the dcache is enabled, as in the above patch, it otherwise hangs immediately. In fact, a recent copy of U-Boot *can* execute seL4 properly: you simply have to use `./tools/mkimage` inside U-Boot to mark the application as `mkimage -C none -A arm -T kernel -O qnx -d <input> <output>` first -- this creates a uImage with the appropriate header to mark the ELF as a QNX binary. U-Boot recognizes this and appropriately disables the dcache before application entry, once you use `bootm` or something. I took the time to write a patch to U-Boot in order to add a new OS definition -- "sel4" -- in order to address this problem more clearly. My change is here: https://github.com/thoughtpolice/u-boot/commit/ 720caf6c398584658abfa883d4d390f4b6200269 With this change, you can mark any seL4 binary as `-O sel4` to create an appropriately bootable uImage, with the dcache appropriately disabled. Assuming this is in place, the following U-Boot commands will execute seL4: U-Boot> setenv bootfile uImage U-Boot> fatload mmc 0 ${loadaddr} ${bootfile} U-Boot> bootm ${loadaddr} ## Booting kernel from Legacy Image at 00200000 ... Image Name: Image Type: ARM seL4 Kernel Image (uncompressed) Data Size: 3385548 Bytes = 3.2 MiB Load Address: 00000000 Entry Point: 00000000 Verifying Checksum ... OK Loading Kernel Image ... OK CACHE: Misaligned operation at range [20000000, 200078bc] CACHE: Misaligned operation at range [200078bc, 2032a720] CACHE: Misaligned operation at range [2032c000, 2033c820] ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4 paddr=[20000000..2033c81f] ELF-loading image 'kernel' paddr=[0..32fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[33000..44dfff] vaddr=[10000..42afff] virt_entry=2a03c Enabling MMU and paging Jumping to kernel-image entry point... ---- So with that all done, it's clear there's a change needed *somewhere* but I'm not sure where or what to do: 1) Is the above the right approach? Clearly, seL4 on the RPi3 assumed a disabled dcache during its development, but this has now changed, so for this platform something will need to be fixed, such as the above. 2) Or perhaps this is not a U-Boot problem, but should be fixed in seL4. Or in sel4test. For example, is there an option to assume the dcache is already enabled in the configuration? Maybe that should be toggled instead. Or does seL4 *always* assume it is disabled at boot? What about non-RPi3 platforms like other ARM systems? These likely use U-Boot as well, but it's unclear if the cache should be disabled here, too. In this case, the above U-Boot patch is (in theory) wrong, but if that's true, it was always wrong to begin with (as it always disabled the cache prior to ELF loading). If something like this was the case, then the rpi3 configurations (or perhaps some bootinfo code) needs to change. 3) Alternatively, this is just an outright bug in seL4 that should be fixed and U-Boot was previously masking it. (I'm not sure if the proofs cover this one :) 4) Perhaps it should be a mix of both. For example, perhaps the sel4/sel4test code should be changed to assume an already-enabled dcache, or fixed outright. But perhaps a U-Boot patch would still be good to submit upstream: for example, I could submit the above patch upstream, but *remove* the dcache code. This would allow U-Boot users to mark seL4 binaries appropriately for clarity and future compatibility and make U-Boot "officially support" seL4. And in the future, should seL4 need more patches/workarounds/requirements from U-Boot, it would be easier to add and maintain them. --- I'd prefer not to run myself into dead ends trying to get the wrong solution upstream to either seL4 or U-Boot, and it would be great to fix this for users. I'd also like to look into more adventurous stuff in the future (like multicore on the RPi3 which seems unsupported), so any advice is appreciated to get started. Even then: bisection and the patch creation only took an hour, so if it's wrong, not much was lost. -- Regards, Austin - PGP: 4096R/0x91384671

2 3