Devel March 2022

devel@sel4.systems

22 participants
22 discussions

Overlapping pointer returned by memalign
by WILLIAMS Stephen 31 Mar '22

31 Mar '22

Hi, I’m currently working on a project porting drivers from U-Boot to seL4 and have run into an unexpected problem seemingly triggered by use of the memalign within the U-Boot drivers. What I am seeing is that calls to memalign from within my CAmkES component can return pointers to regions which overlap with those previously returned by malloc. Obviously this leads to the two allocated regions trampling over each other and resulting corruption of data. I’m at a complete loss to explain this behaviour and would be very grateful to receive any suggestions or pointers. Thanks for your help, Stephen This message contains information that may be privileged or confidential and is the property of the Capgemini Group. It is intended only for the person to whom it is addressed. If you are not the intended recipient, you are not authorized to read, print, retain, copy, disseminate, distribute, or use this message or any part thereof. If you receive this message in error, please notify the sender immediately and delete all copies of this message.

3 9

Re: How to switch virtual machines linux in vm_multi from camkes-vm-example?
by Peter Chubb 31 Mar '22

31 Mar '22

>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: yjy> `screen /dev/ttyUSB0 115200`. I have a shell terminal that can yjy> see the output from VM0. I input @1 to shell, which is useless. It only works at the start of a line. Peter C yjy> At 2022-03-31 14:12:16, peter(a)chubb.wattle.id.au wrote: >>>>>>> "yjy" == yjy <yjy7894(a)126.com> writes: >> yjy> Hi, I have already run the camkes-vm-example vm_multi on my yjy> board, but i don't know how to switch linux vm shell from another yjy> linux vm, Can anyone help me solve this? >> >> If you're talking about controlling the serial console to talk to >> different VMs, the instructions are >> https://github.com/seL4/camkes-vm in the README.md under 'Serial' >> >> >> In brief, output from different VMs is colour coded. Switch >> between them for input with @0, @1, @2 etc. >> >> Peter C _______________________________________________ Devel >> mailing list -- devel(a)sel4.systems To unsubscribe send an email to >> devel-leave(a)sel4.systems yjy> [2 <text/html; GBK (base64)>] -- Dr Peter Chubb https://trustworthy.systems/ Trustworthy Systems Group CSE, UNSW Core hours: Mon 8am-3pm; Wed: 8am-5pm; Fri 8am-12pm.

1 0

How to switch virtual machines linux in vm_multi from camkes-vm-example?
by yjy 31 Mar '22

31 Mar '22

Hi, I have already run the camkes-vm-example vm_multi on my board, but i don't know how to switch linux vm shell from another linux vm, Can anyone help me solve this? Best, Comet

2 1

Question for student research
by Seth Nielson 30 Mar '22

30 Mar '22

Hi. I am mentoring a student group trying to do some work on SEL4. We are trying to setup basic TCP/IP networking and are really struggling to find documentation or up-to-date guides. We found a project that has networking (it even has some filesystem and a small webserver as part of the project). We thought we just about had the networking component working for QEMU but there seems to be issues with QEMU and networking, at least the way we did it. Does anyone have any how-to guides for getting basic networking up and running? If QEMU is not great for networking, please suggest a development board. Thanks much.

2 2

Information for Additional Virtio Driver Support of Sel4
by Tao Heng 陶恒-SW 28 Mar '22

28 Mar '22

Hi list， Is there any specific plan or some related development for supporting the Additional Virtio Driver (* e.g Virtio Blk, Virtio RNG, Virtio Balloon), as you mentioned in READ.md of libsel4vmmplatsupport, especially for the Virtio Blk? 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

2 2

propagating initial thread's capabilities
by Sam Leffler 28 Mar '22

28 Mar '22

The rootserver gets various caps setup for it by the kernel (see Table 9.1 in the manual). This includes the gobal ASID, IRQ, Domain, and Sched controllers. I need these caps in a process created by the rootserver. This is within a CAmkES environment. So far I've created CAmkES component attributes that signal the rootserver should hand-off a cap by moving the rootserver's cap to the designated CNode just before it terminates. This involves modifications to CAmkES, capDL, and the rootserver. Is there a better way? Is there an existing example of doing this? Are any of these global objects accessible some other way than hand-off from the rootserver? -Sam

2 4

Questions about Kscurdomain variable.
by 603644559＠qq.com 25 Mar '22

25 Mar '22

In the case of multiple cores, is the scheduling of each core judged according to the kscurdomain, that is, the scheduling table of the domain is maintained by an operating system, rather than an independent kscurdomain in a core and a scheduling table of the domain in each core?

1 0

Hi,
by ezabujpz＠uuf.me 23 Mar '22

23 Mar '22

Hi, https://www.assortlist.com I would like to use network (TCP) on seL4, I know that I should probably be using lwip, however I have no idea how to properly initialize it (this is the first time I'm working in such a hardware close environment), so I need some help or some kind of example, but I don't know where to look. I'm working on ia32.

1 0

Reminder seL4 developer hangout
by Birgit Brecknell 22 Mar '22

22 Mar '22

Hi all A friendly reminder that the seL4 developer hangout is on this week: Tue, Mar 22, 9pm (UTC), Topics: (open) * Sydney: Wed, Mar 23, 8am * Central Europe: Tue, Mar 22, 10pm * US Pacific Time: Tue, Mar 22, 2pm (There are too many time zones in the world to cite them all :-)) Zoom link: https://unsw.zoom.us/j/82640784431 Cheers, Birg --- Dr. Birgit Brecknell Project Officer Trustworthy Systems, UNSW, birgit.brecknell(a)unsw.edu.au<mailto:birgit.brecknell@unsw.edu.au> seL4 Foundation, birgit(a)sel4.systems<mailto:birgit@sel4.systems> 0433 880 571 Mon 9am-5pm Wed 9am-12pm Fri 9am-5pm

3 2

Report "Failed to touch ram region" error using virtio_console when assigned for Arm-VM more than 3G memory
by Han JingLong 韩景龙 21 Mar '22

21 Mar '22

