- Devel - lists.sel4.systems

ARM LPAE?
by Wladislav Wiebe 20 Jan '17

20 Jan '17

Hello, I am trying to integrate TI Keystone 2 platform to seL4. What I have done so far is basically an initial port of the Kernel/libs/elfloader/Platform components and introducing a new keystone defconfig. Relevant config parts about the setup: CONFIG_ARCH_ARM_V7A=y CONFIG_ARCH_ARM=y CONFIG_ARCH_AARCH32=y CONFIG_ARM_CORTEX_A15=y CONFIG_PLAT_KEYSTONE=y At the end I am able to generate an image which looks like: $ arm-cortexa15-linux-gnueabihf-readelf -e images/sel4test-driver-image-arm-keystone ELF Header: Class: ELF32 .. Entry point address: 0xc0008000 .. (I am using the same entry point as Linux use it) So far, it stops booting in the elfloader -- output log: .. [ 29.705] ## Starting application at 0xc0008000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p4 paddr=[c0008000..c032841f] -> Stop here <- Seems it stops loading @ elf_getMemoryBounds(). I suppose it is related to fact that the physical start address starts @ 0x840000000 which is beyond 32 Bit - so, LPAE support is required. The physical RAM setup looks like: bank 0: addr: 0x840000000 size: 0x17ec5000 (382 MB) bank 1: addr: 0x880000000 size: 0x80000000 (2048 MB) Do you have an idea if this is supposed to be supported on seL4? What should be the "physBase" and the "kernelBase" for such a setup? How should the "static const p_region_t BOOT_RODATA avail_p_regs" looks like? Thanks in advance! -- WBR, Wladislav WIebe

3 10

Re: [seL4] SDHC drivers (cont.)
by Siwei.Zhuang＠data61.csiro.au 20 Jan '17

20 Jan '17

