- Devel - lists.sel4.systems

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

Re: [seL4] Some questions regarding seL4, U-Boot, and Raspberry Pi 3 patches
by Steven Johnston 20 Sep '17

20 Sep '17

Hi Austin I can confirm your blog post building method works. When attempting to boot from the SD card I receive a Wrong Image Format error: Hit any key to stop autoboot: 0 reading kernel.img 3385548 bytes read in 236 ms (13.7 MiB/s) Wrong Image Format for bootm command ERROR: can't get kernel image! However I was able to successfully network load the image and boot: U-Boot> dhcp 192.168.222.123:kernel.img Waiting for Ethernet connection... done. BOOTP broadcast 1 BOOTP broadcast 2 BOOTP broadcast 3 DHCP client bound to address 192.168.216.122 (1257 ms) Using sms0 device TFTP from server 192.168.222.123; our IP address is 192.168.216.122 Filename 'kernel.img'. Load address: 0x200000 Loading: ... done Bytes transferred = 3385548 (33a8cc hex) U-Boot> bootelf 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... ... Starting test 118: Test all tests ran Test suite passed. 118 tests passed. All is well in the universe Thank you for the push on RPI3! It helped me finish a thread I started months ago and also inadvertently confirmed the serial GPIO on a RPI3 I had been using was not operational. Steve > Date: Mon, 18 Sep 2017 01:49:40 +0000 > From: <Adrian.Danis(a)data61.csiro.au> > To: <aseipp(a)pobox.com>, <devel(a)sel4.systems> > Subject: Re: [seL4] Some questions regarding seL4, U-Boot, and > Raspberry Pi 3 patches > Message-ID: <829193ff-4b95-8d98-c2ad-6e626fdb5e1f(a)data61.csiro.au> > Content-Type: text/plain; charset="utf-8" > > Hi Austin, > > Thanks for the detective work! > > seL4 (or more specifically in this case the elfloader-tool) should be able to tolerate being started with either the cache enabled or disabled. In fact if you look in the mmu code (https://github.com/seL4/seL4_tools/blob/master/elfloader-tool/src/arch-arm/…) you should notice some rough logic of > > if cache enabled > clean cache > disable cache > invalidate cache > > That code only operates on the architected caches though, and not on any platform specific cache controllers, although to my knowledge the rpi3 only has ARM architected caches. I would not be surprised if there were any errors in the dcache macro that walks through the cache levels though, which would be my guess as to where the problem is. > > I will create an issue internally to track this down, but will probably be a little while before anyone has time so if you're interested in fixing the elfloader then you're both welcome and encouraged to. Either way appreciate your efforts thus far. > > Adrian > > On Sun 17-Sep-2017 4:21 AM, Austin Seipp wrote: > 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<http://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/995eab8b5b580b67394312b1621c… > > 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/720caf6c398584658abfa883d4d3… > > 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 > > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems<mailto:Devel@sel4.systems> > https://sel4.systems/lists/listinfo/devel > > >

1 0

Problem making the manual
by Raymond Jennings 18 Sep '17

18 Sep '17

I got an error log when I tried "make" in the manual directory. I got this: ====> Generating doxygen-output/xml/group__GeneralSystemCalls.xml ====> Generating doxygen-output/xml/group__DebuggingSystemCalls.xml ====> Generating doxygen-output/xml/group__BenchmarkingSystemCalls.xml ====> Generating doxygen-output/xml/group__ObjectApiX86.xml ====> Generating doxygen-output/xml/group__ObjectApiArm.xml ====> Generating doxygen-output/xml/group__ObjectApiAarch32.xml ====> Generating doxygen-output/xml/group__ObjectApiAarch64.xml ====> Generating doxygen-output/xml/group__ObjectApiIa32.xml ====> Generating doxygen-output/xml/group__ObjectApiX64.xml ====> Generating generated/GeneralSystemCalls.tex Traceback (most recent call last): File "tools/parse_doxygen_xml.py", line 327, in <module> sys.exit(main()) File "tools/parse_doxygen_xml.py", line 321, in main output_str = generate_general_syscall_doc(args.input, args.level) File "tools/parse_doxygen_xml.py", line 276, in generate_general_syscall_doc details, params, ret = parse_detailed_desc(member, ref_dict) File "tools/parse_doxygen_xml.py", line 157, in parse_detailed_desc ret_type = types_iter.next() AttributeError: 'list_iterator' object has no attribute 'next' make: *** [Makefile:126: generated/GeneralSystemCalls.tex] Error 1

