Hello

Thank you for the answer. I simply adjusted the values in kernel/tools/dts/am335x.dts for now and kept the seL4DTBHardware connection.

I have more questions: 1) There are 2 implementations of low_level_init - projects/global-components/components/PicoServer/src/eth_interface.c - projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c What decides which one to invoke? or is the in beaglebone.c not necessary at all?

2) How is projects/camkes/picoserver/ethdriver_seL4Ethdriver_0.c generated? I am debugging my current implementation which gets stuck before ethriver_mac().

Sincerely, Benjamin ________________________________ Von: Lee, Damon (Data61, Kensington NSW) [Damon.Lee@data61.csiro.au] Gesendet: Dienstag, 18. Juni 2019 03:36 An: KAP Benjamin; devel@sel4.systems Betreff: Re: Beaglebone Black: failed to find device frame

Hi,

The problem is that there isn't any untyped memory available to make a 4K page at address 0x4a101200 (if you notice carefully, this address isn't page aligned).

The seL4DTBHardware connector doesn't support the AM335x board as the format of the interrupt fields in the DTS doesn't follow that of the ARM GIC.

The page alignment problem is also a problem that I didn't encounter when developing the seL4DTBHardware connector, so thanks for the alert.

So to resolve your problem you will have to use the seL4HardwareMMIO connector and ask it to make a 4K mapping at 0x4a100000 and 0x4a101000.

You will also need to use the seL4HardwareInterrupt connector to generate the interrupts.

Sincerely, Damon ________________________________ From: Devel devel-bounces@sel4.systems on behalf of KAP Benjamin benjamin.kap.001@student.uni.lu Sent: Tuesday, 18 June 2019 4:10 AM To: devel@sel4.systems Subject: [seL4] Beaglebone Black: failed to find device frame

Hello

I am trying to add am335x support to the pico TCP/IP stack and currently working on the following file: projects/global-components/components/Ethdriver/include/plat/am335x/plat/eth_devices.h.

Current contents of this file (I am creating it step by step, thus it might be incomplete):

#pragma once

#define HARDWARE_ETHERNET_COMPONENT

#define HARDWARE_ETHERNET_INTERFACES \ consumes Dummy EthDriver; \ emits Dummy dummy_source;

#define HARDWARE_ETHERNET_COMPOSITION \ connection seL4DTBHardware ethernet_conn(from dummy_source, to EthDriver);

#define HARDWARE_ETHERNET_CONFIG \ EthDriver.dtb = dtb({ "path" : "/ocp/ethernet@4a100000" }); \ EthDriver.generate_interrupts = 1;

I test the implementation by using the picoserver CAmkES application. However, on boot I receive the following error:

ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..8262e037] No DTB found! Looking for DTB in CPIO archive... Found dtb at 820c1b84 Loaded dtb from 820c1b84 paddr=[80034000..8003cfff] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'capdl-loader' paddr=[8003d000..8059afff] vaddr=[10000..56dfff] virt_entry=1e4dc ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point...

Bootstrapping kernel Booting all finished, dropped to user space create_object@main.c:726 device frame/untyped, paddr = 0x48040000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x48042000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x4a100000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x4a101200, size = 12 bits

create_object@main.c:730 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x4a101200

seL4 root server abort()ed Debug halt syscall from user thread 0xffefd600 "rootserver" halting... Kernel entry via Unknown syscall, word: 65

The am335x.dtb contains the following line in ethernet@4a100000: reg = <0x4a100000 0x00000800 0x4a101200 0x00000100>;

I did find related posts (http://sel4.systems/pipermail/devel/2016-June/000850.html, http://sel4.systems/pipermail/devel/2018-July/002031.html and http://sel4.systems/pipermail/devel/2015-October/000530.html) but didn't help me that much.http://sel4.systems/pipermail/devel/2018-July/002031.html).

If I am correct the hardware block isn't enabled but I don't know exactly how to do this. Could anyone help me out here or give me some hints?

Best Regards,

Kap Benjamin

Hello

Thank you for your help so far. I still have some unclarity about the DMA in seL4 and maybe you could help me again:

With the seL4DTBHardware connection I created the following device frames, given paddr: 0x4a100000, size: 0x4000 device frame/untyped, paddr = 0x4a100000, size = 12 bits device frame/untyped, paddr = 0x4a101000, size = 12 bits device frame/untyped, paddr = 0x4a102000, size = 12 bits device frame/untyped, paddr = 0x4a103000, size = 12 bits

If I am not mistaken these should already be allocated dma memory buffer and thus have a virtual address as well. So I try to retrieve the VADDR from the first device frame by invoking the following runtime API: ps_io_mapper_t *mapper = &io_ops->io_mapper; uintptr_t vaddr = (uintptr_t) mapper->io_map_fn(mapper->cookie, 0x4a100000, 0x4000,0, PS_MEM_NORMAL);

Afterwards vaddr is a valid pointer (here: 0xab4000).

However, by using the next runtime API I always receive a NULL pointer: uintptr_t paddr = camkes_dma_get_paddr(vaddr);

Am I missing a step or is something else going wrong?

Sincerely, Benjamin ________________________________ Von: Lee, Damon (Data61, Kensington NSW) [Damon.Lee@data61.csiro.au] Gesendet: Mittwoch, 19. Juni 2019 07:45 An: KAP Benjamin; devel@sel4.systems Betreff: Re: Beaglebone Black: failed to find device frame

Hi Benjamin,

1) Both are necessary. The low_level_init function in the PicoServer component is paired with the Ethdriver component. This reads in the MAC address that is given to each client of the Ethdriver component.