Hi Oak, I tried your code. It works for me except that it seems that you are using old versions of seL4 kernel and libraries. Attached is the code I'm using, I merely add some initialization code to your code. It should work on the latest version of seL4 kernel and related libraries. If the code doesn't work for you. I would suggest, 1. If you are using u-boot, try its mmc command, see if you can access the card. 2. Have a look at the imx6 reference manual, chapter 67.2 and 67.3, check if the host controller is enabled properly. - Siwei ________________________________ From: Norrathep Rattanavipanon <nrattana(a)uci.edu> Sent: Friday, 20 January 2017 6:12 AM To: Zhuang, Siwei (Data61, Kensington NSW) Subject: Re: [seL4] SDHC drivers (cont.) Hi Siwei, Yes, I believe mmc_card_capacity returns the correct value (4026531840 - my microsd is 4GB). And my code does not do any interrupt handling. In fact, that's all the code in the root userspace process (besides initializing vka, vspace and simple objects) and there is no other process. I also tried using a callback as mmc_block_read's argument, instead of using NULL, but it also does not work. On Wed, Jan 18, 2017 at 8:41 PM, <Siwei.Zhuang(a)data61.csiro.au<mailto:Siwei.Zhuang@data61.csiro.au>> wrote: Hi Oak, Do you get the correct card capacity by calling mmc_card_capacity? If you don't, you'd need to check if the hardware is enabled in your bootloader. Are you doing any interrupt handling? As you don't supply a callback function to mmc_block_read, the read function would block until the hardware responses. In this case, mmc_block_read handles the interrupt itself. It would trigger a dead lock if you also handles the interrupt. - Siwei ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Norrathep Rattanavipanon <nrattana(a)uci.edu<mailto:nrattana@uci.edu>> Sent: Thursday, 19 January 2017 9:54 AM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel(a)sel4.systems; GTS Subject: Re: [seL4] SDHC drivers (cont.) Hi Adrian, Thank you for the reply. I fix it according to what you suggest but it still does not solve the problem (still hang at the same place. Do you have any other suggestions on what I should fix or how I should look into debugging it? Best, Oak On Tue, Jan 17, 2017 at 8:58 PM, <Adrian.Danis(a)data61.csiro.au<mailto:Adrian.Danis@data61.csiro.au>> wrote: Hi Oak, I don't know much about SD cards or this driver but it seems to me like passing it a physical address of 0 isn't what you want, and whilst I know nothing about the mmc hardware it seems reasonable to me that it might hang trying to DMA to memory that doesn't exist. There is also the additional problem that even if paddr was correct for the first page, there is no guarantee that the 5 pages you have allocated are contiguously physically even though they will be mapped contiguous virtually. My recommendation is to use the page dma allocator in seL4_libs/libsel4utils/include/sel4utils/page_dma.h, this will provide you an easy way to allocate/map pages for the purposes of DMA. So instead of void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); uintptr_t paddr = 0; You would have ps_dma_man_t dma_man; error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); void *vaddr = ps_dma_alloc(&dma_man, 5 * PAGE_SIZE_4K, PAGE_SIZE_4K, 0, PS_MEM_NORMAL); uintptr_t paddr = ps_dma_pin(&dma_man, vaddr, 5 * PAGE_SIZE_4K); As I said at the start, I don't know if this will actually fix your current problem, but it's still something you will need to fix. Adrian On Wed 18-Jan-2017 6:31 AM, Norrathep Rattanavipanon wrote: My apology that I have to continue the discussion from the old thread: (http://sel4.systems/pipermail/devel/2016-October/001056.html) My goal is to read and write data from/to micro sd in SabreLite platform. I tried both Adrain and Anna's suggestions in that thread and they dont seem to fix the problem. Nothing returns error and I also changed cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is what Anna meant instead of setting 3rd argument of vspace_new_pages). The code's still stuck inside mmc_block_read function. I tracked it down and it seems like BRR and BWR interrupt statuses are never set to 1 I add my code below, please let me know if anything is wrong with my code. ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); assert(error == 0); ps_io_ops_t io_ops = { .io_mapper = io_mapper }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev, 0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); // return id=3 error = sdio_init(id, &io_ops, dev); assert(error == 0); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); assert(error == 0 && mmc_card != NULL); void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); assert(vaddr != NULL); uintptr_t paddr = 0; printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here printf("read %lu bytes\n", read_len); Thanks Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine _______________________________________________ Devel mailing list Devel(a)sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 0

seL4 System Utilization / Benchmark
by Andrew Gacek 19 Jan '17

19 Jan '17

Hi, I'm interested in seeing how much of the CPU is being used by the various threads in my (camkes) application. I'd like a simple "Task Manager" style report of the form: 70% idle 25% can_obj_7_0_control_9_tcb 5% can_obj_7_Int_3_0000_tcb 0% can_obj_7_0_fault_handler_15_0000_tcb etc I've tried poking around libsel4bench, but I don't see any obvious way of benchmarking the whole system. From what I can tell, it's mostly designed to get cycle counts from specific code segments. Is that right? What's the best way to go about benchmarking the whole system? It's only for debugging, so I'm willing to make some quick-and-dirty changes to the kernel just to see the results. Thanks, Andrew

4 11

SDHC drivers (cont.)
by Norrathep Rattanavipanon 19 Jan '17

19 Jan '17

My apology that I have to continue the discussion from the old thread: ( http://sel4.systems/pipermail/devel/2016-October/001056.html) My goal is to read and write data from/to micro sd in SabreLite platform. I tried both Adrain and Anna's suggestions in that thread and they dont seem to fix the problem. Nothing returns error and I also changed cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is what Anna meant instead of setting 3rd argument of vspace_new_pages). The code's still stuck inside mmc_block_read function. I tracked it down and it seems like BRR and BWR interrupt statuses are never set to 1 I add my code below, please let me know if anything is wrong with my code. ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); assert(error == 0); ps_io_ops_t io_ops = { .io_mapper = io_mapper }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev, 0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); // return id=3 error = sdio_init(id, &io_ops, dev); assert(error == 0); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); assert(error == 0 && mmc_card != NULL); void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); assert(vaddr != NULL); uintptr_t paddr = 0; printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here printf("read %lu bytes\n", read_len); Thanks Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 3

CAmkES Templates
by Chris Guikema 18 Jan '17

18 Jan '17

Hello, I am working on a CAmkES application attempting to build a seL4 Network Stack. I am basing this on the CAmkES-VM and utilizing UDP Protocol with the lwIP library. During my build process, I get quite a few linking errors like this: undefined reference to `pbuf_alloc' This is odd, because in the templates, the proper header files are being linked in. There are also warnings like this: Warning: no template for ethdriver_1.to.source Even though the connection does exist: connection seL4Ethdriver eth_driver(from router.ethdriver, to ethdriver.client); Is there something obvious I am doing wrong? Thanks Chris

2 2

questions about SMMU on TK1 VMM
by PX 18 Jan '17

18 Jan '17

Hi, I have some questions about the SMMU on the new version of TK1 VMM as follows: 1. In the source code, smmu.c, the IO ASID 1 is assigned to hardware engine, AFI, which is supposed to connect with PCIE devices. However, when I add 1 to vm.smmu in vm.camkes, the VM can not access Ethernet and cause a SMMU translation error. But it works if I add 0 to vm.smmu as suggested by Kent. whats the reason to do so? 2. Each IO device is assigned with an IO space mapping. However, there is no IO ASID associated with these mappings. Does that means these mappings are associated with an IO ASID in the order given in vm.smmu? 3. Is it possible for the VMM to change the IO mapping for a specific device? say, invalidate old mapping and load a new mapping? what's the rough idea to do so? thanks Peng

2 1

questions about PCIE SMMU for tk1 vmm
by PX 16 Jan '17

16 Jan '17

Hi, I am confused by the SMMU management for PCIE device in the updated TK1 VMM. The IO ASID for PCIE device is 0. However, the start IO ASID is from 1 as defined in smmu.h. When initialized, the lookup table, smmu_ioasid_to_pd, has no entry for IO asid 0 at all. I don't understand how the page table for PCIE device is generated and used by SMMU? which part source code should I check ? thanks Peng

2 1

Re: [seL4] quesitons about TK1 VMM
by Kent.Mcleod＠data61.csiro.au 13 Jan '17

13 Jan '17

Hi Peng, Adding the ethernet card requires adding the 0 ASID in the vm.camkes file that I mentioned in the previous email. vm.smmu = [0, 10, 24]; This gives permission for PCIE devices to read and write to memory. I confirmed that on the TK1 Jetson the ethernet port works after this change. You may need to run "ifconfig eth0 up" to enable the device once the image boots. Regards, Kent. ? ________________________________ From: PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 12:13 PM To: Mcleod, Kent (Data61, Kensington NSW) Subject: Re: quesitons about TK1 VMM Kent, I am using NVIDIA Jetson TK1 board. The reason I want to use insecure config is to enable VM Linux to use Ethernet port. I do not care about the SD card. How can I just add Ethernet card? is there a way for me to avoid adding SD card to The VM linux as you just suggest in your email? Thanks Peng On Thursday,January 12, 2017, <Kent.Mcleod(a)data61.csiro.au<mailto:Kent.Mcleod@data61.csiro.au>> wrote: Hi Peng, Which hardware are you using to run the image? This project has only been tested on the TK1-SOM made by Colorado Engineering. The ethernet port doesn't work as the version of Linux that we use doesn't support it. As for your second question, we configure the IOMMU to only let Linux use the emmc device and USB device on the TK1-SOM. The error is caused because Linux is trying to access a SD card device that it isn't authorized to access. The TK1-SOM doesn't have any SD card hardware so camkes doesn't set up access. If you want to use the Insecure config then you will need to modify apps/vm/vm.camkes and add the right ID to vm.smmu on line 443. To find out which ID to add we take the ID:98 from your Address translation error and look it up in the TK1 technical reference manual. In the memory controller section of the manual there is a "Error Data Capture: Status" section that starts on page 716. Using the table there you can look up ID:98 to see that it belongs to the SWGROUP sdmmc3a. We can now take this and look in seL4 ("kernel/include/plat/tk1/plat/machine/smmu.h?") to find the relevant ASID. From the list of ASIDs we see that SMMU_SDMMC3A_ASID is defined as 23. This is the ID that needs to be added to the vm.smmu array in vm.camkes. Hope this helps, Regards, Kent. ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 9:03 AM To: devel(a)sel4.systems Subject: [seL4] quesitons about TK1 VMM Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

2 1

quesitons about TK1 VMM
by PX 12 Jan '17

12 Jan '17

Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

1 0

question about SEL4PROJ /camkes-arm-vm-manifest
by PX 12 Jan '17

12 Jan '17

Hi, all I try to build a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. However, I can not compile it. I get errors when the compiler tries to build "camkes-accelerator" . I don't put any new code yet. I just: 1) repo init the url ; 2) repo sync; 3) make tk1_vm_defconfig; and 4) make. Did I do something wrong here? thanks Peng

2 5