Hi,
I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.
I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it: https://pastebin.com/MiMB0N62
Regards, Gábor Székely
Hi Gabor,
We have two ported TCP/IP stacks:
(1) A port of liblwip-1.4.1: https://github.com/seL4/camkes-vm/tree/master/liblwip which is used generally when we need a network implementation. It's used for benchmarking and in the x86 VMM implementation. My understanding is that the library there is self-contained, and that you have to write the plumbing and gluecode to actually link it to your environment manually. So things like providing virtual memory, page mapping and unmapping, a malloc() implementation etc, are left up to the person attempting to use the library.
I'm not very familiary with the VM repositories, but from a quick skim I can probably point you at the following bits to use as a starting point:
* https://github.com/seL4/camkes-vm/tree/master/templates%C2%A0Some of these templates look like the glue code that links liblwip to the CAmkES environment. Specifically, the ones of interest for liblwip seem to be: ** seL4ProdCon-from.template.c ** seL4ProdCon-to.template.c ** seL4UDPRecv-from.template.c ** seL4UDPRecv-to.template.c ** seL4UDPSend-from.template.c ** seL4UDPSend-to.template.c ** seL4VMNet.template.c * https://github.com/seL4/camkes-vm/tree/master/components/Echo This looks like a sample CAmkES component that uses liblwip * https://github.com/seL4/camkes-vm/tree/master/components/UDPServer This looks like another sample CAmkES component that also uses liblwip.
It appears that only glue code for UDP has ever been written, and not any for TCP -- don't take my word as gospel though, I'm not familiar with these repos.
(2) A recent port of picoTCP: https://github.com/seL4/util_libs/tree/master/libpicotcp%E2%80%8B , but only the build system glue and configuration header for building it is included there, and we haven't yet pushed out the library itself. The rest of the gluecode for binding the picoTCP to an environment is also not yet pushed out as far as I can tell.
Sorry, and I hope this gives you something to start with, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO
Hi,
I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.
I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it:
Regards, Gábor Székely
Hi Gabor,
This is a bit a late reply so not sure if it's still helpful but with LWiP I would suggest looking at LWiP Bare Metal and its Native API http://lwip.wikia.com/wiki/Porting_For_Bare_Metal http://lwip.wikia.com/wiki/Raw/native_API
You can also see an example of a raw UDP setup here https://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master..., which is from this manifest https://github.com/SEL4PROJ/ethernet-demo-x86-manifest Be aware though that this project is a testing application and as such is *not* a good system architecture, as everything is jammed into one component. Also you will not be able to just compile and run it as it has hard coded memory addresses and interrupt numbers for a specific machine.
Hope that helps a bit, Adrian
On Wed 28-Jun-2017 7:09 PM, Gábor Székely wrote: Hi,
I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.
I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it: https://pastebin.com/MiMB0N62
Regards, Gábor Székely
_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hello, I have a few questions regarding networking (I also want to be able to communicate with sel4 system over network).
1. I tried the example Adrian pointed out https://github.com/SEL4PROJ/ethernet-demo-x86-manifest When I initialize with default.xml https://github.com/SEL4PROJ/ethernet-demo-x86-manifest/blob/master/default.xml and try to compile, I am getting the following error:
[image: Inline image 1]
I suspect that is something related with the recent changes in camkes/sel4? Or is the default ethernet-demo app simply not configured properly? I am not talking about memory mapping/irsq, this is a different error.
2. When I use the same repository and the working https://github.com/SEL4PROJ/ethernet-demo-x86-manifest/blob/master/working-20170113.xml manifest (pointing to specific commits so it compiles), and change the ethernet memory address and irqs I can compile the application, but I get the following error when running it: [image: Inline image 2] Notably the process fails when sel4 tries to access client iospace. I know I have the irqs and the memory right, as well as the device id (pci_bdf https://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master/ethernet-demo-app/ethernet-demo.camkes#L74). However, the problem is obviously the iospace_id https://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master/ethernet-demo-app/ethernet-demo.camkes#L73.From what I read from the sel4 manual, the iospace_id depends on the type of iommu unit if I understand it correctly. But I am running sel4 in qemu and I don't pass any physical device to it, it is all virtual devices. To verify, I can run Ubuntu in qemu with the very same settings and it detects all virtual devices without issues. I can also run sel4-rumprum app (see below) and it also detects the hardware without issues.
The same error happens even when I disable the IOMMU in the sel4 config ( here https://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master/configs/x64_ethernet_demo_defconfig#L42 ).
Am I missing something fundamental here? Why in one case I need iommu to run sel4 (this case), and why in other case (sel4-rumprun or regular Ubuntu) I dont?
3. I tested the sel4-rumprun-ethernet https://github.com/seL4/camkes/blob/master/apps/rumprun_ethernet/rumprun_ethernet.camkes app in qemu and it works great! I can connect over TCP socket from host and send data to sel4 running in qemu. In this case there was no issue with iommu or iospaces (I am just passing through the irq numbers and device addresses).
So my question is - was this app just a quick test (committed by Kent McLeod https://github.com/seL4/camkes/commit/cd17c313f7f76ffa7ec6981e1140c6343b2f9b54), or do you think using rumpkernels as camkes components is the preferred way forward? Especially because that way we have access to NetBSD drivers without much modifications.
Thank you in advance for your advice.
Regards Michal
On Wed, Jul 26, 2017 at 1:35 AM, Adrian.Danis@data61.csiro.au wrote:
Hi Gabor,
This is a bit a late reply so not sure if it's still helpful but with LWiP I would suggest looking at LWiP Bare Metal and its Native API http://lwip.wikia.com/wiki/Porting_For_Bare_Metal http://lwip.wikia.com/wiki/Raw/native_API
You can also see an example of a raw UDP setup here https://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86- -devel/blob/master/ethernet-demo-app/ethernet-demo.c, which is from this manifest https://github.com/SEL4PROJ/ethernet-demo-x86-manifest Be aware though that this project is a testing application and as such is *not* a good system architecture, as everything is jammed into one component. Also you will not be able to just compile and run it as it has hard coded memory addresses and interrupt numbers for a specific machine.
Hope that helps a bit, Adrian
On Wed 28-Jun-2017 7:09 PM, Gábor Székely wrote:
Hi,
I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.
I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it: https://pastebin.com/MiMB0N62
Regards, Gábor Székely
Devel mailing listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel
Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Michal,
The ethernet-demo application is current written to require the presence of an IOMMU for DMA translation. If you are running in an emulated environment, such as QEMU, that does not emulate an IOMMU, or on hardware without an IOMMU, then it will not work. The rumprun examples currently do not use the iommu and are using the devices "unsafely" as the driver (and hence rumprun) must be trusted not to compromise the system. Eventually our rumprun support will support (although not require) using the IOMMU to reduce the trust needed in them.
Adrian
On Thu 03-Aug-2017 7:24 AM, Michal Podhradsky wrote: Hello, I have a few questions regarding networking (I also want to be able to communicate with sel4 system over network).
1. I tried the example Adrian pointed out https://github.com/SEL4PROJ/ethernet-demo-x86-manifest When I initialize with default.xmlhttps://github.com/SEL4PROJ/ethernet-demo-x86-manifest/blob/master/default.xml and try to compile, I am getting the following error:
[Inline image 1]
I suspect that is something related with the recent changes in camkes/sel4? Or is the default ethernet-demo app simply not configured properly? I am not talking about memory mapping/irsq, this is a different error.
2. When I use the same repository and the workinghttps://github.com/SEL4PROJ/ethernet-demo-x86-manifest/blob/master/working-20170113.xml manifest (pointing to specific commits so it compiles), and change the ethernet memory address and irqs I can compile the application, but I get the following error when running it: [Inline image 2] Notably the process fails when sel4 tries to access client iospace. I know I have the irqs and the memory right, as well as the device id (pci_bdfhttps://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master/ethernet-demo-app/ethernet-demo.camkes#L74). However, the problem is obviously the iospace_idhttps://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master/ethernet-demo-app/ethernet-demo.camkes#L73.From what I read from the sel4 manual, the iospace_id depends on the type of iommu unit if I understand it correctly. But I am running sel4 in qemu and I don't pass any physical device to it, it is all virtual devices. To verify, I can run Ubuntu in qemu with the very same settings and it detects all virtual devices without issues. I can also run sel4-rumprum app (see below) and it also detects the hardware without issues.
The same error happens even when I disable the IOMMU in the sel4 config (herehttps://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master/configs/x64_ethernet_demo_defconfig#L42).
Am I missing something fundamental here? Why in one case I need iommu to run sel4 (this case), and why in other case (sel4-rumprun or regular Ubuntu) I dont?
3. I tested the sel4-rumprun-ethernethttps://github.com/seL4/camkes/blob/master/apps/rumprun_ethernet/rumprun_ethernet.camkes app in qemu and it works great! I can connect over TCP socket from host and send data to sel4 running in qemu. In this case there was no issue with iommu or iospaces (I am just passing through the irq numbers and device addresses).
So my question is - was this app just a quick test (committed by Kent McLeodhttps://github.com/seL4/camkes/commit/cd17c313f7f76ffa7ec6981e1140c6343b2f9b54), or do you think using rumpkernels as camkes components is the preferred way forward? Especially because that way we have access to NetBSD drivers without much modifications.
Thank you in advance for your advice.
Regards Michal
On Wed, Jul 26, 2017 at 1:35 AM, <Adrian.Danis@data61.csiro.aumailto:Adrian.Danis@data61.csiro.au> wrote: Hi Gabor,
This is a bit a late reply so not sure if it's still helpful but with LWiP I would suggest looking at LWiP Bare Metal and its Native API http://lwip.wikia.com/wiki/Porting_For_Bare_Metal http://lwip.wikia.com/wiki/Raw/native_API
You can also see an example of a raw UDP setup here https://github.com/SEL4PROJ/camkes-apps-ethernet-demo-x86--devel/blob/master..., which is from this manifest https://github.com/SEL4PROJ/ethernet-demo-x86-manifest Be aware though that this project is a testing application and as such is *not* a good system architecture, as everything is jammed into one component. Also you will not be able to just compile and run it as it has hard coded memory addresses and interrupt numbers for a specific machine.
Hope that helps a bit, Adrian
On Wed 28-Jun-2017 7:09 PM, Gábor Székely wrote: Hi,
I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.
I also tried to run the rumprun hello world, the compillation finishes, however I get the following output when I try to run it: https://pastebin.com/MiMB0N62
Regards, Gábor Székely
_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
_______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Adrian.Danis＠data61.csiro.au -
Gábor Székely -
Kofidoku.Atuah＠data61.csiro.au -
Michal Podhradsky