The low_level_init function in the libethdrivers is also paired with the Ethdriver component but it reads in the MAC address assigned to the device.

The reason why we have both is because the Ethdriver component was designed to have multiple clients connected to it, i.e. multiplexing a Ethernet card for multiple clients. This is an issue that we will eventually fix.

2) ethdriver_seL4Ethdriver_0.c is generated from the CAmkES template for the seL4DTBHardware connector. The template is located in camkes/templates/seL4DTBHardware-to.template.c in the CAmkES folder which will either be in projects/camkes-tool or tools/camkes from the root of the manifest directory, depending on which manifest you initialised your project from.

Sincerely, Damon

________________________________ From: KAP Benjamin benjamin.kap.001@student.uni.lu Sent: Wednesday, 19 June 2019 11:34 AM To: Lee, Damon (Data61, Kensington NSW); devel@sel4.systems Subject: AW: Beaglebone Black: failed to find device frame

Hello

Thank you for the answer. I simply adjusted the values in kernel/tools/dts/am335x.dts for now and kept the seL4DTBHardware connection.

I have more questions: 1) There are 2 implementations of low_level_init - projects/global-components/components/PicoServer/src/eth_interface.c - projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c What decides which one to invoke? or is the in beaglebone.c not necessary at all?

2) How is projects/camkes/picoserver/ethdriver_seL4Ethdriver_0.c generated? I am debugging my current implementation which gets stuck before ethriver_mac().

Sincerely, Benjamin ________________________________ Von: Lee, Damon (Data61, Kensington NSW) [Damon.Lee@data61.csiro.au] Gesendet: Dienstag, 18. Juni 2019 03:36 An: KAP Benjamin; devel@sel4.systems Betreff: Re: Beaglebone Black: failed to find device frame

Hi,

The problem is that there isn't any untyped memory available to make a 4K page at address 0x4a101200 (if you notice carefully, this address isn't page aligned).

The seL4DTBHardware connector doesn't support the AM335x board as the format of the interrupt fields in the DTS doesn't follow that of the ARM GIC.

The page alignment problem is also a problem that I didn't encounter when developing the seL4DTBHardware connector, so thanks for the alert.

So to resolve your problem you will have to use the seL4HardwareMMIO connector and ask it to make a 4K mapping at 0x4a100000 and 0x4a101000.

You will also need to use the seL4HardwareInterrupt connector to generate the interrupts.

Sincerely, Damon ________________________________ From: Devel devel-bounces@sel4.systems on behalf of KAP Benjamin benjamin.kap.001@student.uni.lu Sent: Tuesday, 18 June 2019 4:10 AM To: devel@sel4.systems Subject: [seL4] Beaglebone Black: failed to find device frame

Hello

I am trying to add am335x support to the pico TCP/IP stack and currently working on the following file: projects/global-components/components/Ethdriver/include/plat/am335x/plat/eth_devices.h.

Current contents of this file (I am creating it step by step, thus it might be incomplete):

#pragma once

#define HARDWARE_ETHERNET_COMPONENT

#define HARDWARE_ETHERNET_INTERFACES \ consumes Dummy EthDriver; \ emits Dummy dummy_source;

#define HARDWARE_ETHERNET_COMPOSITION \ connection seL4DTBHardware ethernet_conn(from dummy_source, to EthDriver);

#define HARDWARE_ETHERNET_CONFIG \ EthDriver.dtb = dtb({ "path" : "/ocp/ethernet@4a100000" }); \ EthDriver.generate_interrupts = 1;

I test the implementation by using the picoserver CAmkES application. However, on boot I receive the following error:

ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..8262e037] No DTB found! Looking for DTB in CPIO archive... Found dtb at 820c1b84 Loaded dtb from 820c1b84 paddr=[80034000..8003cfff] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'capdl-loader' paddr=[8003d000..8059afff] vaddr=[10000..56dfff] virt_entry=1e4dc ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point...

Bootstrapping kernel Booting all finished, dropped to user space create_object@main.c:726 device frame/untyped, paddr = 0x48040000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x48042000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x4a100000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x4a101200, size = 12 bits

create_object@main.c:730 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x4a101200

seL4 root server abort()ed Debug halt syscall from user thread 0xffefd600 "rootserver" halting... Kernel entry via Unknown syscall, word: 65

The am335x.dtb contains the following line in ethernet@4a100000: reg = <0x4a100000 0x00000800 0x4a101200 0x00000100>;

I did find related posts (http://sel4.systems/pipermail/devel/2016-June/000850.html, http://sel4.systems/pipermail/devel/2018-July/002031.html and http://sel4.systems/pipermail/devel/2015-October/000530.html) but didn't help me that much.http://sel4.systems/pipermail/devel/2018-July/002031.html).

If I am correct the hardware block isn't enabled but I don't know exactly how to do this. Could anyone help me out here or give me some hints?

Best Regards,

Kap Benjamin

Hello

The ethernet driver for the beaglebone seem to be working now with the pico TCP/IP stack, at least with ipv4.

After booting, at some point the message "IPv6: DAD verified valid address" appears and then the driver doesn't work properly anymore. Is there a way to disable ipv6 in picoserver/picotcp? For now ipv4 is sufficient for my project.

Best regards, Kap Benjamin ________________________________ Von: Lee, Damon (Data61, Kensington NSW) [Damon.Lee@data61.csiro.au] Gesendet: Dienstag, 25. Juni 2019 08:27 An: KAP Benjamin; devel@sel4.systems Betreff: Re: Beaglebone Black: failed to find device frame

Hi Benjamin,

Device frames and DMA memory are two different things, at least in CAmkES.

DMA memory is allocated from a pool of memory which is initialised by CAmkES and is backed by _normal_ untyped memory.

Device frames, as the name suggests is _device_ untyped memory.

I hope that answers your question.

PS: We have function wrappers around the ps_*_t structures. These make it easier to call specific functions within an interface. So for the io_mapper function, the wrapper is called `ps_io_map`. The wrappers can be found in the libplatsupport/include/platsupport folder of the util_libs repository.

Sincerely, Damon ________________________________ From: KAP Benjamin benjamin.kap.001@student.uni.lu Sent: Tuesday, 25 June 2019 7:17 AM To: Lee, Damon (Data61, Kensington NSW); devel@sel4.systems Subject: AW: Beaglebone Black: failed to find device frame

Hello

Thank you for your help so far. I still have some unclarity about the DMA in seL4 and maybe you could help me again:

With the seL4DTBHardware connection I created the following device frames, given paddr: 0x4a100000, size: 0x4000 device frame/untyped, paddr = 0x4a100000, size = 12 bits device frame/untyped, paddr = 0x4a101000, size = 12 bits device frame/untyped, paddr = 0x4a102000, size = 12 bits device frame/untyped, paddr = 0x4a103000, size = 12 bits

If I am not mistaken these should already be allocated dma memory buffer and thus have a virtual address as well. So I try to retrieve the VADDR from the first device frame by invoking the following runtime API: ps_io_mapper_t *mapper = &io_ops->io_mapper; uintptr_t vaddr = (uintptr_t) mapper->io_map_fn(mapper->cookie, 0x4a100000, 0x4000,0, PS_MEM_NORMAL);

Afterwards vaddr is a valid pointer (here: 0xab4000).

However, by using the next runtime API I always receive a NULL pointer: uintptr_t paddr = camkes_dma_get_paddr(vaddr);

Am I missing a step or is something else going wrong?

Sincerely, Benjamin ________________________________ Von: Lee, Damon (Data61, Kensington NSW) [Damon.Lee@data61.csiro.au] Gesendet: Mittwoch, 19. Juni 2019 07:45 An: KAP Benjamin; devel@sel4.systems Betreff: Re: Beaglebone Black: failed to find device frame

Hi Benjamin,

1) Both are necessary. The low_level_init function in the PicoServer component is paired with the Ethdriver component. This reads in the MAC address that is given to each client of the Ethdriver component.

The low_level_init function in the libethdrivers is also paired with the Ethdriver component but it reads in the MAC address assigned to the device.

The reason why we have both is because the Ethdriver component was designed to have multiple clients connected to it, i.e. multiplexing a Ethernet card for multiple clients. This is an issue that we will eventually fix.

2) ethdriver_seL4Ethdriver_0.c is generated from the CAmkES template for the seL4DTBHardware connector. The template is located in camkes/templates/seL4DTBHardware-to.template.c in the CAmkES folder which will either be in projects/camkes-tool or tools/camkes from the root of the manifest directory, depending on which manifest you initialised your project from.

Sincerely, Damon

