- Devel - lists.sel4.systems

Re: Ethernet device module for odroidc2
by Todd Carpenter 29 Jan '21

29 Jan '21

I've been following this exchange with some interest, since I also could use an odroidc2 ethernet driver supported by camkes. > From: "Lee, Damon (Data61, Eveleigh)" > The issue is more clear now, the issue lies with the fact that the Ethernet > driver structure layout is different from the expected layout in libethdrivers. Yes, very much so. I had looked at this awhile ago, and the differences seemed daunting. > If aren't in a rush to solve these issues, the team is considering porting over > the AOS Ethernet driver for the C2 over to libethdrivers in the next few days. > Though this would take a few days to do, review, and have it pushed out to > upstream. I would really appreciate a this. Two thumbs up!

1 0

RFC discussion before vote
by Gerwin Klein 27 Jan '21

27 Jan '21

If you have an opinion on any of these RFCs before we vote on them on Fri, please comment on the Jira issue: - Ability to build additional bootloaders inside the seL4 build system https://sel4.atlassian.net/browse/RFC-4 - The seL4 Core Platform https://sel4.atlassian.net/browse/RFC-5 - The seL4 Core https://sel4.atlassian.net/browse/RFC-6 Cheers, Gerwin

1 0

Cross VM Connectors
by ndaughety13＠gmail.com 27 Jan '21

27 Jan '21

