- Devel - lists.sel4.systems

by inf19109＠lehre.dhbw-stuttgart.de

Dear seL4 devs and community, I'm trying to do the seL4-tutorials on a RISC-V architecture. Now I'm stuck on the untyped tutorial. I tried to run the solution of the tutorial but I get the following error: <<seL4(CPU 0) [decodeUntypedInvocation/128 T0xffffffc17fee7200 "rootserver" @103fc]: Untyped Retype: Destination cap invalid or read-only.>> main@main.c:48 [Cond failed: error != seL4_NoError] Failed to retype seL4 root server abort()ed Debug halt syscall from user thread 0xffffffc17fee7200 "rootserver" halting... I'm calling the function as follows: seL4_Untyped_Retype(parent_untyped, seL4_UntypedObject, // type untyped_size_bits, //size seL4_CapInitThreadCNode, // root 0, // node_index 0, // node_depth child_untyped, // node_offset 1 // num_caps ); parent_untyped = info->untyped.start + i (where i is incremented until (info->untypedList[i].sizeBits >= untyped_size_bits && !info->untypedList[i].isDevice) untyped_size_bits = seL4_TCBBits+1 child_untyped = info->empty.start It seams as if the function is not allowed for RISC-V. I don't know where the problem lies and I would appreciate any help or ideas. Best regards Miriam

2 days, 20 hours

2
3
0 0

Anyone using capability transfer in an seL4 project? Looking for examples for research

by sjwebb＠student.unimelb.edu.au

Hi all, I'm working on a Masters research project looking into mapping an object-capability programming language onto seL4, in a way that includes some kind of mapping from the language object capabilities onto seL4's capabilities (or vice versa). I'm at a stage of the project now where it would be really helpful to have some 'motivating examples' for transferring caps between threads/CSpaces. So I was hoping I could reach out to other seL4 developers to see if they had built any systems that made extensive use of moving capabilities around. Ideally, in an ocap language, these examples would be much easier to program than they currently would be in C... The simplest example I can think of is a memory allocation server, but that wouldn't necessarily involve handing caps on beyond the one (requesting) process, which is the kind of thing I think more interesting examples would comprise of. Cheers, Stewart Webb [Masters Research student at University of Melbourne]

4 days, 7 hours

2
1
0 0

Reminder seL4 developer hangout

by Birgit Brecknell

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Tue, May 17, 10pm (UTC), Topics: (open) * Sydney: Wed, May 18, 8am * Central Europe: Wed, May 18, 12 midnight * US Pacific Time: Tue, May 17, 3pm 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

4 days, 19 hours

1
0
0 0

VPPI IRQ 27 dropped on vcpu 3

by Han JingLong 韩景龙

Dear seL4 devs and community, I had made VMM work well on my platform(armv8, six A55 cpus, RAM is 8G) based on vm_multi with Linux Guest OS(vm0.num_vcpus = 4;) and Android Guest OS(vm1.num_vcpus = 6;). But I meet an error(vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3) when I enable SMP support with -DNUM_NODES=6. Actually, VPPI IRQ 27 dropped on some vcpu number is not fixed, maybe 1 or 2 or 3. Once this error appears, it will brush the screen crazily, the recurrence rate is about 10%. 1.Some logs are added for debugging this issue: --- a/seL4_projects_libs/libsel4vmmplatsupport/src/arch/arm/psci.c +++ b/seL4_projects_libs/libsel4vmmplatsupport/src/arch/arm/psci.c @@ -53,18 +53,24 @@ int handle_psci(vm_vcpu_t *vcpu, seL4_Word fn_number, bool convention) uintptr_t target_cpu = smc_get_arg(&regs, 1); uintptr_t entry_point_address = smc_get_arg(&regs, 2); uintptr_t context_id = smc_get_arg(&regs, 3); + printf("[hjl] handle_psci target_cpu:%d\n", target_cpu); vm_vcpu_t *target_vcpu = vm_vcpu_for_target_cpu(vcpu->vm, target_cpu); if (target_vcpu == NULL) { target_vcpu = vm_find_free_unassigned_vcpu(vcpu->vm); if (target_vcpu && start_new_vcpu(target_vcpu, entry_point_address, context_id, target_cpu) == 0) { + printf("[hjl] handle_psci vm:%p vcpu_id:%d on success\n", vcpu->vm, target_vcpu->vcpu_id); smc_set_return_value(&regs, PSCI_SUCCESS); } else { + printf("[hjl] handle_psci vm:%p vcpu_id:%d on failure\n", vcpu->vm, target_vcpu->vcpu_id); smc_set_return_value(&regs, PSCI_INTERNAL_FAILURE); } } else { if (is_vcpu_online(target_vcpu)) { + printf("[hjl] handle_psci vm:%p target_cpu is online\n", vcpu->vm); smc_set_return_value(&regs, PSCI_ALREADY_ON); } else { + printf("[hjl] handle_psci vm:%p target_cpu is not online\n", vcpu->vm); smc_set_return_value(&regs, PSCI_INTERNAL_FAILURE); } } --- a/seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c +++ b/seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c @@ -570,6 +570,9 @@ static int vgic_dist_enable_irq(struct vgic_dist_device *d, vm_vcpu_t *vcpu, int vgic = vgic_device_get_vgic(d); DDIST("enabling irq %d\n", irq); set_enable(gic_dist, irq, true, vcpu->vcpu_id); + if (irq == 27) { + printf("[hjl] enabling irq:%d on vcpu:%d\n", irq, vcpu->vcpu_id); + } virq_data = virq_find_irq_data(vgic, vcpu, irq); if (virq_data) { /* STATE b) */ @@ -619,6 +622,7 @@ static int vgic_dist_set_pending_irq(struct vgic_dist_device *d, vm_vcpu_t *vcpu return err; } else { + printf("[hjl] virq_data:%p, gic_dist->enable:%d, is_enabled:%d\n", virq_data, gic_dist->enable, is_enabled(gic_dist, irq, vcpu->vcpu_id)); /* No further action */ DDIST("IRQ not enabled (%d) on vcpu %d\n", irq, vcpu->vcpu_id); return -1; } 2.The detailed log is as follows: [hjl] enabling irq 27, vcpu->vcpu_id:0 [hjl] handle_psci target_cpu:256 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:1 on success [hjl] enabling irq 27, vcpu->vcpu_id:1 [hjl] handle_psci target_cpu:512 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:2 on success [hjl] enabling irq 27, vcpu->vcpu_id:2 [hjl] handle_psci target_cpu:768 [hjl] handle_psci vm:0x1584bbb0 vcpu_id:3 on success [hjl] enabling irq 27, vcpu->vcpu_id:3 [hjl] enabling irq 27, vcpu->vcpu_id:0 [hjl] handle_psci target_cpu:256 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:1 on success [hjl] enabling irq 27, vcpu->vcpu_id:1 [hjl] handle_psci target_cpu:512 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:2 on success [hjl] enabling irq 27, vcpu->vcpu_id:2 [hjl] handle_psci target_cpu:768 [hjl] handle_psci vm:0x1584fbb0 vcpu_id:3 on success [hjl] enabling irq 27, vcpu->vcpu_id:3 [hjl] IRQ not enabled (27) on vcpu 3 virq_data:0x15794ad0, gic_dist->enable:1, is_enabled:0 vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3 [hjl] IRQ not enabled (27) on vcpu 3 virq_data:0x15794ad0, gic_dist->enable:1, is_enabled:0 vm_vppi_event_handler@vm.c:97 VPPI IRQ 27 dropped on vcpu 3 ...... 3.Present situation: At present, I tracked and found that secondary cpus has been on by Host, but Guest OS's secondary_start_kernel function seem like not excuted. Does anyone know what caused it? 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 week, 2 days

1
0
0 0

camkes q's

by Sam Leffler

1. I need multiple VSpace "holes" to map page frames. This is the equivalent of what capdl_loader_app sets up in init_copy_frame. To do this I setup named static arrays and unmap the frame caps in camkes.c:post_main. This works but using a per-component attribute to enable this was awkward so I ended up adding a "copyregion" primitive to camkes. Is there a way to do this without adding to the camkes' syntax? It would also be nice not to allocate page frames only to release them at start but I didn't see a way to do this in capdl; is it possible (e.g. an easy way to leave an empty slot in the pt/pd)? 2. I pass capabilities with ipc msgs using camkes' rpc-connector templates. This requires multiple small changes that I want to enable only when being used (e.g. parameters to seL4_MessageInfo_new). My current plan is to add an optional keyword to a connection defn to enable support; e.g. connection seL4RPCCall foo(xfer_caps, from a, to b); Does this make sense or is there a better way? I rejected creating new connector templates that enable xfer_caps because I see this as a concept that applies to any ipc-based connector.

1 week, 3 days

2
2
0 0

Information for Smmuv3 support of Sel4

by Tao Heng 陶恒-SW

Hi, list We are trying to porting Sel4 Vmm project on our platform.But we found there was no information about smmuv3 support of Sel4. Do you have some related development work for supporting this? Or can you give us some advice for supporting Smmuv3 on Sel4? 邮件免责申明 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 weeks

1
0
0 0

One week left to propose a talk at the seL4 summit 2022!

by June Andronick (seL4 Foundation)

A reminder that you have until Monday 9th of May 2022 to propose a talk for the seL4 Summit 2022 :) http://sel4.systems/news/2022 <http://sel4.systems/news/2022> http://sel4.systems/Foundation/Summit/ <http://sel4.systems/Foundation/Summit/> http://sel4.systems/Foundation/Summit/cfp <http://sel4.systems/Foundation/Summit/cfp>

2 weeks

1
1
0 0

Reminder seL4 developer hangout

by Birgit Brecknell

Hi all A friendly reminder that the seL4 developer hangout is on again this week: Wed, May 4, 7am (UTC), Topics: (open) * Sydney: Wed, May 4, 5pm * Central Europe: Wed, May 4, 9am * US Pacific Time: Wed, May 4, 12 midnight 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

2 weeks, 4 days

1
0
0 0

Getting Badge Value of a badged EP capability

by Sid Agrawal

Hi seL4-devs and users, I have a question about implementing server and client using badged endpoints. Below I have laid out the scenario, the issue, and some questions. *Scenario* I have a userspace server that implements the functionality for an object(say type obj_T1). The server hands out badged-endpoints to clients to interact with this object. The badge is the virtual address of the object's struct in the server’s virtual address space. A client can interact with the object by sending messages on this badged endpoint. The client never learns the badge value. The kernel extracts the badged value when the server receives a message on this endpoint. By using the badge value, the server knows which object the client is trying to manipulate. The same PD, which implements the 1st server, also implements another server(in a separate thread, but same address space) for another object type (say type obj_T2). The server follows the same paradigm of handing out badged endpoints and using the badges values to keep track of the object. *Issue* I have a scenario where the client wants to invoke the functionality of obj_T1. This functionality needs access to obj_T2 as well. The client has badged EP caps to both objects. The client can invoke the badged EP handed out by server-1 for obj_T1 and give the badged EP of obj_T2 as an extraCap in the IPC message(or vice versa). Since the server has no way to look up the badge of the second cap, it cannot look up the underlying object for obj_T2. So my questions are: 1. Is there a way for a PD to look up the badge value of badged EP? I think the answer is no, but I thought I would still ask. 2. Is my idea of using the badge to keep track of the underlying object on the right track? Is there a better way of going about doing it? 3. As a potential solution, I can extend my server to add a new function, say GETID, which returns the badge value of a given object(i.e., EP). Since I know that the server always badges the EP with the virtual address of the struct, it is a trivial call to implement. But I somehow feel like this is not a neat idea, not quite sure why. Thanks for the help, everyone! Sid CS Graduate Student @ UBC sid-agrawal.ca

2 weeks, 5 days

3
5
0 0

The seL4 Summit 2022 will be in Munich, Germany, on 10-12 Oct 2022

by June Andronick (seL4 Foundation)

It is our pleasure to confirm that the seL4 Summit 2022 will be in: Munich, Germany in the week of Oct 10th, 2022 It will be hosted by seL4 Foundation member Hensoldt Cyber. It will be a hybrid in-person/online event (if you'd like to propose a talk to be delivered remotely, please notify it in the submission). Remember that you have until Monday 9th of May 2022 to propose a talk. https://sel4.systems/news/2022 https://sel4.systems/Foundation/Summit/ https://sel4.systems/Foundation/Summit/cfp

3 weeks

1
0
0 0

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel