- Devel - lists.sel4.systems

seL4 Linux guest mmap() crashes the VM
by Hugo V.C. 02 Jul '21

02 Jul '21

Hi, my seL4 Linux VM box just crashed when trying to access a memory address. Basically I simply wanted to use "devmem" tool to just print the content of a specific address in memory and looked like seL4 was unable to handle the guest OS mmap() correctly. Below the console log: # ls /proc/283/maps /proc/283/maps # cat /proc/283/maps 00400000-00532000 r-xp 00000000 00:02 6023 /bin/lighttpd 00541000-00543000 r--p 00131000 00:02 6023 /bin/lighttpd 00543000-00546000 rw-p 00133000 00:02 6023 /bin/lighttpd 00546000-0054d000 rw-p 00000000 00:00 0 0bd0b000-0bd2d000 rw-p 00000000 00:00 0 [heap] 0bd2d000-0bd91000 rw-p 00000000 00:00 0 [heap] ffff82084000-ffff82085000 r--p 00000000 00:00 0 [vvar] ffff82085000-ffff82086000 r-xp 00000000 00:00 0 [vdso] ffffe6c58000-ffffe6c79000 rw-p 00000000 00:00 0 [stack] # devmem 0xffffe6c58000 8 _utspace_split_alloc@split.c:266 Failed to find any untyped capable of creating an object at address 0xffffe6c58000 map_page@mapping.c:68 Failed to map page at address 0xffffe6c58000 with cap 396187, error: 1 sel4utils_map_page_pd@vspace.c:153 Error mapping pages, bailing: 1 map_vm_memory_reservation@guest_memory.c:477 Failed to map address 0xe6c58000 into guest vm vspace vm_map_reservation@guest_memory.c:510 Failed to map vm reservation: Error when mapping into VM's vspace -------- Pagefault from [Linux]: read fault @ PC: 0x414c38 IPA: 0xffffe6c58000, FSR: 0x93020004 Context: x0: 0xffff9cfe6000 x1: 0x0 x2: 0x0 x3: 0x1 x4: 0x3 x5: 0xffffe6c58000 x6: 0x5 x7: 0x20 x8: 0xde x9: 0xffffe539cf54 x10: 0xffff9cfe8050 x11: 0x1 x12: 0x436 pc: 0x414c38 x14: 0xffffffff sp: 0xffffe539bb70 spsr: 0x60000000 x13: 0x1 x15: 0x3 x16: 0xffff9cf486c8 x17: 0x4c3870 x18: 0x0 x19: 0x8 x20: 0x0 x21: 0x4c3000 x22: 0xffffe539bd98 x23: 0xffffe6c58000 x24: 0x0 x25: 0x0 x26: 0x0 x27: 0x0 x28: 0x0 x29: 0xffffe539bc60 x30: 0x414bac m-------- main_continued@main.c:1134 Failed to run VM Halting... My three concerns here are: 1) Why this guest mmap() is crashing the VM? Memory address is valid (just guest user space process stack). 2) Is it possible to have some kind of "dump and reboot VM" when a VM and/or guest OS crashes? 3) Are there any plans to formally verify the seL4's VM camkes code? Thank you!

2 6

Camkes SerialServer and util_libs/libplatsupport with ODROID-C4
by Robert Reid 01 Jul '21

01 Jul '21

Hi everyone Summary - trying to get util_libs/libplatsupport going for a HardKernel ODROID-C4, using the camkes serialserver_polling app - but not having any luck with mapping the UART. I'd welcome any explanations of what you think is happening here. The background and my progress follows. I thought I'd dive into the seL4 world and do some experimenting. I thought a good place to start would be the UNSW AOS project (17 years after I first did it) - but with no more ODROID-C2, got a hold of an ODROID-C4 and figured that would be a good project in itself (and well timed with a Sydney lockdown). So - good news: The peripheral devices we need are all very similar to a C2, so by getting a new DTS file and updating a few addresses it starts off fairly happily. sel4-test builds and runs (All is well...); so does the camkes adder app; and with some mods to provide enough slots (maybe because it has 4GB rather than 2GB) I have got the AOS milestone 0 stub to run (including the uart initialisation). (More work to actually finish m0 and keep going, but a job for later) But then: I moved onto the util_libs / libplatsupport project to try and port over as much of the device settings as possible; and using the camkes app serialserver_polling, under the hood using SerialServer, I can't get the uart to initialiise (or more strictly can't get the uart address to map). chardev_map / ps_io_map fails, returning a vaddr of 0. I've added a bunch of debug prints to the process; and for comparison also run it on QEMU emulating a Sabre board. On odroidc4 hardware: ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[95e000..d5710f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at a86de8. Loaded DTB from a86de8. paddr=[23f000..24afff] ELF-loading image 'kernel' to 0 paddr=[0..23efff] vaddr=[ffffff8000000000..ffffff800023efff] virt_entry=ffffff8000000000 ELF-loading image 'capdl-loader' to 24b000 paddr=[24b000..563fff] vaddr=[400000..718fff] virt_entry=408e48 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space pre_init@serial.c:501 About to init port, io_ops=0x487cf0 ps_cdev_init@chardev.c:46 About to init_fn 3 ps_cdev_init@chardev.c:47 dev_defn[3].paddr: 0xff803000, size 1000 uart_init@serial.c:51 about to chardev_map: dev=0x473948, defn->id=3, defn->padd r=0xff803000 chardev_map@chardev.h:26 ops->io_mapper=0x487be0 &(ops->io_mapper)=0x442728 dev- >paddr=0xff803000 dev->size=0x1000 uart_init@serial.c:56 chardev_map mapped page_vaddr 0 plat_pre_init@plat.c:64 Failed to initialise character device plat_pre_init@plat.c:65 PS_SERIAL_DEFAULT: 3 On Sabre QEMU: ./simulate: qemu-system-arm -machine sabrelite -nographic -serial null -serial mon:stdio -m size=1024M -kernel images/capdl-loader-image- arm-imx6 ELF-loader started on CPU: ARM Ltd. Cortex-A9 r0p0 paddr=[106fc000..10aa98e3] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 107fe33c. Loaded DTB from 107fe33c. paddr=[1003d000..10047fff] ELF-loading image 'kernel' to 10000000 paddr=[10000000..1003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ELF-loading image 'capdl-loader' to 10048000 paddr=[10048000..10300fff] vaddr=[10000..2c8fff] virt_entry=187f8 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Warning: Could not infer GIC interrupt target ID, assuming 0. Booting all finished, dropped to user space pre_init@serial.c:501 About to init port, io_ops=0x69cf0 ps_cdev_init@chardev.c:45 About to init_fn 1 ps_cdev_init@chardev.c:46 dev_defn[1].paddr: 0x21e8000, size 1000 uart_init@serial.c:224 about to chardev_map: dev=0x7f8c8, defn->id=1, defn->paddr=0x21e8000 chardev_map@chardev.h:26 ops->io_mapper=0x69cf0 &(ops->io_mapper)=0x1f328 dev->paddr=0x1f654 dev->size=0x4ebc4 uart_init@serial.c:226 chardev_map mapped vaddr 0xbb000 pollcli: Hello Serial Server! pollcli: abc This has me confused - it's good it works, but I can't follow in the flow how the paddr gets changed from the value supplied to chardev_map (ie 0x21e80000 becomes 0x1f654), yet in that case it works. Or is it a complication of using QEMU? A similar kind of test with AOS on odroidc4 - particularly the success of "*uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000*" ## Starting application at 0x01080000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A55 r1p0 paddr=[88a000..c2b10f] No DTB passed in from boot loader. Looking for DTB in CPIO archive...found at 9f3068. Loaded DTB from 9f3068. paddr=[247000..252fff] ELF-loading image 'kernel' to 0 paddr=[0..246fff] vaddr=[ffffff8000000000..ffffff8000246fff] virt_entry=ffffff8000000000 ELF-loading image 'sos' to 253000 paddr=[253000..48cfff] vaddr=[400000..639fff] virt_entry=4172e0 Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Booting all finished, dropped to user space SOS Starting... <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> <<seL4(CPU 0) [handleInterruptEntry/52 T0xffffff803fff8400 "SOS:root" @400630]: Spurious interrupt!>> uart_init@uart.c:35 Mapped uart paddr:ff803000 size:1000 vaddr:b0000000 SOS Started! test_cspace@tests.c:59 Test cspace run_tests@tests.c:174 Root CSpace test passed! test_cspace@tests.c:59 Test cspace run_tests@tests.c:182 Single level cspace test passed! test_cspace@tests.c:59 Test cspace cspace_alloc_slot@cspace.c:335 Cspace is full! run_tests@tests.c:195 Double level cspace test passed! run_tests@tests.c:199 DMA test passed! run_tests@tests.c:203 Frame table test passed! Network init dwmac.b0002000 Waiting for PHY auto negotiation to complete........ done Speed: 1000, full duplex Protocol ethernet registered (layer: 2). Protocol ipv4 registered (layer: 3). Protocol ipv6 registered (layer: 3). Protocol icmp4 registered (layer: 4). Protocol icmp6 registered (layer: 4). Protocol igmp registered (layer: 4). Protocol udp registered (layer: 4). Protocol tcp registered (layer: 4). Assigned ipv4 0.0.0.0 to device sos picotcp DHCP client: update link Assigned ipv4 192.168.200.125 to device sos picotcp DHCP client: renewal time (T1) 43200 DHCP client: rebinding time (T2) 75600 DHCP client: lease time 86400 DHCP client: netmask 255.255.255.0 DHCP client: gateway 192.168.200.4 Timer init Start first process Starting ttytest at 0x4001c8 SOS entering syscall loop aos: Error attempting syscall 29 task: Hello world, I'm tty_test! handle_syscall@main.c:128 Unknown syscall 1 <<seL4(CPU 0) [receiveIPC/148 T0xffffff803fff8400 "SOS:root" @407a48]: Reply obj ect already has unexecuted reply!>> In this case it has worked, sos_map_device works as expected (although the spurious interrupts are another task to figure out). But trying to understand what's really going on underneath ps_io_map and ultimately why libplatsupport won't work for me has got me confused. Any ideas would be appreciated. Regards Rob

2 4

camkes-vm-linux kernel example
by Hugo V.C. 01 Jul '21

01 Jul '21

Hi, just a simple question: why this tutorial: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html shows this output: Welcome to Buildroot buildroot login: root Password: # grep poke /proc/devices # figure out the major number of our driver 244 poke # mknod /dev/poke c 244 0 # create the special file # echo > /dev/poke # write to the file [ 57.389643] hi -sh: write error: Bad address # the shell complains, but our module is being invoked! I'm not getting the shell complain error, just this: # grep poke /proc/devices 247 poke # mknod /dev/poke c 247 0 # echo > /dev/poke [ 138.946905] TOC TOC NEO... # FYI: my kernel is a custom compiled one but same version as the pre-compiled you provide: # uname -a Linux buildroot 4.9.189 #4 SMP Thu Jun 24 00:16:49 CEST 2021 aarch64 GNU/Linux Any hint? Cheers,

2 2

How will drivers work?
by Isaac Beckett 01 Jul '21

01 Jul '21

Hello! Operating system noob here, I understand that in most mainstream operating systems (Linux, BSDs, MacOS, Windows) drivers are part of the kernel. And in micro kernel operating systems like Minix and seL4, drivers are part of user space. But Minix is a lot closer to a traditional POSIX kernel, and seems to implement some of that (IE posix threads, IPC) in the kernel, which makes the environment for a driver programmer a bit more familiar. How do drivers work in seL4, then? How does a driver obtain permission for hardware access from the kernel? I imagine it works with a capability delegated by the root task, but how do you solve chicken and the egg type problems, like loading driver code, without driver code already loaded? Is it an initramfs like Linux/Unix? Also, what if seL4 is being used _as_ the firmware/bootloader? Obviously it can load the seL4 kernel and user space OS components from a file system to put them in the booting OS’ memory, but how does it load drivers for itself? I’m assuming there’s some low level platform specific code, but is that code verified or part of the proofs?

2 1

Re: Tutorial Problem
by Peter Chubb 30 Jun '21

30 Jun '21

>>>>> "Michael" == Michael Neises <neisesmichael(a)gmail.com> writes: Michael> Peter, When I try to remove vme from the -cpu line, I get the Michael> following error at simulation time: OK, so you need nested virtualisation. That's not supported in code-translation mode, only when you're using the KVM kernel module. The message you got was about the simulated CPU, not your host. If you can enable KVM, qemu will pass through your host to the simulation. Looks like you have the kernel packages installed, now you need to make sure that: 1, The version of qemu you're using supports KVM, and 2. you have permissions to use KVM. The first is easy. On Debian-derived systems (debian, ubuntu, mint, etc) sudo apt install qemu-kvm should do the trick. Similarly sudo yum install qemu-kvm on Redhat-derived systems. The second is a little harder. Do ls -l /dev/kvm You'll see something like crw-rw----+ 1 root kvm 10, 232 Jun 30 09:13 /dev/kvm if kvm is installed. The second username (in this case, 'kvm') is the group you need to be in. Do sudo useradd your-login kvm (replacing 'kvm' with the actual group /dev/kvm is in, and 'your-login' with you local login name.) qemu-system-x86_84 -enable-kvm should then work. Peter C -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW

1 0

Tutorial Problem
by Michael Neises 30 Jun '21

30 Jun '21

Hello everyone, The tutorials provided here are failing to build for me: https://github.com/seL4/sel4-tutorials Here are the steps to reproduce the errors: git clone git@github.com:seL4/seL4-CAmkES-L4v-dockerfiles.git && git clone git@github.com:seL4/sel4-tutorials.git && make -C ./seL4-CAmkES-L4v-dockerfiles user HOST_DIR=$(pwd)\ followed by cd sel4-tutorials && mkdir build && cd build && ../init.py --plat pc99 --tut camkes-vm-linux Then I am met with the error: ERROR:root:Parent directory is not tutorials root directory which I can fix by changing this line to read "init.py": https://github.com/seL4/sel4-tutorials/blob/d040028999b83c6af2309785f746810… Trying again after this edit, I meet the following errors: loading initial cache file ../projects/sel4-tutorials/settings.cmake CMake Error: Error processing file: ../projects/sel4-tutorials/settings.cmake CMake Error: The source directory "/host/sel4-tutorials/build" does not appear to contain CMakeLists.txt. Specify --help for usage, or press the help button on the CMake GUI. Traceback (most recent call last): File "../init.py", line 90, in <module> sys.exit(main()) File "../init.py", line 78, in main result = common.init_directories(args.plat, args.tut, args.solution, File "/host/sel4-tutorials/common.py", line 101, in init_directories return _init_build_directory(config, initialised, build_directory, tute_directory, output, config_dict=config_dict) File "/host/sel4-tutorials/common.py", line 69, in _init_build_directory return sh.cmake(args + [tute_directory], _cwd=directory, _out=output, _err=output) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 1520, in __call__ return RunningCommand(cmd, call_args, stdin, stdout, stderr) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 784, in __init__ self.wait() File "/usr/local/lib/python3.8/dist-packages/sh.py", line 841, in wait self.handle_command_exit_code(exit_code) File "/usr/local/lib/python3.8/dist-packages/sh.py", line 865, in handle_command_exit_code raise exc sh.ErrorReturnCode_1: RAN: /usr/bin/cmake -G Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DFORCE_IOMMU=ON -DTUTORIAL_DIR=build -C ../projects/sel4-tutorials/settings.cmake /host/sel4-tutorials/build STDOUT: STDERR: Either I'm missing something obvious or these instructions have fallen out of date. In any case I would be grateful for any advice. Best, Michael Neises

4 5

How to avoid seL4 passing packets to Linux VM guest
by Hugo V.C. 25 Jun '21

25 Jun '21

Hi, I wonder how to have seL4 host not passing network frames to Linux VM guest. I mean, I would like to have seL4 dealing with TCP/IP and processing packets at the host level but then I want to use a custom communication channel with the Linux guest. So, the very first step would be to stop forwarding network frames to the guest. Any hint where I can start experimenting with this? Cheers,

2 4

Some small details in kernel code and docs
by Mark Jones 24 Jun '21

24 Jun '21

Hi All, Here are a few minor details/questions about the kernel code & documentation. (I've confirmed that these are present in the new seL4-12.1.0 release.) 1) kernel/include/arch/x86/arch/32/mode/machine.h has the following definition (some code elided): static inline word_t FORCE_INLINE x86_read_fs_base_impl(void) { word_t base = 0; base &= ...; base &= ...; base &= ...; return base; } I'm pretty sure that the three &= operators here should be |= or else the result is always going to be zero. The same issue occurs in x86_read_gs_base_impl in the same file. Some follow-up questions: Can anyone say if this would have been detected if the PC99 (32-bit) platform had been verified? More generally, where can I find information about how ia32 segment registers are handled by the kernel? Why aren't they just stored/restored like other user-level registers on kernel entry/exit? Is there something that prevents user-level changes in the ES register, for example, from being observed in other threads? 2) A CNodeRotate will generate a FailedLookup error if the pivot slot either doesn't exist or contains a null capability. But, in the first case the "lookup failed for a source capability" field in the error message is 1, while in the second it is 0. Hardly a serious problem, but this does seem inconsistent. Is this intentional, or a mistake in the specification that has been carried over to the implementation? 3) Section "3.4 Lookup Failure Description" of the manual describes how capability lookup errors are represented in an IPC buffer. But it seems the layout information is incorrect. For example, Section 3.4.2 says that "Offset + 0" will contain seL4_MissingCapability while the number of bits left will be at "Offset + seL4_CapFault_BitsLeft", which is probably supposed to be equivalent to "Offset + 1". But, based on kernel/libsel4/include/sel4/shared_types.h, it would seem that this gives "Offset + 4". Sections 3.4.3 and 3.4.4 have similar problems. 4) On https://docs.sel4.systems/GettingStarted, in the section labeled "Fetching, Configuring and Building seL4test", there are missing line breaks between the commands in the text boxes for Steps 1 and 2, and there are some tags in the text box for Step 4 that probably should not be displayed. Best wishes, and thanks for any feedback! Mark

6 7

CAmkES ARM VM: SATA Passthrough
by Olof Holmberg 21 Jun '21

21 Jun '21

