- Devel - lists.sel4.systems

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. 12 Jun '21

12 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. 11 Jun '21

11 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 10 Jun '21

10 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 09 Jun '21

09 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