Hello everyone, There is a new release of Microkit, version 2.0.0. This release contains various bug fixes, quality-of-life changes, features, and new board support. This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1. You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0 Ivan
Hi Ivan, where I can find info about: "Add support for ARM platforms to use SMC forwarding. Note that this requires a kernel option to be set that right now is not set by default on any ARM platforms in Microkit." I want to enable SMC forwarding. Best, On Thursday, March 6, 2025, Ivan Velickovic via Devel <devel@sel4.systems> wrote:
Hello everyone,
There is a new release of Microkit, version 2.0.0.
This release contains various bug fixes, quality-of-life changes, features, and new board support.
This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1.
You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0
Ivan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hugo, This is how I did it: Here is an example of enabling SMC forwarding for the zcu102 development board: https://github.com/seL4/microkit/commit/b6a1386cdd2488b416dbc280ebcea87e4490... You will then need to follow the Microkit readme to build your own Microkit with that change. Then you need to set `smc="true"` in any PDs where you want to enable SMC forwarding. Here is an example for a vmm: https://github.com/dornerworks/inspecta-open-platform/blob/main/open-platfor... The kernel implementation allows for fine-grained control over specifically which SMC calls are allowed by a PD, however, I don't think Microkit has implemented that granularity yet. That means you can either forward all SMC calls or none of them. Thanks, Robbie -----Original Message----- From: Hugo V.C. via Devel <devel@sel4.systems> Sent: Thursday, March 6, 2025 4:37 AM To: Ivan Velickovic <i.velickovic@unsw.edu.au> Cc: devel <devel@sel4.systems> Subject: [seL4] Re: Release 2.0.0 of Microkit CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you recognize the sender and know the content is safe. Hi Ivan, where I can find info about: "Add support for ARM platforms to use SMC forwarding. Note that this requires a kernel option to be set that right now is not set by default on any ARM platforms in Microkit." I want to enable SMC forwarding. Best, On Thursday, March 6, 2025, Ivan Velickovic via Devel <devel@sel4.systems> wrote:
Hello everyone,
There is a new release of Microkit, version 2.0.0.
This release contains various bug fixes, quality-of-life changes, features, and new board support.
This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1.
You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0
Ivan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hugo,
This is how I did it:
Here is an example of enabling SMC forwarding for the zcu102 development board: https://github.com/seL4/microkit/commit/b6a1386cdd2488b416dbc280ebcea87e4490...
You will then need to follow the Microkit readme to build your own Microkit with that change.
Then you need to set `smc="true"` in any PDs where you want to enable SMC forwarding. Here is an example for a vmm: https://github.com/dornerworks/inspecta-open-platform/blob/main/open-platfor...
The kernel implementation allows for fine-grained control over specifically which SMC calls are allowed by a PD, however, I don't think Microkit has implemented that granularity yet. That means you can either forward all SMC calls or none of them.
Thanks, Robbie
-----Original Message----- From: Hugo V.C. via Devel <devel@sel4.systems> Sent: Thursday, March 6, 2025 4:37 AM To: Ivan Velickovic <i.velickovic@unsw.edu.au> Cc: devel <devel@sel4.systems> Subject: [seL4] Re: Release 2.0.0 of Microkit
CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you recognize the sender and know
Thank you Robert! I'll give it a try. On Thursday, March 6, 2025, Robert VanVossen < Robert.VanVossen@dornerworks.com> wrote: the content is safe.
Hi Ivan,
where I can find info about:
"Add support for ARM platforms to use SMC forwarding.
Note that this requires a kernel option to be set that right now is
not set by default on any ARM platforms in Microkit."
I want to enable SMC forwarding.
Best,
On Thursday, March 6, 2025, Ivan Velickovic via Devel <devel@sel4.systems> wrote:
Hello everyone,
There is a new release of Microkit, version 2.0.0.
This release contains various bug fixes, quality-of-life changes, features, and new board support.
This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1.
You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0
Ivan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to
devel-leave@sel4.systems
On 7 Mar 2025, at 00:06, Robert VanVossen <Robert.VanVossen@dornerworks.com> wrote: The kernel implementation allows for fine-grained control over specifically which SMC calls are allowed by a PD, however, I don't think Microkit has implemented that granularity yet. That means you can either forward all SMC calls or none of them. Can you expand on this? I do not see anything in the seL4 manual or the implementation that suggests any granularity with SMC forwarding. Ivan
If you badge the SMC cap, the kernel will only allow smc calls with x0 matching the badge value. In the smc calling convention this is the function ID. On Fri, 7 Mar 2025 at 12:19 pm, Ivan Velickovic via Devel <devel@sel4.systems> wrote:
On 7 Mar 2025, at 00:06, Robert VanVossen < Robert.VanVossen@dornerworks.com> wrote:
The kernel implementation allows for fine-grained control over specifically which SMC calls are allowed by a PD, however, I don't think Microkit has implemented that granularity yet. That means you can either forward all SMC calls or none of them.
Can you expand on this? I do not see anything in the seL4 manual or the implementation that suggests any granularity with SMC forwarding.
Ivan _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Ah okay. It’s not in the manual which is why I missed it. Thanks. Should be fairly easy to add to Microkit. Ivan On 7 Mar 2025, at 13:31, Kent Mcleod <kent.mcleod72@gmail.com> wrote: If you badge the SMC cap, the kernel will only allow smc calls with x0 matching the badge value. In the smc calling convention this is the function ID. On Fri, 7 Mar 2025 at 12:19 pm, Ivan Velickovic via Devel <devel@sel4.systems> wrote: On 7 Mar 2025, at 00:06, Robert VanVossen <Robert.VanVossen@dornerworks.com<mailto:Robert.VanVossen@dornerworks.com>> wrote: The kernel implementation allows for fine-grained control over specifically which SMC calls are allowed by a PD, however, I don't think Microkit has implemented that granularity yet. That means you can either forward all SMC calls or none of them. Can you expand on this? I do not see anything in the seL4 manual or the implementation that suggests any granularity with SMC forwarding. Ivan _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Ivan, Congratulations! I am wondering if we use microkit on a QEMU riscv64 virt board with smaller memory size (like 128MB)? Are there any notes about how to achieve this? Regards, yf On Thu, 2025-03-06 at 06:43 +0000, Ivan Velickovic via Devel wrote:
Hello everyone,
There is a new release of Microkit, version 2.0.0.
This release contains various bug fixes, quality-of-life changes, features, and new board support.
This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1.
You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0
Ivan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hi Yanfeng Right now attributes like main memory are determined at compile time so if you want to change how much QEMU has you’d have to modify how Microkit compiles support for it. Here’s a patch that should work: ```patch diff --git a/build_sdk.py b/build_sdk.py index 2aefff6..aafc08c 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -208,11 +208,11 @@ SUPPORTED_BOARDS = ( name="qemu_virt_riscv64", arch=KernelArch.RISCV64, gcc_cpu=None, - loader_link_address=0x90000000, + loader_link_address=0x84000000, kernel_options={ "KernelPlatform": "qemu-riscv-virt", "KernelIsMCS": True, - "QEMU_MEMORY": "2048", + "QEMU_MEMORY": "128", "KernelRiscvExtD": True, "KernelRiscvExtF": True, }, ``` Ivan
On 8 Mar 2025, at 22:22, Yanfeng Liu via Devel <devel@sel4.systems> wrote:
Ivan,
Congratulations!
I am wondering if we use microkit on a QEMU riscv64 virt board with smaller memory size (like 128MB)?
Are there any notes about how to achieve this?
Regards, yf
On Thu, 2025-03-06 at 06:43 +0000, Ivan Velickovic via Devel wrote:
Hello everyone,
There is a new release of Microkit, version 2.0.0.
This release contains various bug fixes, quality-of-life changes, features, and new board support.
This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1.
You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0
Ivan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Ivan, Thanks a lot! Regards, yf On Sat, 2025-03-08 at 11:39 +0000, Ivan Velickovic via Devel wrote:
Hi Yanfeng
Right now attributes like main memory are determined at compile time so if you want to change how much QEMU has you’d have to modify how Microkit compiles support for it.
Here’s a patch that should work: ```patch diff --git a/build_sdk.py b/build_sdk.py index 2aefff6..aafc08c 100644 --- a/build_sdk.py +++ b/build_sdk.py @@ -208,11 +208,11 @@ SUPPORTED_BOARDS = ( name="qemu_virt_riscv64", arch=KernelArch.RISCV64, gcc_cpu=None, - loader_link_address=0x90000000, + loader_link_address=0x84000000, kernel_options={ "KernelPlatform": "qemu-riscv-virt", "KernelIsMCS": True, - "QEMU_MEMORY": "2048", + "QEMU_MEMORY": "128", "KernelRiscvExtD": True, "KernelRiscvExtF": True, }, ```
Ivan
On 8 Mar 2025, at 22:22, Yanfeng Liu via Devel <devel@sel4.systems> wrote:
Ivan,
Congratulations!
I am wondering if we use microkit on a QEMU riscv64 virt board with smaller memory size (like 128MB)?
Are there any notes about how to achieve this?
Regards, yf
On Thu, 2025-03-06 at 06:43 +0000, Ivan Velickovic via Devel wrote:
Hello everyone,
There is a new release of Microkit, version 2.0.0.
This release contains various bug fixes, quality-of-life changes, features, and new board support.
This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1.
You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0
Ivan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Ivan Does microkit 2.0 support running VM on qemu_virt_riscv64 now? Regards, yf On Thu, 2025-03-06 at 06:43 +0000, Ivan Velickovic via Devel wrote:
Hello everyone,
There is a new release of Microkit, version 2.0.0.
This release contains various bug fixes, quality-of-life changes, features, and new board support.
This is a major version bump due to a breaking change. Below the release notes, there is a section on how to upgrade from Microkit 1.4.1.
You can download the pre-built SDK from GitHub: https://github.com/seL4/microkit/releases/tag/2.0.0
Ivan
_______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
The kernel does not currently support running as a hypervisor on RISC-V so there are no VMs on RISC-V in Microkit. If you look at [1] and the PR description you can find the relevant branches/ patches needed to run virtual machines on RISC-V. [1]: https://github.com/au-ts/libvmm/pull/121 Ivan
participants (5)
-
Hugo V.C. -
Ivan Velickovic -
Kent Mcleod -
Robert VanVossen -
Yanfeng Liu