I recently spent a lot of time getting the camkes-vm-linux tutorial to
work, because it is the only example I could find of compiling a kernel
module for the linux vm as a part of the camkes build process.
Unfortunately, the kernel module doesn't seem to work. For more
information, see the previous email chain as well as
In lieu of doing things the right way, I believe I could compile a kernel
module for the linux kernel that is provided as part of the camkes build
system. I believe this is how the introspect-app accomplishes its work.
However, I need to have the exact kernel and exact configuration in order
to compile the kernel module correctly.
Can anyone point me to the correct kernel version and configuration, so
that I can target the provided linux kernel for module compilation?
Or if there's a better way to get a kernel module in there, please let me
I am doing a feasibility study to ascertain whether Linux can be deployed
to a seL4 kernel running on a Pi 4B with 8GB of memory. I have seen that
there is explicit support for the Pi 3B, and that Linux can be run in a
virtual machine on top of seL4. But I did not see explicit support for a Pi
4B and the ability to have the Pi run the Linux VM. Please let me know if
this would be possible.
I'm in the process of porting seL4 to a cartesi-machine, which is basically a riscv:rv64ima without PMP (at least for now).
after increasing the available memory 4G and a tweak in the elfloader to accept the flattened device tree from OpenSBI I got the kernel to start, but with errors.
Tried to boot a hello world and the sel4tests, both give pretty much the same result.
I have a suspicion that the unsupported PMP may have something to do with this but since I'm still pretty new to seL4 so I would like advice on how to debug this further.
____ _____ ____ _____
/ __ \ / ____| _ \_ _|
| | | |_ __ ___ _ __ | (___ | |_) || |
| | | | '_ \ / _ \ '_ \ \___ \| _ < | |
| |__| | |_) | __/ | | |____) | |_) || |_
\____/| .__/ \___|_| |_|_____/|____/_____|
Platform Name : Cartesi
Platform Features : mfdeleg
Platform HART Count : 1
Platform IPI Device : aclint-mswi
Platform Timer Device : aclint-mtimer
Platform Console Device : htif
Platform HSM Device : ---
Platform SysReset Device : htif
Firmware Base : 0x80000000
Firmware Size : 260 KB
Runtime SBI Version : 0.3
Domain0 Name : root
Domain0 Boot HART : 0
Domain0 HARTs : 0*
Domain0 Region00 : 0x0000000002080000-0x00000000020bffff (I)
Domain0 Region01 : 0x0000000002000000-0x000000000207ffff (I)
Domain0 Region02 : 0x0000000080000000-0x000000008007ffff ()
Domain0 Region03 : 0x0000000000000000-0xffffffffffffffff (R,W,X)
Domain0 Next Address : 0x0000000080200000
Domain0 Next Arg1 : 0x000000017fff0000
Domain0 Next Mode : S-mode
Domain0 SysReset : yes
Boot HART ID : 0
Boot HART Domain : root
Boot HART ISA : rv64imasu
Boot HART Features : scounteren,mcounteren,time
Boot HART PMP Count : 0
Boot HART PMP Granularity : 0
Boot HART PMP Address Bits: 0
Boot HART MHPM Count : 0
Boot HART MIDELEG : 0x0000000000000222
Boot HART MEDELEG : 0x000000000000b109
ELF-loader started on (HART 0) (NODES 1)
Loaded DTB from 17fff0000.
ELF-loading image 'kernel' to 84000000
ELF-loading image 'sel4test-driver' to 84026000
Enabling MMU and paging
Jumping to kernel-image entry point...
Init local IRQ
Booting all finished, dropped to user space
/host/cartesi/kernel/src/kernel/faulthandler.c:156 :: Caught cap fault in send phase at address 0
while trying to handle:
user exception 0x2 code 0
in thread 0xffffffc17feca200 "rootserver" at address 0x101f0
Recently I have been trying to use sel4 rumprun on another build system
after compiling but I've noticed that rumprun or musl libc only produce
static libraries. How would I compile libc as a shared object?
I have a couple questions about the `DeclareCAmkESComponent` CMake function.
First, is there a way to add a dependency to a CAmkES component? Normally I would use the CMake function `add_dependencies`, but this requires a target name, and I don't believe that the `DeclareCAmkESComponent` function exposes any such target name. If the function deliberately obscures the target name, perhaps a `DEPENDENCIES` argument could be added to the function?
Second, does the `INCLUDES` argument to `DeclareCAmkESComponent` ignore / filter out certain include paths? My compilation was failing because it could not find the proper headers packaged with my compiler. Even if I added the path explicitly by passing it to the `INCLUDES` argument, it was seemingly ignored. It wasn't until I copied the headers to a new directory, and explicitly passed that directory to `INCLUDES` that my compilation succeeded. Any ideas what's going on here?
This isn't a big issue, but I'm curious about how seL4_CNode_Mutate is intended to be used, and have found that the description in the seL4 reference manual doesn't seem to match the implementation.
Is it for changing rights? The manual (Section 3.1.2) says: "seL4_CNode_Mutate() can move a capability similarly to seL4_CNode_Move() and also reduce its rights..." Section 3.1.4 also refers to the possibility to specify a new set of rights with an invocation of seL4_CNode_Mutate(). However, the summary of seL4_CNode_Mutate in Section 10.3.1.6 does not include a parameter that specifies any rights information, so it appears that it cannot actually be used in this way.
Is it for changing badges? In Section 4.2.1, the manual says that "An endpoint capability with a zero badge ... can be badged with the seL4_CNode_Mutate() or seL4_CNode_Mint() invocations" There is a similar statement for Notifications in Section 5.1. But a comment in the (Haskell version of the) spec says "endpoint capabilities may not have their badges changed" when they are updated by a Mutate or Rotate operation. And the kernel seems to follow this: I added a test to sel4test to confirm that you get an illegal operation error if you try to badge an endpoint using Mutate. (Assuming I wrote the test correctly ...)
Unless there are other arch-specific use cases, it looks like the only thing you can do with Mutate is to change the guard of a CNode capability. Even then, that is only possible if you are moving the capability at the same time. Of course, you could combine a mutate with a regular move to simulate an in-place update ... but you could also use an in-place mutate and a separate move to simulate the current behavior, without having to find an empty slot if you just wanted the in-place operation.
One conclusion is that the manual's description of Mutate probably needs an update. But if nobody else has tripped over problems using it to create badged endpoints, then perhaps Mutate just isn't being used very much at all and could be removed altogether? A second thought is whether Mutate could be modified to perform an in-place update if the source and destination are the same (i.e., similar in some ways to how you specify a swap with Rotate)?
about portint doc：(https://docs.sel4.systems/projects/sel4/porting)
“You may need to add device nodes depending on what Linux uses and what is required by seL4. For example, in the port of the Rockpro64 a memory node and an extra timer node were needed so these had to be defined manually.”
how can I get the required by seL4? have any doc about it?