Hi, I ran into the issue of not being able to fit the whole rootfs in RAM (using a qemu-arm-virt device). Therefore I opted for booting the initramfs instead and from there switch root to the proper file system. The booting of the initramfs works fine but the /dev/sda device is not visible to the guest. For x86 (according to these instructions: https://docs.sel4.systems/projects/camkes-vm/) this seems to be done by passing through access to the SATA controller. But since the x86 device configuration is different to the ARM device configuration it requires a different config than the one shown in the instructions. I was wondering how you achieve this SATA passthrough for a ARM VM or if there are any tutorials, other projects or examples that shows how it is done? Best regards, Olof

2 1

Re: Devel Digest, Vol 104, Issue 8
by jonas.cl＠protonmail.com 14 Jun '21

14 Jun '21

Sent from ProtonMail, Swiss-based encrypted email. ‐‐‐‐‐‐‐ Original Message ‐‐‐‐‐‐‐ On Monday, June 14, 2021 4:00 AM, <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via email, send a message with subject or > body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > Today's Topics: > > 1. sel4 camkes stability (mrshafiei(a)aut.ac.ir) > 2. sel4 camkes stability mechanisms for crash handling and thread failure > (mrshafiei(a)aut.ac.ir) > > > Message: 1 > Date: Sun, 13 Jun 2021 10:47:43 +0430 > From: mrshafiei(a)aut.ac.ir > Subject: [seL4] sel4 camkes stability > To: Siwei.Zhuang(a)data61.csiro.au, devel(a)sel4.systems > Message-ID: 1623565063345060169(a)aut.ac.ir > > Content-Type: text/plain; charset="utf-8" > > Hi Siwei. > I have some problem with my sel4 project, as you know, I'm work on my master project and develop a project on sel4 (camkes) which provide filesystem interfaces, and use ethernet and lwip network stack. This section is ok but sometimes my project crashed and my threads failed. I think that you should start by getting core files from all the crashes. This will point to why the threads fail. I haven't done that for projects running seL4 on hardware, but it is easy to connect gdb to an image running in qemu. I'm sure someone here can point you in the right direction on how to catch core-dump files from hardware. You can of course also implement a watchdog, but start with solving the crashes. /Jonas Claesson > In another words, I wrote my > components and its work correctly but some times (rarely) my threads > crashes and I couldn't find problem. So i decide to use a service like > watch dog timer for garanty all of threads work and when one of therm > failed or crashed, this mechanism detect it and start another thread or > reset the system. > A simple solution can implement is use some thread controlling > (implement WDT in user mode). But I want to know is there in camkes or > sel4 any mechanism for this need? a mechanism for garanti stability and > system availability? > can any body help me? > Is there anybody which confront with this need? > > -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > This email was Anti Virus checked by Security Gateway. > > ------------------------------------------------------- > > Message: 2 > Date: Sun, 13 Jun 2021 10:50:18 +0430 > From: mrshafiei(a)aut.ac.ir > Subject: [seL4] sel4 camkes stability mechanisms for crash handling > and thread failure > To: devel(a)sel4.systems > Message-ID: 1623565218534753237(a)aut.ac.ir > > Content-Type: text/plain; charset="utf-8" > > Hi there. > I have some problem with my sel4 project, as > you know, I'm work on my master project and develop a project on sel4 > (camkes) which provide filesystem interfaces, and use ethernet and lwip > network stack. This section is ok but sometimes my project crashed and > my threads failed. > In another words, I wrote my > components and its work correctly but some times (rarely) my threads > crashes and I couldn't find problem. So i decide to use a service like > watch dog timer for garanty all of threads work and when one of therm > failed or crashed, this mechanism detect it and start another thread or > reset the system. > A simple solution can implement is use some thread controlling > (implement WDT in user mode). But I want to know is there in camkes or > sel4 any mechanism for this need? a mechanism for garanti stability and > system availability? > can any body help me? > Is there anybody which confront with this need? > > -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > This email was Anti Virus checked by Security Gateway. > > ------------------------------------------------------- > > Subject: Digest Footer > > Devel mailing list -- devel(a)sel4.systems > To unsubscribe send an email to devel-leave(a)sel4.systems > > > --------------------------------------------------------------------------------------------------- > > End of Devel Digest, Vol 104, Issue 8

1 0

MMC wait after second command in intialization with mmc_init
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi there . i'm work on mmc storage with sel4. i wrote a simple app that use mmc an here is that : ////////////////////////////////////////////////////////////////////// static int count = 0; ps_io_ops_t io_ops = {0}; struct netif* net_if; mmc_card_t mmc_card = 0; sdio_host_dev_t sdio_host_dev; int mmc_found = 0; void mmc_irq_handle(ps_irq_t* irq) { printf("mmc irq handle .... \n"); if(!mmc_found){ mmc_irq_acknowledge(irq); // printf("mmc not found yet :)\n"); sdio_host_dev.handle_irq(&sdio_host_dev,irq->irq.number); return ; } mmc_irq_acknowledge(irq); mmc_handle_irq(mmc_card,irq->irq.number); } int run(void) { notification = timer_notification(); int err = camkes_io_ops(&io_ops); if (err != 0) { ZF_LOGF("Can not init ops : %d\n", err); }; printf("initialize sdhc1 ...\n"); err = sdio_init(SDHC1, &io_ops, &sdio_host_dev); // while card not present check while(sdio_host_dev.reset(&sdio_host_dev) == -1){ delay(1000); } printf("before mmc_init\n"); mmc_init(&sdio_host_dev, &io_ops, &mmc_card); mmc_found = 1; printf("after mmc_init\n"); if (!err) { printf("SDHC1 inited successfully.\n"); } else { printf("SDHC1 initizatino failed!: %d", err); } while (true) { printf(".\n"); delay(1000); } return 0; //////////////////////////////////////////////// its work but in mmc_init after going to mmc_reset , first command sent but in second command (ie MMC_SEND_EXT_CSD ) wait for ever... can any body help me? best regards -- This email was Anti Virus checked by Security Gateway.

2 1

lighttpd as non root user in sel4webserver demo
by Hugo V.C. 13 Jun '21

13 Jun '21

Hi, I was trying to run lighttpd as non root user in " https://github.com/seL4/sel4webserver" demo and realized it didn't allowed me no matter if I configured /etc/passwd, /etc/group and /etc/shadow and /etc/lighttpd.conf correctly. As I don't have debug tools in this Linux VM to look what's going on I decided to directly modify the lighttpd source code to bypass some native code of the web server and hardcode my own user/group. Looks like it works and I now have lighttpd running with it's own user: # ps -ef PID USER COMMAND 1 root init (...) 60 root /sbin/syslogd -n 64 root /sbin/klogd -n 108 lighttpd lighttpd -f /etc/lighttpd.conf 110 root /sbin/getty -L tty1 0 vt100 (...) I also changed the ownership of the /run/site tree to be owned by root. The changes I did in the source code are basically to bypass "getgrnam()" and "getpwnam()" syscalls as I suspect for some reason (musl libc guilty??) and manually set the setgid value before the chroot. I know this is a very dirty hack... but it works for me. My question is if anyone thinks this can be useful to others I can create a pull request with the changes. I think that even if this is a demo, it is not nice to run lighttpd as root, even for a static website. Of course the "right"/elegant way of solving this would be not to change lighttpd source code... but I was unable to do that way. Let me know your opinions. Cheers,

1 0

Camkes-vm-linux on
by Hugo V.C. 12 Jun '21

12 Jun '21

Hi, I'm trying the camkes-vm-linux tutorial and can't run it in qemu despite having nested guests enabled: hugo@dev:~/seL4/sel4-tutorials-manifest/camkes-vm-linux_build$ cat /sys/module/kvm_intel/parameters/nested Y --------- hugo@dev:~/seL4/sel4-tutorials-manifest/camkes-vm-linux_build$ sudo ./simulate --machine q35,accel=kvm,kernel-irqchip=split --mem-size 2G --extra-cpu-opts "+vmx" --extra-qemu-args="-enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0" ./simulate: qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu Nehalem,+vme,+pdpe1gb,-xsave,-xsaveopt,-xsavec,-fsgsbase,-invpcid,+syscall,+lm,enforce,+vmx -nographic -serial mon:stdio -m size=2G -enable-kvm -device intel-iommu,intremap=off -net nic,model=e1000 -net tap,script=no,ifname=tap0 -kernel images/kernel-x86_64-pc99 -initrd images/capdl-loader-image-x86_64-pc99 qemu-system-x86_64: warning: host doesn't support requested feature: CPUID.80000001H:EDX.pdpe1gb [bit 26] qemu-system-x86_64: warning: host doesn't support requested feature: MSR(48FH).vmx-exit-load-perf-global-ctrl [bit 12] qemu-system-x86_64: warning: host doesn't support requested feature: MSR(490H).vmx-entry-load-perf-global-ctrl [bit 13] qemu-system-x86_64: Host doesn't support requested features ./simulate: QEMU failed; resetting terminal in 5 seconds--interrupt to abort --------- any tutorial to build/boot it natively on x86_64? Thanks,

2 1

Clean repo init
by Hugo V.C. 11 Jun '21

11 Jun '21

Hi, I'm trying to start a new "clean" repo init in my "/seL4/sel4webserver" directory so I deleted everything there, then I executed: repo forall -c "git reset --hard HEAD" repo forall -c "git clean -df" the I executed: repo init -u https://github.com/SEL4PROJ/sel4webserver-manifest.git repo sync but when I go to the "/projects/webserver/lighttpd" directory and check the content of local "lighttpd.sh" I see different (old) content than what you can see via web interface here: https://github.com/seL4/sel4webserver/blob/master/lighttpd/lighttpd.sh Specifically, via web interface I can see the recent commit: https://github.com/seL4/sel4webserver/commit/6a98bdcb2be6ffc693325bbb48df9d… but in my local copy of the file I can't see the changes. Is it due to come kind of cache issue of Git...? Does it require some time to be synced what you see via web interface and what you get downloaded via CLI? Am I doing something wrong? Thank you in advance and sorry for this newbie like question. Hugo

3 3

Proving there exists a valid execution of a function
by Ben Fiedler 11 Jun '21

11 Jun '21

Hi seL4 devs, I'm not sure whether this list is the right spot to ask about AutoCorres issues, but I gather you have some experience with that :-) I'm currently working on proving that some CAmkES component behaves well wrt some higher- level specification. I want to prove this by simulation: Each step of my concrete CAmkES code corresponds to a step of some abstract machine. I've proven the behavioural lemmas as Hoare-triples using the validNF framework, and now want to lift the AutoCorres-generated executions to my higher-level representation. I'm having issues with this however. Concretely, I want to be able to extract some resulting state after e.g. execution function f. For example: I have the following triple: {| P |} f {| Q |}! Now given a state s such that P s is satisfied, I want to obtain some resulting state s' such that Q' _ s' holds. This is easy enough, as Isabelle has Hilbert's choice operator: fun get_next_state where "get_next_state f s = SOME s'. s' : (snd ` fst (f s))" Here is my problem: The choice operator only works when selecting from a non-empty set. I have a feeling that since I've shown that {P} f {Q} is a non-failing and valid hoare-triple this should somehow follow, but it doesn't. There is an easy counter-example: {| top |} select {} {| toptop |} This is a valid triple, however there are no valid executions for `select {}`. I have a feeling that this is the only counterexample though, since all other potential sources of empty executions are covered (namely nonterminating while loops, as they must always terminate in the validNF framework). If `select A` included a guard that A is non-empty, then I believe one could show that vaildNF P f Q implies exs_valid P f Q, although I'm not sure on this. I've looked into the exs_valid framework, which proves exactly what I want. However, I have two issues with this: 1. I have already proven all the invariants I wanted in the validNF framework, and repeating these proofs seems redundant to me. 2. The exs_valid framework has very little utilities provided for use with the wp tool, which makes working with it more tedious than the validNF framework. Another avenue I've looked at is using termination proofs from the SIMPL code: The AutoCorres ac_corres lemmas derived for my functions guarantee termination of the concrete SIMPL code if the abstract version does not fail, which I have proven. Since, as far as I understand it, the SIMPL layer has no problematic `select`-equivalent, termination should be sufficient to guarantee that a following state actually exists, and somehow lifting that guarantee to the AutoCorres layer. I haven't had success with this though. Any help/pointers is appreciated. Thanks a lot in advance! Cheers, Ben

1 1

Increase Initrd Max Size Beyond DTB Address Limitation
by Olof Holmberg 10 Jun '21

10 Jun '21

Hi, I was wondering if there is a way to increase the RAM size of the Initrd in the qemu-arm-virt VM to more than the initially allowed which seems to be around 250MB. These are my current settings for the VM RAM: #define VM_RAM_OFFSET 0x00000000 #define VM_INITRD_MAX_SIZE 0x9000000 // 150 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x20000000 #define VM_DTB_ADDR 0x4F000000 // VM0_RAM_BASE + 0xF000000 #define VM_INITRD_ADDR 0x46000000 // VM0_DTB_ADDR - VM_INITRD_MAX_SIZE And what I would want is something like this: #define VM_RAM_OFFSET 0x00000000 #define VM_INITRD_MAX_SIZE 0x20000000 // 500 MB #define VM_RAM_BASE 0x40000000 #define VM_RAM_SIZE 0x30000000 #define VM_DTB_ADDR 0x6F000000 // VM0_RAM_BASE + 0xF000000 #define VM_INITRD_ADDR 0x4F000000 // VM0_DTB_ADDR - VM_INITRD_MAX_SIZE VM_DTB_ADDR should probably be 0x4F000000. If I interpreted it correctly it means that the VM_INITRD_ADDR will be below the VM_RAM_BASE_ADDR and therefore outside of the allocated memory for the VM. But I assume that the comments regarding the address of the DTB that it is not possible to have a larger size of Initrd than the difference between VM_DTB_ADDR and the VM_RAM_BASE allows for. I have tested with some different configurations and it either results in the boot hanging after touching the pages for the VM or results in a page error during the touching of pages. It however seems to work with having the VM_INITRD_MAX_SIZE larger than what could fit between the base and Initrd address but I assume that it would result in an error should the actual loaded initramfs require the whole allocated space. What would be the correct way to achieve this if it is even possible? I assume that it might not even be possible if the addresses that has to be allocated for the larger Initrd is already used and allocated for other things. Best regards, Olof

1 0

Running vm_multi on TK1 and TX2
by Mike Clark 10 Jun '21

10 Jun '21

The camkes-vm-examples readme mentions that the Nvidia TX2 should support multiple VMs but it is untested. If you try to build the vm_multi app for TX2 you just get an error that the platform is unsupported. Has anyone tried vm_multi on TX2? Do you have a working devices.camkes that you can share? On the TK1 board, the readme says multiple VMs is unsupported, but in the Notes it says that Multi-VM is untested. Could multi-vm work for TK1? Mike

1 0

Bug when compling in release mode
by Ben Fiedler 09 Jun '21

09 Jun '21

Hello everyone, I've recently found an interesting bug that only occurs when compiling in release mode. Use of the ZF_LOG library (for normal log output) leads to syscalls being made when the capdl-loader runs. These are invoked via musllibc's __stdio_write, which relies on __sysinfo being set correctly for syscalls to work. When compiling with RELEASE=OFF this works fine, however when compiling with RELEASE=ON, __sysinfo is not set (yet?), and subsequently leads to an illegal prefetch exception when __stdio_write tries to invoke a syscall. Setting __sysinfo to sel4_vsyscall using gdb during runtime fixes this. I don't really know the correct place to fix this in the code, but I hope that you can provide some hints on where to fix this bug. Thanks a lot for your help! Cheers, Ben

2 2

Pull request of S91lighttpd
by Hugo V.C. 08 Jun '21

08 Jun '21

Hi, I'm trying to make a pull request as I want to make a very simple (yet useful) change to S91lighttpd file. I wonder where I can find this file in Git as I can find it locally in my build directory: build/overlay/etc/init.d/S91lighttpd but can not find it anywhere else in Git. I assume it is part of some prebuilt file system (overlay?) but still I can't find where this file system is in Git. Any help will be appreciated. Hugo

2 2

Status of the seL4 RISC-V platform Rocketchip
by Axel Heider 07 Jun '21

07 Jun '21

Hi, I'm wondering about the state of the seL4 RISC-V platform "Rocketchip", is anybody actively using this? At the seL4 hardware status page https://docs.sel4.systems/Hardware/rocketchip.html there is not much, and the repo https://github.com/ucb-bar/fpga-zynq has been abandoned. It points to https://github.com/sifive/freedom which has also been abandoned recently. So I wonder, is this platform effectively dead and should be removed? Axel

1 0

watch dog timer and stability mechanisms in sel4 and camkes
by MOHAMAD REZA SHAFIEI 05 Jun '21

05 Jun '21

Hi there. i'm working on my master project and try to implement a system which act as a storage system (a simple sample). so i write my components and its work correctly but some times (rarely) my threads crashes and I couldn't find problem. So i decide to use a service like watch dog timer for garanti all of threads work and when one thread failed and crashed, this mechanism detect it and start another thread or reset the system. My project is on sle4 and camkes framework, a simple solution can implement by some thread controlling (implement WDT in user mode). But I want to know is there in camkes or sel4 any mechanism for this need? a mechanism for garanti stability and system availability? can any body help me? Is there anybody which confront with this need? -- This email was Anti Virus checked by Security Gateway.

1 0

libsel4utils: load_segment memory leak bug
by wzt wzt 05 Jun '21

05 Jun '21

hello: i found a bug memory leak bug in libsel4utils/src/elf.c static int load_segment(vspace_t *loadee_vspace, vspace_t *loader_vspace, vka_t *loadee_vka, vka_t *loader_vka, const char *src, size_t file_size, int num_regions, sel4utils_elf_region_t regions[num_regions], int region_index) { seL4_CPtr loader_slot; cspacepath_t loader_frame_cap; error = vka_cspace_alloc(loader_vka, &loader_slot); [1] while (pos < segment_size && error == seL4_NoError) { reservation_t reservation; if (loadee_vaddr < region.reservation_vstart) { if ((region_index - 1) < 0) { ZF_LOGE("Invalid regions: bad elf file."); return 1; [2] } } if [2] happned, it not free the prev alloc memory, and then it's memory will be leaked. i think the correct way is invoke vka_cspace_free() before return.

3 2

Mapping VM Kernel Memory
by Michael Neises 05 Jun '21

05 Jun '21

Hello everyone, I have a question about some code I'm using from the seL4 repositories. I have a follow-up question about whether a certain memory mapping strategy is feasible. I'm looking at this kernel module: https://github.com/seL4/camkes-vm-linux/blob/master/camkes-linux-artifacts/… and at this user-space app: https://github.com/seL4/camkes-vm-linux/blob/master/camkes-linux-artifacts/… In short, there is shared memory between a camkes component and the vm-linux. I can tell that the shared memory region is given by accessing /dev/uio0. However, it's not clear to me what exactly this memory region is. As I simulate the kernel, I find this: [ 0.000000] Virtual kernel memory layout: [ 0.000000] modules : 0xffff000000000000 - 0xffff000008000000 ( 128 MB) [ 0.000000] vmalloc : 0xffff000008000000 - 0xffff7dffbfff0000 (129022 GB) [ 0.000000] .text : 0xffff000008080000 - 0xffff0000087d0000 ( 7488 KB) [ 0.000000] .rodata : 0xffff0000087d0000 - 0xffff000008a50000 ( 2560 KB) [ 0.000000] .init : 0xffff000008a50000 - 0xffff000008e00000 ( 3776 KB) [ 0.000000] .data : 0xffff000008e00000 - 0xffff000008f31200 ( 1221 KB) [ 0.000000] .bss : 0xffff000008f31200 - 0xffff000008fb9034 ( 544 KB) [ 0.000000] fixed : 0xffff7dfffe7fb000 - 0xffff7dfffec00000 ( 4116 KB) [ 0.000000] PCI I/O : 0xffff7dfffee00000 - 0xffff7dffffe00000 ( 16 MB) [ 0.000000] vmemmap : 0xffff7e0000000000 - 0xffff800000000000 ( 2048 GB maximum) [ 0.000000] 0xffff7e0000000000 - 0xffff7e0000200040 ( 2 MB actual) [ 0.000000] memory : 0xffff800000000000 - 0xffff800008001000 ( 128 MB) My belief is that /dev/uio0 points to the section here labeled "memory." Is that right? My goal is to perform memory introspection on vm-linux kernel modules. To that end, I think I want to look at the section labeled "modules." Is that possible? Best, Michael Neises

1 0

QEMU simulation: Passing drive to CAmkES ARM VM
by Olof Holmberg 04 Jun '21

04 Jun '21

Hi, I am currently booting a initramfs as the VM so that I later would be able to switch root to a filesystem disk that allows for larger storage and has other software installed that I want inside the VM. I have started the simulate script with a few variants of the following line (Passing the virtio device was a guess since the virtio-net device is supported for networking for the VM. I have also tried to pass only the drive part but it has the same result.): sudo ./simulate --extra-qemu-args="-device virtio-blk-pci,drive=drive0 -drive file=filesystem/testimage,format=raw,if=none,id=drive0" However there are no devices appearing in /dev/ that seem to be the drive passed to qemu such as sdaX or vdaX. There is no output from running "fdisk -l" either. So therefore I wonder if this kind of passthrough is supported by seL4? I have tried to find documentation that relates passing a disk to the VM in seL4 but have not found anything yet. This was done for the qemu-arm-virt platform if that has some significance regarding platform support. Best regards, Olof

2 2

Running ninja twice fails in https://github.com/seL4/sel4webserver
by skydivebcn＠gmail.com 04 Jun '21

04 Jun '21

Hi, I have noticed I'm never unable to run "ninja" for a second time and I'm required to rm -rf all the contents of "build" directory, and run "../init-build.sh" again before running ninja again. If I try to simpley run "ninja" twice the error I get is: (...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated (many times...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /home/hugo/seL4/sel4webserver/build/docsite-prefix/src/docsite/_plugins/include_absolute.rb:71: warning: Using the last argument as keyword parameters is deprecated done in 10.04 seconds. Auto-regeneration: disabled. Use --watch to enable. ninja: build stopped: subcommand failed. Any hint on what could be happening? Anyone else having same issue? I'm doing something wrong?

3 5

VGA pass-through using CAmkES VM on x86
by Nicholas Pahl 03 Jun '21

03 Jun '21

Hello all, I am working out of a CAmkES VM manifest and have a function build running on an x86 platform. I have successfully pass-through various PCIe devices (Ethernet, Sata, USB) to a RHEL8 VM. I am attempting to pass-through the VGA controller in the same way as the other PCIe devices, but I am running into errors. I am assuming VGA pass-through requires more effort than just passing the PCIe device through. If anyone has any tips for VGA pass-through or an example CAmkES project that would be greatly appreciated. Also, if anyone has VESA framebuffer pass-through working I would also be interested. I have tried using LibSel4VMMPlatsupportVESAFrameBuffer but have not had any success getting a VM to use it. The card I am trying to pass-through is a Radeon HD 3450. The kernel log's call stack indicates that it is getting into radeon initialization functions, so it does see the VGA controller on the bus. The log seems to be failing to retrieve info from the BIOS. Below is a log of the kernel panic. [ 2.472635] BUG: unable to handle kernel paging request at ffffc90000548480 [ 2.472635] PGD 1013a067 P4D 1013a067 PUD 1013b067 PMD 6fdb8067 PTE 0 [ 2.472635] Oops: 0000 [#1] SMP PTI [ 2.472635] CPU: 0 PID: 349 Comm: systemd-udevd Not tainted 4.18.0-305.el8.x86_64 #1 [ 2.472635] RIP: 0010:radeon_card_posted+0x147/0x200 [radeon] [ 2.472635] Code: 48 8b 83 e8 01 00 00 48 89 c1 83 fa 38 74 53 83 fa 26 0f 87 09 ff ff ff 83 fa 11 76 4d 8b 90 80 60 00 00 48 8b 83 e8 01 00 00 <8b> 80 80 68 00 00 09 d0 a8 01 74 9f 5b b8 01 00 00 00 5d 41 5c c3 [ 2.472635] RSP: 0018:ffffc900005f7960 EFLAGS: 00010202 [ 2.472635] RAX: ffffc90000541c00 RBX: ffff888014950000 RCX: ffffc90000541c00 [ 2.472635] RDX: 0000000016dd1440 RSI: 0000000000000296 RDI: ffff888014950000 [ 2.472635] RBP: ffffc900005f79d8 R08: 0000000000000002 R09: 0000000000000000 [ 2.472635] R10: ffffc900005f79c8 R11: ffffc90000541000 R12: 0000000000000000 [ 2.472635] R13: ffff888014951d90 R14: 0000000000000000 R15: ffff888014950000 [ 2.472635] FS: 00007fe597ad8180(0000) GS:ffff88806fc00000(0000) knlGS:0000000000000000 [ 2.472635] CS: 0010 DS: 0000 ES: 0000 CR0: 0000000080050033 [ 2.472635] CR2: ffffc90000548480 CR3: 0000000016444000 CR4: 00000000000006b0 [ 2.472635] Call Trace: [ 2.472635] igp_read_bios_from_vram+0x18/0xa0 [radeon] [ 2.472635] radeon_get_bios+0x2be/0xf10 [radeon] [ 2.472635] ? __debugfs_create_file+0xc1/0x120 [ 2.472635] ? __debugfs_create_file+0xd5/0x120 [ 2.472635] ? mutex_lock+0xe/0x30 [ 2.472635] ? drm_debugfs_create_files+0x104/0x120 [drm] [ 2.472635] r600_init+0x2b/0x5c0 [radeon] [ 2.472635] radeon_device_init+0x5e7/0xb70 [radeon] [ 2.472635] radeon_driver_load_kms+0x8d/0x240 [radeon] [ 2.472635] drm_dev_register+0xc6/0x1b0 [drm] [ 2.472635] radeon_pci_probe+0x12a/0x1d0 [radeon] [ 2.472635] ? __pm_runtime_resume+0x54/0x70 [ 2.472635] local_pci_probe+0x41/0x90 [ 2.472635] pci_device_probe+0x105/0x1c0 [ 2.472635] really_probe+0x255/0x4a0 [ 2.472635] driver_probe_device+0x49/0xc0 [ 2.472635] device_driver_attach+0x50/0x60 [ 2.472635] __driver_attach+0x61/0x130 [ 2.472635] ? device_driver_attach+0x60/0x60 [ 2.472635] bus_for_each_dev+0x77/0xc0 [ 2.472635] ? klist_add_tail+0x3b/0x70 [ 2.472635] bus_add_driver+0x14d/0x1e0 [ 2.472635] ? 0xffffffffc03fd000 [ 2.472635] driver_register+0x6b/0xb0 [ 2.472635] ? 0xffffffffc03fd000 [ 2.472635] do_one_initcall+0x46/0x1c3 [ 2.472635] ? do_init_module+0x22/0x220 [ 2.472635] ? kmem_cache_alloc_trace+0x131/0x270 [ 2.472635] do_init_module+0x5a/0x220 [ 2.472635] load_module+0x14c5/0x17f0 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __switch_to_asm+0x35/0x70 [ 2.472635] ? __switch_to_asm+0x41/0x70 [ 2.472635] ? __do_sys_init_module+0x13b/0x180 [ 2.472635] __do_sys_init_module+0x13b/0x180 [ 2.472635] do_syscall_64+0x5b/0x1a0 [ 2.472635] entry_SYSCALL_64_after_hwframe+0x65/0xca [ 2.472635] RIP: 0033:0x7fe5966b680e [ 2.472635] Code: 48 8b 0d 7d 16 2c 00 f7 d8 64 89 01 48 83 c8 ff c3 66 2e 0f 1f 84 00 00 00 00 00 90 f3 0f 1e fa 49 89 ca b8 af 00 00 00 0f 05 <48> 3d 01 f0 ff ff 73 01 c3 48 8b 0d 4a 16 2c 00 f7 d8 64 89 01 48 [ 2.472635] RSP: 002b:00007ffc53efb408 EFLAGS: 00000246 ORIG_RAX: 00000000000000af [ 2.472635] RAX: ffffffffffffffda RBX: 00005626ca9314d0 RCX: 00007fe5966b680e [ 2.472635] RDX: 00007fe59722486d RSI: 00000000002c4878 RDI: 00005626cb200450 [ 2.472635] RBP: 00007fe59722486d R08: 00005626ca91501a R09: 0000000000000005 [ 2.472635] R10: 00005626ca915010 R11: 0000000000000246 R12: 00005626cb200450 [ 2.472635] R13: 00005626ca92d120 R14: 0000000000020000 R15: 0000000000000000 [ 2.472635] Modules linked in: radeon(+) i2c_algo_bit drm_kms_helper syscopyarea sysfillrect sysimgblt fb_sys_fops ttm drm ahci libahci e1000e(+) libata crc32c_intel dm_mirror dm_region_hash dm_log dm_mod fuse [ 2.472635] CR2: ffffc90000548480 [ 2.472635] ---[ end trace a2f824fed053010d ]--- [ 2.472635] RIP: 0010:radeon_card_posted+0x147/0x200 [radeon] [ 2.472635] Code: 48 8b 83 e8 01 00 00 48 89 c1 83 fa 38 74 53 83 fa 26 0f 87 09 ff ff ff 83 fa 11 76 4d 8b 90 80 60 00 00 48 8b 83 e8 01 00 00 <8b> 80 80 68 00 00 09 d0 a8 01 74 9f 5b b8 01 00 00 00 5d 41 5c c3 [ 2.472635] RSP: 0018:ffffc900005f7960 EFLAGS: 00010202 [ 2.472635] RAX: ffffc90000541c00 RBX: ffff888014950000 RCX: ffffc90000541c00 [ 2.472635] RDX: 0000000016dd1440 RSI: 0000000000000296 RDI: ffff888014950000 [ 2.472635] RBP: ffffc900005f79d8 R08: 0000000000000002 R09: 0000000000000000 [ 2.472635] R10: ffffc900005f79c8 R11: ffffc90000541000 R12: 0000000000000000 [ 2.472635] R13: ffff888014951d90 R14: 0000000000000000 R15: ffff888014950000 [ 2.472635] FS: 00007fe597ad8180(0000) GS:ffff88806fc00000(0000) knlGS:0000000000000000 [ 2.472635] CS: 0010 DS: 0000 ES: 0000 CR0: 0000000080050033 [ 2.472635] CR2: ffffc90000548480 CR3: 0000000016444000 CR4: 00000000000006b0 [ 2.472635] Kernel panic - not syncing: Fatal exception [ 2.472635] Kernel Offset: disabled [ 2.472635] ---[ end Kernel panic - not syncing: Fatal exception ]---

1 0

Pass Ethernet device to CAmkES ARM VM when using QEMU
by Olof Holmberg 03 Jun '21

03 Jun '21

Hi, I am currently trying to pass a device for ethernet access through qemu to the vm. However there seems to be some issue since the device is not passed through correctly. I have looked at some resources for guidance on how to solve it: https://github.com/seL4/sel4webserver (webserver example) https://lists.sel4.systems/hyperkitty/list/devel@sel4.systems/message/X34TX… (old devel thread) And the important parts for this to work seems to be untyped_mmios for the vm (in devices.camkes for qemu-arm-virt): vm0.untyped_mmios = [ "0x8040000:12", // Interrupt Controller Virtual CPU interface (Virtual Machine view) /* TODO: QEMU PCI addresses could change - ideally need to decode from pcie node */ "0x10040000:17", // QEMU PCI MMIO "0x3eff0000:16", // QEMU PCI IO ports "0x40000000:29", // Linux kernel memory regions ]; And passing the device to QEMU in the simulation script: $ sudo ./simulate --extra-qemu-args="-netdev tap,id=mynet0,ifname=tap0,script=no,downscript=no -device virtio-net,netdev=mynet0,mac=52:55:00:d1:55:01" However when listing the devices with "ip a" on the VM it does not show an eth0 device: # ip a 1: lo: <LOOPBACK,UP,LOWER_UP> mtu 65536 qdisc noqueue qlen 1 link/loopback 00:00:00:00:00:00 brd 00:00:00:00:00:00 inet 127.0.0.1/8 scope host lo valid_lft forever preferred_lft forever inet6 ::1/128 scope host valid_lft forever preferred_lft forever 2: tunl0@NONE: <NOARP> mtu 1480 qdisc noop qlen 1 link/ipip 0.0.0.0 brd 0.0.0.0 3: ip6tnl0@NONE: <NOARP> mtu 1452 qdisc noop qlen 1 link/tunnel6 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 brd 00:00:00:00:00:00:00:00:00:00:00:00:00:00:00:00 But on the host the device that is passed to qemu can be seen: $ ip link show tap0 6: tap0: <BROADCAST,MULTICAST> mtu 1500 qdisc noop state DOWN mode DEFAULT group default qlen 1000 link/ether 62:43:43:54:2d:e6 brd ff:ff:ff:ff:ff:ff I am not sure if I missed something or if it is the QEMU addresses for the pci region that are not correct. Is there any output during boot or build that could give insight in what went wrong when it tries to passthrough the device? Also are there are any resources or guidelines on how to decode the pcie node? (Since I assume this has to be done inside the vm with the limited selection of commands available). Best regards, Olof

1 1

Blocking and unblocking under the MCS kernel
by Robert Kaiser 02 Jun '21

02 Jun '21

Hi all, I'm working on the SOS example of the AOS course, trying to adapt code that used to work under the non-MCS kernel to the now used MCS kernel. So far, this mostly works. However, I'm having problems in resuming a thread that is blocked in an IPC Call operation. In simple cases where the server can reply immediately, the thread is successfully unblocked, simply by replying to the reply object as with the reply capability in the non-MCS kernel. However, if the server does not respond immediately, (i.e. it leaves the calling thread in blocked state, serves some other requests and/or notifications in the meantime, then comes back to reply), replying to the reply object silently fails to unblock the thread for some reason. In the non-MCS kernel, it was necessary in these cases to save the reply capability in a cspace. Therefore I tried to similarly copy/move the reply object to a thread-specific cspace slot, but that doesn't help. I'm sure I'm missing something very basic here. Can anybody point me to the right direction? Best, Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2

Easy way to edit VM guest file system
by skydivebcn＠gmail.com 02 Jun '21

02 Jun '21

Hi, I'm learning about this project: https://github.com/seL4/sel4webserver and would like to edit the guest filesystem. Digging around I found some cpio files that looks to me like may be the right place (output_overlay_rootfs.cpio, rootfs.cpio) but I'm not sure. So, as far I understand in theory I can just edit them and the execute "ninja" again. Before going that way, can anyone confirm this is the easiest/right way? Thanks,

3 2

CAmkES Tutorial, check_deps.py - what does good look like?
by Roderick Chapman 02 Jun '21

02 Jun '21

The first CAmkES tutorial points me at the "Usage" section of the CAmkES manual, which tells me to run "./tools/check_deps.py" to see if I have "the appropriate dependencies installed" but I have no idea what that means... What does good look like? I assume I'm supposed to run that from within the Docker container? If I do that, I get the output below, but I have no idea if that's right. I would expect the Docker container to "Pass" this test with flying colours... so I think I might have screwed up somewhere... Can anyone advise please? Thanks, Rod --- rchapman@in-container:/host/sel4-tutorials-manifest/projects/camkes-tool$ tools/check_deps.py Dependencies of CAmkES runner jinja2 (Python templating module)... Not found plyplus (Python parsing module)... Not found ply (Python parsing module)... Not found elftools (Python ELF parsing module)... Not found orderedset (Python OrderedSet module (orderedset))... Not found six (Python 2/3 compatibility layer)... Found sqlite3 (Python SQLite module)... Found pyfdt (Python flattened device tree parser)... Not found You will not be able to build/run this component Dependencies of CAmkES test suite expect (automation utility)... Found pylint (Python linter)... Found qemu-system-arm (ARM emulator)... Found qemu-system-i386 (IA32 emulator)... Found pycparser (Python C parsing module)... Not found gcc (C compiler)... Found spin (model checker)... Found sha256sum (file hashing utility)... Found You will not be able to build/run this component Dependencies of CapDL translator stack (Haskell version manager)... Found Dependencies of seL4 gcc (C compiler)... Found tempita (Python templating module)... Not found xmllint (XML validator)... Found bash (shell)... Found make (GNU Make build tool)... Found cpio (CPIO file system tool)... Found You will not be able to build/run this component Suggestions: c-parser (NICTA C-to-Simpl parser): you will need this installed if you want to validate code for verification clang-format (Clang code reformatter): installing this will reflow generated C code to make it more readable VBoxManage (VirtualBox administration tool): you will need this installed if you want to build VMWare images mformat (formatting tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 figleaf (code coverage tool for Python): you will need this installed if you want to measure code coverage within CAmkES python-coverage (code coverage tool for Python): you will need this installed if you want to measure code coverage within CAmkES syslinux (Linux bootloader tool): you will need this installed if you want to build QEMU images for IA32 mpartition (partitioning tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 pandoc (document format translator): you will need this if you want to build the CAmkES documentation mcopy (copying tool for MSDOS disks): you will need this installed if you want to build QEMU images for IA32 sponge (input coalescer from moreutils): installing this will give a marginal improvement in compilation times

2 1

Running ninja twice fails in https://github.com/seL4/sel4webserver
by skydivebcn＠gmail.com 02 Jun '21

02 Jun '21

Hi, I have noticed I'm never unable to run "ninja" for a second time and I'm required to rm -rf all the contents of "build" directory, and run "../init-build.sh" again before running ninja again. If I try to simpley run "ninja" twice the error I get is: (...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated (many times...) /var/lib/gems/2.7.0/gems/jekyll-4.0.0/lib/jekyll/tags/include.rb:179: warning: Using the last argument as keyword parameters is deprecated /home/hugo/seL4/sel4webserver/build/docsite-prefix/src/docsite/_plugins/include_absolute.rb:71: warning: Using the last argument as keyword parameters is deprecated done in 10.04 seconds. Auto-regeneration: disabled. Use --watch to enable. ninja: build stopped: subcommand failed. Any hint on what could be happening? Anyone else having same issue? I'm doing something wrong?

1 0

sel4webserver on qemu
by Hugo V.C. 31 May '21

31 May '21

Hi, I just did a commit: https://github.com/hugusmaximus/sel4webserver/blob/master/README.md so people can test this project without having to use a Odroid-XU4 (myself I had this problem...). Notice that I worked on this repository because in the below tutorial: https://docs.sel4.systems/Tutorials/camkes-vm-linux.html I was failing all the time at running in qemu the x86_64 image. Not sure what was happening there, I fixed many things but still not working, maybe because my laptop is somewhat old (Latitude E6410), and even if VT-x is supported for some reason I was unable to make it work (fixed BIOS disabling trusted execution, had OS nested guests supported, etc). As I think having "easy things to play" is key for people to test seL4 stuff, I think it would be nice to make extra effort to have things working on user available equipment (x86_64, qemu, etc). Having said that, I excuse myself in advance for any mistakes in the pull request process as this is the first time in my life doing this, so any suggestion and corrections will be welcome. Last but not least important I'm very happy to have a working Linux guest on a seL4 running on my laptop as this opens to me a big door for tests so I can build prototypes and test many things hoping that as soon as possible I will have some developer doing this job and building native apps for seL4 to interact with an (isolated) guest. Cheers,

2 2

Troubles with hello-world tutorial
by Roderick Chapman 30 May '21

30 May '21

Hello everyone, I am a newbie with seL4, and trying to get the first hello-world tutorial to build and run. I am a bit stuck on a few issues. 1. I had to add the Python "sh" module before the "init" script would run. 2. It is not clear if the "init" script should be run on my main Linux VM, or within the Docker container. 3. The instructions here https://docs.sel4.systems/Tutorials/hello-world.html and https://docs.sel4.systems/Tutorials/ appear to be contradictory, and neither actually works. It appears that the correct sequence of commands is: 3.1. Start the docker container in the directory above sel4-tutorials-manifest 3.2. In the container: cd sel4-tutorials-manifest mkdir hello-world cd hello-world ../init --plat pc99 --tut hello-world cd ../hello-world_build ninja ./simulate Does that look right? The build finishes with "[181/181] objcopy kernel into bootable elf" although https://docs.sel4.systems/Tutorials/hello-world.html says it should be "[150/150] objcopy kernel into bootable elf" Is that still OK? Should I raise an Issue in GitHub to get the documentation pages updated? All the best, Rod Chapman, Director, Protean Code Limited

8 19

ARM64: Handle SError in user-space instead of halting the kernel
by Indan Zupancic 27 May '21

27 May '21

Hello, By default any SError interrupt will halt the kernel. SErrors may be caused by e.g. writes to read-only device registers or ECC errors. With this patch SErrors can instead be reported as a VM data fault for the currently running task. Because SError is asynchronous it is not assured that the faulting task caused the error. With ARMv8.2 there is a new RAS feature which solves the SError problem for common cases: This patch does not use that, our hardware is v8.0, we need another solution for the SError problem. We would rather log the SError and continue than halt the whole system. As SError is easily triggered by device drivers, halting the whole system would make user-space device drivers not much more reliable than in-kernel ones. I do not know if VMs can also cause SErrors in seL4. However, that seems likely, in which case guest OSes can also halt the whole system. One thing I'm not sure about: SError is edge-triggered, while handleVMFaultEvent() does a MCS_DO_IF_BUDGET check. Does this means that if the current task has no budget, the SError IRQ will be lost? Or are pending faults saved by the schedule code? For us missing the SError would be better than halting the kernel, so it doesn't really matter, but I would like to know. I have an Atlassian account, but it seems you can't attach patches there, so I'm not sure how else to send this patch, other than creating a Github account. What is the preferred way to submit patches as an outsider? Best regards, Indan

4 5

Running seL4Test for RISCV with QEMU
by basho1600＠pm.me 13 May '21

13 May '21

Working on Ubuntu, I have built the seL4Test project for RISCV64. I think. At least, there were no build errors. I have qemu-system-riscv64 installed. But when I get to the ./simulate command, all I get is an echo of "Unsupported platform or architecture for simulation". I configured this test as follows: ../init-build.sh -DPLATFORM=hifive -DRELEASE=FALSE -DSIMULATION=TRUE After the 'ninja' command completes, in the images/ directory there is a 6.6MB file named sel4test-driver-image-riscv-hifive which I am guessing is the resulting image to run, though qemu is not impressed by it, saying that the image format is not specified. Maybe I am just not finding the instructions on how to run this, or what 'simulate' WOULD have contained, had things been working as I expect. Or the complete qemu command line to run it.

2 1

Generating CAmkES glue-spec and glue-proofs
by Ben Fiedler 11 May '21

11 May '21

Hi everyone, I'm having troubles generating the CAmkES glue component specification and proofs from our source. I can and have successfully generated the ADL/CDL spec and implementations using the documented CMake parameters. Grepping around the docs I've found references to a 'camkes.sh' script, but neither the project tree nor the files generated during build contain it. One candidate reason could be that we set up our build environment strangely: We currently check out seL4/camkes-manifest and then symlink our component into the 'projects/global-components' subtree of the seL4. This works for generating bootable images, but I haven't found out how to generate the glue spec yet. Why we have set it up this way I don't know, and I suspect that there is a right way TM that we have overlooked/not found in the documentation. I appreciate any help in this regard. Thanks and have a nice day! Cheers, Ben

4 6

Multiple ARM VMs with different CAmkES component configurations
by Olof Holmberg 11 May '21

11 May '21

Hi, I am currently performing research for my master thesis which involves seL4 and ideally retrofitting a SDN controller application for it. As a part of retrofitting applications for seL4 the suggested way is the incremental cyber retrofit approach wich involves dividing subsystems of the application onto several VMs that each runs in a VMM. Therefore I was wondering if it is currently possible to run several VMs on the ARM architecture that has different component configurations in CAmkES? (ARM is mostly preferable for the simple simulation in QEMU when building for qemu-arm-virt, so switching architecture is an option if this is not achievable) I noted that the macros for VMs on x86 and ARM were different when defining components: x86: /* VM and per VM componenents */ #define VM_PER_VM_COMPONENTS(num) \ component Init##num vm##num; \ /**/ ARM: #define VM_COMPONENT_DEF(num) \ component VM vm##num; \ And to clarify using the vm-examples where in the optiplex9020.camkes there are two VMs that are configured differently: component Init0 { dataport Buf(STRING_REVERSE_BUFSIZE) dp1; dataport Buf(STRING_REVERSE_BUFSIZE) dp2; emits Ready ready; consumes Done done; has mutex cross_vm_event_mutex; VM_INIT_DEF() } component Init1 { VM_INIT_DEF() } But in the ARM vm_multi.camkes there is only one VM component that is used for all three VMs: component VM { VM_INIT_DEF() maybe uses VirtQueueDev recv1; maybe uses VirtQueueDrv send1; maybe uses VirtQueueDev recv2; maybe uses VirtQueueDrv send2; attribute vswitch_mapping vswitch_layout[] = []; attribute string vswitch_mac_address = ""; } So it is at least it is not as simple as defining Init##num components for ARM since currently only one VM component is allowed in the macros. Do you have a recommended way that could achieve a CAmkES structure that allows for multiple differently configured VMs for ARM without altering the macros? If it is not possible at the time I assume that switching to x86 is the easiest alternative to achive this? Best regards, Olof

2 2

CAmkES Access to TCBs
by John Shackleton 06 May '21

06 May '21

I am attempting to develop a userland scheduler to manage the release times and deadlines of other threads executing in the system. I would like to use CAmkES as much as possible, since it abstracts away many messy and error-prone details. Question: How do we specify in CAmkES that a scheduler component has access to TCBs of other CAmkES components? Thanks, -John

1 0

Reducing memory footprint - RISC-V
by porter.188＠osu.edu 19 Apr '21

19 Apr '21

I'm trying to build a low memory footprint of RISC-V based seL4. I'm using QEMU/spike for now. In seL4 12.0 I can modify spike.dts to 8.5 MB of memory 0x00880000. 42 memory@80000000 { 43 device_type = "memory"; 44 reg = <0x00000000 0x80000000 0x00000000 0x00880000>; 45 }; This is the smallest value that builds, lower than this I get the error: [0/1] Re-running CMake... -- Found GCC with prefix riscv64-unknown-linux-gnu- STATUS,KernelDTSList: tools/dts/spike.dts -- /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... STATUS,platform_yaml: /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml -- Detecting cached version of: musllibc -- Found valid cache entry for musllibc -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/femur_12.0/build [18/36] Generating gen_headers/image_start_addr.h FAILED: elfloader-tool/gen_headers/image_start_addr.h cd /mnt/data/femur_12.0/build/elfloader-tool && sh -c "/mnt/data/femur_12.0/tools/elfloader-tool/../cmake-tool/helpers/shoehorn.py /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml /mnt/data/femur_12.0/build/elfloader-tool/archive.o > /mnt/data/femur_12.0/build/elfloader-tool/gen_headers//image_start_addr.h" shoehorn: fatal error: ELF-loader image "/mnt/data/femur_12.0/build/elfloader-tool/archive.o" of size 0x107548 does not fit within any memory region described in "{'devices': [{'end': 2147483648, 'start': 0}, {'end': 549755809792, 'start': 2155872256}], 'memory': [{'end': 2155872256, 'start': 2149580800}]}" ninja: build stopped: subcommand failed. What do I need to modify to get to < 2 MB? Thanks!

4 8

seL4 Crowdsourcing Portal
by Gernot Heiser 15 Apr '21

15 Apr '21

Dear seL4 community, It is a pleasure to announce that seL4 now has a crowdsourcing portal, using the Linux Foundation’s LFX platform. Please help making seL4 stronger by donating, and encouraging others to do the same! https://crowdfunding.lfx.linuxfoundation.org/projects/e94c998c-bac2-4224-b0… Gernot

1 0

Choosing correct hardware platform for CAmkES-arm-vmm Cross VM connector support
by Zohra Charania 15 Apr '21

15 Apr '21

Hi everyone, I am a PhD student. For my research, I want to use sel4 and developa system based on it. The idea is to use the arm based multi VM and cross VM communication ability of sel4 and provide a secure and isolated environment for the various applications running on the system. I was reading through the sel4 tutorials and documentation to find out which hardware would be suitable for this. I started learning sel4 with Raspberry Pi 3, but as Rpi3 does not have GICv2 or GICv3, I am not sure how do I develop the CAmkES-arm-vmm, multi VM and cross VM connector on it. As I wish to develop an application i.e a system architecture using sel4, itwould be good to have a device that provides me the starting point of having a multi VM and Cross VM communication. I read in the documentation that we can use Nvidia TK1-SOM from Colorado engineering to develop CAmkES-arm-vmm. But if I see the table here: _https://docs.sel4.systems/projects/camkes-arm-vm/_ , it says that CrossVM and Multi VM support is unsupported and in notes it says untested. According to the table, this is true for TK1, TX1 and TX2. Could someone please clarify what does this mean? Does it mean that we cannot have these features for these hardware or is it that they are not tested? It will be a great help to get this information, as then I can purchase the correct hardware and advance my work. I am new to micro-kernel community, so I apologize if I have missed anything obvious and would be glad to receive guidance and advice. Hoping for a kind response. Thank you. Sincerely, Zohra

1 0

[seL4 Announce] Operating System based on seL4.
by Gernot Heiser 12 Apr '21

12 Apr '21

<comment> The below message was posted to announce(a)sel4.systems. It was inappropriate for that list, but got though due to a configuration error (now fixed). I’m reposting it here as it would be appropriate for this list. Feel free to respond here. </comment> Hello, Which operating systems are based on seL4 Microkernel? Any home usage? Thanks.

2 1

hello world difficulty
by Royce Mitchell III 09 Apr '21

09 Apr '21

I feel like an idiot for having to ask for help so early, but I'm trying to get started with the hello world tutorial and ran into a problem very quickly. First off I want to say thank you for all the work that's been put into the tutorils. The amount of information in them is quite daunting, but considering the subject matter it's actually very accessible all things considered. I have a Debian 10 linux VM that I'm using for testing. I'm okay building a VM dedicated solely to seL4 development if that's necessary, but I'm assuming it's not. FYI I had some difficulty with the prerequisites instructions regarding Debian. This may be the source of the problem I'm having but I'm not sure how to resolve it. Your setup instructions said to refer to the docker requirements but when I went there I couldn't find anything on that page that indicated what exactly I was supposed to install. All that being said, here is a capture from my terminal which I'm hoping illustrates the problem I'm having specifically: rmitchell@ou812:~/sel4-tutorials-manifest$ ./init --tut hello-world Traceback (most recent call last): File "./init", line 16, in <module> import common File "/home/rmitchell/sel4-tutorials-manifest/projects/sel4-tutorials/common.py", line 16, in <module> import sh ModuleNotFoundError: No module named 'sh' rmitchell@ou812:~/sel4-tutorials-manifest$ python Python 3.9.1 (default, Mar 19 2021, 01:08:36) [GCC 8.3.0] on linux Type "help", "copyright", "credits" or "license" for more information. >>> import sh >>> sh.__version__ '1.14.1' >>> exit() As you can see from my example above, I have Python 3.9.1 installed and it is the default python interpreter on my system. The "sh" module is installed and accessible from Python's interactive interpreter, yet when the common.py file tries to import it, it complains that it can't find the 'sh' module. FYI sh is installed both at the system and user levels. I'll try digging into your source and see if I can figure out what the issue is. I'll share my findings if I figure it out before you guys point out my mistakes. Thanks! Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

3 6

seL4 service discovery question
by Royce Mitchell III 08 Apr '21

08 Apr '21

Hi all, I've been passively following seL4 for several years. I've been reading the documentation, tutorials, watching YouTube videos. The concepts behind capabilities and other types of kernel objects are starting to sink in but there's one piece of understanding that's eluding me. If I just haven't stumbled across it yet in the documentation, then pointing me in the right direction would be greatly appreciated. Given: * An ethernet driver named "e1000" and 2 devices "eth0" and "eth1" controlled by that driver. * A "tcp" service that would implement that network protocol. * A higher level service named "network" that implemented some kind of networking abstraction for us. How would: 1) the "network" service advertise its services as available via IPC? 2) an application locate this "network" service to be able to IPC with it? I assume the mechanisms here would also apply to interactions between services as well. I picked the "network" service in this example only because it would be the boundary between application and OS services. I'm guessing that maybe this is purely an OS design decision and not the purvue of the kernel itself. Perhaps init could launch a "service manager" process that would be responsible for starting up services and drivers for example and this "service manager" could provide an IPC endpoint back to init (or whomever) to use for IPC discovery. Then, whenever a new process is started, it is provided with the IPC discovery endpoint information that it is to inherit. If my assumptions are correct or close, or even dead wrong, would someone be willing to share some pseudo-code on what this could/should look like in seL4? If a central service manager is needed to glue the core OS together, does it represent a single point of failure and how would the OS recover if it crashes and loses it's database of available services without having to rebuild and restart all drivers and services? (I'm not saying that's a bad thing, just trying to wrap my head around how this particular part of seL4 works) Thanks, Royce Mitchell, IT Consultant ITAS Solutions royce3(a)itas-solutions.com There are three hard problems in computer science: naming things, and off-by-one errors.

6 14

Small question about copiing threads
by Сергей Волкович 07 Apr '21

07 Apr '21

Hello. My name is Serhgey Volkovich. Currently i trying to write my own posix compilant os subset. But i cannot understand some momments such what happen with main process memory if i create new thread with same pointer as it have main, and second process will try to change something in own memory. Will it change memory of main process?

1 0

About the BuildSystem of seL4
by Jerry Zhou 29 Mar '21

29 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

2 2

seL4 as bootloader
by Isaac Beckett 29 Mar '21

29 Mar '21

The Linux kernel has support via the EFISTUB module to be loaded directly as an EFI bootloader, which if I recall correctly, also allows it to chainload another OS and be used as a fully-fledged multiboot bootloader. Is it practical to do something similar with seL4? Obviously on non-UEFI platforms it'd be entirely different code, but still.

2 1

About the BuildSystem of seL4
by zhouchunhua＠lixiang.com 26 Mar '21

26 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

1 0

About the BuildSystem of seL4
by Jerry Zhou 26 Mar '21

26 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

1 0

some confuse about Camkes and AOS sel4
by yadong.li 25 Mar '21

25 Mar '21

hi: I am try to understand the designing philosophy of seL4 kernel base on CAmkES, I didn't find a global memory server in this system But the AOS may be have memory server,even though I am not familiar with AOS now, I have three question: 1. what is the purpose of the existing of CAmkES and AOS meanwhile ? (static and dynamic ) 2. which one (AOS or CAmkES) will be vigorously developed by the seL4 community and fund later. 3. Is a good idea to provide global memory server in CAmkES system? I found usually CAmkES alloc untyped pool Statically for componet in .camkes file. Thank you very much

1 0

Pull requests now directly merged on GitHub
by Gerwin Klein 25 Mar '21

25 Mar '21

The next step in the making contributions easier is now complete: Pull requests for repositories in the seL4 GitHub org can now be merged on GitHub directly, without the loop thought Data61's CI infrastructure. Hopefully this will make merging pull requests faster and less painful. The exception for now are repositories with manifests (such as sel4test-manifest), because parts of these manifests are generated automatically. We're working on moving these as well. The testing and verification regime is the same as before, including extensive hardware tests and proofs, but the results and logs should now be visible directly on GitHub. Happy merging :-) Cheers, Gerwin

1 0

AMD-V Support
by ndaughety13＠gmail.com 24 Mar '21

24 Mar '21

I found "Your host machine has to have a CPU that supports Vt-x virtualization (for Intel CPUs), or AMD-V (for AMD CPUs, but that wasn’t tested)" at https://docs.sel4.systems/projects/camkes-vm/. In context, my understanding is that seL4 should work with AMD-V but it doesn't work on my AMD system. I also do not see any mention of it anywhere else -- not even in the source (could not find amd-v counter part to vtx in grep search of source). Noting that it has not been tested, could this be a build configuration problem or has support not actually been implemented? ...or am I missing something?

1 0

Introduction Ben Fiedler
by Ben Fiedler 19 Mar '21

19 Mar '21

Hello seL4-devs, I'm currently working on a CS MSc thesis at ETH Zurich supervised by David Cock, working on verified low-level system components using seL4 and CAmkES, which I'll be doing until August. I haven't worked with seL4 or CAmkES before, but I have some rudimentary Isabelle/ITP experience from my BSc thesis (mainly typing sledgehammer ;) ). During the course of my thesis I will probably have some questions which I'll post here, and hopefully I can contribute to improving the tooling around seL4+CAmkES verification. Nice to meet you all! Cheers, Ben

2 1

Re: Creating process from not root process
by Seo Yeon Hwang 05 Mar '21

05 Mar '21

Hello, Sorry for bringing this old post up, but could anyone let me know the answer of this post? I’m quite new to seL4 and I’ve been following tutorials and modifying it, and I have the exact same question as this post. Basically, how can I create a process from non-root process? Thanks a lot! Seoyeon Hwang

2 1

Picotcp and Lwip issues on OdroidC2
by ogosinkem＠gmail.com 03 Mar '21

03 Mar '21

Hi, I'm currently trying to include either the picotcp or lwip library into an application in order to connect to or show a connection to a network. As such I have added some lines to some of my files. CMakeLists.txt: DeclareCAmkESComponent(Client SOURCES components/Client/src/main.c LIBS lwip picotcp) hello_world.camkes: component Client{ uses Ethdriver eth_drv; has mutex lwip; control;} When trying to build I get a long error message which boils down to: /usr/lib/gcc-cross/aarch64-linux-gnu/7/../../../../aarch64-linux-gnu/bin/ld: cannot find -llwip /usr/lib/gcc-cross/aarch64-linux-gnu/7/../../../../aarch64-linux-gnu/bin/ld: cannot find -lpicotcp collect2: error: ld returned 1 exit status [258/316] Building C object CMakeFiles/ethdriver.instance.bin.dir/ethdriver/seL4SingleThreadedComponent.template.c.obj ninja: build stopped: subcommand failed. How to I go about solving this issue? Thanks, Nkem

1 0

Ethernet device module for odroidc2
by ogosinkem＠gmail.com 24 Feb '21

24 Feb '21

I have been trying to use the ethernet driver for the UNSW Asdvanced Operating Systems course but I still get these messages: find_compatible_driver_module@io.c:434 No suitable driver was found for path /soc/ethernet@c9410000, ignoring server_init@ethdriver.c:382 Unable to find an ethernet device I thought that I had to copy the driver to the utils lib folder and provide a preprocessor macro as someone else had suggested but I may be missing a few other things. Best, Nkem

3 6

Sporadic Server Implementation Details
by msudvarg＠wustl.edu 11 Feb '21

11 Feb '21

Hi all, I hope this is the right forum to be posting this question. I've reached out to Anna Lyons, the first author on the EuroSys 2018 "Scheduling Context Capabilities" paper (https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf) but I do not know if her listed email address is still active. I want to ask for more clarification on the sporadic server implementation in seL4. My interpretation of how the Lyons et al. paper describes the implementation is different than my understanding of the sporadic server definition as described by Sprunt et al. in 1989 (https://link.springer.com/article/10.1007/BF02341920) However, looking at the seL4 kernel source code, it seems that the actual implementation follows very closely with the improved POSIX sporadic server mechanism described by Stanovic et al. in 2010 (https://www.cs.fsu.edu/~awang/papers/rtas2010.pdf) In particular, the Lyons et al. paper states that when a thread is preempted at time t, a replenishment is scheduled for time t + T. My understanding of the sporadic server is that if a thread becomes active at time t, the replenishment is scheduled for time t + T. In other words, the replenishment is scheduled one period from when the thread begins execution, not when it ends execution. Further, a thread becomes active when it becomes unblocked (i.e. returns from a blocking system call, or is activated by the release of an aperiodic task that it handles). In other words, a thread that is preempted by a higher-priority thread is not considered to have become inactive, according to the sporadic server definition. This seems to be the case in both the Sprunt and Stanovic papers. I think the distinction is significant in a system (like seL4) where only a finite number of replenishments are tracked. Determining what number of replenishments each thread’s server must track is much easier if only voluntary yielding of the processor, and not preemption by higher-priority threads, triggers a replenishment. Can somebody explain to me in more detail how the sporadic server has been implemented in seL4? Like I said, from my reading of the kernel source, it seems that it has been implemented according to the improved POSIX sporadic server detailed by Stanovic, but I’m not certain that I’ve identified all conditions that cause a replenishment to be scheduled.

3 2

Use sel4 and mmc for storage but sdhc driver wait for SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB
by MOHAMAD REZA SHAFIEI 10 Feb '21

10 Feb '21

hi there ... i'm working on mmc in sel4 for storage memory. i port your code for i.mx7 (modify registers and all need for that). so when i init mmc with calling mmc_init, sdhc driver wait at sdhc.c@249 and in this line: while (readl(host->base + PRES_STATE) & (SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB)); indeed sdhc driver send function (sdhc_next_cmd(..)) send first command in mmc_reset (): which is : struct mmc_cmd cmd = {.data = NULL}; cmd.index = MMC_GO_IDLE_STATE; cmd.arg = 0; cmd.rsp_type = MMC_RSP_TYPE_NONE; printf("2-1\n"); host_send_command(card, &cmd, NULL, NULL); and status= 65 returned whicm means this command sent completely. so when program continue to send another command (still in mmc_reset) which is : /* TODO: review this command. */ struct mmc_cmd cmd2 = {.data = NULL}; ps_mdelay(10); cmd2.index = MMC_SEND_EXT_CSD; cmd2.arg = 0x1AA; cmd2.rsp_type = MMC_RSP_TYPE_R1; printf("2-2\n"); host_send_command(card, &cmd2, NULL, NULL); status which returned with sdhc send command in sdhc driver is 0. but this worked too. and when program execution continue to call mmc_voltage_validation(..) sdhc driver wait in while (readl(host->base + PRES_STATE) & (SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB)); ... I don't have any idea why this happened .. can you help me? I didn't modify any code in sdhc.c or mmc.c ... my app for using mmc is here: #include <autoconf.h> #include <camkes.h> #include <camkes/io.h> #include <camkes/sync.h> #include <stdio.h> #include <utils/util.h> #include "string.h" //sdio test #include <sdhc/mmc.h> #include <sdhc/plat/sdio.h> #include <sdhc/sdio.h> #define max(x, y) (((x) >= (y)) ? (x) : (y)) //build config // #define TEST_FILESYSTEM 0 #ifdef CONFIG_64BIT #define BITS_PER_LONG 64 #else #define BITS_PER_LONG 32 #endif /* CONFIG_64BIT */ #define IMX7_GPIO1_BASE_ADDR ((uint32_t)NULL) #define IMX7_GPIO4_BASE_ADDR ((uint32_t)NULL) #define IMX7_SPI_BASE_ADDR ((uint32_t)NULL) #define IMX7_CTL_MUX_BASE_ADDR ((uint32_t)NULL) /** * we have two keyboard driver () */ bool STDKBD = true; #define IMX7_CTL_MUX_GPIO1_09 (0x18) seL4_CPtr timer_notification(void); seL4_CPtr notification; static void delay(uint64_t ms) { seL4_Word badge; /* test a relative timeout */ uint64_t t1 = timer_time(); // printf("Cur time: %"PRIu64"\n", t1); timer_oneshot_relative(0, ms * NS_IN_MS); seL4_Wait(notification, &badge); // printf("Badge: %x\n", badge); t1 = timer_time(); // printf("Cur time: %"PRIu64"\n", t1); } /* * Required for the camkes_sys_clock_gettime() in sys_clock.c of libsel4camkes. */ int clk_get_time(void) { uint64_t time_in_ms = timer_time() / NS_IN_MS; return (time_in_ms & 0xFFFFFFFF); } static int count = 0; ps_io_ops_t io_ops = {0}; struct netif* net_if; mmc_card_t mmc_card = 0; sdio_host_dev_t sdio_host_dev; int mmc_found = 0; void mmc_irq_handle(ps_irq_t* irq) { printf("mmc irq handle .... \n"); if(!mmc_found){ // printf("mmc not found yet :)\n"); // mmc_init handle this self // sdio_host_dev.handle_irq(&sdio_host_dev,irq->irq.number); mmc_irq_acknowledge(irq); return ; } // sdio_host.handle_irq(&sdio_host, irq); mmc_handle_irq(mmc_card,irq->irq.number); mmc_irq_acknowledge(irq); } int run(void) { notification = timer_notification(); int err = camkes_io_ops(&io_ops); if (err != 0) { ZF_LOGF("Can not init ops : %d\n", err); }; printf("initialize sdhc1 ...\n"); err = sdio_init(SDHC1, &io_ops, &sdio_host_dev); // while card not present check while(sdio_host_dev.reset(&sdio_host_dev) == -1){ delay(1000); } printf("before mmc_init\n"); mmc_init(&sdio_host_dev, &io_ops, &mmc_card); mmc_found = 1; printf("after mmc_init\n"); if (!err) { printf("SDHC1 inited successfully.\n"); // sdhc_ls(); } else { printf("SDHC1 initizatino failed!: %d", err); } // sdio_host_dev.reset(&sdio_host_dev); // mmc_init(&sdio_host_dev, &io_ops, mmc_card); // sdio_host_dev.handle_irq =mmc_handle_irq_func; while (true) { printf(".\n"); delay(1000); } return 0; } best regards.. shafie -- This email was Anti Virus checked by Security Gateway.

1 0

Public seL4 TSC meeting on Fri, 12 Feb
by Gerwin Klein 08 Feb '21

08 Feb '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: Fri 12 Feb 2021 15:30-17:00 Sydney time (5:30am in Berlin, 8:30pm in San Francisco). This is the continuation of the meeting last week. The meeting is by Zoom, and you can register here: https://unsw.zoom.us/meeting/register/tZcqf--prz8jGNdE-zpwZXIBsbdYlN3fQn1Y Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: Discussion points - when/how should Committer/Admin role change for people who have left D61 and had the role based on org membership - endorsement process for training and products Vote on: - Platform Owner proposal Discuss, potentially vote on RFC proposals: - https://sel4.atlassian.net/browse/RFC-6 - https://sel4.atlassian.net/browse/RFC-5 - https://sel4.atlassian.net/browse/RFC-4 If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.htmld

1 0

Public TSC meeting on Fri, 29 Jan
by Gerwin Klein 08 Feb '21

08 Feb '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: Fri 29 Jan 2021 15:30-17:00 Sydney time (5:30am in Berlin, 8:30pm in San Francisco). The meeting is by Zoom, and you can register here: https://unsw.zoom.us/meeting/register/tZ0ocO6hrDwiGtTYlzULbKeTK8ybYJyCC7_p Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. Sorry about the very early time for Europe, but there are no time slots that work for the US, Australia, and Europe at the same time. We are planning to swap between better times for Europe and the US for the next meetings. The TSC is the body that decides on the technical direction of seL4: https://sel4.systems/Foundation/TSC/ The agenda for the meeting so far is: - updates from the TSC chair and committees: - seL4 public Jira - Jira + GitHub sync - reviewers who have joined - more GitHub tests - discussion points: - do we have too many different forums? - bug/issue classification (Jira is now public, we shouldn't call everything a bug) - more in-tree docs - test infrastructure - extend RFC process slightly? (see https://sel4.atlassian.net/browse/RFC-6?focusedCommentId=14886& ) - when/how should Committer/Admin role change for people who have left D61 and had the role based on org membership - endorsement process for training and products - vote on: - Platform Owner proposal - discuss, potentially vote on RFC proposals: - https://sel4.atlassian.net/browse/RFC-4 - https://sel4.atlassian.net/browse/RFC-5 - https://sel4.atlassian.net/browse/RFC-6 This is probably already too much for 90min and we may have to prioritise, but we will see how far we get. If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

2 5

Errors while running Virtual Machines on SeL4;
by Jorge Pereira 07 Feb '21

07 Feb '21

Hi all, I’m getting familiar with SeL4 build system and I’ve been running several application examples and also creating my own on top of the kernel using CAmKES. Very good. $ mkdir camkes-project; $ cd camkes-project; $ repo init -u https://github.com/seL4/camkes-manifest.git; $ repo sync; $ ../init-build.sh -DPLATFORM=sabre -DAARCH32=1 -DCAMKES_APP=helloworld -DSIMULATION=1 $ ninja $ ./simulate Again, so far, so good! Several CAmKES examples up and running. Now, I want to run virtual machines on top of it, I’ve seen several posts on internet and even in the official SeL4 website and none of them are working on my side. Can you please give me some pointers to be able to do so? We really want to start using SeL4 in our products with virtual machines, but current documentation is not ideal. I don’t have experience in CMAKE and that might be the real problem 😊. I need your help to ramp up in the SeL4 project! https://docs.sel4.systems/projects/camkes-arm-vm/ repo init -u https://github.com/seL4/camkes-vm-examples-manifest repo sync mkdir build cd build ../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1 When running ../init-build.sh I get the following: “ CMake Error at /home/jorge/hdd/work/projects/vm/Findcamkes-arm-vm.cmake:39 (find_package): By not providing "Findcamkes-vm-images.cmake" in CMAKE_MODULE_PATH this project has asked CMake to find a package configuration file provided by "camkes-vm-images", but CMake did not find one. Could not find a package configuration file provided by "camkes-vm-images" with any of the following names: camkes-vm-imagesConfig.cmake camkes-vm-images-config.cmake Add the installation prefix of "camkes-vm-images" to CMAKE_PREFIX_PATH or set "camkes-vm-images_DIR" to a directory containing one of the above files. If "camkes-vm-images" provides a separate development package or SDK, be sure it has been installed. Call Stack (most recent call first): CMakeLists.txt:19 (camkes_arm_vm_setup_arm_vm_environment) -- Configuring incomplete, errors occurred! See also "/home/jorge/hdd/work/build/CMakeFiles/CMakeOutput.log". “ Best, Jorge

1 0

seek for some help
by abdi mahmud haji 01 Feb '21

01 Feb '21

hi sorry for bothering you but i get some problem with sel4 tutorial when i trying to get starting with "repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest" i got down bellow error and how can i fix it pls Traceback (most recent call last): File "/home/sel4/sel4-tutorials-manifest/.repo/repo/main.py", line 56, in <module> from subcmds.version import Version File "/home/sel4/sel4-tutorials-manifest/.repo/repo/subcmds/__init__.py", line s 38, in <module> ['%s' % name]) File "/home/sel4/sel4-tutorials-manifest/.repo/repo/subcmds/upload.py", line 27, in <module> from hooks import RepoHook File "/home/sel4/sel4-tutorials-manifest/.repo/repo/hooks.py", line 472 file=sys.stderr) ^ SyntaxError: invalid syntax tnks

3 2

Fwd: Regarding Ken Thompson's Reflecting on trusting trust...
by Bora Agca 30 Jan '21

30 Jan '21

Hi, i have one question: since the seL4 was written with a C compiler and it is possible that this compiler has an in-built backdoor, how can you still claim, that seL4 is "safe", i.e. non-hackable. Best regards and thanks in advance ___________________________ Bora Agca Diplom Informatiker Oracle Certified Programmer Java SE 6

2 1

Request for Speakers/Collaboration with WASI
by Zach Lym 29 Jan '21

29 Jan '21

I'm a community organizer for WASI <https://wasi.dev/>, a post-POSIX runtime with features that I think make it suitable for SeL4's planned post-POSIX runtime: * Fast and fine grained SFI via WASM. * Fast IPC and capability oriented security via WASM Reference Types <https://github.com/WebAssembly/reference-types/blob/master/proposals/refere…> . * High level interoperability across programming languages via WASI Interface Types <https://hacks.mozilla.org/2019/08/webassembly-interface-types/> and shared garbage collection <https://github.com/WebAssembly/gc/blob/master/proposals/gc/Overview.md>. * Wide range of targets: embedded, TEE, blockchain, browser, server, and (eventually) consumer operating systems. Industry cooperation is happening through the Bytecode Alliance <https://bytecodealliance.org/>, with partners like Red Hat ensuring commercial viability [1 <https://github.com/bytecodealliance/wasmtime/issues/70#issuecomment-4773292…> , 2 <https://github.com/bytecodealliance/wasmtime/issues/71#issuecomment-5180066…>]. Fastly is already using it for their serverless offering <https://www.youtube.com/watch?v=QdWaQOgvd-g>, which can scale to 20K processes/machine with a 35.4 microsecond cold start time. However, I believe the project would benefit *greatly* from the SeL4 community's experience architecting high-performance/high-assurance microkernels, IPC, and capability based security models. SOIL <https://soil-initiative.org/> is an academic effort to foster cross-pollination through biweekly seminars <https://soil-initiative.org/seminar/>. *We are seeking presenters from the SeL4 to better understand your needs and potential areas of collaboration*. Please contact Ross Tate (ross(a)cs.cornell.edu) if you are interested in presenting and jump on our Zulip Channel <https://bytecodealliance.zulipchat.com/> if you have any questions! Thank you, -Zach Lym

1 0

Accessing GPIOs on Raspberry Pi
by Zohra Charania 29 Jan '21

29 Jan '21

Hello All, I am new to seL4. I want to use seL4 in my project. As a starting point, I have compiled seL4 for Raspberry pi 3. As a next step, I have been trying to access GPIOs on Raspberry Pi. I used gpio.h from util_libs/libplatsupport/arch_include/arm/platsupport. I could not find any gpio.c for Rpi3/bcm2837 platform. When I compile the code, I am getting error: undefined reference to `gpio_sys_init'. Is there any support for GPIO access already available for Raspberry Pi? Could you please provide me guidance on how I can work with the Raspberry Pi GPIOs with seL4. Best Regards Zohra

1 0

Re: Cross VM Connectors
by PityTheFool 29 Jan '21

29 Jan '21

I discovered the answer by looking at the optiplex9020 example. Because the tutorial used the old modules, I had not fully integrated the new connector module into my project.

1 0

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

I.MX7, Timeout in SEL4 USB driver
by MOHAMAD REZA SHAFIEI 16 Dec '20

16 Dec '20

Hi there, I'm working on USB Storage in Sel4 on I.MX7, when I read/write some block of data from/to USB Driver , sometimes US‌‌‌B Driver fails with this output by this output: ehci_wait_for_completion@async.c:594 Timeout this error happened in ehci_schedule_xact function that waiting for transaction completion. I port USB Driver on I.MX7 but because of above bug, it isn't Stable. Can anyone help me how to fix this bug? regards, Mohamad -- This email was Anti Virus checked by Security Gateway.

1 0

[Camkes] Access control for memory or the entire component?
by Seo Yeon Hwang 11 Dec '20

11 Dec '20

Hello all, I wonder if it is possible for a component to directly access some specific part of memory with an address or access the whole component (not some dataports) using Camkes. I can see how to set up the permissions (R/W) for each dataport in the tutorial #port_privileges part, but I wonder if one component can read some specific memory region with starting and ending addresses, or read the whole memory where another component is located. Thanks for your help! Best regards, Seoyeon

2 1

CfP: FOSDEM 2021 - Microkernel Devroom
by Martin Decky 08 Dec '20

08 Dec '20

Microkernel Devroom at FOSDEM 2021 CALL FOR PARTICIPATION On-line version of this CfP: http://fosdem.microkernel.info/ The developers and users of several free and open source microkernel-based operating systems will meet on-line as part of FOSDEM 2021 [1] and will share a developer room. The devroom is currently looking for content in the form of talks and activities related to the area of microkernel-based, unikernel-based, component-based operating systems and similar topics. The devroom has been preliminarily scheduled to Saturday February 6th 2021. The devroom will take place during European day hours. Possible topics of the devroom include, but are not limited to: * introduction of a specific OS or framework * design of subsystems and the general architecture of an OS * used languages, tools and toolchains * enabling support for hardware (architectures, device drivers) * enabling support for programming languages * development processes, debugging * maintenance, testing and release engineering * security and robustness * trends and challenges * community and governance * use cases, experiences and status updates * best practices, lessons learned and demos This is a call for your participation. We kindly ask you to submit your proposals no later than on December 26th 2020. Please use the Pentabarf website [2] to submit your proposals. If you already have a user account in Pentabarf, please do not create a new one. Please make sure to select the Microkernel devroom as the track when submitting your talk and include at least the following information in your proposal: * title of your talk * your full name * short abstract of your talk (one or two paragraphs) * duration of your talk (at least 20 minutes and no longer than 50 minutes), excluding a Q&A part * your short bio * your photo The talks will be pre-recorded in advance in January and streamed during the event. This means that you will need to complete and submit your talk by around mid January. However, each speaker should be also present on-line just after the streaming of the talk for a live Q&A. You can specify your prefered time slot of your talk. The communication language of the devroom is English. The official devroom schedule (along with the accepted talks) will be announced on December 31st 2020 on the devroom's mailing list [3] and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM website. You are also invited to send any other suggestions for what you want to see or do at the devroom to the mailing list. About the Devroom Since the first Microkernel devroom at FOSDEM 2012 [4], this devroom has been part of each following FOSDEM. The focus gradually widened to include component-based and unikernel-based operating systems. By now it has become a somewhat institutionalized tradition for the community to meet there. To this date, over a dozen projects have participated in one way or another. Each of the projects face similar challenges but come up with partially different solutions. Therefore, the goal of the devroom is to bring the various projects together, let them exchange ideas, cross-pollinate and socialize. Extraordinary Circumstances in 2021 Due to the extraordinary mode of organization of FOSDEM 2021 (being an on-line event for the first time), many practical aspects of the devroom are still in the process of determination. For example, the devroom talks will be required to be pre-recorded in January and streamed during the event (with a live Q&A), but the technical details are still sketchy at this moment. The talk videos will be published under Creative Commons license by FOSDEM. By submitting a recorded talk, the speaker agrees to have it made available publicly indefinitively. For organizational purposes, we also need contact information of the speakers of accepted talks. Please check the official CfP page [5] of our devroom regularly. We will keep updating it as new guidelines will be determined by the FOSDEM organizers. Sadly, it will not be possible to arrange our traditional microkernel dinner and other in-person social gatherings in Brussels this time. However, we plan to organize an on-line replacement. The details will be announced later in January. On the other hand, the on-line nature of the devroom allows us to "overflow" to a second day in case we receive a substatial number of quality proposals. About FOSDEM FOSDEM [6] is a two-day event organised by volunteers to promote the widespread use of free and open source software. FOSDEM is widely recognised as one of the best such conferences worldwide. FOSDEM covers a wide spectrum of free and open source software and hardware projects and offers a platform for people to collaborate. To this end, FOSDEM has set up developer rooms (devrooms) where teams can meet and showcase their projects. Devrooms are a place for teams to discuss, hack and publicly present latest directions, lightning talks, news and proposals. Besides developer rooms, FOSDEM also offers main tracks, lightning talks, and in the past instances certification exams and project stands. In recent years, FOSDEM has been hosting more than 5000 developers at the ULB Solbosch campus. Due to the circumstances, FOSDEM 2021 will be organized as an on-line event. Despite this, the participation in FOSDEM is still totally free, although the organisers gratefully accept donations and sponsorship. No registration is necessary, but attendees are expected to follow the FOSDEM's code of conduct [7]. Important Dates Recap * 2020-12-26: Deadline for talk proposal submission * 2020-12-31: Schedule published and speakers notified of acceptance * mid January 2021: Time frame for talk pre-recoding * 2021-02-06: Devroom taking place on-line Contact In case of any questions, comments and suggestions, please do not hesitate to contact the devroom organizers via the devroom's mailing list [3]. The primary organizers of the devroom in 2021 are: * Martin Decky * Jakub Jermar Links [1] https://fosdem.org/2021/ [2] https://penta.fosdem.org/submission/FOSDEM21/ [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://archive.fosdem.org/2012/schedule/track/microkernel_os_devroom.html [5] http://fosdem.microkernel.info/ [6] https://fosdem.org/ [7] https://fosdem.org/2021/practical/conduct/

1 0

More enhancements for general-purpose systems that wouldn't be accepted into seL4?
by Andrew Warkentin 06 Dec '20

06 Dec '20

Am I correct to assume that support for running 32-bit code on a 64-bit kernel using compatibility mode rather than virtualization and support for (presumably limited) direct system calls from VMs, bypassing any user-mode VMM (using something like Xen's trampoline page) wouldn't be accepted into seL4? These are yet more things that I am going to want at some point and can't think of any other way to do them (besides adding them to the kernel) without significant penalties to hardware compatibility (in the case of the 32-bit support; while UX/RT will mostly be focused on 64-bit systems, it will support 32-bit Linux programs in its compatibility layer) or performance (in the case of direct kernel traps from VMs; I am planning to write a dynamic general-purpose hypervisor to go with UX/RT eventually, and adding an extra trap into the VMM on every IPC would likely add a fair bit of overhead).

4 8

whether seL4 support c++ code
by yadong.li 03 Dec '20

03 Dec '20

Hi， I have two questions about whether seL4 support C++: 1. When we create a component, whether the src file of component can be c++ style file like **.cxx, or **.cpp ? I found it will print “camkes.environment.c : undefined reference to run” error when compile 2. If our app code write by c++, how can I use it in seL4 environment as native component？Is there some example ？ Thank you very much.

3 2

repo move from sel4proj to sel4 on github
by Klein, Gerwin (Data61, Kensington NSW) 01 Dec '20

01 Dec '20

As some may have already noticed, we have moved a few repositories from github.com/sel4proj/ to github.com/seL4/ recently, This is part of the hand-over of these repositories to the seL4 foundation. Github will forward all related URLs and git operations etc, so there is nothing really that you need to do, and old manifests and repo collections should continue to work as before. For those who would still like to update their mirrors or own manifests to avoid the redirect, below the list of repos that were moved: sel4-tutorials-manifest polyml seL4-CAmkES-L4v-dockerfiles camkes-arm-vm-manifest sel4webserver-manifest rumprun-sel4-demoapps camkes-vm-linux riscv-pk camkes-arm-vm cakeml_libs rumprun-packages seL4_projects_libs sel4-tutorials global-components camkes-vm-images projects_libs sel4webserver sel4runtime rumprun HOL camkes-vm-apps mcs-examples-manifest mcs-examples picotcp picotcp-bsd Cheers, Gerwin

1 0

Building a simple RISC-V project
by porter.188＠osu.edu 30 Nov '20

30 Nov '20

I am trying to build a simple RISC-V seL4 project. I mean "hello world" simple. I using version 12.0.0. I looked at the documentation here https://docs.sel4.systems/projects/buildsystem/incorporating.html to follow what the project layout is. I also followed this project for x86 v10.0.0. https://github.com/manu88/SeL4_101 I was able rebuild this last one for RISC-V after modifying the CMakeLists.txt to include the proper libraries in my hello project. When I try to use the seL4 12.0.0 kernel there are some configuration differences that I haven't figured out yet. Can anyone shed some light on what the parameters are that need to be set for RISC-V? The verified config in ../kernel/configs/RISCV64_verified.cmake are this, is this all that need set? I suppose these could be modified as necessary. 12 set(KernelSel4Arch "riscv64" CACHE STRING "") 13 set(KernelPlatform "hifive" CACHE STRING "") 14 set(KernelPTLevels "3" CACHE STRING "") 15 set(KernelVerificationBuild ON CACHE BOOL "") 16 set(KernelMaxNumNodes "1" CACHE STRING "") 17 set(KernelOptimisation "-O2" CACHE STRING "") 18 set(KernelRetypeFanOutLimit "256" CACHE STRING "") 19 set(KernelBenchmarks "none" CACHE STRING "") 20 set(KernelDangerousCodeInjection OFF CACHE BOOL "") 21 set(KernelFastpath ON CACHE BOOL "") 22 set(KernelPrinting OFF CACHE BOOL "") 23 set(KernelNumDomains 16 CACHE STRING "") 24 set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "") 25 set(KernelRootCNodeSizeBits 19 CACHE STRING "") 26 set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")

2 1

CAmKes Ethdriver Odroid-C2
by Nkem Ogosi 26 Nov '20

26 Nov '20

Hi all, I'm trying to add an odroid-c2 ethdriver implementation and I'm quite confused bout an error im getting. ERROR:CAmkES:CPP failed: /home/nkem/learningHydra/projects/global-components/components/Ethdriver/Ethdriver.camkes:13:10: fatal error: plat/eth_devices.h: No such file or directory ERROR:CAmkES: #include <plat/eth_devices.h> ERROR:CAmkES: ^~~~~~~~~~~~~~~~~~~~ ERROR:CAmkES:compilation terminated. ERROR:CAmkES: CMake Error at /home/nkem/learningHydra/projects/camkes-tool/camkes.cmake:545 (message): Failed to generate /home/nkem/learningHydra/build/ast.pickle Call Stack (most recent call first): It suggests I'm missing the eth_devices header for the odroid-c2 platform but I think I have added all the necessary files in the correct folders. Is there any way to know exactly what files I need or where to look to debug this issue. Thanks, Nkem

2 1

Re: Quotation
by Chubb, Peter (Data61, Kensington NSW) 25 Nov '20

25 Nov '20

>>>>> "Andrew" == Andrew Warkentin <andreww591(a)gmail.com> writes: Andrew> How are these spammers getting onto the list? Is there some Andrew> kind of configuration issue? The person sending it subscribed then unsubscribed. I've temporarily set all messages to moderated to try to catch any others who are doing this. PeterC -- Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group CSIRO's Data61

1 0

Connectivity of 2 sel4 powered systems
by ogosinkem＠gmail.com 24 Nov '20

24 Nov '20

Hi all, I asked earlier about how to connect the odroid-c2 board via Ethernet and I was wondering what additional files I would need to get a CAmkES implementation of an ethernet driver working for this board. Thanks, Nkem Ogosi

1 0

Possibility of adding a system call origin limit similar to that of OpenBSD?
by Andrew Warkentin 23 Nov '20

23 Nov '20

I am wanting to implement a system call origin limit (akin to that of OpenBSD) in UX/RT. This could probably be accomplished by adding a "set system call range" TCB method that takes the start and end addresses of the range in which system calls will be permitted without interception. Any system call issued from code outside this range would incur a user exception (which would provide all the state required for user code to handle the system call and resume the thread if desired). UX/RT will require all binaries to be dynamically linked with a minimal "libroot" library that will contain an IPC transport layer that will be the only part of the system outside the root server that makes direct system calls. This will make it easier for later versions to retain backwards compatibility. Limiting system call origin should also make certain kinds of attacks more difficult. I am also planning to use the system call origin limit in the Linux compatibility environment in order to distinguish Linux syscalls from seL4 ones, since Linux syscalls will never come from libroot. Each process in the Linux compatibility environment will have a fault handler thread that looks up the syscall and calls the corresponding UX/RT APIs, and will also replace the trap with a call to a jump table if the function containing it is a known syscall wrapper in order to cut down on the number of trips through the kernel. Would it be possible to add something like this to the mainline seL4 tree?

4 7

Proposed future Core Platform extension: hosting other seL4-native OSs
by Demi M. Obenour 23 Nov '20

23 Nov '20

While reading Andrew’s message on syscall origin checking, I realized that UX/RT could potentially replace Linux VMs in Core Platform applications. I imagine that this would require changes to both the Core Platform and UX/RT. Andrew, would you be interested in adding a hosting interface to UX/RT, so that static systems such as the Core Platform can use UX/RT as a Linux VM replacement? UX/RT seems like a fantastic alternative, with both better security and (eventually) better performance. I would imagine that it also would use less memory than a Linux VM. Gernot (and the rest of the seL4 team): would it be possible to support running other seL4-based systems as protection domains in a future version of the Core Platform? Such systems would be opaque from the Core Platform’s perspective, but they might need capabilities that normal protection domains are not provided. Of course, they would not be granted any capabilities that would allow them to violate system security. Yes, I know that one can run seL4 in a VM, but it seems rather wasteful to do so. Sincerely, Demi

3 2

RFC-5: seL4 Core Platform
by Gernot Heiser 23 Nov '20

23 Nov '20

Dear seL4 Community, Those who attended today’s closing session at the seL4 Summit have heard about this, for the rest I’m pleased to announce that we have an RFC out for the seL4 Core Platform, a minimal seL4-based OS for embedded/cyberphysical/IoT applications, see https://sel4.atlassian.net/browse/RFC-5 Feedback welcome. Gernot

6 16

Issues with PR
by Iker Galardi 22 Nov '20

22 Nov '20

Hi! I'm having certain issues with the PR where I propose another way to get the gic cpu id directly from hardware registers instead of guessing like before. First of all, inside CI/Links some errors appear about sel4 webpage links that I haven't touched, how can I solve this? At last, on the PR/Preprocess test failure appears but it's not clear what the problem is and after the compilation test is successful. Thanks for your time. Sincerely, Iker Galardi.

3 4

RCF-6: seL4 Core
by Gernot Heiser 22 Nov '20

22 Nov '20

Dear seL4 Community, There is a second RFC just released, for the seL4 Core, a policy-free runtime and build environment for “plain” seL4, see https://sel4.atlassian.net/browse/RFC-6 Again, we are looking for feedback. Gernot

3 2

QEMU vs Spike on RISC-V Debugging
by Porter, Jeremy 20 Nov '20

20 Nov '20

I've built a simple hello for RISC-V. It runs in Spike as expected. In QEMU it doesn't run. It stops at loading the kernel in elfloader/src/common.c at the lines below: 199 printf("ELF-loading 199\n"); 200 /* Copy the data. */ 201 unpack_elf_to_paddr(elf, dest_paddr); I'd really like to use QEMU/GDB to debug my kernel. Can anyone shed some light on what's happening here? The failed output from QEMU looks like this: user@user-KVM:/mnt/data/femur/build$ qemu-system-riscv64 --machine spike --nographic --bios images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 The output from spike is the same but complete: ser@user-KVM:/mnt/data/femur/build$ /mnt/data/rocket-tools/bin/spike images/hello-image-riscv-spike bbl loader ELF-loader started on paddr=[80200000..802fb90f] ELF-loading image 'kernel' paddr=[c0000000..c0026fff] vaddr=[ffffffff80000000..ffffffff80026fff] virt_entry=ffffffff80000000 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 ELF-loading image 'hello' paddr=[c0027000..c013afff] vaddr=[10000..123fff] virt_entry=10216 ELF-loading 187 ELF-loading 195 ELF-loading 199 ELF-loading 203 ELF-loading 211 Jumping to kernel-image entry point... 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 seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc0bffd8a00 "rootserver" halting...Power off

3 4

Re: [seL4] Simple hello for RISC-V/spike
by Porter, Jeremy 11 Nov '20

11 Nov '20

Answering my own question here--maybe this will help someone else trying to get this kind of setup running. The problem is that there are additional libraries required. The CMakeLists.txt for the hello project looks like this: cmake_minimum_required(VERSION 3.7.2) project(hello C) # create a new C project called 'Hello' add_executable(hello src/main.c) # add files to our project. Paths are relative to this file. target_link_libraries(hello sel4platsupport sel4muslcsys ) # we need to link against the standard C lib for printf # Set this image as the rootserver DeclareRootserver(hello) ---------------------------------- This works for the debug build. For the release build there is a dependency on some debugging for early print functions. I think if those are removed it might work ok.

1 0

Odroid-C2 help
by ogosinkem＠gmail.com 07 Nov '20

07 Nov '20

Hi, Ive been following all the steps at https://www.cse.unsw.edu.au/~cs9242/19/project/linux.shtml and I'm not too clear on how to put a built image on the board. Or even if I've done the whole setup correctly for that matter. Any tips would be appriecated? Thanks, Nkem Ogosi

1 0

How is CMake told to build a given app.
by Chris Koziarz 06 Nov '20

06 Nov '20

I'm setting up a new application (and the libraries coming with it) but I have hard time figuring out the process of building, esp. how CMake knows where to start building from.. By way of example, I'm trying to follow the process of setting up and building sel4test. Setting up the source dir structure: repo init -u https://github.com/seL4/sel4test-manifest.git & repo sync and creating the build dir md build & cd build Are perfectly understandable steps: create source tree that includes the app sources (./projects/sel4test/apps/sel4test-driver/ in this case) kernel (./kernel/) libraries (other subdirs under ./projects/) and misc tools (./tools/) and an extra subdir for build output The third "magic" CMake setup step ../init-build.sh -DPLATFORM=<platform> -DRELEASE=FALSE -DSIMULATION=TRUE enables a simple "ninja" command (without any params) to build an application from the sources at ./projects/sel4test/apps/sel4test-driver/ This is a mystery to me. Where is the target (sel4test-driver) specification in these steps? I looked into init-build.sh and my understanding is the CMake setup must be carried by this command: cmake -G Ninja "$@" -DSEL4_CACHE_DIR="$CACHE_DIR" -C "$project_dir/settings.cmake" "$project_dir" but I cannot figure how said command finds that the application we are trying to build is located in ./projects/sel4test/apps/sel4test-driver/ Now, when I try to setup my own app, how do I tell init-build.sh command where my app is? Thanks for any clarification, Chris

2 1

what does "#include <autoconf.h>" do and how to set the path to include it ?
by Chris Koziarz 05 Nov '20

05 Nov '20

I'm creating a new project that uses existing libraries, e.g. seL4_libs/libsel4utils, a header page_dma.h, because I want to use dma in my IO transfer. When I include header page_dma.h in question, at line 15, <autoconf.h> is pulled in. There are 100s of autoconf.h files (usually auto-generated ones in kernel binaries) and I have no idea which one should be included and how to setup -I option for gcc to include it. Can anyone educate me on it? Thanks very much! Chris ninja output: [1/9] Building C object apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj FAILED: apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj /usr/bin/ccache /usr/bin/aarch64-linux-gnu-gcc --sysroot=/home/chris/sel4_test/tqma8xqp_build -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/inc -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/config -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/../../../sel4_projects_libs/libsdhcdrivers/include/sdhc -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/../../../util_libs/libplatsupport/include -I/home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/../../../util_libs/libutils/include -Iapps/sel4test-driver/musllibc/build-temp/stage/include -march=armv8-a -D__KERNEL_64__ -g -nostdinc -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec -mstrict-align -std=gnu11 -MD -MT apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj -MF apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj.d -o apps/sel4test-driver/fat32-sel4/CMakeFiles/fat32-sel4.dir/src/interfaces/sel4.c.obj -c /home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/src/interfaces/sel4.c In file included from /home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/src/interfaces/sel4.c:12: /home/chris/sel4_test/projects/sel4test/apps/fat32-sel4/src/interfaces/../../../../../seL4_libs/libsel4utils/include/sel4utils/page_dma.h:15:10: fatal error: autoconf.h: No such file or directory 15 | #include <autoconf.h>

2 2

raspberry pi 4
by Sachin More 04 Nov '20

04 Nov '20

Hi: Thanks to Nick and Peter. I have made some progress: 1. For the kernel code, used origin/rpi4 branch from https://github.com/nspin/seL4.git 2. Used https://github.com/seL4/camkes.git for the build and replaced the kernel with the one in step 1. 3. There is no bcm2711.dts in origin/rpi4, so got one one from linux. The final version, called rpi4.dts is listed at the end this email. 4. Made changes to add rpi4 as a new platform. However, I am stumped trying to reconcile rpi4.dts and overlay-rpi4.dts. The latter contains a reference to a node /soc/gic400@40041000. The equivalent node in rpi4.dts is /sic/gicv2. But I am getting the following error from init-build.sh when it is trying to create kernel.dtb: /host/VPI/camkes-project/build/kernel/kernel.dtb: ERROR (path_references): /chosen: Reference to non-existent node or label "/soc/gicv2" Any ideas? thanks, Sachin -------------------- rpi4.dts ----------------------------- /dts-v1/; /memreserve/ 0x00000000 0x00001000; / { compatible = "brcm,bcm2835"; model = "BCM2835"; #address-cells = <1>; #size-cells = <1>; aliases { serial0 = &uart0; serial1 = &uart1; }; chosen { stdout-path = "serial0:115200n8"; }; rmem: reserved-memory { #address-cells = <1>; #size-cells = <1>; ranges; cma: linux,cma { compatible = "shared-dma-pool"; size = <0x4000000>; reusable; linux,cma-default; }; }; thermal-zones { cpu_thermal: cpu-thermal { polling-delay-passive = <0>; polling-delay = <1000>; trips { cpu-crit { temperature = <90000>; hysteresis = <0>; type = "critical"; }; }; cooling-maps { }; }; }; soc { compatible = "simple-bus"; #address-cells = <1>; #size-cells = <1>; system_timer: timer@7e003000 { compatible = "brcm,bcm2835-system-timer"; reg = <0x7e003000 0x1000>; interrupts = <1 0>, <1 1>, <1 2>, <1 3>; clock-frequency = <1000000>; }; txp: txp@7e004000 { compatible = "brcm,bcm2835-txp"; reg = <0x7e004000 0x20>; interrupts = <1 11>; }; clocks: cprman@7e101000 { compatible = "brcm,bcm2835-cprman"; #clock-cells = <1>; reg = <0x7e101000 0x2000>; clocks = <&clk_osc>, <&dsi0 0>, <&dsi0 1>, <&dsi0 2>, <&dsi1 0>, <&dsi1 1>, <&dsi1 2>; }; mailbox: mailbox@7e00b880 { compatible = "brcm,bcm2835-mbox"; reg = <0x7e00b880 0x40>; interrupts = <0 1>; #mbox-cells = <0>; }; gpio: gpio@7e200000 { compatible = "brcm,bcm2835-gpio"; reg = <0x7e200000 0xb4>; interrupts = <2 17>, <2 18>, <2 19>, <2 20>; gpio-controller; #gpio-cells = <2>; interrupt-controller; #interrupt-cells = <2>; dpi_gpio0: dpi_gpio0 { brcm,pins = <0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27>; brcm,function = <6>; }; emmc_gpio22: emmc_gpio22 { brcm,pins = <22 23 24 25 26 27>; brcm,function = <7>; }; emmc_gpio34: emmc_gpio34 { brcm,pins = <34 35 36 37 38 39>; brcm,function = <7>; brcm,pull = <0 2 2 2 2 2>; }; emmc_gpio48: emmc_gpio48 { brcm,pins = <48 49 50 51 52 53>; brcm,function = <7>; }; gpclk0_gpio4: gpclk0_gpio4 { brcm,pins = <4>; brcm,function = <4>; }; gpclk1_gpio5: gpclk1_gpio5 { brcm,pins = <5>; brcm,function = <4>; }; gpclk1_gpio42: gpclk1_gpio42 { brcm,pins = <42>; brcm,function = <4>; }; gpclk1_gpio44: gpclk1_gpio44 { brcm,pins = <44>; brcm,function = <4>; }; gpclk2_gpio6: gpclk2_gpio6 { brcm,pins = <6>; brcm,function = <4>; }; gpclk2_gpio43: gpclk2_gpio43 { brcm,pins = <43>; brcm,function = <4>; brcm,pull = <0>; }; i2c0_gpio0: i2c0_gpio0 { brcm,pins = <0 1>; brcm,function = <4>; }; i2c0_gpio28: i2c0_gpio28 { brcm,pins = <28 29>; brcm,function = <4>; }; i2c0_gpio44: i2c0_gpio44 { brcm,pins = <44 45>; brcm,function = <5>; }; i2c1_gpio2: i2c1_gpio2 { brcm,pins = <2 3>; brcm,function = <4>; }; i2c1_gpio44: i2c1_gpio44 { brcm,pins = <44 45>; brcm,function = <6>; }; jtag_gpio22: jtag_gpio22 { brcm,pins = <22 23 24 25 26 27>; brcm,function = <3>; }; pcm_gpio18: pcm_gpio18 { brcm,pins = <18 19 20 21>; brcm,function = <4>; }; pcm_gpio28: pcm_gpio28 { brcm,pins = <28 29 30 31>; brcm,function = <6>; }; sdhost_gpio48: sdhost_gpio48 { brcm,pins = <48 49 50 51 52 53>; brcm,function = <4>; }; spi0_gpio7: spi0_gpio7 { brcm,pins = <7 8 9 10 11>; brcm,function = <4>; }; spi0_gpio35: spi0_gpio35 { brcm,pins = <35 36 37 38 39>; brcm,function = <4>; }; spi1_gpio16: spi1_gpio16 { brcm,pins = <16 17 18 19 20 21>; brcm,function = <3>; }; spi2_gpio40: spi2_gpio40 { brcm,pins = <40 41 42 43 44 45>; brcm,function = <3>; }; uart0_gpio14: uart0_gpio14 { brcm,pins = <14 15>; brcm,function = <4>; }; uart0_ctsrts_gpio16: uart0_ctsrts_gpio16 { brcm,pins = <16 17>; brcm,function = <7>; }; uart0_ctsrts_gpio30: uart0_ctsrts_gpio30 { brcm,pins = <30 31>; brcm,function = <7>; brcm,pull = <2 0>; }; uart0_gpio32: uart0_gpio32 { brcm,pins = <32 33>; brcm,function = <7>; brcm,pull = <0 2>; }; uart0_gpio36: uart0_gpio36 { brcm,pins = <36 37>; brcm,function = <6>; }; uart0_ctsrts_gpio38: uart0_ctsrts_gpio38 { brcm,pins = <38 39>; brcm,function = <6>; }; uart1_gpio14: uart1_gpio14 { brcm,pins = <14 15>; brcm,function = <2>; }; uart1_ctsrts_gpio16: uart1_ctsrts_gpio16 { brcm,pins = <16 17>; brcm,function = <2>; }; uart1_gpio32: uart1_gpio32 { brcm,pins = <32 33>; brcm,function = <2>; }; uart1_ctsrts_gpio30: uart1_ctsrts_gpio30 { brcm,pins = <30 31>; brcm,function = <2>; }; uart1_gpio40: uart1_gpio40 { brcm,pins = <40 41>; brcm,function = <2>; }; uart1_ctsrts_gpio42: uart1_ctsrts_gpio42 { brcm,pins = <42 43>; brcm,function = <2>; }; }; uart0: serial@7e201000 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201000 0x200>; interrupts = <2 25>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; }; sdhost: mmc@7e202000 { compatible = "brcm,bcm2835-sdhost"; reg = <0x7e202000 0x100>; interrupts = <2 24>; clocks = <&clocks 20>; status = "disabled"; }; i2s: i2s@7e203000 { compatible = "brcm,bcm2835-i2s"; reg = <0x7e203000 0x24>; clocks = <&clocks 31>; status = "disabled"; }; spi: spi@7e204000 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204000 0x200>; interrupts = <2 22>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c0: i2c@7e205000 { compatible = "brcm,bcm2835-i2c"; reg = <0x7e205000 0x200>; interrupts = <2 21>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; dpi: dpi@7e208000 { compatible = "brcm,bcm2835-dpi"; reg = <0x7e208000 0x8c>; clocks = <&clocks 20>, <&clocks 44>; clock-names = "core", "pixel"; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; dsi0: dsi@7e209000 { compatible = "brcm,bcm2835-dsi0"; reg = <0x7e209000 0x78>; interrupts = <2 4>; #address-cells = <1>; #size-cells = <0>; #clock-cells = <1>; clocks = <&clocks 32>, <&clocks 47>, <&clocks 49>; clock-names = "phy", "escape", "pixel"; clock-output-names = "dsi0_byte", "dsi0_ddr2", "dsi0_ddr"; status = "disabled"; }; aux: aux@7e215000 { compatible = "brcm,bcm2835-aux"; #clock-cells = <1>; reg = <0x7e215000 0x8>; clocks = <&clocks 20>; }; uart1: serial@7e215040 { compatible = "brcm,bcm2835-aux-uart"; reg = <0x7e215040 0x40>; interrupts = <1 29>; clocks = <&aux 0>; status = "disabled"; }; spi1: spi@7e215080 { compatible = "brcm,bcm2835-aux-spi"; reg = <0x7e215080 0x40>; interrupts = <1 29>; clocks = <&aux 1>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi2: spi@7e2150c0 { compatible = "brcm,bcm2835-aux-spi"; reg = <0x7e2150c0 0x40>; interrupts = <1 29>; clocks = <&aux 2>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; pwm: pwm@7e20c000 { compatible = "brcm,bcm2835-pwm"; reg = <0x7e20c000 0x28>; clocks = <&clocks 30>; assigned-clocks = <&clocks 30>; assigned-clock-rates = <10000000>; #pwm-cells = <2>; status = "disabled"; }; sdhci: sdhci@7e300000 { compatible = "brcm,bcm2835-sdhci"; reg = <0x7e300000 0x100>; interrupts = <2 30>; clocks = <&clocks 28>; status = "disabled"; }; hvs@7e400000 { compatible = "brcm,bcm2835-hvs"; reg = <0x7e400000 0x6000>; interrupts = <2 1>; }; dsi1: dsi@7e700000 { compatible = "brcm,bcm2835-dsi1"; reg = <0x7e700000 0x8c>; interrupts = <2 12>; #address-cells = <1>; #size-cells = <0>; #clock-cells = <1>; clocks = <&clocks 35>, <&clocks 48>, <&clocks 50>; clock-names = "phy", "escape", "pixel"; clock-output-names = "dsi1_byte", "dsi1_ddr2", "dsi1_ddr"; status = "disabled"; }; i2c1: i2c@7e804000 { compatible = "brcm,bcm2835-i2c"; reg = <0x7e804000 0x1000>; interrupts = <2 21>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; vec: vec@7e806000 { compatible = "brcm,bcm2835-vec"; reg = <0x7e806000 0x1000>; clocks = <&clocks 24>; interrupts = <2 27>; status = "disabled"; }; usb: usb@7e980000 { compatible = "brcm,bcm2835-usb"; reg = <0x7e980000 0x10000>; interrupts = <1 9>; #address-cells = <1>; #size-cells = <0>; clocks = <&clk_usb>; clock-names = "otg"; phys = <&usbphy>; phy-names = "usb2-phy"; }; }; clocks { clk_osc: clk-osc { compatible = "fixed-clock"; #clock-cells = <0>; clock-output-names = "osc"; clock-frequency = <19200000>; }; clk_usb: clk-usb { compatible = "fixed-clock"; #clock-cells = <0>; clock-output-names = "otg"; clock-frequency = <480000000>; }; }; usbphy: phy { compatible = "usb-nop-xceiv"; #phy-cells = <0>; }; }; / { compatible = "brcm,bcm2711"; #address-cells = <2>; #size-cells = <1>; interrupt-parent = <&gicv2>; vc4: gpu { compatible = "brcm,bcm2711-vc5"; status = "disabled"; }; clk_27MHz: clk-27M { #clock-cells = <0>; compatible = "fixed-clock"; clock-frequency = <27000000>; clock-output-names = "27MHz-clock"; }; clk_108MHz: clk-108M { #clock-cells = <0>; compatible = "fixed-clock"; clock-frequency = <108000000>; clock-output-names = "108MHz-clock"; }; soc { ranges = <0x7e000000 0x0 0xfe000000 0x01800000>, <0x7c000000 0x0 0xfc000000 0x02000000>, <0x40000000 0x0 0xff800000 0x00800000>; dma-ranges = <0xc0000000 0x0 0x00000000 0x40000000>; local_intc: local_intc@40000000 { compatible = "brcm,bcm2836-l1-intc"; reg = <0x40000000 0x100>; }; gicv2: interrupt-controller@40041000 { interrupt-controller; #interrupt-cells = <3>; compatible = "arm,gic-400"; reg = <0x40041000 0x1000>, <0x40042000 0x2000>, <0x40044000 0x2000>, <0x40046000 0x2000>; interrupts = <1 9 ((((1 << (4)) - 1) << 8) | 4)>; }; avs_monitor: avs-monitor@7d5d2000 { compatible = "brcm,bcm2711-avs-monitor", "syscon", "simple-mfd"; reg = <0x7d5d2000 0xf00>; thermal: thermal { compatible = "brcm,bcm2711-thermal"; #thermal-sensor-cells = <0>; }; }; dma: dma@7e007000 { compatible = "brcm,bcm2835-dma"; reg = <0x7e007000 0xb00>; interrupts = <0 80 4>, <0 81 4>, <0 82 4>, <0 83 4>, <0 84 4>, <0 85 4>, <0 86 4>, <0 87 4>, <0 87 4>, <0 88 4>, <0 88 4>; interrupt-names = "dma0", "dma1", "dma2", "dma3", "dma4", "dma5", "dma6", "dma7", "dma8", "dma9", "dma10"; #dma-cells = <1>; brcm,dma-channel-mask = <0x07f5>; }; pm: watchdog@7e100000 { compatible = "brcm,bcm2835-pm", "brcm,bcm2835-pm-wdt"; #power-domain-cells = <1>; #reset-cells = <1>; reg = <0x7e100000 0x114>, <0x7e00a000 0x24>, <0x7ec11000 0x20>; clocks = <&clocks 21>, <&clocks 29>, <&clocks 23>, <&clocks 22>; clock-names = "v3d", "peri_image", "h264", "isp"; system-power-controller; }; rng@7e104000 { compatible = "brcm,bcm2711-rng200"; reg = <0x7e104000 0x28>; }; uart2: serial@7e201400 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201400 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; uart3: serial@7e201600 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201600 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; uart4: serial@7e201800 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201800 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; uart5: serial@7e201a00 { compatible = "arm,pl011", "arm,primecell"; reg = <0x7e201a00 0x200>; interrupts = <0 121 4>; clocks = <&clocks 19>, <&clocks 20>; clock-names = "uartclk", "apb_pclk"; arm,primecell-periphid = <0x00241011>; status = "disabled"; }; spi3: spi@7e204600 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204600 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi4: spi@7e204800 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204800 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi5: spi@7e204a00 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204a00 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; spi6: spi@7e204c00 { compatible = "brcm,bcm2835-spi"; reg = <0x7e204c00 0x0200>; interrupts = <0 118 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c3: i2c@7e205600 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205600 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c4: i2c@7e205800 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205800 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c5: i2c@7e205a00 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205a00 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; i2c6: i2c@7e205c00 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; reg = <0x7e205c00 0x200>; interrupts = <0 117 4>; clocks = <&clocks 20>; #address-cells = <1>; #size-cells = <0>; status = "disabled"; }; pixelvalve0: pixelvalve@7e206000 { compatible = "brcm,bcm2711-pixelvalve0"; reg = <0x7e206000 0x100>; interrupts = <0 109 4>; status = "disabled"; }; pixelvalve1: pixelvalve@7e207000 { compatible = "brcm,bcm2711-pixelvalve1"; reg = <0x7e207000 0x100>; interrupts = <0 110 4>; status = "disabled"; }; pixelvalve2: pixelvalve@7e20a000 { compatible = "brcm,bcm2711-pixelvalve2"; reg = <0x7e20a000 0x100>; interrupts = <0 101 4>; status = "disabled"; }; pwm1: pwm@7e20c800 { compatible = "brcm,bcm2835-pwm"; reg = <0x7e20c800 0x28>; clocks = <&clocks 30>; assigned-clocks = <&clocks 30>; assigned-clock-rates = <10000000>; #pwm-cells = <2>; status = "disabled"; }; pixelvalve4: pixelvalve@7e216000 { compatible = "brcm,bcm2711-pixelvalve4"; reg = <0x7e216000 0x100>; interrupts = <0 110 4>; status = "disabled"; }; hvs: hvs@7e400000 { compatible = "brcm,bcm2711-hvs"; interrupts = <0 97 4>; }; pixelvalve3: pixelvalve@7ec12000 { compatible = "brcm,bcm2711-pixelvalve3"; reg = <0x7ec12000 0x100>; interrupts = <0 106 4>; status = "disabled"; }; dvp: clock@7ef00000 { compatible = "brcm,brcm2711-dvp"; reg = <0x7ef00000 0x10>; clocks = <&clk_108MHz>; #clock-cells = <1>; #reset-cells = <1>; }; hdmi0: hdmi@7ef00700 { compatible = "brcm,bcm2711-hdmi0"; reg = <0x7ef00700 0x300>, <0x7ef00300 0x200>, <0x7ef00f00 0x80>, <0x7ef00f80 0x80>, <0x7ef01b00 0x200>, <0x7ef01f00 0x400>, <0x7ef00200 0x80>, <0x7ef04300 0x100>, <0x7ef20000 0x100>; reg-names = "hdmi", "dvp", "phy", "rm", "packet", "metadata", "csc", "cec", "hd"; clock-names = "hdmi", "bvb", "audio", "cec"; resets = <&dvp 0>; ddc = <&ddc0>; dmas = <&dma 10>; dma-names = "audio-rx"; status = "disabled"; }; ddc0: i2c@7ef04500 { compatible = "brcm,bcm2711-hdmi-i2c"; reg = <0x7ef04500 0x100>, <0x7ef00b00 0x300>; reg-names = "bsc", "auto-i2c"; clock-frequency = <97500>; status = "disabled"; }; hdmi1: hdmi@7ef05700 { compatible = "brcm,bcm2711-hdmi1"; reg = <0x7ef05700 0x300>, <0x7ef05300 0x200>, <0x7ef05f00 0x80>, <0x7ef05f80 0x80>, <0x7ef06b00 0x200>, <0x7ef06f00 0x400>, <0x7ef00280 0x80>, <0x7ef09300 0x100>, <0x7ef20000 0x100>; reg-names = "hdmi", "dvp", "phy", "rm", "packet", "metadata", "csc", "cec", "hd"; ddc = <&ddc1>; clock-names = "hdmi", "bvb", "audio", "cec"; resets = <&dvp 1>; dmas = <&dma 17>; dma-names = "audio-rx"; status = "disabled"; }; ddc1: i2c@7ef09500 { compatible = "brcm,bcm2711-hdmi-i2c"; reg = <0x7ef09500 0x100>, <0x7ef05b00 0x300>; reg-names = "bsc", "auto-i2c"; clock-frequency = <97500>; status = "disabled"; }; }; emmc2bus: emmc2bus { compatible = "simple-bus"; #address-cells = <2>; #size-cells = <1>; ranges = <0x0 0x7e000000 0x0 0xfe000000 0x01800000>; dma-ranges = <0x0 0xc0000000 0x0 0x00000000 0x40000000>; emmc2: emmc2@7e340000 { compatible = "brcm,bcm2711-emmc2"; reg = <0x0 0x7e340000 0x100>; interrupts = <0 126 4>; clocks = <&clocks 51>; status = "disabled"; }; }; arm-pmu { compatible = "arm,cortex-a72-pmu", "arm,armv8-pmuv3"; interrupts = <0 16 4>, <0 17 4>, <0 18 4>, <0 19 4>; interrupt-affinity = <&cpu0>, <&cpu1>, <&cpu2>, <&cpu3>; }; timer { compatible = "arm,armv8-timer"; interrupts = <1 13 ((((1 << (4)) - 1) << 8) | 8)>, <1 14 ((((1 << (4)) - 1) << 8) | 8)>, <1 11 ((((1 << (4)) - 1) << 8) | 8)>, <1 10 ((((1 << (4)) - 1) << 8) | 8)>; arm,cpu-registers-not-fw-configured; }; cpus: cpus { #address-cells = <1>; #size-cells = <0>; enable-method = "brcm,bcm2836-smp"; cpu0: cpu@0 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <0>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000d8>; }; cpu1: cpu@1 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <1>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000e0>; }; cpu2: cpu@2 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <2>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000e8>; }; cpu3: cpu@3 { device_type = "cpu"; compatible = "arm,cortex-a72"; reg = <3>; enable-method = "spin-table"; cpu-release-addr = <0x0 0x000000f0>; }; }; scb { compatible = "simple-bus"; #address-cells = <2>; #size-cells = <1>; ranges = <0x0 0x7c000000 0x0 0xfc000000 0x03800000>, <0x6 0x00000000 0x6 0x00000000 0x40000000>; pcie0: pcie@7d500000 { compatible = "brcm,bcm2711-pcie"; reg = <0x0 0x7d500000 0x9310>; device_type = "pci"; #address-cells = <3>; #interrupt-cells = <1>; #size-cells = <2>; interrupts = <0 148 4>, <0 148 4>; interrupt-names = "pcie", "msi"; interrupt-map-mask = <0x0 0x0 0x0 0x7>; interrupt-map = <0 0 0 1 &gicv2 0 143 4>; msi-controller; msi-parent = <&pcie0>; ranges = <0x02000000 0x0 0xf8000000 0x6 0x00000000 0x0 0x04000000>; dma-ranges = <0x02000000 0x0 0x00000000 0x0 0x00000000 0x0 0xc0000000>; brcm,enable-ssc; }; genet: ethernet@7d580000 { compatible = "brcm,bcm2711-genet-v5"; reg = <0x0 0x7d580000 0x10000>; #address-cells = <0x1>; #size-cells = <0x1>; interrupts = <0 157 4>, <0 158 4>; status = "disabled"; genet_mdio: mdio@e14 { compatible = "brcm,genet-mdio-v5"; reg = <0xe14 0x8>; reg-names = "mdio"; #address-cells = <0x0>; #size-cells = <0x1>; }; }; }; }; &clk_osc { clock-frequency = <54000000>; }; &clocks { compatible = "brcm,bcm2711-cprman"; }; &cpu_thermal { coefficients = <(-487) 410040>; thermal-sensors = <&thermal>; }; &dsi0 { interrupts = <0 100 4>; }; &dsi1 { interrupts = <0 108 4>; }; &gpio { compatible = "brcm,bcm2711-gpio"; interrupts = <0 113 4>, <0 114 4>, <0 115 4>, <0 116 4>; gpclk0_gpio49: gpclk0_gpio49 { pin-gpclk { pins = "gpio49"; function = "alt1"; bias-disable; }; }; gpclk1_gpio50: gpclk1_gpio50 { pin-gpclk { pins = "gpio50"; function = "alt1"; bias-disable; }; }; gpclk2_gpio51: gpclk2_gpio51 { pin-gpclk { pins = "gpio51"; function = "alt1"; bias-disable; }; }; i2c0_gpio46: i2c0_gpio46 { pin-sda { function = "alt0"; pins = "gpio46"; bias-pull-up; }; pin-scl { function = "alt0"; pins = "gpio47"; bias-disable; }; }; i2c1_gpio46: i2c1_gpio46 { pin-sda { function = "alt1"; pins = "gpio46"; bias-pull-up; }; pin-scl { function = "alt1"; pins = "gpio47"; bias-disable; }; }; i2c3_gpio2: i2c3_gpio2 { pin-sda { function = "alt5"; pins = "gpio2"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio3"; bias-disable; }; }; i2c3_gpio4: i2c3_gpio4 { pin-sda { function = "alt5"; pins = "gpio4"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio5"; bias-disable; }; }; i2c4_gpio6: i2c4_gpio6 { pin-sda { function = "alt5"; pins = "gpio6"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio7"; bias-disable; }; }; i2c4_gpio8: i2c4_gpio8 { pin-sda { function = "alt5"; pins = "gpio8"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio9"; bias-disable; }; }; i2c5_gpio10: i2c5_gpio10 { pin-sda { function = "alt5"; pins = "gpio10"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio11"; bias-disable; }; }; i2c5_gpio12: i2c5_gpio12 { pin-sda { function = "alt5"; pins = "gpio12"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio13"; bias-disable; }; }; i2c6_gpio0: i2c6_gpio0 { pin-sda { function = "alt5"; pins = "gpio0"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio1"; bias-disable; }; }; i2c6_gpio22: i2c6_gpio22 { pin-sda { function = "alt5"; pins = "gpio22"; bias-pull-up; }; pin-scl { function = "alt5"; pins = "gpio23"; bias-disable; }; }; i2c_slave_gpio8: i2c_slave_gpio8 { pins-i2c-slave { pins = "gpio8", "gpio9", "gpio10", "gpio11"; function = "alt3"; }; }; jtag_gpio48: jtag_gpio48 { pins-jtag { pins = "gpio48", "gpio49", "gpio50", "gpio51", "gpio52", "gpio53"; function = "alt4"; }; }; mii_gpio28: mii_gpio28 { pins-mii { pins = "gpio28", "gpio29", "gpio30", "gpio31"; function = "alt4"; }; }; mii_gpio36: mii_gpio36 { pins-mii { pins = "gpio36", "gpio37", "gpio38", "gpio39"; function = "alt5"; }; }; pcm_gpio50: pcm_gpio50 { pins-pcm { pins = "gpio50", "gpio51", "gpio52", "gpio53"; function = "alt2"; }; }; pwm0_0_gpio12: pwm0_0_gpio12 { pin-pwm { pins = "gpio12"; function = "alt0"; bias-disable; }; }; pwm0_0_gpio18: pwm0_0_gpio18 { pin-pwm { pins = "gpio18"; function = "alt5"; bias-disable; }; }; pwm1_0_gpio40: pwm1_0_gpio40 { pin-pwm { pins = "gpio40"; function = "alt0"; bias-disable; }; }; pwm0_1_gpio13: pwm0_1_gpio13 { pin-pwm { pins = "gpio13"; function = "alt0"; bias-disable; }; }; pwm0_1_gpio19: pwm0_1_gpio19 { pin-pwm { pins = "gpio19"; function = "alt5"; bias-disable; }; }; pwm1_1_gpio41: pwm1_1_gpio41 { pin-pwm { pins = "gpio41"; function = "alt0"; bias-disable; }; }; pwm0_1_gpio45: pwm0_1_gpio45 { pin-pwm { pins = "gpio45"; function = "alt0"; bias-disable; }; }; pwm0_0_gpio52: pwm0_0_gpio52 { pin-pwm { pins = "gpio52"; function = "alt1"; bias-disable; }; }; pwm0_1_gpio53: pwm0_1_gpio53 { pin-pwm { pins = "gpio53"; function = "alt1"; bias-disable; }; }; rgmii_gpio35: rgmii_gpio35 { pin-start-stop { pins = "gpio35"; function = "alt4"; }; pin-rx-ok { pins = "gpio36"; function = "alt4"; }; }; rgmii_irq_gpio34: rgmii_irq_gpio34 { pin-irq { pins = "gpio34"; function = "alt5"; }; }; rgmii_irq_gpio39: rgmii_irq_gpio39 { pin-irq { pins = "gpio39"; function = "alt4"; }; }; rgmii_mdio_gpio28: rgmii_mdio_gpio28 { pins-mdio { pins = "gpio28", "gpio29"; function = "alt5"; }; }; rgmii_mdio_gpio37: rgmii_mdio_gpio37 { pins-mdio { pins = "gpio37", "gpio38"; function = "alt4"; }; }; spi0_gpio46: spi0_gpio46 { pins-spi { pins = "gpio46", "gpio47", "gpio48", "gpio49"; function = "alt2"; }; }; spi2_gpio46: spi2_gpio46 { pins-spi { pins = "gpio46", "gpio47", "gpio48", "gpio49", "gpio50"; function = "alt5"; }; }; spi3_gpio0: spi3_gpio0 { pins-spi { pins = "gpio0", "gpio1", "gpio2", "gpio3"; function = "alt3"; }; }; spi4_gpio4: spi4_gpio4 { pins-spi { pins = "gpio4", "gpio5", "gpio6", "gpio7"; function = "alt3"; }; }; spi5_gpio12: spi5_gpio12 { pins-spi { pins = "gpio12", "gpio13", "gpio14", "gpio15"; function = "alt3"; }; }; spi6_gpio18: spi6_gpio18 { pins-spi { pins = "gpio18", "gpio19", "gpio20", "gpio21"; function = "alt3"; }; }; uart2_gpio0: uart2_gpio0 { pin-tx { pins = "gpio0"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio1"; function = "alt4"; bias-pull-up; }; }; uart2_ctsrts_gpio2: uart2_ctsrts_gpio2 { pin-cts { pins = "gpio2"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio3"; function = "alt4"; bias-disable; }; }; uart3_gpio4: uart3_gpio4 { pin-tx { pins = "gpio4"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio5"; function = "alt4"; bias-pull-up; }; }; uart3_ctsrts_gpio6: uart3_ctsrts_gpio6 { pin-cts { pins = "gpio6"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio7"; function = "alt4"; bias-disable; }; }; uart4_gpio8: uart4_gpio8 { pin-tx { pins = "gpio8"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio9"; function = "alt4"; bias-pull-up; }; }; uart4_ctsrts_gpio10: uart4_ctsrts_gpio10 { pin-cts { pins = "gpio10"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio11"; function = "alt4"; bias-disable; }; }; uart5_gpio12: uart5_gpio12 { pin-tx { pins = "gpio12"; function = "alt4"; bias-disable; }; pin-rx { pins = "gpio13"; function = "alt4"; bias-pull-up; }; }; uart5_ctsrts_gpio14: uart5_ctsrts_gpio14 { pin-cts { pins = "gpio14"; function = "alt4"; bias-pull-up; }; pin-rts { pins = "gpio15"; function = "alt4"; bias-disable; }; }; }; &rmem { #address-cells = <2>; }; &cma { alloc-ranges = <0x0 0x00000000 0x40000000>; }; &i2c0 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; interrupts = <0 117 4>; }; &i2c1 { compatible = "brcm,bcm2711-i2c", "brcm,bcm2835-i2c"; interrupts = <0 117 4>; }; &mailbox { interrupts = <0 33 4>; }; &sdhci { interrupts = <0 126 4>; }; &sdhost { interrupts = <0 120 4>; }; &spi { interrupts = <0 118 4>; }; &spi1 { interrupts = <0 93 4>; }; &spi2 { interrupts = <0 93 4>; }; &system_timer { interrupts = <0 64 4>, <0 65 4>, <0 66 4>, <0 67 4>; }; &txp { interrupts = <0 75 4>; }; &uart0 { interrupts = <0 121 4>; }; &uart1 { interrupts = <0 93 4>; }; &usb { interrupts = <0 73 4>; }; &vec { interrupts = <0 123 4>; }; / { leds { compatible = "gpio-leds"; act { label = "ACT"; default-state = "keep"; linux,default-trigger = "heartbeat"; }; }; soc { firmware: firmware { compatible = "raspberrypi,bcm2835-firmware", "simple-mfd"; #address-cells = <1>; #size-cells = <1>; mboxes = <&mailbox>; dma-ranges; }; power: power { compatible = "raspberrypi,bcm2835-power"; firmware = <&firmware>; #power-domain-cells = <1>; }; vchiq: mailbox@7e00b840 { compatible = "brcm,bcm2835-vchiq"; reg = <0x7e00b840 0x3c>; interrupts = <0 2>; }; }; }; &gpio { pinctrl-names = "default"; gpioout: gpioout { brcm,pins = <6>; brcm,function = <1>; }; alt0: alt0 { brcm,pins = <4 5 7 8 9 10 11>; brcm,function = <4>; }; }; &i2c0 { pinctrl-names = "default"; pinctrl-0 = <&i2c0_gpio0>; status = "okay"; clock-frequency = <100000>; }; &i2c1 { pinctrl-names = "default"; pinctrl-0 = <&i2c1_gpio2>; status = "okay"; clock-frequency = <100000>; }; &usb { power-domains = <&power 6>; }; &vec { power-domains = <&power 7>; status = "okay"; }; &dsi0 { power-domains = <&power 17>; }; &dsi1 { power-domains = <&power 18>; }; &usb { dr_mode = "peripheral"; g-rx-fifo-size = <256>; g-np-tx-fifo-size = <32>; g-tx-fifo-size = <256 256 512 512 512 768 768>; }; / { compatible = "raspberrypi,4-model-b", "brcm,bcm2711"; model = "Raspberry Pi 4 Model B"; chosen { stdout-path = "serial1:115200n8"; }; memory@0 { device_type = "memory"; reg = <0 0 0>; }; aliases { emmc2bus = &emmc2bus; ethernet0 = &genet; pcie0 = &pcie0; }; leds { act { gpios = <&gpio 42 0>; }; pwr { label = "PWR"; gpios = <&expgpio 2 1>; default-state = "keep"; linux,default-trigger = "default-on"; }; }; wifi_pwrseq: wifi-pwrseq { compatible = "mmc-pwrseq-simple"; reset-gpios = <&expgpio 1 1>; }; sd_io_1v8_reg: sd_io_1v8_reg { compatible = "regulator-gpio"; regulator-name = "vdd-sd-io"; regulator-min-microvolt = <1800000>; regulator-max-microvolt = <3300000>; regulator-boot-on; regulator-always-on; regulator-settling-time-us = <5000>; gpios = <&expgpio 4 0>; states = <1800000 0x1 3300000 0x0>; status = "okay"; }; sd_vcc_reg: sd_vcc_reg { compatible = "regulator-fixed"; regulator-name = "vcc-sd"; regulator-min-microvolt = <3300000>; regulator-max-microvolt = <3300000>; regulator-boot-on; enable-active-high; gpio = <&expgpio 6 0>; }; }; &ddc0 { status = "okay"; }; &ddc1 { status = "okay"; }; &firmware { firmware_clocks: clocks { compatible = "raspberrypi,firmware-clocks"; #clock-cells = <1>; }; expgpio: gpio { compatible = "raspberrypi,firmware-gpio"; gpio-controller; #gpio-cells = <2>; gpio-line-names = "BT_ON", "WL_ON", "PWR_LED_OFF", "GLOBAL_RESET", "VDD_SD_IO_SEL", "CAM_GPIO", "SD_PWR_ON", ""; status = "okay"; }; reset: reset { compatible = "raspberrypi,firmware-reset"; #reset-cells = <1>; }; }; &gpio { gpio-line-names = "ID_SDA", "ID_SCL", "SDA1", "SCL1", "GPIO_GCLK", "GPIO5", "GPIO6", "SPI_CE1_N", "SPI_CE0_N", "SPI_MISO", "SPI_MOSI", "SPI_SCLK", "GPIO12", "GPIO13", "TXD1", "RXD1", "GPIO16", "GPIO17", "GPIO18", "GPIO19", "GPIO20", "GPIO21", "GPIO22", "GPIO23", "GPIO24", "GPIO25", "GPIO26", "GPIO27", "RGMII_MDIO", "RGMIO_MDC", "CTS0", "RTS0", "TXD0", "RXD0", "SD1_CLK", "SD1_CMD", "SD1_DATA0", "SD1_DATA1", "SD1_DATA2", "SD1_DATA3", "PWM0_MISO", "PWM1_MOSI", "STATUS_LED_G_CLK", "SPIFLASH_CE_N", "SDA0", "SCL0", "RGMII_RXCLK", "RGMII_RXCTL", "RGMII_RXD0", "RGMII_RXD1", "RGMII_RXD2", "RGMII_RXD3", "RGMII_TXCLK", "RGMII_TXCTL", "RGMII_TXD0", "RGMII_TXD1", "RGMII_TXD2", "RGMII_TXD3"; }; &hdmi0 { clocks = <&firmware_clocks 13>, <&firmware_clocks 14>, <&dvp 0>, <&clk_27MHz>; clock-names = "hdmi", "bvb", "audio", "cec"; status = "okay"; }; &hdmi1 { clocks = <&firmware_clocks 13>, <&firmware_clocks 14>, <&dvp 1>, <&clk_27MHz>; clock-names = "hdmi", "bvb", "audio", "cec"; status = "okay"; }; &hvs { clocks = <&firmware_clocks 4>; }; &pixelvalve0 { status = "okay"; }; &pixelvalve1 { status = "okay"; }; &pixelvalve2 { status = "okay"; }; &pixelvalve4 { status = "okay"; }; &pwm1 { pinctrl-names = "default"; pinctrl-0 = <&pwm1_0_gpio40 &pwm1_1_gpio41>; status = "okay"; }; &sdhci { #address-cells = <1>; #size-cells = <0>; pinctrl-names = "default"; pinctrl-0 = <&emmc_gpio34>; bus-width = <4>; non-removable; mmc-pwrseq = <&wifi_pwrseq>; status = "okay"; brcmf: wifi@1 { reg = <1>; compatible = "brcm,bcm4329-fmac"; }; }; &emmc2 { vqmmc-supply = <&sd_io_1v8_reg>; vmmc-supply = <&sd_vcc_reg>; broken-cd; status = "okay"; }; &genet { phy-handle = <&phy1>; phy-mode = "rgmii-rxid"; status = "okay"; }; &genet_mdio { phy1: ethernet-phy@1 { reg = <0x1>; }; }; &pcie0 { pci@1,0 { #address-cells = <3>; #size-cells = <2>; ranges; reg = <0 0 0 0 0>; usb@1,0 { reg = <0x10000 0 0 0 0>; resets = <&reset 0>; }; }; }; &uart0 { pinctrl-names = "default"; pinctrl-0 = <&uart0_ctsrts_gpio30 &uart0_gpio32>; uart-has-rtscts; status = "okay"; bluetooth { compatible = "brcm,bcm43438-bt"; max-speed = <2000000>; shutdown-gpios = <&expgpio 0 0>; }; }; &uart1 { pinctrl-names = "default"; pinctrl-0 = <&uart1_gpio14>; status = "okay"; }; &vchiq { interrupts = <0 34 4>; }; &vc4 { status = "okay"; }; &vec { status = "disabled"; };

3 5

Odroid-C2 help
by ogosinkem＠gmail.com 03 Nov '20

03 Nov '20

Hi, I was wondering if there were any verbose guides that explain how to setup an odroid c2 board to run sel4. As a side note, are there any tools that i could use to simulate this board if need be? Thanks, Nkem Ogosi

1 0

Simple hello for RISC-V/spike
by Porter, Jeremy 03 Nov '20

03 Nov '20

I'm trying to build a simple hello world project for RISC-V/spike. I've been through the tutorials and through the sel4test for RISC-V/spike. That project is too large for what I need. I tried following this: https://github.com/manu88/SeL4_101 and modified the CMakeLists.txt to configure as required: ### SeL4_101 CMakeLists.txt ### cmake_minimum_required(VERSION 3.7.2) #message(STATUS "Femur print " ${KernelX86Sel4Arch_all_strings}) #if (${PLATFORM} IN_LIST KernelRiscVSel4Arch_all_strings) if (${PLATFORM} IN_LIST KernelRiscVPlatform_all_strings) #if (${PLATFORM} IN_LIST ${KernelX86Sel4Arch_all_strings} ${KernelARMPlatform_all_strings} ${KernelRiscVPlatform_all_strings}) set(KernelArch riscv CACHE STRING "" FORCE) set(KernelRiscVSel4Arch riscv64 CACHE STRING "" FORCE) endif() include(tools/cmake-tool/default-CMakeLists.txt) if(SIMULATION) ApplyCommonSimulationSettings("riscv64") else() if(KernelArchX86) set(KernelIOMMU ON CACHE BOOL "" FORCE) endif() endif() # We must build the debug kernel because the tutorials rely on seL4_DebugPutChar # and they don't initialize a platsupport driver. ApplyCommonReleaseVerificationSettings(FALSE FALSE) GenerateSimulateScript() ############################################################################## When I build, I get the following error: user@user-KVM:/mnt/data/femur/build$ ninja [55/90] Building C object projects/util_libs/libplatsupport/CMakeFiles/platsupport.dir/src/plat/spike/serial.c.obj ../projects/util_libs/libplatsupport/src/plat/spike/serial.c:18:28: warning: 'struct dev_defn' declared inside parameter list will not be visible outside of this definition or declaration int uart_init(const struct dev_defn* defn, ^~~~~~~~ [73/90] Linking C executable projects/hello/hello FAILED: projects/hello/hello : && ccache /mnt/data/rocket-tools/bin/riscv64-unknown-elf-gcc --sysroot=/mnt/data/femur/build -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -g -D__KERNEL_64__ -static -nostdlib -z max-page-size=0x1000 -u _sel4_start -e _sel4_start -T /mnt/data/femur/tools/cmake-tool/tls_rootserver.lds /mnt/data/femur/build/lib/crt1.o /mnt/data/femur/build/lib/crti.o /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/rv64imac/lp64/crtbegin.o projects/hello/CMakeFiles/hello.dir/src/main.c.obj -lgcc projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/util_libs/libelf/libelf.a projects/musllibc/build-temp/lib/libc.a -lgcc projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4debug/libsel4debug.a libsel4/libsel4.a projects/util_libs/libutils/libutils.a projects/util_libs/libelf/libelf.a projects/musllibc/build-temp/lib/libc.a /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/rv64imac/lp64/crtend.o /mnt/data/femur/build/lib/crtn.o -o projects/hello/hello && : /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/../../../../riscv64-unknown-elf/bin/ld: projects/seL4_libs/libsel4platsupport/libsel4platsupport.a(common.c.obj): in function `vspace_map_pages': /mnt/data/femur/build/../projects/seL4_libs/libsel4vspace/include/vspace/vspace.h:492: undefined reference to `__ctzdi2' /mnt/data/rocket-tools/lib/gcc/riscv64-unknown-elf/7.2.0/../../../../riscv64-unknown-elf/bin/ld: projects/seL4_libs/libsel4platsupport/libsel4platsupport.a(common.c.obj): in function `platsupport_alloc_device_vaddr': /mnt/data/femur/build/../projects/seL4_libs/libsel4platsupport/src/common.c:83: undefined reference to `__ctzdi2' collect2: error: ld returned 1 exit status ninja: build stopped: subcommand failed. The missing symbol is in fact in the build, it shows up in kernel_all_pp.c etc. user@user-KVM:/mnt/data/femur/build$ grep -r ctzdi2 kernel/kernel_all_pp.c:uint32_t __ctzdi2(uint64_t x); kernel/kernel_all_pp.c:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all_copy.c:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all.i:uint32_t __ctzdi2(uint64_t x); kernel/kernel_all.i:uint32_t __ctzdi2(uint64_t x) Binary file kernel/kernel.elf matches kernel/kernel_all_pp_prune_wrapper_temp.c:uint32_t __ctzdi2(uint64_t x) kernel/CMakeFiles/kernel_i_wrapper_temp_lib.dir/kernel_all_copy.c.obj:uint32_t __ctzdi2(uint64_t x); kernel/CMakeFiles/kernel_i_wrapper_temp_lib.dir/kernel_all_copy.c.obj:uint32_t __ctzdi2(uint64_t x) Binary file kernel/CMakeFiles/kernel.elf.dir/kernel_all.i.obj matches kernel/CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj:uint32_t __ctzdi2(uint64_t x); kernel/CMakeFiles/kernel_all_pp_prune_wrapper_temp_lib.dir/kernel_all_pp_prune_wrapper_temp.c.obj:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all.c:uint32_t __ctzdi2(uint64_t x) kernel/kernel_all_pp_prune.c:uint32_t __ctzdi2(uint64_t x); kernel/kernel_all_pp_prune.c:uint32_t __ctzdi2(uint64_t x) Binary file projects/seL4_libs/libsel4utils/CMakeFiles/sel4utils.dir/src/irq_server/irq_server.c.obj matches Binary file projects/seL4_libs/libsel4utils/libsel4utils.a matches Binary file projects/seL4_libs/libsel4platsupport/libsel4platsupport.a matches Binary file projects/seL4_libs/libsel4platsupport/CMakeFiles/sel4platsupport.dir/src/common.c.obj matches What am I missing here?

1 0

Docker / gnat
by dave＠synergy.org 02 Nov '20

02 Nov '20

Hello, I converted over from my old development environment to the docker-based version this weekend. Everything worked fine, except for one thing. I was using the gnat-6-aarch64-linux-gnu and gnat-6-arm-linux-gnueabihf packages to compile Ada code. Ada is not installed by default in the docker container. I can install it, but it goes away when the container terminates. I am brand new to docker. Can I make these changes permanent myself or does it require the container provider to do so? Thanks! Dave

2 2