seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Added rockpro64 #71

Open sand7000 opened 9 months ago

sand7000 commented 9 months ago

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.

Ivan-Velickovic commented 9 months ago

Can you show the log of when it's not working? It might help me remember what patch is needed.

sand7000 commented 9 months ago

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.

Ivan-Velickovic commented 9 months ago

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.

Ivan-Velickovic commented 8 months ago

Hey @sand7000, any luck? Let me know if I can help in any way.

sand7000 commented 8 months ago

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.