Hi Siwei, So, I tried the code using Kingston microSDHC but it still couldnt read the card. However, the code works perfectly when loaded from the SD slot (with microSD to SD adapter), instead of the microSD slot. I also found that for some reasons, if mmc dev 1 is used in u-boot, the program wouldnt be able to read/write the micro-sd card. I'm kind of good for now but still curious about that. Do you have any idea what might have caused this? Best, Oak On Mon, Jan 23, 2017 at 11:07 AM, Norrathep Rattanavipanon <nrattana@uci.edu
wrote:
Thanks Siwei. I really appreciate your help. Yeah so I tried your image with three different micro-sd cards and none of them works (still stuck after printing the card's capacity). I'll buy Kingston microsdhc class 4 and try on that, will let you know if it works or not.
Best, Oak
On Mon, Jan 23, 2017 at 12:03 AM, <Siwei.Zhuang@data61.csiro.au> wrote:
Hi Oak,
Here is what exactly I did,
$ mkdir sel4-sdcard
$ cd sel4-sdcard
$ repo init -u https://github.com/SEL4PROJ/sel4-tutorials-manifest.git -m sel4-tutorials-master.xml
$ repo sync
$ cd projects
$ git clone https://github.com/SEL4PROJ/projects_libs.git
$ cd ../libs
$ ln -sf ../projects/projects_libs/libsdhcdrivers libsdhcdrivers
$ ln -sf ../projects/seL4_libs/libsel4sync libsel4sync
Then, I copied my sdcard app into sel4-sdcard/apps.
The sdcard app directory has Kconfig, Kbuild, Makefile and src/main.c
------------ Kconfig ---------------- menuconfig APP_SDCARD bool "SD card" default y depends on HAVE_LIBC depends on LIB_SEL4_PLAT_SUPPORT depends on LIB_SEL4_VKA depends on LIB_SEL4_UTILS depends on LIB_UTILS depends on LIB_CPIO depends on LIB_SEL4 depends on LIB_ELF help SD card app.
------------ Kbuild ----------------- apps-$(CONFIG_APP_SDCARD) += sdcard
sdcard: common libsel4utils libutils libsel4 libmuslc libsel4muslcsys \ libsel4vka libsel4allocman libsel4vspace libsel4simple libsel4simple-default \ libsel4platsupport libsel4platsupport libcpio libelf \ libsel4sync libsdhcdrivers libsel4debug
------------ Makefile --------------- # Targets TARGETS := sdcard.bin
ENTRY_POINT := _sel4_start
# Source files required to build the target CFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/*.c)) ASMFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/*.S)) OFILES := archive.o
# Libraries required to build the target LIBS = c sel4 sel4muslcsys sel4vka sel4allocman \ platsupport sel4platsupport sel4vspace elf \ sel4utils sel4simple utils sel4simple-default cpio \ sel4sync sdhcdrivers sel4debug #CFLAGS += -Werror
include $(SEL4_COMMON)/common.mk
archive.o: ${COMPONENTS} $(Q)mkdir -p $(dir $@) ${COMMON_PATH}/files_to_obj.sh $@ _cpio_archive $^
I also edited sel4-sdcard/Kconfig, added the following to the related menus,
source "apps/sdcard/Kconfig"
source "libs/libsdhcdrivers/Kconfig"
source "libs/libsel4sync/Kconfig"
I've attached the config file, copy it to configs directory, then do "make sdcard_defconfig".
I've also attached the binary image that I compiled.
Since the u-boot command works, it doesn't seem that the controller is disabled. Also try another card if possible, my card is Kingston micro SDHC class 4. The driver only implements very basic single block read/write. I'm not surprised that it doesn't work for some cards.
- Siwei
------------------------------ *From:* Norrathep Rattanavipanon <nrattana@uci.edu> *Sent:* Monday, 23 January 2017 4:59 PM *To:* Zhuang, Siwei (Data61, Kensington NSW)
*Subject:* Re: [seL4] SDHC drivers (cont.)
Hi Siwei,
Thank you for helping me out. I am still unable to get it to work even if using your code with the latest kernel (4.0) and latest libraries (downloaded from https://github.com/SEL4PROJ/sel4-tutorials-manifest master branch)
I also tried calling mmc read command in u-boot and it was able to read data from the card just fine. I'm not really sure how I can check if the host controller works properly. Do you mean I can do it in seL4?
Also, is it possible if you can upload the binary image file (and the build config) so that I can test on my board really quick? I suspect that either I miss something for the build or my micro-sd is not working.
Thank you again for your help, Oak
On Thu, Jan 19, 2017 at 11:12 AM, Norrathep Rattanavipanon < nrattana@uci.edu> wrote:
Hi Siwei,
Yes, I believe mmc_card_capacity returns the correct value (4026531840 <(402)%20653-1840> - 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@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@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.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 listDevel@sel4.systemshttps://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
-- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine
-- 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, That's interesting. i.MX6 has 4 host controllers(SDHC). The first and the second one are not connected on SabreLite. SDHC3 is connected to the SD card slot, and SDHC4 is connected to the micro-SD card slot. If you take a closer look at the board, on the left side of the micro-SD card slot, there's a label says "SD4" and "SD3" right above the SD card slot. When calling "sdio_default_id()", the function would return "SDHC4"(defined in libsdhcdrivers/plat_include/imx6/sdhc/plat/sdio.h) which should be the micro-SD card slot. I double-checked with the reference manual, the device memory address in the source code is correct. Maybe your SabreLite is a different revision. You could try passing SDHC1/2/3 to function "sdio_init()" as sdio_id, to find out which one is connected to the micro-SD card slot. But this doesn't explain why you've got the correct card capacity out of a different slot. I'm totally confused. Anyway, good to know the code works finally, although in an unexpected way. - Siwei On Fri, Feb 10, 2017 at 08:20:09PM -0800, Norrathep Rattanavipanon wrote: #Hi Siwei, # #So, I tried the code using Kingston microSDHC but it still couldnt read the #card. # #However, the code works perfectly when loaded from the SD slot (with microSD to #SD adapter), instead of the microSD slot. I also found that for some reasons, #if mmc dev 1 is used in u-boot, the program wouldnt be able to read/write the #micro-sd card. # #I'm kind of good for now but still curious about that. Do you have any idea #what might have caused this? # #Best, #Oak # #On Mon, Jan 23, 2017 at 11:07 AM, Norrathep Rattanavipanon <nrattana@uci.edu> #wrote: # # Thanks Siwei. I really appreciate your help. # Yeah so I tried your image with three different micro-sd cards and none of # them works (still stuck after printing the card's capacity). # I'll buy Kingston microsdhc class 4 and try on that, will let you know if # it works or not. # # Best, # Oak # # On Mon, Jan 23, 2017 at 12:03 AM, <Siwei.Zhuang@data61.csiro.au> wrote: # # # Hi Oak, # # # Here is what exactly I did, # # # $ mkdir sel4-sdcard # # $ cd sel4-sdcard # # $ repo init -u https://github.com/SEL4PROJ/ # sel4-tutorials-manifest.git -m sel4-tutorials-master.xml # # $ repo sync # # $ cd projects # # $ git clone https://github.com/SEL4PROJ/projects_libs.git # # $ cd ../libs # # $ ln -sf ../projects/projects_libs/libsdhcdrivers libsdhcdrivers # # $ ln -sf ../projects/seL4_libs/libsel4sync libsel4sync # # # Then, I copied my sdcard app into sel4-sdcard/apps. # # The sdcard app directory has Kconfig, Kbuild, Makefile and src/main.c # # # ------------ Kconfig ---------------- # # menuconfig APP_SDCARD # bool "SD card" # default y # depends on HAVE_LIBC # depends on LIB_SEL4_PLAT_SUPPORT # depends on LIB_SEL4_VKA # depends on LIB_SEL4_UTILS # depends on LIB_UTILS # depends on LIB_CPIO # depends on LIB_SEL4 # depends on LIB_ELF # help # SD card app. # # # # ------------ Kbuild ----------------- # # apps-$(CONFIG_APP_SDCARD) += sdcard # # sdcard: common libsel4utils libutils libsel4 libmuslc libsel4muslcsys # \ # libsel4vka libsel4allocman libsel4vspace libsel4simple # libsel4simple-default \ # libsel4platsupport libsel4platsupport libcpio libelf \ # libsel4sync libsdhcdrivers libsel4debug # # # ------------ Makefile --------------- # # # Targets # TARGETS := sdcard.bin # # ENTRY_POINT := _sel4_start # # # Source files required to build the target # CFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/ # src/*.c)) # ASMFILES := $(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/ # src/*.S)) # OFILES := archive.o # # # Libraries required to build the target # LIBS = c sel4 sel4muslcsys sel4vka sel4allocman \ # platsupport sel4platsupport sel4vspace elf \ # sel4utils sel4simple utils sel4simple-default cpio \ # sel4sync sdhcdrivers sel4debug # #CFLAGS += -Werror # # include $(SEL4_COMMON)/common.mk # # archive.o: ${COMPONENTS} # $(Q)mkdir -p $(dir $@) # ${COMMON_PATH}/files_to_obj.sh $@ _cpio_archive $^ # # # # I also edited sel4-sdcard/Kconfig, added the following to the related # menus, # # source "apps/sdcard/Kconfig" # # source "libs/libsdhcdrivers/Kconfig" # # source "libs/libsel4sync/Kconfig" # # # I've attached the config file, copy it to configs directory, then do # "make sdcard_defconfig". # # I've also attached the binary image that I compiled. # # # Since the u-boot command works, it doesn't seem that the controller is # disabled. Also try another card if possible, my card is Kingston micro # SDHC class 4. The driver only implements very basic single block read/ # write. I'm not surprised that it doesn't work for some cards. # # # - Siwei # # # ━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━━ # From: Norrathep Rattanavipanon <nrattana@uci.edu> # Sent: Monday, 23 January 2017 4:59 PM # To: Zhuang, Siwei (Data61, Kensington NSW) # # Subject: Re: [seL4] SDHC drivers (cont.) # # Hi Siwei, # # Thank you for helping me out. I am still unable to get it to work even # if using your code with the latest kernel (4.0) and latest libraries # (downloaded from https://github.com/SEL4PROJ/sel4-tutorials-manifest # master branch) # # I also tried calling mmc read command in u-boot and it was able to read # data from the card just fine. # I'm not really sure how I can check if the host controller works # properly. Do you mean I can do it in seL4? # # Also, is it possible if you can upload the binary image file (and the # build config) so that I can test on my board really quick? I suspect # that either I miss something for the build or my micro-sd is not # working. # # Thank you again for your help, # Oak # # On Thu, Jan 19, 2017 at 11:12 AM, Norrathep Rattanavipanon < # nrattana@uci.edu> wrote: # # 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@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@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.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.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 # # # # # -- # Norrathep (Oak) Rattanavipanon # M.S. in Computer Science # University of California - Irvine # # # # # -- # Norrathep (Oak) Rattanavipanon # M.S. in Computer Science # University of California - Irvine # # # # #-- #Norrathep (Oak) Rattanavipanon #M.S. in Computer Science #University of California - Irvine -- Siwei Zhuang Research Engineer DATA61 | CSIRO E siwei.zhuang@data61.csiro.au T +61 2 8306 0516 Level 3, K17 Building, UNSW Gate 14, Barker Street, Kensington, NSW 2033 www.data61.csiro.au CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61
participants (2)
-
Norrathep Rattanavipanon -
Siwei.Zhuang＠data61.csiro.au