3 3

I need help porting camkes/arm/vmm to new hardware
by Michael DeFrancis 14 Sep '17

14 Sep '17

To the sel4 development community: I am working on porting the sel4 virtual machine from the tk1 to a variety of arm hardware platforms, starting with the Xilinx parts listed below - and I could use some help getting started. I have the following hardware: - Tegra tk1 - Xilinx zynq7000 (zc706) - Xilinx zynq9000 (zcu102) I am successfully ported the 64 bit sel4 kernel to run on the zynq9000, but now I need to port the arm/vmm to run on the zynq9000 hardware as well. I am happy to share these updates with the sel4 community at large. I am uncertain what the best way to do this is - should I submit all of the changes to github, or is there another development repository? I would like to first port the arm/vmm from https://github.com/SEL4PROJ/camkes-arm-vm to the zynq7000<https://github.com/SEL4PROJ/camkes-arm-vm%20to%20the%20zynq7000> for testing, before porting it to the 64 bit zynq9000 platform. Could someone please put me in touch with the author of the arm/vmm that is designed to run on the tegra/tk1 hardware? I have some specific questions to ask regarding platform-specific files. At a high level, I know that I need to change the addresses of peripherals that are passed to my linux kernel (buildroot) for the zynq7000, but I am uncertain where to start. If someone could point me in the right direction, that would be very helpful. Further, if I could talk to a real person about this over the phone, that would be even better. My work phone is (1)(301)294-5263 and my cell phone is (1)(571)271-7278 - feel free to call me and leave me a message. I have not posted to devel(a)sel4.systems<mailto:devel@sel4.systems> previously, though I have been working on the sel4 project for a few months now. I work for Intelligent Automation Inc. in Rockville, Maryland - USA. ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Announcing 7.0.0 release
by Kent.Mcleod＠data61.csiro.au 05 Sep '17

05 Sep '17

= seL4 Version 7.0.0 Release = Announcing the release of seL4 7.0.0 with the following changes: == Changes == * Support for building standalone ia32 kernel added in e7327fa6df3 * ia32: Set sensible defaults for FS and GS selectors in c2f6d48bcf2 * aarch64: Use tpidrro_el0 for IPC buffer instead of tpidr_el0 in ae9fe9b5d18 * More seL4 manual documentation added for aarch64 object invocations * Default NUM_DOMAINS set to 16 for x86-64 standalone builds in baa9798f793 * libsel4: Return seL4_Error in invocation stubs in 8fb06eecff9 ''' This is a source code level breaking change ''' * Add a CMake based build system in 0b73072016e * x86: Increase TCB size for debug builds in 4c8be8f4f91 * libsel4: x86: Remove nested struct declarations in a8d6315eb16 ''' This is a source code level breaking change ''' * Bugfix: x86: Unmap pages when delete non final frame caps in 08b9265563a = Notable changes = * CMake based build system added: Initial experimental support has been added for using CMake for building the kernel and some user level libraries. Currently the only project that takes advantage of this is seL4test when using the cmake.xml manifest in sel4test-manifest. Documentation can be found at: https://github.com/seL4/seL4_tools/tree/master/cmake-tool = Upgrade notes = * This release is not source compatible with previous releases. * seL4 invocations that previously returned long now return seL4_Error which is an enum. Our libraries have already been updated to reflect this change, but in other places where seL4 invocations are used directly, the return types will need to be updated to reflect this change. * On x86 some structs in the Bootinfo have been rearranged. This only affects seL4_VBEModeInfoBlock_t which is used if VESA BIOS Extensions (VBE) information is being used. = Known issues = * One of our tests is non-deterministicly becoming unresponsive on the SMP release build on the Sabre IMX.6 platform, which is a non verified configuration of the kernel. We are working on fixing this problem, and will likely do a point release once it is fixed. = Full changelog = Use `git log 6.0.0..7.0.0` in https://github.com/seL4/seL4 = More details = See the 7.0.0 manual <http://sel4.systems/Info/Docs/seL4-manual-7.0.0.pdf> included in the release or ask on the mailing list!

