seL4
Added rockpro64
I added the rock pro to Ivan's fork:
https://github.com/Ivan-Velickovic/microkit
and I was able to boot the hello example on the rockpro64 without issues. I have added my changes against the upstream version and it boots but doesn't print hello on the UART. Something is different in Ivan's for that is missing in upstream. I don't want to make a pull request for changes that aren't mine so I am just adding the changes for the rockpro64.
Can you show the log of when it's not working? It might help me remember what patch is needed.
When I added the changes to your fork I saw successful boot like this:
## Starting application at 0x20000000 ...
Bootstrapping kernel
available phys memory regions: 1
[10000000..f8000000]
reserved virt address space regions: 3
[ffffff8010000000..ffffff8010243000]
[ffffff8010243000..ffffff8010247000]
[ffffff8010247000..ffffff801024e000]
Booting all finished, dropped to user space
MON|INFO: seL4 Core Platform Bootstrap
MON|INFO: bootinfo untyped list matches expected list
MON|INFO: Number of bootstrap invocations: 0x00000009
MON|INFO: Number of system invocations: 0x00000023
MON|INFO: completed bootstrap invocations
MON|INFO: completed system invocations
hello, world
Adding equivalent changes to the upstream yields:
Load address: 0x20000000
Loading: #################################################################
#################################################################
######################################
8.2 MiB/s
done
Bytes transferred = 2455016 (2575e8 hex)
## Starting application at 0x20000000 ...
Bootstrapping kernel
available phys memory regions: 1
[10000000..f8000000]
reserved virt address space regions: 2
[ffffff8010000000..ffffff8010243000]
[ffffff8010247000..ffffff801024e000]
Booting all finished, dropped to user space
MON|INFO: Microkit Bootstrap
MON|ERROR: cap start mismatch. Expected cap start: 0x0000001a boot info cap start: 0x0000001b
FAIL: cap start mismatch
I should note though that I saw some flaky behavior on this board today. It was not getting further than:
## Starting application at 0x20000000 ...
for either version for about a dozen attempts. I don't have another board to test.
My guess is that the commit of seL4 doesn't match what's in this README. The fork uses a different version of seL4.
I also notice no UART output from the loader? There should be a bunch of LDR|INFO:... printing at the start.
I'm not sure what's going on with ## Starting application at 0x20000000 ... and then nothing happening. If we know the loader output works and it's still not outputting, something else is going wrong. Either the image hasn't been transferred to U-Boot successfully or the loader is not getting to main for some reason.
Hey @sand7000, any luck? Let me know if I can help in any way.
Sorry for delayed response, I have been traveling and busy on another project. I think you are right. I rebuilt today but I can't test because our board seems to be bad. I bought a new one and will test when I have it.
Hi @sand7000, I've made https://github.com/seL4/microkit/pull/230 and tested it on a ROCKPro64 locally and have managed to get it working.
I made a new PR since there's been a bunch of conflicting changes to Microkit since this PR was created.
Thanks!