**Problem:** In my unsuccessful attempt to complete the cross vm connectors tutorial, [1](https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html), I discovered [2](https://github.com/seL4/sel4-tutorials/issues/49). I am now trying to use [3](https://github.com/seL4/camkes-vm-examples/tree/master/apps) with the new connection module which I thought would expose the dataport device to the VM but the corresponding device does not exist in */dev*. I have confirmed that the module is loaded with *lsmod* in the guest. The original tutorial uses an executable *dataport_init*, which is called from the *camkes_init* script. I assume that this executable would provide the setup for the dataport, however the executable *dataport_init* is not in the *default_buildroot_rootfs.cpio* (note: *consumes_event_init* and *emits_event_init* do exist in the rootfs archive) or as a project anywhere in the project files to be overlayed. Because I could not find this executable in the arm example, I assumed that the connection module aided in the dataport initialization process. **Questions:** 1. Where and how is the dataport device (*/dev/uio0* in this case) exposed/initialized so that read/write can occur? 2. Is there an up-to-date version of the Cross VM Connectors tutorial for x86? I have limited knowledge on this and I may not even be asking the right questions -- therefore any feed back and responses are welcome, thanks. **References:** [1]: https://docs.sel4.systems/Tutorials/camkes-vm-crossvm.html [2]: https://github.com/seL4/sel4-tutorials/issues/49 [3]: https://github.com/seL4/camkes-vm-examples/tree/master/apps

1 0

Cross VM Connectors
by Nathan Daughety 26 Jan '21

26 Jan '21

To whom it may concern, I am looking at https://github.com/seL4/camkes-vm-examples repo, specifically, vm_cross_connectors. Side note, I am just learning CAmkES and seL4 so my knowledge is limited. Looking at the connection kernel module, it looks like it should be initializing the dataport device in /dev but when I run the example, it does not appear that the device has been exposed (no uio0 in /dev) which is what I thought the module did. I confirmed with lsmod that the connection module (connection.ko) is loaded. What do I need to do to expose /dev/uio0 (or any device name that refers to the dataport)? I am looking at seL4HardwareMMIO but I noticed that the example does not use it. If you could point me in the right direction I would really appreciate it. Thanks, Nathan

1 0

Ethernet device module for odroidc2
by ogosinkem＠gmail.com 22 Jan '21

22 Jan '21

Im having trouble with creating a ethernet driver device module for odroid c2. I have tried to create one based on the examples that exists in "/util_libs/libethdrivers/src/plat" to no avail. Looking at it, it does not seem to call the function to intialise the module. This is also evident when I step through the "find_compatible_driver_module" function in the "/camkes-tool/libsel4camkes/src/io.c" file as it does not go in to the loop that, from my understanding, should cycle through a list of modules in order to select an appropriate one. Any suggestions to what I may be missing or any references that would help point me in the right direction will be much appreciated.

3 2

Re: Rust bindings, was: Re: What do you want from the next seL4 Summit?
by Andrew Warkentin 13 Jan '21

13 Jan '21

On 1/12/21, Jimmy Brush <code(a)jimmah.com> wrote: > > Based on these discussions we have started prototyping a > procedurally-generated native rust seL4 library built from a complete > seL4 IDL specification. > > Once we have built this out we intend to share our learnings and > continue to advocate for changes to seL4 and/or upstream work that > improves the experience for everyone building their own language > bindings or dynamic systems on seL4. > Is there any particular reason why you didn't just port your bindings to feL4? It does use the C bindings underneath (through bindgen), but I don't think that's a big problem, as they don't have much room for memory bugs (and UX/RT is not meant to be a "Rust OS" like Redox and Robigalia; it will just be an OS that has a lot of subsystems written in Rust, but there will still be a lot of third-party C code). It was relatively easy for me to port your old bindings and allocators to my fork of feL4. Here is the UX/RT subproject with the bindings and allocators (rust-bitmap, rust-sel4, and sel4-alloc are forked from Robigalia; the rest is from feL4 except for sel4-slabmalloc): https://gitlab.com/uxrt/core-supervisor/fel4/

1 0

What do you want from the next seL4 Summit?
by Gernot Heiser 13 Jan '21

13 Jan '21

Dear seL4 community, A couple months ago we had a successful 3rd seL4 Summit. Despite having to revert to virtual format, it was a very good event, and I’m sure I’m not the only one who enjoyed it. Thanks for the great work to our friends at IAI, Siege Technologies and the Griffiss Institute for the organisation, and DARPA and AFRL for funding the Summit in particular, and seL4 in general for many years. DARPA funding for the seL4 Summits is coming to an end, and, as you know, the seL4 Foundation has been created as the community-driven guardians of seL4. Among others, this means it is time to think about how future summits will look like. For example, much of the funding for seL4 has come from defence budgets, but the technology is equally important for critical civilian systems, and the Summit should reflect this. We would also like to see broadened community participation, maybe a flavour of FODSEM or LCA, while continuing to involve our corporate partners, who are key to financial support and widespread deployment. So we are asking you, the seL4 developer community, what you would like to see at the next summit, in content and format. After this informal community consultation we expect to issue an EOI for organising the next Summit, anticipated timeframe is similar as in the past, Sep–Nov. Please make/discuss suggestions via reply email within a month (and note that I’ll be off-lline for a fair chunk of this). Gernot PS: For those who have missed it, the Summit presentations are still available for about another month to those registered, see https://www.sel4-us.org/summit2020/

4 4

Ethdriver OdroidC2
by Nkem Ogosi 06 Jan '21

06 Jan '21

I have been trying to get an example sel4 programs that demonstrate a network connection, most notably picoserver, to work on an odroid board. Many resources were referenced such as an eth driver and the types of files I needed to get a camkes implementation to work. However, I haven't been very successful. I don't really understand what I am supposed to be included in some of the files or more importantly where to find the information I need to populate the file specifically for odroid as similar files for other boards have other files as dependecies. Sincerly, Nkem

1 0

seL4 YouTube Channel
by Gernot Heiser 31 Dec '20

31 Dec '20

Dear seL4 community, As some of you have already noticed, we now have a YouTube channel run by the seL4 Foundation: https://www.youtube.com/channel/UCIqVY1XFPOPIZ1z2A9TrmMA/about. It presently has two playlists, one with the recordings of the seL4 material from this year’s UNSW Advanced Operating Systems course, and one with seL4 Summit talks from Trustworthy Systems. More to come, enjoy Gernot

2 2

Debugging seL4 for RISC-V
by porter.188＠osu.edu 24 Dec '20

24 Dec '20

I'm building a simple "hello, world" project and running into some bugs. The code works, but the after execution there is an exception. It appears to be in restore_user_context or nearby. Can anyone point out what the problem could be here? user@user-KVM:/mnt/data/sel4hello_manifest/build$ qemu-system-riscv64 --machine spike --nographic --serial mon:stdio --m size=4095M --bios images/hello-image-riscv-spike bbl loader ELF-loader started on (HART 0) (NODES 1) paddr=[80200000..80312d0f] Looking for DTB in CPIO archive...found at 802e5910. Loaded DTB from 802e5910. paddr=[8401e000..8401efff] ELF-loading image 'kernel' paddr=[84000000..8401dfff] vaddr=[ffffffff84000000..ffffffff8401dfff] virt_entry=ffffffff84000000 ELF-loading image 'hello' paddr=[8401f000..84157fff] vaddr=[10000..148fff] virt_entry=14aa4 Jumping to kernel-image entry point... Init local IRQ Initialing PLIC... Booting all finished, dropped to user space hello, world! Warning: using printf before serial is set up. This only works as your printf is backed by seL4_Debug_PutChar() hrintf is bac Caught cap fault in send phase at address 0 while trying to handle: vm fault on code at address 0 with status 0x1 in thread 0xffffffc17fee8200 "rootserver" at address 0 With stack: 0x143ea0: 0x143ec0 0x143ea8: 0x101ea 0x143eb0: 0x143f00 0x143eb8: 0x14b90 0x143ec0: 0x0 0x143ec8: 0x143f30 0x143ed0: 0x143f20 0x143ed8: 0x143f10 0x143ee0: 0x1 0x143ee8: 0x101d6 0x143ef0: 0x144000 0x143ef8: 0x14cbc 0x143f00: 0x0 0x143f08: 0x14a000 0x143f10: 0x20110 0x143f18: 0x0

1 0