1 0

UX/RT - an seL4-based OS in the style of QNX and Plan 9
by Andrew Warkentin 03 Sep '17

03 Sep '17

I mentioned this here earlier, but I haven't really gone into a lot of detail about it here. I am planning to write an seL4-based OS similar to QNX and Plan 9 called UX/RT. I am intending it to be both an embedded OS (mostly for the larger types of embedded systems where QNX or Linux would be used, as opposed to simpler ones) as well as a desktop OS. I plan to use as much third-party code as possible to avoid making lots of extra work (likely LKL <https://github.com/lkl/linux> and/or the NetBSD rump kernel for device drivers, disk filesystems, and the network stack; a libc based on musl; and basic commands forked from those of FreeBSD). UX/RT will be a pure Unix-like system with no concept of "personality-neutral" services, and the root server will implement a subset of the Unix API directly (as in QNX, although the root server will be completely separate from the kernel of course, unlike that of QNX). However, there will be a Linux compatibility layer implemented with libraries and filesystem servers. I am going to avoid C for new code as much as possible for security, preferring Rust for anything performance-critical. The main concept behind the design will be to take "everything is a file" as far as it possibly can go. Nearly all resources in the system will appear in the filesystem, even things like process memory (kernel memory and the interface to the root server will be among the few non-files in the system, although the API of the root server will be implemented with an anonymous FD internally). The filesystem will be a combination of a thin layer on top of L4 IPC with read() and write() calling L4 IPC directly (short transfers will probably be sent entirely in message registers and long ones sent by using shared pages), and a memory mapping layer. The VFS will implement the name service and memory mapping parts of the filesystem; read() and write() will bypass the VFS layer entirely and will use seL4 IPC to communicate directly with the other thread. There will also be APIs that expose message registers and shared pages more directly although they will do it in a way that interoperates with read() and write() (these will mostly be used with a new "message-special" file type that preserves message boundaries but otherwise acts like a normal byte stream if used with read() or write()). No provisions will be made for use of IPC or capabilities outside the filesystem. Security will be based on an ACL-per-process model, where the root server will have an in-memory list of files for each process specifying which files it is allowed to access, as opposed to a hierarchical pure-capability model like other L4-based systems (a pure capability model seems like it would be a poor fit for a pure Unix-like system). It will be possible to either specify rwx permission bits explicitly or use the mode from the filesystem; it will also be possible for an ACL entry to specify all files under a particular directory. File descriptors will be implemented as groups of capabilities, and the root server will hand them out when a process successfully opens a file (unlike in QNX there will be no need for individual filesystem servers to check whether the client process is authorized to access a file). There will be an ACL management server that will persistently associate permissions with programs, and it will also be possible for sufficiently privileged processes to dynamically modify the ACLs of other processes. I currently have a bootloader, some basic infrastructure for building boot ISO images, and a patch for seL4 to support QNX-like XIP single-image boot using a variant of Multiboot2. I can build a boot ISO with a system image containing only the kernel, but it crashes with a triple fault somewhere in either the bootloader or the kernel (I haven't yet tried to track down where it's occurring). Once I move on to user mode code, I'm going to be using the Rust libraries from Robigalia as a basis for the root server (higher-level Rust-based components will use a normal Unix build of the Rust standard library instead). The code I have so far can be found at <https://gitlab.com/uxrt> for UX/RT itself and <https://gitlab.com/uxrt-bos> for the bootloader. I have some (long and not particularly well-organized) notes on my plans for UX/RT's architecture at <https://gitlab.com/uxrt/uxrt-toplevel/blob/master/architecture_notes>. Anybody is more than welcome to contribute if they want.