Hi I had make virtio_console work well on my environment(armv8, RAM is 8G) based on vm_multi with Linux Guest OS(512M) and Android Guest OS(<= 3G) But I meet an error(vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region) when assign for a VM(Android Guest OS) more than 3G memory. 1. Some logs are added for debugging this issue： +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c @@ -86,6 +86,7 @@ static int emul_io_out(virtio_emul_t *emul, unsigned int offset, unsigned int si assert(size == 4); int queue = emul->virtq.queue; emul->virtq.queue_pfn[queue] = value; + printf("[hjl] queue_size:%d desc:%p\n", emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12)); vring_init(&emul->virtq.vring[queue], emul->virtq.queue_size[queue], (void *)(uintptr_t)(value << 12), VIRTIO_PCI_VRING_ALIGN); break; +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul_helpers.c @@ -25,10 +25,43 @@ static int write_guest_mem(vm_t *vm, uintptr_t phys, void *vaddr, size_t size, s int vm_guest_write_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] write mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] write mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } + return vm_ram_touch(vm, address, size, write_guest_mem, data); } int vm_guest_read_mem(vm_t *vm, void *data, uintptr_t address, size_t size) { + bool is_inram = false; + vm_mem_t *guest_memory = &vm->mem; + for (int i = 0; i < guest_memory->num_ram_regions; i++) { + if (guest_memory->ram_regions[i].start <= address && + guest_memory->ram_regions[i].start + guest_memory->ram_regions[i].size >= address + size) { + /* We are within a ram region*/ + is_inram = true; + } + } + + if (!is_inram) { + printf("[hjl] read mem addr:%p size:0x%lx\n", address, size); + for (int index = 0; index < guest_memory->num_ram_regions; index++) { + printf("[hjl] read mem ram_regions start:%p size:0x%lx\n", guest_memory->ram_regions[index].start, guest_memory->ram_regions[index].size); + } + } return vm_ram_touch(vm, address, size, read_guest_mem, data); } 2. The detailed log is as follows: [hjl] queue_size:128 desc:0x8eb6000 [hjl] queue_size:128 desc:0x8eb8000 [hjl] read mem addr:0x8eb8802 size:0x2 [hjl] read mem ram_regions start:0x80000000 size:0x80000 [hjl] read mem ram_regions start:0x80080000 size:0x17cda00 [hjl] read mem ram_regions start:0x8184da00 size:0xa5b2600 [hjl] read mem ram_regions start:0x8be00000 size:0x83ae98 [hjl] read mem ram_regions start:0x8c63ae98 size:0x29c5168 [hjl] read mem ram_regions start:0x8f000000 size:0x26d35 [hjl] read mem ram_regions start:0x8f026d35 size:0xc0fd92cb vm_ram_touch@guest_ram.c:157 Failed to touch ram region: Not registered RAM region 3. devices.camkes configuration reference is as follows: #define VM1_RAM_BASE 0x80000000 #define VM1_RAM_SIZE 0xD0000000 #define VM1_DTB_ADDR 0x8F000000 //VM1_RAM_BASE + 0xF000000 #define VM1_INITRD_ADDR 0x8BE00000 //VM1_DTB_ADDR - VM1_INITRD_MAX_SIZE vm1.untyped_mmios = [ "0x80000000:28", // RAM "0x90000000:28", // RAM "0xa0000000:28", // RAM "0xb0000000:28", // RAM "0xc0000000:28", // RAM "0xd0000000:28", // RAM "0xe0000000:28", // RAM "0xf0000000:28", // RAM "0x100000000:28", // RAM "0x110000000:28", // RAM "0x120000000:28", // RAM "0x130000000:28", // RAM "0x140000000:28", // RAM /* "0x150000000:28", // RAM "0x160000000:28", // RAM "0x170000000:28", // RAM "0x180000000:28", // RAM "0x190000000:28", // RAM "0x1a0000000:28", // RAM "0x1b0000000:28", // RAM */ ]; 4. Present situation: At present, I tracked and found that When the Guest OS's virtio_console driver do the probe, it created the vring and iowrite to notify VMM of the virtqueue desc 's physical address in setup_vq() /* create the vring */ static void *vring_alloc_queue(struct virtio_device *vdev, size_t size, dma_addr_t *dma_handle, gfp_t flag) { ...... void *queue = alloc_pages_exact(PAGE_ALIGN(size), flag); if (queue) { phys_addr_t phys_addr = virt_to_phys(queue); *dma_handle = (dma_addr_t)phys_addr; /* activate the queue */ iowrite32(virtqueue_get_desc_addr(vq) >> VIRTIO_PCI_QUEUE_ADDR_SHIFT, vp_dev->ioaddr + VIRTIO_PCI_QUEUE_PFN); I'm very confused why is the physical memory allocated for virtqueue desc not within the effective memory range of VM when assign the memory to it exceeds 3G? BR. Allen 邮件免责申明 Email Disclaimer 本邮件仅供本邮件指定收件人使用，其所载内容可能因含有保密信息或其它原因而不得披露。除本公司及本邮件指定收件人外，任何人不得公开、传播、分发、复制、印刷或使用本邮件之任何部分或其所载之任何内容。如您误收到本邮件，请立即通知本公司，并将原始邮件、附件及其所有复本从系统中删除，切勿使用。 This email is for the use of the designated receivers only，and the content is not allowed to be disclosed due to the confidential information or other reasons. Except for the Company and the designated receivers of this email, no one shall disclose, disseminate, distribute, copy, print or use any part of this email or any content contained therein. If you receive this email by mistake, please notify the Company immediately, and delete the original email, attachments and all copies from the system. Do not use it. 网络通信可能含有计算机病毒或其它缺陷，可能无法准确和/或及时送达其它系统，亦可能受阻而不为本公司或本邮件指定收件人所知。本公司对此类错误或遗漏以及任何因使用本邮件而引致之任何损失概不承担责任。 Network communication may contain computer viruses or other defects, which may not be delivered to other systems accurately and / or in time, or may be blocked by the Company or the designated receivers of this email. The Company shall not be liable for such errors or omissions and for any loss arising from this email. 本邮件所载任何内容仅作为业务层面交流与参考，除非明确说明，本公司不对邮件所载内容之准确性、完整性或公平性等承担任何法律责任。 Any contents contained in this email are only for the purpose of business communication and reference only. Unless explicitly stated otherwise, the Company shall not assume any legal responsibility for the accuracy, completeness or fairness of the content contained in the email. 本邮件指定收件人应特别注意：本邮件所载任何内容不构成本公司对本邮件指定收件人和/或其所属商业实体的任何要约、要约邀请或承诺，任何权利义务皆以双方签字盖章的书面文件为准。除经本公司以签字盖章的书面文件确认外，收件人和/或其所属商业实体不得以本邮件所载任何内容作为其向本公司主张任何权利或利益的正式依据。 The designated receivers should pay special attention to the fact that nothing contained in this email shall constitute an offer, invitation or acceptance by the Company to the designated receivers of this email and/or its affiliated business entities, and any rights and obligations are subject to the written documents signed and sealed by both parties. Except from the written document signed ,sealed and confirmed by the Company, the receivers and / or its affiliated business entity shall not rely on anything contained in this email as the formal basis for claiming any rights or interests to the Company.

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel March 2022