Блог

Короче говоря:

Я пытаюсь запустить микроядро sel4 внутри виртуальной машины x86_64 и не могу заставить интерфейс Ethernet работать. Какова правильная процедура для подключения к Интернету (через устройство vitio-net ethernet) на микроядре sel4? И каковы правильные адреса (памяти)?

Длинная версия:

Я пробовал примеры camkes (picoserver) с сетевым устройством e1000, но не смог заставить их работать, поэтому я решил изучить некоторые новые вещи и начать с нуля. Также я решил использовать virtio-net (вместе с vhost) вместо эмулируемого устройства e1000 для повышения производительности. Мой план состоит в том, чтобы использовать ethif_virtio_pci_init для инициализации eth_driver структуры, а затем передать структуру в picoTCP. На данный момент я могу найти устройство virtio PCI в sel4, но я не уверен, как правильно получить к нему доступ и создать ethif_virtio_pci_config_t необходимое для ethif_virtio_pci_init .

Некоторая информация из libethdrivers virtio_pci.h:

 typedef struct ethif_virtio_pci_config {
    uint16_t io_base;
    void *mmio_base;
} ethif_virtio_pci_config_t;

/**
 * This function initialises the hardware and conforms to the ethif_driver_init
 * type in raw.h
 * @param[out] eth_driver   Ethernet driver structure to fill out
 * @param[in] io_ops        A structure containing os specific data and
 *                          functions.
 * @param[in] config        Pointer to a ethif_virtio_pci_config struct
 */
int ethif_virtio_pci_init(struct eth_driver *eth_driver, ps_io_ops_t io_ops, void *config);
 

итак, для ethif_virtio_pci_config_t мне нужен адрес uint16_t io_base и указатель на базу MMIO.

Это информация, которую я получил до сих пор:

 Found virtio_net_pci device
    BASE_ADDR[0] ----
        base_addr_space[0]: 0x1 [PCI_BASE_ADDRESS_SPACE_IO]
        base_addr_type[0]: 0x0 [ 32bit ]
        base_addr_prefetchable[0]: no
        base_addr[0]: 0xc000
        base_addr_size_mask[0]: 0xffffffe0
    BASE_ADDR[1] ----
        base_addr_space[1]: 0x0 [PCI_BASE_ADDRESS_SPACE_MEMORY]
        base_addr_type[1]: 0x0 [ 32bit ]
        base_addr_prefetchable[1]: no
        base_addr[1]: 0xfeb91000
        base_addr_size_mask[1]: 0xfffff000
    BASE_ADDR[2] ----
    BASE_ADDR[3] ----
    BASE_ADDR[4] ----
        base_addr_space[4]: 0x0 [PCI_BASE_ADDRESS_SPACE_MEMORY]
        base_addr_type[4]: 0x4 [ 64bit ]
        base_addr_prefetchable[4]: yes
        base_addr[4]: 0xfe000000
        base_addr_size_mask[4]: 0xffffc000
    BASE_ADDR[5] ----
 

Насколько я понимаю, теперь мне нужно сопоставить физический адрес с виртуальным. Для этого я создал IO-mapper, но я не уверен, что сопоставлять. Вся область dma, начинающаяся с 0x8000000, или только адрес устройства virtio? Насколько я понимаю, новый виртуальный адрес будет моим базовым указателем MMIO, но что такое uint16_t io_base, чем?

Пока это мой код, часть, в которой я не уверен, находится в конце:

 #define ALLOCATOR_STATIC_POOL_SIZE ((1 << seL4_LargePageBits) * 10)
static simple_t simple;
static ps_io_mapper_t io_mapper;
static char allocator_mem_pool[ALLOCATOR_STATIC_POOL_SIZE];
static vka_t vka;
static vspace_t vspace;
static sel4utils_alloc_data_t data;
static ltimer_t timer;

int main() {

    PRINT_DBG("Hello Worldn");
    seL4_BootInfo *info = platsupport_get_bootinfo();

    simple_default_init_bootinfo(amp;simple, info);

    /* print out bootinfo and other info about simple */
    // simple_print(amp;simple);

    allocman_t *allocman = bootstrap_use_current_simple(amp;simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool);
    if (allocman == NULL) {
        ZF_LOGF("Failed to create allocman");
    }
    allocman_make_vka(amp;vka, allocman);

    int error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(amp;vspace,
                                                          amp;data, simple_get_pd(amp;simple),
                                                          amp;vka, info);
    if (error != 0) {
       PRINT_DBG("Failed to create virtual memory manager. Error: %dn", error);
       return -1;
    }


    error = sel4platsupport_new_io_mapper(amp;vspace, amp;vka, amp;io_mapper);
    if (error != 0) {
        PRINT_DBG("Failed to create io mapper. Error: %dn", error);
        return -1;
    }

    ps_io_ops_t io_ops;
    error = sel4platsupport_new_io_ops(amp;vspace, amp;vka, amp;simple, amp;io_ops);
    if (error != 0) {
        PRINT_DBG("Failed to create io ops. Error: %dn", error);
        return -1;
    }

    ps_io_port_ops_t port_ops;
    int error = sel4platsupport_get_io_port_ops(amp;port_ops, amp;simple, amp;vka);
    if (error != 0) {
      PRINT_DBG("Failed to find io port ops. Error: %dn", error);
      return -1;
    }

    printf("Start scannningn");

    libpci_scan(port_ops);
    PRINT_DBG("Found %u devicesn", libpci_num_devices);
    for (uint32_t i = 0; i < libpci_num_devices;   i) {
      PRINT_DBG("PCI device %u. Vendor id: %x. Device id: %xn",
          i, libpci_device_list[i].vendor_id, libpci_device_list[i].device_id);
    }

    libpci_device_t* virtio_net_pci = libpci_find_device(0x1af4, 0x1000);
    if (!virtio_net_pci) {
      PRINT_DBG("Failed to find the virtio_net_pci devicen");
      // return -1;
    }else{
    // libpci_device_iocfg_debug_print(amp;virtio_net_pci->cfg,true);
        PRINT_DBG("Found virtio_net_pci devicen");
        libpci_device_iocfg_debug_print(amp;virtio_net_pci->cfg,false);
    }


    //Now what?

    unsigned long phys = 0x8000000; //what physical address to map?
    void *mmio_ptr = ps_io_map(amp;io_mapper, phys, 4096, 0, PS_MEM_NORMAL);
    memset(ptr, 0, 4096);
    if (mmio_ptr == NULL) {
        PRINT_DBG("Failed to map phys addr. Error: %pn", ptr);
        return -1;
    }

    ethif_virtio_pci_config_t me_config;
    me_config.mmio_base = mmio_ptr; //is this correct?
    //me_config.io_base = ?
 

Я много читал о ядре sel4, но я все еще новичок в большинстве концепций микроядра sel4 (и ядра Linux), поэтому я очень благодарен за любые советы и рекомендации. Обычно я работаю со встроенными, микроконтроллерами и другими «голыми металлическими» платформами и хотел узнать что-то новое, но пока многое очень сбивает с толку.