- Devel - lists.sel4.systems

ARM Vchan Error
by Daniel Wang 10 Jul '18

10 Jul '18

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

2 1

reading thread registers
by Michael Neises 10 Jul '18

10 Jul '18

Hello, I know there exists a function seL4_TCB_ReadRegisters, which can read the registers of a certain thread, given a/the capability to the thread. Ultimately, I'm interested in reading memory at runtime to determine whether the data I expect is present. So I'm wondering, is there in seL4 an init process, whose registers contain all the working memory of the system? And furthermore, how can I access a capability to a given thread in order to pass it into the ReadRegisters function mentioned above? Cheers, Michael

2 1

Memory Region overlap error
by Jeremy Fields 09 Jul '18

09 Jul '18

Hello- I'm trying to boot Genode/seL4 on hardware. I've tried a few different combinations of versions, and GRUB configurations, without success. I keep getting the same error despite these different combinations There was a thread that touched on this, but I couldn't find any resolution http://sel4.systems/pipermail/devel/2017-December/001776.html @##################################### Bender: Hello World. framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type framebuffer at [b8000+b8fa0) 80x25@16 warning - unknown framebuffer type Boot config: parsing cmdline 'sel4 disable_iommu' Boot config: console_port = 0x3f8 ▒Boot config: debug_port = 0x3f8 Boot config: disable_iommu = true module #0: start=0xf8f0000 end=0xffff228 size=0x70f228 name='image.elf' Physical Memory Region from 0 size 9ac00 type 1 Physical Memory Region from 9ac00 size 5400 type 2 Physical Memory Region from e0000 size 20000 type 2 Physical Memory Region from 100000 size 18dbb000 type 1 Adding physical memory region 0x100000-0x18ebb000 Physical Memory Region from 18ebb000 size 12d000 type 4 Physical Memory Region from 18fe8000 size 1000 type 1 Adding physical memory region 0x18fe8000-0x18fe9000 Physical Memory Region from 18fe9000 size 17000 type 4 Physical Memory Region from 19000000 size 4ffd000 type 1 Adding physical memory region 0x19000000-0x1dffd000 Physical Memory Region from 1dffd000 size 3000 type 3 Physical Memory Region from 1e000000 size 8e784000 type 1 Adding physical memory region 0x1e000000-0x1f800000 Physical Memory Region from ac784000 size 94000 type 2 Physical Memory Region from ac818000 size fe8000 type 1 Physical Memory Region from b0000000 size 4000000 type 2 Physical Memory Region from fed20000 size 20000 type 2 Physical Memory Region from fed50000 size 40000 type 2 Physical Memory Region from ffa00000 size 40000 type 2 Physical Memory Region from 1000000000 size 350000000 type 1 Physical memory region not addressable Adding physical memory region 0x0-0x1f800000 seL4 failed assertion '!p_region_overlaps(reg)' at /home/critical/Downloads/genode-18.05/contrib/sel4-c59276cc6e3aa138a1e56af8c8a56ce64cf327b8/src/kernel/sel4/src/ arch/x86/kernel/boot.c:123 in function add_allocated_p_region halting... Kernel entry via Interrupt, irq 0 @##################################### Any thoughts? Anything I can try? Any information I can provide to help diagnose? -- Sincerely, Jeremy ______________________________ Software Engineer Critical Technologies Inc.

3 3

We're hiring OS engineers
by Gernot.Heiser＠data61.csiro.au 06 Jul '18

06 Jul '18

Would you like to work on seL4 inside the TS team? Here’s your chance: https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-System-Engineer/488529400/ https://jobs.csiro.au/job/Sydney%2C-NSW-Operating-Systems-Senior-Engineer/4… Gernot

1 0

Re: [seL4] IOMUX on iMX6 conflict with libethdrivers
by Kofidoku.Atuah＠data61.csiro.au 06 Jul '18

06 Jul '18

Hey Fabrizio?, I'm sorry we took so long to get back to you: The underlying problem here is that we haven't yet finished defining and implementing a driver framework for our userspace code, so in order to satisfy dependencies, we began stuffing them into the io_ops struct. So since lots of devices depend on an initialized mux driver, what you see here is the result of that, unfortunately -- the good news is that we're currently defining a driver framework internally (https://docs.sel4.systems/seL4DriverAPI/ChildEnumeration.html is one of the draft pages of documentation -- but none of this is finalized) over the course of this year. What I'd recommend is that you use the helper function, mux_sys_valid() in mux.h (https://github.com/seL4/util_libs/blob/master/libplatsupport/arch_include/a…) inside of the ethernet driver, and map the whole 16K range inside of the IO-Ops initializer -- essentially what's going on there is that there's a dependency on the mux driver that's satisfied by the IO-Ops object. Thanks very much for your patience,? and this sort of thing should be cleaned up soon. Yours truly, -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO

2 3

Re: [seL4] seL4 CNode and capability question
by 송대영 05 Jul '18

05 Jul '18

*I have a question about capability. 1. I know that CNode can consist of hierarchy of CNodes like 1-level, 2-level, 3-level.Can I create new CNode object like them? 2. If I can create hierarchy of CNode, I want to create hierarchy of CNode in order to retype new object to new CNode object.I tried it like below source code but it doesn't work with message "Untyped Retype: Invalid destination address".Would you give some advices?--------------------- source code // ** create CNode & mapping seL4_CPtr new_CNode_cap = info->empty.start + 5; error = untyped_retype_root(untyped, seL4_CapTableObject, seL4_SlotBits, cspace_cap, new_CNode_cap); ZF_LOGF_IFERR(error, "Failed to retype our chosen untyped into an CNode object.\n"); printf("================== seL4_DebugCapIdentify ======================\n"); printf("seL4_DebugCapIdentify seL4_CPtr CNode_cap : %u \n", seL4_DebugCapIdentify(new_CNode_cap)); // ** create new Endpoint object and mapping to new CNode seL4_CPtr new_CNode_cap_Endpoint; new_CNode_cap_Endpoint = info->empty.start + 6; error = seL4_Untyped_Retype(untyped /* untyped cap */, seL4_EndpointObject /* type */, seL4_SlotBits /* size */, new_CNode_cap /* root cnode cap */, new_CNode_cap_Endpoint /* destination cspace */, 32 /* depth */, new_CNode_cap_Endpoint /* offset */, 1 /* num objects */); if(error == 0) printf("error : %d \n", error);3. Can I check CNode level? It means like CNode level number.*

1 0

IPC
by tj5527 04 Jul '18

04 Jul '18

Searching on the sel4 repository, I find there is a manual talking about IPC (https://github.com/seL4/seL4/blob/9dba8e67ccb54e207bbec22e25f21c65e5c6a45f/…) In addition to this material, where - particularly source code - would be a good start point to look into IPC design and implementation? Thanks

2 1

IOMUX on iMX6 conflict with libethdrivers
by Fabrizio Bertocci 26 Jun '18

26 Jun '18

Hi, I need your help in trying to understand what is the best way to implement a permanent fix I can push on the seL4 repository regarding the incompatibility issues between the libethdriver and MUX interface of the platsupport. This apply to the iMX6 ethernet driver. I'm not sure about other platforms. In short, the problem is that platsupport takes ownership of the entire MUX (maps the I/O) when the io_ops are initialized: Repo: seL4/seL4_libs File: libsel4platsupport/src/io.c Function: sel4platsupport_new_io_ops ... mux_sys_init(io_ops, get_mux_dependencies(), &io_ops->mux_sys); ... The above call end up calling the platform-specific mux_sys_init that maps only the first 4Kb of IO space from address 0x020e0000 (the base address of the IOMUX controller - note: the IOMUX controller uses 16Kb of address space for its registers, not 4Kb!!!): Repo: seL4/util_libs File: libplatsupport/src/plat/imx6/mux.c Function: mux_sys_init ... MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc); return imx6_mux_init_common(mux); The pointer "io_ops->mux_sys->priv" should point to the base address of the IOMUX of the SoC (in the virtual memory space of the calling process). The Ethernet driver unfortunately attempts to map the IOMUX again: Repo: seL4/util_libs File: libethdrivers/src/plat/imx6/uboot/mx6qsabrelite.c Function: setup_iomux_enet ... void *base = RESOURCE(&io_ops->io_mapper, IOMUXC); ... // Modify the IOMUX registers, then release the mapped IO: ... UNRESOURCE(&io_ops->io_mapper, IOMUXC, base); but using a larger size (the full 16Kb from the same base address of the IOMUX controller). So, the ethernet controller attempt to map the IO fails because it is already mapped, and nothing works. Right now in my project I've entirely commented out the initialization of the MUXC from the sel4platsupport_new_io_ops function. I understand that if the io_ops attempt to map the MUX (and leave it mapped) there must be a reason, unfortunately I fail to see it. The structure describing the MUXC register (struct imx6_iomuxc_regs, defined in libplatsupport/src/plat/imx6/mux.c) is private and not accessible outside that file, and the only two interface functions available (mux_feature_enable/mux_feature_disable) are not enough to be usable by the ethernet driver. The ethernet driver could also attempt to reuse the same mapped IOMUX (beside that the size of the mapped area is different and won't work anyway), but that will require using the 'priv' field of the io_ops->mux_sys (beside, even trying to map the whole 16Kb of the IOMUX and have the driver to reuse the same mapped address, for some unknown reasons it doesn't work). So, what is the right approach to fix this problem? Why the MUX subsystem maps some IO, never release it and keep it private for most of it? The IOMUX has been introduced somewhere between version 1.0 and 9.x... and it seems a half-baked job... Can we just comment it out if nobody is using it? Or if you have some ideas/suggestions on how to expand it in such a way the ethernet driver could use, please let me know. I'll be happy to implement it. Regards, Fabrizio

2 2

Problems with tk1 nonsecure
by Mike Clark 26 Jun '18

26 Jun '18

I just checked out a fresh copy of https://github.com/ SEL4PROJ/camkes-arm-vm-manifest and built an image for the TK1 using the docker build environment. I copied the resulting image to an SD card and it boots fine. If I switch to the unsecure mode, I get an error on boot. SMMU Address translation error: ID: 98 address: 0xae5be000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.204777] mmc1: ADMA error I have not made any changes, so my vm.smmu settings are all default. Any thoughts or help? Mike

3 9

Question about process and thread in tutorials
by 송대영 21 Jun '18

21 Jun '18

* I have question about process and thread in tutorials. 1. sel4 doesn't have process concept.But making new process is exist in tutorial hello-4.What is the exactly difference trhead in hello-2 and process in hello-4?2. In tutorials hello-4, where can I find access path that hello-4 process link hello-4-app?It means I think hello-4 process should designate hello-4-app's path.*

2 1