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@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

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@sel4.systems on behalf of Norrathep Rattanavipanon nrattana@uci.edu Sent: Thursday, 19 January 2017 9:54 AM To: Danis, Adrian (Data61, Kensington NSW) Cc: devel@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@data61.csiro.aumailto: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@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine