So I use the following code to create a new buffer for vaddr and paddr : void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 1, seL4PageBits); seL4_CPtr frame_cap = vsapce_get_cap(&vspace, vaddr); seL4_ARM_Page_GetAddress_t gaddr = seL4_ARCH_Page_GetAddress(frame_cap); uintptr_t paddr = (uintptr_t) gaddr.paddr; long read_len = mmc_block_read(*mmc_card, 0x5, 1, vaddr, paddr, NULL, NULL); but the code is still stuck in mmc_block_read function. Anything I might be missing here? Thanks for the help, Oak On Fri, Oct 14, 2016 at 11:06 AM, Norrathep Rattanavipanon

wrote:

Ah I see. That might be a problem. I thought that function will automatically build a mapping so I can use any vaddr,

Thanks Alex!

On Thu, Oct 13, 2016 at 8:38 PM, wrote:

...

Hi Oak,

Your code looks fine, but where do these numbers come from?

void* vaddr = (void*) 0x1980000; uintptr_t paddr = (uintptr_t) 0x119a7000;

vaddr should be the virtual address of a buffer to which the block should be read, and paddr should be the physical address of this buffer.

- Alex

On Thu, 2016-10-13 at 17:33 -0700, Norrathep Rattanavipanon wrote:

...

Is there any example on how to use sdhc driver in (https://github.com/SEL4PROJ/projects_libs/tree/master/libsdhcdrivers)?

Currently, I'm struggling to read a block of data from micro-sd in seL4. I use the following code (assertions are omitted here for readability) to instantiate the driver :

ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper);

ps_dma_man_t dma_man = {0}; error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man);

ps_io_ops_t io_ops = { .io_mapper = io_mapper, .dma_manager = dma_man };

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(); error = sdio_init(id, &io_ops, dev);

mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card);

void* vaddr = (void*) 0x1980000;

uintptr_t paddr = (uintptr_t) 0x119a7000;

long read_len = mmc_block_read(*mmc_card, 0, 5, vaddr, paddr, NULL, NULL);

And the code's stuck in mmc_block_read function where interrupt status (BRR and BWR) are never on.

Thanks in advance, Oak

-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine _______________________________________________ Devel mailing list 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

Hi Oak, You can also try setting the 3rd argument of vspace_new_pages to 0 instead of 1. Currently it will map the pages in cached, and unless the driver is flushing the caches itself (which it can't, as it doesn't have the caps passed into it) the changes won't get past the caches. 0 tells the vspace code to map the pages in uncached. Cheers, Anna. -----Original Message----- From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of Alexander.Kroh@data61.csiro.au Sent: Wednesday, 19 October 2016 12:06 PM To: nrattana@uci.edu Cc: devel@sel4.systems; Kroh, Alexander (Data61, Kensington NSW) Subject: Re: [seL4] SDHC driver in Sabre Lite Hi Oak, I don't suppose that any of those calls are returning errors? DMA is optional for the SDHC. It has been a while since I looked at the code, but I believe that passing 0 as the paddr will prevent the driver from using DMA. Of course, this is not a solution to your problem, but it could eliminate one point of failure as you could allocate a buffer with malloc isntead. - Alex On Tue, 2016-10-18 at 17:28 -0700, Norrathep Rattanavipanon wrote:

So I use the following code to create a new buffer for vaddr and paddr : void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 1, seL4PageBits);

seL4_CPtr frame_cap = vsapce_get_cap(&vspace, vaddr); seL4_ARM_Page_GetAddress_t gaddr = seL4_ARCH_Page_GetAddress(frame_cap);

uintptr_t paddr = (uintptr_t) gaddr.paddr;

long read_len = mmc_block_read(*mmc_card, 0x5, 1, vaddr, paddr, NULL, NULL); but the code is still stuck in mmc_block_read function. Anything I might be missing here? Thanks for the help, Oak

On Fri, Oct 14, 2016 at 11:06 AM, Norrathep Rattanavipanon wrote: Ah I see. That might be a problem. I thought that function will automatically build a mapping so I can use any vaddr,

Thanks Alex!

On Thu, Oct 13, 2016 at 8:38 PM, wrote: Hi Oak,

Your code looks fine, but where do these numbers come from?

void* vaddr = (void*) 0x1980000; uintptr_t paddr = (uintptr_t) 0x119a7000;

vaddr should be the virtual address of a buffer to which the block should be read, and paddr should be the physical address of this buffer.

- Alex

On Thu, 2016-10-13 at 17:33 -0700, Norrathep Rattanavipanon wrote: > Is there any example on how to use sdhc driver in > (https://github.com/SEL4PROJ/projects_libs/tree/master/libsdhcdrivers)? > > > Currently, I'm struggling to read a block of data from micro-sd in > seL4. > I use the following code (assertions are omitted here for readability) > to instantiate the driver : > > > > > ps_io_mapper_t io_mapper = {0}; > error = sel4platsupport_new_io_mapper(simple, vspace, vka, > &io_mapper); > > ps_dma_man_t dma_man = {0}; > error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); > > ps_io_ops_t io_ops = { > .io_mapper = io_mapper, > .dma_manager = dma_man > }; > > 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(); > error = sdio_init(id, &io_ops, dev); > > mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); > error = mmc_init(dev, &io_ops, mmc_card); > > > void* vaddr = (void*) 0x1980000; > > uintptr_t paddr = (uintptr_t) 0x119a7000; > > long read_len = mmc_block_read(*mmc_card, 0, 5, vaddr, paddr, NULL, > NULL); > > > > And the code's stuck in mmc_block_read function where interrupt status > (BRR and BWR) are never on. > > > Thanks in advance, > Oak > > > > > -- > Norrathep (Oak) Rattanavipanon > M.S. in Computer Science > University of California - Irvine

> _______________________________________________ > Devel mailing list > 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

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel