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
Hi Miriam,
What platform are you targeting on RISC-V? I was able to get the tutorial working when doing `./init —tut untyped —solution` and targeting the Spike platform. `seL4_Untyped_Retype` is not architecture dependent, so should work on RISC-V.
Ivan
On 7/05/2022, at 3:13 AM, inf19109@lehre.dhbw-stuttgart.de wrote:
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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
Hi Ivan,
thanks for your fast reply and confirming that it actually works.
However for me it's still not working.
How did you manage to target the tutorial for Spike (which I'm also using as target platform)? And did you change any parameters of the function?
Best regards, Miriam
Hi Miriam,
You should be able to reproduce the tutorial using this patch and applying it to "projects/sel4-tutorials": https://gist.github.com/Ivan-Velickovic/71a232a39d686b6a9cf33e83d9342086
Then you’ll need to clone OpenSBI and checkout v0.8 in the “tools” directory.
From there, you should be able to run "./init —tut untyped —solution —plat spike”. Running the simulate script should print out a success message and so should the check script.
I did not change anything in the solution code.
Ivan
On 17/05/2022, at 12:01 AM, inf19109@lehre.dhbw-stuttgart.demailto:inf19109@lehre.dhbw-stuttgart.de wrote:
Hi Ivan,
thanks for your fast reply and confirming that it actually works.
However for me it's still not working.
How did you manage to target the tutorial for Spike (which I'm also using as target platform)? And did you change any parameters of the function?
Best regards, Miriam _______________________________________________ Devel mailing list -- devel@sel4.systemsmailto:devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systemsmailto:devel-leave@sel4.systems
-
inf19109＠lehre.dhbw-stuttgart.de -
Ivan Velickovic