mmc.system

<?xml version="1.0" encoding="UTF-8"?>
<system>
    <!-- This is a 4KB, page-aligned memory region at the physical address of
    0x3f200000, which is where the GPIO registers are mapped to. -->
    <memory_region
            name="gpio"
            size="0x1_000"
            phys_addr="0x3f200000"/>
    <!-- This is a 4KB, page-aligned memory region at the physical address of
    0x3f_003_000, which is where the Timer registers are mapped to. -->
    <memory_region
            name="timer"
            size="0x1_000"
            phys_addr="0x3f_003_000"/>
    <!-- This is a 4KB, page-aligned memory region at the physical address of
    0x3f_300_000, which is where the EMMC registers are mapped to. -->
    <memory_region
            name="emmc"
            size="0x1_000"
            phys_addr="0x3f_300_000"/>
    <!-- This is a 4KB, page-aligned memory region at the physical address of
    0x3f215000, which is where the UART device registers are mapped to. Note, we
    are mapping in the Rpi3B's "Mini" UART device registers and NOT its "PL011"
    UART device registers. An important aspect to note that the base of the Mini
    UART device registers are actually mapped to 0x3f215040 in physical memory.
    Unfortunately, 0x3f215040 is not a 4K page-aligned address, so we can't map
    a page at that physical address. As such in our `serial_driver.c` code, we
    must remember to obtain the real base address of the Mini UART device by
    adding 0x40 to 0x3f215000. -->
    <memory_region
            name="uart"
            size="0x1_000"
            phys_addr="0x3f215000"/>
    <!-- In the SDDF's design-documentation, `shared_dma` is referred to as the
    "Data Region". `shared_dma` is an array of I/O buffers that will be used to
    pass/transport data from `serial_client` to `serial_driver` and vice-versa.
    The `shared_dma` memory region MUST be mapped at the exact same virtual
    memory address in all the PDs that use the `shared_dma`. If they aren't
    mapped to the same address, the SDDF's ring buffer mechanism of transporting
    data across PDs will NOT work. This is because the SDDF's ring buffer
    mechanism passes the virtual address of a `shared_dma` buffer from PD to PD,
    which enables the SDDF's transport mechanism to be zero-copy. Theoretically,
    the requirement to map the `shared_dma` to the same virtual address in
    various PDs could be alleviated if there existed a mechanism to translate
    virtual addresses across PDs (VSpaces); however, such a mechanism does NOT
    currently exist. -->
    <memory_region
            name="shared_dma"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- This is a 2MB memory region with a 2MB page size. An explanation of the
    purpose of this memory region is provided in `serial_client.c`. The SDDF
    does not require this memory region to be mapped to a specific virtual
    address. -->
    <memory_region
            name="tx_avail_ring_buf"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- This is a 2MB memory region with a 2MB page size. An explanation of the
    purpose of this memory region is provided in `serial_client.c`. The SDDF
    does not require this memory region to be mapped to a specific virtual
    address. -->
    <memory_region
            name="tx_used_ring_buf"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- This is a 2MB memory region with a 2MB page size. An explanation of the
    purpose of this memory region is provided in `serial_client.c`. The SDDF
    does not require this memory region to be mapped to a specific virtual
    address. -->
    <memory_region
            name="rx_avail_ring_buf"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- This is a 2MB memory region with a 2MB page size. An explanation of the
    purpose of this memory region is provided in `serial_client.c`. The SDDF
    does not require this memory region to be mapped to a specific virtual
    address. -->
    <memory_region
            name="rx_used_ring_buf"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- A shared buffer to pass chars from `mmc_driver.c` to `serial_client.c`. -->
    <memory_region
            name="mmc_to_serial_client_putchar_buf"
            size="0x1_000"
            page_size="0x1_000"/>
    <!-- A shared buffer to pass chars from `fatfs.c` to `serial_client.c`. -->
    <memory_region
            name="fatfs_to_serial_client_putchar_buf"
            size="0x1_000"
            page_size="0x1_000"/>
    <!-- A 2MB shared data region for passing data between `mmc_driver` and
    `fatfs`. -->
    <memory_region
            name="mmc_driver_shared_data"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- A 2MB shared data region for sending requests from `fatfs` to
    `mmc_driver`. -->
    <memory_region
            name="mmc_driver_request_queue"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- A 2MB shared data region for sending responses from `mmc_driver` to
    `fatfs`. -->
    <memory_region
            name="mmc_driver_response_queue"
            size="0x200_000"
            page_size="0x200_000"/>
    <!-- The `serial_driver` PD must have a higher priority than the
    `serial_client` PD so that it doesn't get preempted by `serial_client` when
    it is busy writing to the UART device. -->
    <protection_domain
            name="serial_driver"
            priority="101"
            pp="true">
        <program_image path="serial_driver.elf"/>
        <!-- We map our physical memory to the virtual address at 0x5_000_000 -->
        <map
                mr="uart"
                vaddr="0x5_000_000"
                perms="rw"
                cached="false"
                setvar_vaddr="uart_base_vaddr"/>
        <!--
        BCM2835/2837 TRM
        Section 7.5
        The mini-UART from the AUX peripheral triggers IRQ 29 ("Aux int")
        on the VideoCore, which then signals pending GPU interrupts
        to the ARM core.

        The PL011 triggers IRQ 57 ("uart_int").

        The seL4 kernel's interrupt controller driver creates a linear mapping
        of all interrupts in the system (see
        include/drivers/bcm2836-armctrl-ic.h) with 32 ARM PPIs, 32 basic
        interrupts and 64 GPU interrupts.

        Thus, the actual interrupts to be used in userland are: 93 (=32+32+29).
        mini-UART 32+32+29 = 93
        PL011 UART 32+32+57 = 121
        -->
        <irq irq="93" id="2" />
        <!-- As per our earlier comment on `shared_dma`, `shared_dma` is always
        mapped to the same virtual address of 0x2_400_000 for ALL PDs (which is
        a requirement and assumption of the SDDF's transport mechanism). -->
        <map
                mr="shared_dma"
                vaddr="0x2_400_000"
                perms="rw"
                cached="true"
                setvar_vaddr="shared_dma" />
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="tx_avail_ring_buf"
                vaddr="0x7_000_000"
                perms="rw"
                cached="true"
                setvar_vaddr="tx_avail_ring_buf"/>
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="tx_used_ring_buf"
                vaddr="0x7_200_000"
                perms="rw"
                cached="true"
                setvar_vaddr="tx_used_ring_buf"/>
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="rx_avail_ring_buf"
                vaddr="0x7_400_000"
                perms="rw"
                cached="true"
                setvar_vaddr="rx_avail_ring_buf"/>
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="rx_used_ring_buf"
                vaddr="0x7_600_000"
                perms="rw"
                cached="true"
                setvar_vaddr="rx_used_ring_buf"/>
    </protection_domain>
    <!-- The `serial_client` PD must have a lower priority than the
    `serial_driver` PD so that it doesn't preempt `serial_client` when it is
    busy writing to the UART device. -->
    <protection_domain
            name="serial_client"
            priority="100"
            pp="true">
        <program_image path="serial_client.elf"/>
        <!-- As per our earlier comment on `shared_dma`, `shared_dma` is always
        mapped to the same virtual address of 0x2_400_000 for ALL PDs (which is
        a requirement and assumption of the SDDF's transport mechanism). -->
        <map
                mr="shared_dma"
                vaddr="0x2_400_000"
                perms="rw"
                cached="true"
                setvar_vaddr="shared_dma" />
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="tx_avail_ring_buf"
                vaddr="0x6_000_000"
                perms="rw"
                cached="true"
                setvar_vaddr="tx_avail_ring_buf"/>
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="tx_used_ring_buf"
                vaddr="0x6_200_000"
                perms="rw"
                cached="true"
                setvar_vaddr="tx_used_ring_buf"/>
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="rx_avail_ring_buf"
                vaddr="0x6_400_000"
                perms="rw"
                cached="true"
                setvar_vaddr="rx_avail_ring_buf"/>
        <!-- Unlike `shared_dma`, there is no limitation to where this memory
        region is mapped to in this PD's virtual address space. -->
        <map
                mr="rx_used_ring_buf"
                vaddr="0x6_600_000"
                perms="rw"
                cached="true"
                setvar_vaddr="rx_used_ring_buf"/>
        <map
                mr="mmc_to_serial_client_putchar_buf"
                vaddr="0x6_800_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_to_serial_client_putchar_buf"/>
        <map
                mr="timer_driver_to_serial_client_putchar_buf"
                vaddr="0x7_000_000"
                perms="rw"
                cached="true"
                setvar_vaddr="timer_driver_to_serial_client_putchar_buf"/>
        <map
                mr="fatfs_to_serial_client_putchar_buf"
                vaddr="0x7_200_000"
                perms="rw"
                cached="true"
                setvar_vaddr="fatfs_to_serial_client_putchar_buf"/>
    </protection_domain>
    <!-- Channel between `serial_client` and `serial_driver` for printf() calls
    by `serial_client`. -->
    <channel>
        <end pd="serial_client" id="3" />
        <end pd="serial_driver" id="4" />
    </channel>
    <!-- Channel between `serial_client` and `serial_driver` for getchar() calls
    by `serial_client`. -->
    <channel>
        <end pd="serial_client" id="5" />
        <end pd="serial_driver" id="6" />
    </channel>
    <!-- A shared buffer for `mmc_driver.c` to obtain num ticks from
    `timer_driver.c`. -->
    <memory_region
            name="timer_driver_to_mmc_driver_numticks_buf"
            size="0x1_000"
            page_size="0x1_000"/>
    <!-- A shared buffer to pass chars from `timer_driver.c` to `serial_client.c`. -->
    <memory_region
            name="timer_driver_to_serial_client_putchar_buf"
            size="0x1_000"
            page_size="0x1_000"/>
    <!-- Protection Domain for Timer driver. -->
    <protection_domain
            name="timer_driver"
            priority="99"
            pp="true">
        <program_image path="timer_driver.elf"/>
        <!-- Memory region mapped to Timer registers. -->
        <map
                mr="timer"
                vaddr="0x2_200_000"
                perms="rw"
                cached="false"
                setvar_vaddr="timer_base_vaddr"/>
        <!-- Shared memory region for `timer_driver` PD to pass num ticks to
        `mmc` PD.-->
        <map
                mr="timer_driver_to_mmc_driver_numticks_buf"
                vaddr="0x2_600_000"
                perms="rw"
                cached="true"
                setvar_vaddr="timer_driver_to_mmc_driver_numticks_buf"/>
    </protection_domain>
    <!-- Channel between `timer_driver` and `serial_client` for printf()
    calls by `timer_driver`. -->
    <channel>
        <end pd="timer_driver" id="9" />
        <end pd="serial_client" id="10" />
    </channel>
    <!-- Protection Domain for MultiMediaCard driver. -->
    <protection_domain
            name="mmc_driver"
            priority="98"
            pp="true">
        <program_image path="mmc_driver.elf"/>
        <!-- Shared memory region for `timer_driver` PD to pass num ticks to
        `mmc` PD.-->
        <map
                mr="timer_driver_to_mmc_driver_numticks_buf"
                vaddr="0x2_600_000"
                perms="rw"
                cached="true"
                setvar_vaddr="timer_driver_to_mmc_driver_numticks_buf"/>
        <!-- Shared memory region for `mmc_driver` PD to pass characters to
        `serial_client` to print. -->
        <map
                mr="mmc_to_serial_client_putchar_buf"
                vaddr="0x3_000_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_to_serial_client_putchar_buf"/>
        <!-- Memory region mapped to GPIO registers. Since this region of memory
        is memory-mapped, we turn caching off. -->
        <map
                mr="gpio"
                vaddr="0x3_002_000"
                perms="rw"
                cached="false"
                setvar_vaddr="gpio_base_vaddr"/>
        <!-- Memory region mapped to EMMC registers. Since this region of memory
        is memory-mapped, we turn caching off. -->
        <map
                mr="emmc"
                vaddr="0x3_004_000"
                perms="rw"
                cached="false"
                setvar_vaddr="emmc_base_vaddr"/>
        <!-- A shared memory region for passing requests from `fatfs` to
        `mmc_driver`. -->
        <map
                mr="mmc_driver_request_queue"
                vaddr="0x3_200_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_driver_request_queue" />
        <!-- A shared memory region for passing responses from `mmc_driver` to
        `fatfs`. -->
        <map
                mr="mmc_driver_response_queue"
                vaddr="0x3_400_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_driver_response_queue" />
        <!-- A shared memory region for passing data between `mmc_driver` and
        `fatfs`. -->
        <map
                mr="mmc_driver_shared_data"
                vaddr="0x4_000_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_driver_shared_data" />
    </protection_domain>
    <!-- Channel between `mmc_driver` and `serial_client` for printf()
    calls by `mmc_driver`. -->
    <channel>
        <end pd="mmc_driver" id="7" />
        <end pd="serial_client" id="8" />
    </channel>
    <!-- Channel between `mmc_driver` and `timer_driver` for get_num_ticks()
    calls by `mmc_driver`. -->
    <channel>
        <end pd="mmc_driver" id="11"/>
        <end pd="timer_driver" id="12"/>
    </channel>
    <!-- Protection Domain for FAT File System. -->
    <protection_domain
            name="fatfs"
            priority="97"
            pp="true">
        <program_image path="fatfs.elf"/>
        <!-- Shared memory region for `fatfs` PD to pass characters to
        `serial_client` to print. -->
        <map
                mr="fatfs_to_serial_client_putchar_buf"
                vaddr="0x2_600_000"
                perms="rw"
                cached="true"
                setvar_vaddr="fatfs_to_serial_client_putchar_buf"/>
        <!-- A shared memory region for passing requests from `fatfs` to
        `mmc_driver`. -->
        <map
                mr="mmc_driver_request_queue"
                vaddr="0x2_800_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_driver_request_queue" />
        <!-- A shared memory region for passing responses from `mmc_driver` to
        `fatfs`. -->
        <map
                mr="mmc_driver_response_queue"
                vaddr="0x3_000_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_driver_response_queue" />
        <!-- A shared memory region for passing data between `mmc_driver` and
        `fatfs`. -->
        <map
                mr="mmc_driver_shared_data"
                vaddr="0x4_000_000"
                perms="rw"
                cached="true"
                setvar_vaddr="mmc_driver_shared_data" />
    </protection_domain>
    <channel>
        <end pd="fatfs" id="13"/>
        <end pd="serial_client" id="14"/>
    </channel>
    <channel>
        <end pd="fatfs" id="15"/>
        <end pd="mmc_driver" id="16"/>
    </channel>
</system>