- Devel - lists.sel4.systems

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

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

07 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