[seL4] ARM Vchan Error

21 Mar 2018

      Hi all,

I’m trying to make Vchan work on camkes-arm-vm in the process I encountered a couple problems. Hope you can give me some advice. I knew that Vchan is out dated and never finished on ARM. But it seems the only option for now (please correct me if I’m wrong).

Here is what I did so far:

1. modified tk1_vmlinux.c by adding the virtual device and fault handler and installed it to guest linux with vm_add_device(vm, &vchan_dev);

---------------------------------------------------
vchan_device_fault_handler(struct device* d UNUSED, vm_t* vm, fault_t* fault){
    //uint32_t data = fault_get_data(fault);
    uint32_t data = fault_get_ctx(fault)->r1;
    vchan_entry_point(vm, data);
    // fflush(stdout);
    advance_fault(fault);
    return 0;
}

struct device vchan_dev = {
        .devid = DEV_CUSTOM,
        .name = "vchan-driver",
        .pstart = 0x2040000,
        .size = 0x1000,
        .handle_page_fault = &vchan_device_fault_handler,
        .priv = NULL,
    }; 
---------------------------------------------------

2. compiled linux-tegra using buildroot (by the way the current linux-tegra is 4.9.0 which is not supported by buildroot-2016, the earliest version works for me is buildroot-2017-2), added a vmm-manager kernel driver similar to the one in camkes-x86-vm. But I changed the call_into_hypervisor() to the following:

---------------------------------------------------
int call_into_hypervisor(int cmd, void *data, size_t sz, vmcall_args_t *vmcall) {

    int res = 0;
    int err;
    unsigned phys_ptr = virt_to_phys(vmcall);

    vmcall->data = data;
    vmcall->cmd = cmd;
    vmcall->phys_data = virt_to_phys(data);
    vmcall->size = sz;

    down(&hyp_sem);

    /*
        Set up arguments for the ARM hyp call
    */
    asm volatile ("mov r0, %0; mov r1, %1" : : "r" (VMM_MANAGER_TOKEN), "r" (phys_ptr): "%r0", "%r1");
    asm volatile (".arch_extension virt\n\t” "hvc #0");
    asm volatile ("mov %0, r0" : "=r" (res) : : );

    err = vargs->err;
    up(&hyp_sem);
    return err;
}
---------------------------------------------------

The kernel built and run correctly. But when I try to install the kernel driver. It crashed with following information.

---------------------------------------------------
# modprobe driver.ko
[81.826621] driver: loading out-of-tree module taints kernel
Bad sys call from [Linux]: scone 0 at PC: 0xbf000214
Assertion failed” !err (/camkes-arm-vm/libs/libsel4arm-vmm/src/vm.c: vm_event: 407)
—————————————————————————

I’m not sure if this error is triggered by the modified  call_into_hypervisor() or by event_thread_run()->eventfd_signal(). 

Any help would be appreciated! Thanks in advance.

Best Regards
-Daniel Wang