So Sam and I are at the point now where we're attempting to get our
untrusted user threads running in a different scheduling domain, and it's
not exactly clear how this is supposed to work in terms of enabling more
than one domain in the kernel.
So far, I've set KernelNumDomains to 2 in the easy-settings.cmake for our
project, but unless I provide a separate implementation of
kernel/config/default_domain.c by overriding KernelDomainSchedule, the
resulting kernel will only think it has one domain and only ever schedule
domain 0 for execution.
Are we expected to override the default_domain.c file with our own in the
project, like sel4test seems to do?
This is only of interest for those physically in Sydney.
We have seL4 Day coming up (29 July, the 13th anniversary of completion of the seL4 verification and 8th anniversary of its open-sourcing). It would be great to use the occasion to get together.
The continuing abnormal (i.e. very wet) weather in Sydney makes planning such an event difficult (and I’ll be on leave and out of town until the evening of the 28th), so things may have to happen on short notice. But weather permitting, a BYO BBQ in Maroubra would be great, and I would really love to catch up with the rest of the Sydney-based seL4 community. So I suggest people interested save the date (and let us know if you’re interested).
Jumping off from the recent thread, I was curious if anyone had any
thoughts about how to optimally design API's for seL4.
I noticed we had a bit of info about what not to do (don't do long IPC,
don't implement Posix, don't use messaging as synchronization, etc.)
Are there any shining examples of what _to_ do with an API?
I have been trying to make some understandings of smmuv2.0 features provided by sel4. According to the vmm project for the tx2 platform, such as the vm_minimal apps, after all the compiling, there will be two caps,vm0_sid and vm0_cb,which is supposed to be used for stage2 address translation. My questions are as followed:
1. Which smmu device was the sid cap assigned to ?
2. How were these two caps created in the cdl file? There seems no special configuration for Cmakes that is related to the caps.
3. According to the tx2.dts, there are many sid numbers assigned to the smmu device. Why was there just one sid cap created by sel4?
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.
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.
[Masters Research student at University of Melbourne]
I'm having similar issues getting seL4test to work on riscv32/64 on QEMU 6.0.0 and 7.0.0. I tried debugging with a connected gdb, but I'm new at this and setting breakpoints in user mode seems to fail, so I'm not sure what happens once the root task starts, other than it eventually runs an infinite loop (0: j 0b, specifically).
Any ideas? Thanks.