________________________________ From: KAP Benjamin benjamin.kap.001@student.uni.lu Sent: Wednesday, 19 June 2019 11:34 AM To: Lee, Damon (Data61, Kensington NSW); devel@sel4.systems Subject: AW: Beaglebone Black: failed to find device frame

Hello

Thank you for the answer. I simply adjusted the values in kernel/tools/dts/am335x.dts for now and kept the seL4DTBHardware connection.

I have more questions: 1) There are 2 implementations of low_level_init - projects/global-components/components/PicoServer/src/eth_interface.c - projects/util_libs/libethdrivers/src/plat/am335x/beaglebone.c What decides which one to invoke? or is the in beaglebone.c not necessary at all?

2) How is projects/camkes/picoserver/ethdriver_seL4Ethdriver_0.c generated? I am debugging my current implementation which gets stuck before ethriver_mac().

Sincerely, Benjamin ________________________________ Von: Lee, Damon (Data61, Kensington NSW) [Damon.Lee@data61.csiro.au] Gesendet: Dienstag, 18. Juni 2019 03:36 An: KAP Benjamin; devel@sel4.systems Betreff: Re: Beaglebone Black: failed to find device frame

Hi,

The problem is that there isn't any untyped memory available to make a 4K page at address 0x4a101200 (if you notice carefully, this address isn't page aligned).

The seL4DTBHardware connector doesn't support the AM335x board as the format of the interrupt fields in the DTS doesn't follow that of the ARM GIC.

The page alignment problem is also a problem that I didn't encounter when developing the seL4DTBHardware connector, so thanks for the alert.

So to resolve your problem you will have to use the seL4HardwareMMIO connector and ask it to make a 4K mapping at 0x4a100000 and 0x4a101000.

You will also need to use the seL4HardwareInterrupt connector to generate the interrupts.

Sincerely, Damon ________________________________ From: Devel devel-bounces@sel4.systems on behalf of KAP Benjamin benjamin.kap.001@student.uni.lu Sent: Tuesday, 18 June 2019 4:10 AM To: devel@sel4.systems Subject: [seL4] Beaglebone Black: failed to find device frame

Hello

I am trying to add am335x support to the pico TCP/IP stack and currently working on the following file: projects/global-components/components/Ethdriver/include/plat/am335x/plat/eth_devices.h.

Current contents of this file (I am creating it step by step, thus it might be incomplete):

#pragma once

#define HARDWARE_ETHERNET_COMPONENT

#define HARDWARE_ETHERNET_INTERFACES \ consumes Dummy EthDriver; \ emits Dummy dummy_source;

#define HARDWARE_ETHERNET_COMPOSITION \ connection seL4DTBHardware ethernet_conn(from dummy_source, to EthDriver);

#define HARDWARE_ETHERNET_CONFIG \ EthDriver.dtb = dtb({ "path" : "/ocp/ethernet@4a100000" }); \ EthDriver.generate_interrupts = 1;

I test the implementation by using the picoserver CAmkES application. However, on boot I receive the following error:

ELF-loader started on CPU: ARM Ltd. Cortex-A8 r3p2 paddr=[82000000..8262e037] No DTB found! Looking for DTB in CPIO archive... Found dtb at 820c1b84 Loaded dtb from 820c1b84 paddr=[80034000..8003cfff] ELF-loading image 'kernel' paddr=[80000000..80033fff] vaddr=[f0000000..f0033fff] virt_entry=f0000000 ELF-loading image 'capdl-loader' paddr=[8003d000..8059afff] vaddr=[10000..56dfff] virt_entry=1e4dc ELF loader relocated, continuing boot... Enabling MMU and paging Jumping to kernel-image entry point...

Bootstrapping kernel Booting all finished, dropped to user space create_object@main.c:726 device frame/untyped, paddr = 0x48040000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x48042000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x4a100000, size = 12 bits

create_object@main.c:726 device frame/untyped, paddr = 0x4a101200, size = 12 bits

create_object@main.c:730 [Cond failed: err != seL4_NoError] Failed to find device frame/untyped at paddr = 0x4a101200

seL4 root server abort()ed Debug halt syscall from user thread 0xffefd600 "rootserver" halting... Kernel entry via Unknown syscall, word: 65

The am335x.dtb contains the following line in ethernet@4a100000: reg = <0x4a100000 0x00000800 0x4a101200 0x00000100>;

I did find related posts (http://sel4.systems/pipermail/devel/2016-June/000850.html, http://sel4.systems/pipermail/devel/2018-July/002031.html and http://sel4.systems/pipermail/devel/2015-October/000530.html) but didn't help me that much.http://sel4.systems/pipermail/devel/2018-July/002031.html).

If I am correct the hardware block isn't enabled but I don't know exactly how to do this. Could anyone help me out here or give me some hints?

Best Regards,

Kap Benjamin