2 2

VGA buffer as stdout
by Michal Podhradsky 31 Aug '17

31 Aug '17

Hello, I have a question about standard output. I have a camkes component than can write into text-mode VGA buffer (basically it follows this simple example http://wiki.osdev.org/Bare_Bones#Writing_a_kernel_in_C ) but I would like to be able to redirect the kernel messages during startup to be printed on screen using VGA buffer. Once another component (either Linux in a VM, or some other camkes app) will initialize, it will be able to take control over the screen output (and for example show login window etc). My questions is - is this possible with seL4? And if so, what would it entail? I guess in the minimal version, I would have to provide a different implementation of seL4_DebugPutChar, is that correct? The VGA standard seems to define the buffer to be at 0xB8000, so it should be consistent between x86 platforms. Regards Michal

5 11

benchmark - idle utilization
by Alexander Boettcher 31 Aug '17

31 Aug '17

Hello, we use the seL4 benchmark interface to feed Genode's trace infrastructure with information about the CPU utilization of threads and of idle times. In general the integration was reasonable straightforward. One minor point we had. It seems that the idle time of a CPU can only be requested by a thread running on the vary same CPU. Requesting the CPU idle times of a remote CPU (the calling thread is on another CPU) is not supported, right ? In principle we may start on each CPU a thread just for the sake of requesting the idle utilization time, which however looks a bit of overkill. We "kind of" circumvent the issue for us by changing the syscall handling in the kernel in that regard, that the CPU number of the requested target thread is taken instead that of the caller thread, e.g. like this: --- a/src/benchmark/benchmark_utilisation.c +++ b/src/benchmark/benchmark_utilisation.c @@ -36,6 +36,11 @@ void benchmark_track_utilisation_dump(void) tcb = TCB_PTR(cap_thread_cap_get_capTCBPtr(lu_ret.cap)); buffer[BENCHMARK_TCB_UTILISATION] = tcb->benchmark.utilisation; /* Requested thread utilisation */ +#if CONFIG_MAX_NUM_NODES > 1 + if (tcb->tcbAffinity < ksNumCPUs) + buffer[BENCHMARK_IDLE_UTILISATION] = NODE_STATE_ON_CORE(ksIdleThread, tcb->tcbAffinity)->benchmark.utilisation; /* Idle thread utilisation */ + else +#endif buffer[BENCHMARK_IDLE_UTILISATION] = NODE_STATE(ksIdleThread)->benchmark.utilisation; /* Idle thread utilisation */ #ifdef CONFIG_ARM_ENABLE_PMU_OVERFLOW_INTERRUPT With this change, we still have to create a thread on every CPU (since we need a capability for the syscall), but at least the threads must not be running actively. Does this change (the patch) make sense to you and is it worthwhile to adjust in general on your side - or would you advise/envision another approach/direction ? (like specifying the cpu number for the idle times directly via the syscall or having a explicit syscall just for cpu idle times [but there are no specific thread idle capabilities as syscall parameter] etc.) Another question: Currently it seems that no idle CPU times are provided, as long as no user thread is actively running on that specific CPU. We can handle it, no problem in general - however we would have to adjust generic code (which runs on 8 different kernels) specifically 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.-Ing. Norman Feske, Christian Helmuth

2 3

Compile errors for Beaglebone Black
by Todd_Peterson＠mgtsciences.com 31 Aug '17

31 Aug '17

Hi, I am trying to compile seL4 for the BBB. I am getting the following errors when it gets to timer_service. I am following the instructions at https://github.com/seL4/refos-manifest. I got past another compile error by adding a typedef to device_timer.h for pstimer_t. Any help is appreciated. // tfp, added to avoid compiler error typedef uint32_t pstimer_t; [apps/timer_server] building... [HEADERS] [STAGE] autoconf.h [CC] src/state.o In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:22:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h: In function 'data_open_map': /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client_helper.h:95:69: warning: passing argument 6 o f 'data_open' from incompatible pointer type [-Wincompatible-pointer-types] d.dataspace = data_open(session, name, flags, mode, dspaceSize, &errnoRetVal); ^ In file included from /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-util/device_io.h:21:0, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.h:21, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.h:27, from /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/state.c:24: /home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/include/refos-rpc/data_client.h:72:11: note: expected 'int ** (*)()' but ar gument is of type 'int *' seL4_CPtr data_open(seL4_CPtr session, char* name, int flags, int mode, int size, int* errno); ^ [CC] src/device_timer.o /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_handle_irq': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:146:5: warning: implicit declaration of function 'timer _handle_irq' [-Wimplicit-function-declaration] timer_handle_irq(s->timerDev, irq); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_init': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:239:5: error: unknown type name 'timer_config_t' timer_config_t config; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: error: 'dm_timer_paddrs' undeclared (first use in this function) config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TIMER_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:240:52: note: each undeclared identifier is reported on ly once for each function it appears in /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:242:18: error: 'dm_timer_irqs' undeclared (first use in this function) config.irq = dm_timer_irqs[TIMER_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:243:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:19: warning: implicit declaration of function 'ps_g et_timer' [-Wimplicit-function-declaration] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:248:17: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->timerDev = ps_get_timer(TIMER_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:250:11: error: request for member 'vaddr' in something not a structure or union config.vaddr = ps_io_map(&io->opsIO.io_mapper, dm_timer_paddrs[TICK_ID], ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:252:11: error: request for member 'irq' in something no t a structure or union config.irq = dm_timer_irqs[TICK_ID]; ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:253:16: error: request for member 'vaddr' in something not a structure or union if (!config.vaddr) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:258:16: warning: assignment makes pointer from integer without a cast [-Wint-conversion] s->tickDev = ps_get_timer(TICK_ID, &config); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:273:41: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->timerDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:274:19: warning: implicit declaration of function 'time r_get_nth_irq' [-Wimplicit-function-declaration] int irq = timer_get_nth_irq(s->timerDev, i); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:282:44: error: request for member 'properties' in somet hing not a structure or union for (uint32_t i = 0; i < s->tickDev->properties.irqs; i++) { ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:289:21: warning: implicit declaration of function 'time r_start' [-Wimplicit-function-declaration] int error = timer_start(s->tickDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:310:13: warning: implicit declaration of function 'time r_periodic' [-Wimplicit-function-declaration] error = timer_periodic(s->timerDev, TIMER_PERIODIC_MAX); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c: In function 'device_timer_get_time': /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:344:21: warning: implicit declaration of function 'time r_get_time' [-Wimplicit-function-declaration] uint64_t time = timer_get_time(s->timerDev); ^ /home/users/staff/tpeterson/sel4/beagle/apps/timer_server/src/device_timer.c:345:21: error: request for member 'properties' in somet hing not a structure or union if (!s->timerDev->properties.upcounter) { ^ make[1]: *** [/home/users/staff/tpeterson/sel4/beagle/stage/arm/am335x/common/common.mk:265: src/device_timer.o] Error 1 make: *** [tools/common/project.mk:331: timer_server] Error 2 Todd Peterson Chief Embedded Systems Engineer Management Sciences, Inc. 6022 Constitution Ave NE Albuquerque, NM 87144 505-255-8611 (office) 505-205-7057 (cell) This email message and any attachments are for the sole use of the intended recipient(s) and may contain proprietary and/or confidential information which may be privileged or otherwise protected from disclosure. Any unauthorized review, use, disclosure or distribution is prohibited. If you are not the intended recipient(s), please contact the sender by reply email and destroy the original message and any copies of the message as well as any attachments to the original message.

1 0