microkit
microkit copied to clipboard
seL4
Compatibility Problems with Raspberry Pi 4
I am experiencing the same issue mentioned in this pull request, but with a Raspberry Pi 4.
Running a “Hello World” sample on the Raspberry Pi 4 using Ivan’s fork works correctly, as shown in the logs below:
## Starting application at 0x10000000 ...
LDR|INFO: altloader for seL4 starting
LDR|INFO: Flags: 0x0000000000000001
seL4 configured as hypervisor
LDR|INFO: Kernel: entry: 0x0000008001000000
LDR|INFO: Root server: physmem: 0x0000000001247000 -- 0x000000000124f000
LDR|INFO: virtmem: 0x000000008a000000 -- 0x000000008a008000
LDR|INFO: entry : 0x000000008a000000
LDR|INFO: region: 0x00000000 addr: 0x0000000001000000 size: 0x0000000000243000 offset: 0x0000000000000000 type: 0x0000000000000001
LDR|INFO: region: 0x00000001 addr: 0x0000000001247000 size: 0x00000000000075e0 offset: 0x0000000000243000 type: 0x0000000000000001
LDR|INFO: region: 0x00000002 addr: 0x0000000001243000 size: 0x00000000000009a0 offset: 0x000000000024a5e0 type: 0x0000000000000001
LDR|INFO: region: 0x00000003 addr: 0x0000000001244000 size: 0x0000000000000390 offset: 0x000000000024af80 type: 0x0000000000000001
LDR|INFO: region: 0x00000004 addr: 0x0000000001245000 size: 0x0000000000001070 offset: 0x000000000024b310 type: 0x0000000000000001
LDR|INFO: copying region 0x00000000
LDR|INFO: copying region 0x00000001
LDR|INFO: copying region 0x00000002
LDR|INFO: copying region 0x00000003
LDR|INFO: copying region 0x00000004
LDR|INFO: CurrentEL=EL2
LDR|INFO: Resetting CNTVOFF
LDR|INFO: enabling MMU
LDR|INFO: jumping to kernel
Bootstrapping kernel
available phys memory regions: 3
[1000000..3b400000]
[40000000..fc000000]
[100000000..200000000]
reserved virt address space regions: 3
[8001000000..8001243000]
[8001243000..8001247000]
[8001247000..800124f000]
Booting all finished, dropped to user space
MON|INFO: Microkit 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
However, running the same sample in the seL4/microkit project, which includes minor changes to support the Raspberry Pi 4 similar to Ivan’s fork, encounters issues. Both the seL4's branch and commit I am using are compatible with what is mentioned in the README.md. The logs for this attempt are as follows:
## Starting application at 0x10000000 ...
LDR|INFO: altloader for seL4 starting
LDR|INFO: Flags: 0x0000000000000001
seL4 configured as hypervisor
LDR|INFO: Kernel: entry: 0x0000008001000000
LDR|INFO: Root server: physmem: 0x0000000001246000 -- 0x000000000124e000
LDR|INFO: virtmem: 0x000000008a000000 -- 0x000000008a008000
LDR|INFO: entry : 0x000000008a000000
LDR|INFO: region: 0x00000000 addr: 0x0000000001000000 size: 0x0000000000243000 offset: 0x0000000000000000 type: 0x0000000000000001
LDR|INFO: region: 0x00000001 addr: 0x0000000001246000 size: 0x0000000000007160 offset: 0x0000000000243000 type: 0x0000000000000001
LDR|INFO: region: 0x00000002 addr: 0x0000000001243000 size: 0x0000000000000908 offset: 0x000000000024a160 type: 0x0000000000000001
LDR|INFO: region: 0x00000003 addr: 0x0000000001244000 size: 0x0000000000000378 offset: 0x000000000024aa68 type: 0x0000000000000001
LDR|INFO: region: 0x00000004 addr: 0x0000000001245000 size: 0x0000000000000040 offset: 0x000000000024ade0 type: 0x0000000000000001
LDR|INFO: copying region 0x00000000
LDR|INFO: copying region 0x00000001
LDR|INFO: copying region 0x00000002
LDR|INFO: copying region 0x00000003
LDR|INFO: copying region 0x00000004
LDR|INFO: CurrentEL=EL2
LDR|INFO: Resetting CNTVOFF
LDR|INFO: enabling MMU
LDR|INFO: jumping to kernel
Bootstrapping kernel
available phys memory regions: 3
[1000000..3b400000]
[40000000..fc000000]
[100000000..200000000]
reserved virt address space regions: 3
[8001000000..8001243000]
[8001243000..8001246000]
[8001246000..800124e000]
Booting all finished, dropped to user space
MON|INFO: Microkit Bootstrap
Bootinfo: 0x000000008a009000
extraLen = 0x0000000000000000
nodeID = 0x0000000000000000
numNodes = 0x0000000000000001
numIOPTLevels = 0x0000000000000000
ipcBuffer* = 0x000000008a008000
initThreadCNodeSizeBits = 0x000000000000000c
initThreadDomain = 0x0000000000000000
userImagePaging = 0x0000000000000010..0x0000000000000012
schedcontrol = 0x0000000000000013..0x0000000000000013
userImageFrames = 0x0000000000000014..0x000000000000001b
untyped = 0x000000000000001c..0x000000000000006b
empty = 0x000000000000006c..0x0000000000000fff
sharedFrames = 0x0000000000000000..0xffffffffffffffff
ioSpaceCaps = 0x0000000000000000..0xffffffffffffffff
extraBIPages = 0x0000000000000000..0xffffffffffffffff
untypedList[0x00000000] = slot: 0x0000001c, paddr: 0x0000000001243000 - 0x0000000001244000 (device) bits: 0x0000000c
untypedList[0x00000001] = slot: 0x0000001d, paddr: 0x0000000001244000 - 0x0000000001246000 (device) bits: 0x0000000d
untypedList[0x00000002] = slot: 0x0000001e, paddr: 0x0000000000000000 - 0x0000000001000000 (device) bits: 0x00000018
untypedList[0x00000003] = slot: 0x0000001f, paddr: 0x000000003b400000 - 0x000000003b800000 (device) bits: 0x00000016
untypedList[0x00000004] = slot: 0x00000020, paddr: 0x000000003b800000 - 0x000000003c000000 (device) bits: 0x00000017
untypedList[0x00000005] = slot: 0x00000021, paddr: 0x000000003c000000 - 0x0000000040000000 (device) bits: 0x0000001a
untypedList[0x00000006] = slot: 0x00000022, paddr: 0x00000000fc000000 - 0x00000000fe000000 (device) bits: 0x00000019
untypedList[0x00000007] = slot: 0x00000023, paddr: 0x00000000fe000000 - 0x00000000ff000000 (device) bits: 0x00000018
untypedList[0x00000008] = slot: 0x00000024, paddr: 0x00000000ff000000 - 0x00000000ff800000 (device) bits: 0x00000017
untypedList[0x00000009] = slot: 0x00000025, paddr: 0x00000000ff801000 - 0x00000000ff802000 (device) bits: 0x0000000c
untypedList[0x0000000a] = slot: 0x00000026, paddr: 0x00000000ff802000 - 0x00000000ff804000 (device) bits: 0x0000000d
untypedList[0x0000000b] = slot: 0x00000027, paddr: 0x00000000ff804000 - 0x00000000ff808000 (device) bits: 0x0000000e
untypedList[0x0000000c] = slot: 0x00000028, paddr: 0x00000000ff808000 - 0x00000000ff810000 (device) bits: 0x0000000f
untypedList[0x0000000d] = slot: 0x00000029, paddr: 0x00000000ff810000 - 0x00000000ff820000 (device) bits: 0x00000010
untypedList[0x0000000e] = slot: 0x0000002a, paddr: 0x00000000ff820000 - 0x00000000ff840000 (device) bits: 0x00000011
untypedList[0x0000000f] = slot: 0x0000002b, paddr: 0x00000000ff840000 - 0x00000000ff841000 (device) bits: 0x0000000c
untypedList[0x00000010] = slot: 0x0000002c, paddr: 0x00000000ff843000 - 0x00000000ff844000 (device) bits: 0x0000000c
untypedList[0x00000011] = slot: 0x0000002d, paddr: 0x00000000ff845000 - 0x00000000ff846000 (device) bits: 0x0000000c
untypedList[0x00000012] = slot: 0x0000002e, paddr: 0x00000000ff846000 - 0x00000000ff848000 (device) bits: 0x0000000d
untypedList[0x00000013] = slot: 0x0000002f, paddr: 0x00000000ff848000 - 0x00000000ff850000 (device) bits: 0x0000000f
untypedList[0x00000014] = slot: 0x00000030, paddr: 0x00000000ff850000 - 0x00000000ff860000 (device) bits: 0x00000010
untypedList[0x00000015] = slot: 0x00000031, paddr: 0x00000000ff860000 - 0x00000000ff880000 (device) bits: 0x00000011
untypedList[0x00000016] = slot: 0x00000032, paddr: 0x00000000ff880000 - 0x00000000ff900000 (device) bits: 0x00000013
untypedList[0x00000017] = slot: 0x00000033, paddr: 0x00000000ff900000 - 0x00000000ffa00000 (device) bits: 0x00000014
untypedList[0x00000018] = slot: 0x00000034, paddr: 0x00000000ffa00000 - 0x00000000ffc00000 (device) bits: 0x00000015
untypedList[0x00000019] = slot: 0x00000035, paddr: 0x00000000ffc00000 - 0x0000000100000000 (device) bits: 0x00000016
untypedList[0x0000001a] = slot: 0x00000036, paddr: 0x0000000200000000 - 0x0000000400000000 (device) bits: 0x00000021
untypedList[0x0000001b] = slot: 0x00000037, paddr: 0x0000000400000000 - 0x0000000800000000 (device) bits: 0x00000022
untypedList[0x0000001c] = slot: 0x00000038, paddr: 0x0000000800000000 - 0x0000001000000000 (device) bits: 0x00000023
untypedList[0x0000001d] = slot: 0x00000039, paddr: 0x0000001000000000 - 0x0000002000000000 (device) bits: 0x00000024
untypedList[0x0000001e] = slot: 0x0000003a, paddr: 0x0000002000000000 - 0x0000004000000000 (device) bits: 0x00000025
untypedList[0x0000001f] = slot: 0x0000003b, paddr: 0x0000004000000000 - 0x0000008000000000 (device) bits: 0x00000026
untypedList[0x00000020] = slot: 0x0000003c, paddr: 0x0000008000000000 - 0x0000018000000000 (device) bits: 0x00000028
untypedList[0x00000021] = slot: 0x0000003d, paddr: 0x0000018000000000 - 0x0000038000000000 (device) bits: 0x00000029
untypedList[0x00000022] = slot: 0x0000003e, paddr: 0x0000038000000000 - 0x0000078000000000 (device) bits: 0x0000002a
untypedList[0x00000023] = slot: 0x0000003f, paddr: 0x0000078000000000 - 0x00000f8000000000 (device) bits: 0x0000002b
untypedList[0x00000024] = slot: 0x00000040, paddr: 0x00000f8000000000 - 0x0000100000000000 (device) bits: 0x00000027
untypedList[0x00000025] = slot: 0x00000041, paddr: 0x0000000001000000 - 0x0000000001010000 (normal) bits: 0x00000010
untypedList[0x00000026] = slot: 0x00000042, paddr: 0x000000000124e000 - 0x0000000001250000 (normal) bits: 0x0000000d
untypedList[0x00000027] = slot: 0x00000043, paddr: 0x0000000001250000 - 0x0000000001260000 (normal) bits: 0x00000010
untypedList[0x00000028] = slot: 0x00000044, paddr: 0x0000000001260000 - 0x0000000001280000 (normal) bits: 0x00000011
untypedList[0x00000029] = slot: 0x00000045, paddr: 0x0000000001280000 - 0x0000000001300000 (normal) bits: 0x00000013
untypedList[0x0000002a] = slot: 0x00000046, paddr: 0x0000000001300000 - 0x0000000001400000 (normal) bits: 0x00000014
untypedList[0x0000002b] = slot: 0x00000047, paddr: 0x0000000001400000 - 0x0000000001800000 (normal) bits: 0x00000016
untypedList[0x0000002c] = slot: 0x00000048, paddr: 0x0000000001800000 - 0x0000000002000000 (normal) bits: 0x00000017
untypedList[0x0000002d] = slot: 0x00000049, paddr: 0x0000000002000000 - 0x0000000004000000 (normal) bits: 0x00000019
untypedList[0x0000002e] = slot: 0x0000004a, paddr: 0x0000000004000000 - 0x0000000008000000 (normal) bits: 0x0000001a
untypedList[0x0000002f] = slot: 0x0000004b, paddr: 0x0000000008000000 - 0x0000000010000000 (normal) bits: 0x0000001b
untypedList[0x00000030] = slot: 0x0000004c, paddr: 0x0000000010000000 - 0x0000000020000000 (normal) bits: 0x0000001c
untypedList[0x00000031] = slot: 0x0000004d, paddr: 0x0000000020000000 - 0x0000000030000000 (normal) bits: 0x0000001c
untypedList[0x00000032] = slot: 0x0000004e, paddr: 0x0000000030000000 - 0x0000000038000000 (normal) bits: 0x0000001b
untypedList[0x00000033] = slot: 0x0000004f, paddr: 0x0000000038000000 - 0x000000003a000000 (normal) bits: 0x00000019
untypedList[0x00000034] = slot: 0x00000050, paddr: 0x000000003a000000 - 0x000000003b000000 (normal) bits: 0x00000018
untypedList[0x00000035] = slot: 0x00000051, paddr: 0x000000003b000000 - 0x000000003b400000 (normal) bits: 0x00000016
untypedList[0x00000036] = slot: 0x00000052, paddr: 0x0000000040000000 - 0x0000000080000000 (normal) bits: 0x0000001e
untypedList[0x00000037] = slot: 0x00000053, paddr: 0x0000000080000000 - 0x00000000c0000000 (normal) bits: 0x0000001e
untypedList[0x00000038] = slot: 0x00000054, paddr: 0x00000000c0000000 - 0x00000000e0000000 (normal) bits: 0x0000001d
untypedList[0x00000039] = slot: 0x00000055, paddr: 0x00000000e0000000 - 0x00000000f0000000 (normal) bits: 0x0000001c
untypedList[0x0000003a] = slot: 0x00000056, paddr: 0x00000000f0000000 - 0x00000000f8000000 (normal) bits: 0x0000001b
untypedList[0x0000003b] = slot: 0x00000057, paddr: 0x00000000f8000000 - 0x00000000fc000000 (normal) bits: 0x0000001a
untypedList[0x0000003c] = slot: 0x00000058, paddr: 0x0000000100000000 - 0x0000000180000000 (normal) bits: 0x0000001f
untypedList[0x0000003d] = slot: 0x00000059, paddr: 0x0000000180000000 - 0x00000001c0000000 (normal) bits: 0x0000001e
untypedList[0x0000003e] = slot: 0x0000005a, paddr: 0x00000001c0000000 - 0x00000001e0000000 (normal) bits: 0x0000001d
untypedList[0x0000003f] = slot: 0x0000005b, paddr: 0x00000001e0000000 - 0x00000001f0000000 (normal) bits: 0x0000001c
untypedList[0x00000040] = slot: 0x0000005c, paddr: 0x00000001f0000000 - 0x00000001f8000000 (normal) bits: 0x0000001b
untypedList[0x00000041] = slot: 0x0000005d, paddr: 0x00000001f8000000 - 0x00000001fc000000 (normal) bits: 0x0000001a
untypedList[0x00000042] = slot: 0x0000005e, paddr: 0x00000001fc000000 - 0x00000001fe000000 (normal) bits: 0x00000019
untypedList[0x00000043] = slot: 0x0000005f, paddr: 0x00000001fe000000 - 0x00000001ff000000 (normal) bits: 0x00000018
untypedList[0x00000044] = slot: 0x00000060, paddr: 0x00000001ff000000 - 0x00000001ff800000 (normal) bits: 0x00000017
untypedList[0x00000045] = slot: 0x00000061, paddr: 0x00000001ff800000 - 0x00000001ffc00000 (normal) bits: 0x00000016
untypedList[0x00000046] = slot: 0x00000062, paddr: 0x00000001ffc00000 - 0x00000001ffe00000 (normal) bits: 0x00000015
untypedList[0x00000047] = slot: 0x00000063, paddr: 0x00000001ffe00000 - 0x00000001fff00000 (normal) bits: 0x00000014
untypedList[0x00000048] = slot: 0x00000064, paddr: 0x00000001fff00000 - 0x00000001fff80000 (normal) bits: 0x00000013
untypedList[0x00000049] = slot: 0x00000065, paddr: 0x00000001fff80000 - 0x00000001fffc0000 (normal) bits: 0x00000012
untypedList[0x0000004a] = slot: 0x00000066, paddr: 0x00000001fffe7880 - 0x00000001fffe7900 (normal) bits: 0x00000007
untypedList[0x0000004b] = slot: 0x00000067, paddr: 0x00000001fffe7900 - 0x00000001fffe7a00 (normal) bits: 0x00000008
untypedList[0x0000004c] = slot: 0x00000068, paddr: 0x00000001fffe7a00 - 0x00000001fffe7c00 (normal) bits: 0x00000009
untypedList[0x0000004d] = slot: 0x00000069, paddr: 0x00000001fffe7c00 - 0x00000001fffe8000 (normal) bits: 0x0000000a
untypedList[0x0000004e] = slot: 0x0000006a, paddr: 0x00000001fffe8000 - 0x00000001ffff0000 (normal) bits: 0x0000000f
untypedList[0x0000004f] = slot: 0x0000006b, paddr: 0x00000001ffff0000 - 0x0000000200000000 (normal) bits: 0x00000010
Untyped Memory Ranges
paddr: 0x0000000001243000 - 0x0000000001246000 (device)
paddr: 0x0000000000000000 - 0x0000000001000000 (device)
paddr: 0x000000003b400000 - 0x0000000040000000 (device)
paddr: 0x00000000fc000000 - 0x00000000ff800000 (device)
paddr: 0x00000000ff801000 - 0x00000000ff841000 (device)
paddr: 0x00000000ff843000 - 0x00000000ff844000 (device)
paddr: 0x00000000ff845000 - 0x0000000100000000 (device)
paddr: 0x0000000200000000 - 0x0000100000000000 (device)
paddr: 0x0000000001000000 - 0x0000000001010000 (normal)
paddr: 0x000000000124e000 - 0x000000003b400000 (normal)
paddr: 0x0000000040000000 - 0x00000000fc000000 (normal)
paddr: 0x0000000100000000 - 0x00000001fffc0000 (normal)
paddr: 0x00000001fffe7880 - 0x0000000200000000 (normal)
MON|ERROR: cap start mismatch. Expected cap start: 0x0000001b boot info cap start: 0x0000001c
FAIL: cap start mismatch
It seems there is a difference in depth between Ivan’s fork and the main project. Is there a reason why the supported boards in Ivan’s fork have not been added to the main project?
I haven't added support for Raspberry Pi because it's a very annoying and difficult platform to work with. However, if the community wants it I can add it, I understand it's a popular platform.
Is there a reason why the supported boards in Ivan’s fork have not been added to the main project?
Is there anything else missing other than the Raspberry Pi 4? My plan wasn't to add every single platform that seL4 supports unless people wanted them, feel free to post an issue if there are more platforms missing.
Thank you for your response and for considering the community’s needs. I understand that the Raspberry Pi can be a challenging platform to work with. However, given its popularity, adding support for it would be greatly appreciated by many users, including myself. Also, I appreciate your openness to adding more platforms based on community demand. Besides the Raspberry Pi platforms, I don’t have any other specific platforms in mind at the moment, but I’ll post an issue if I come across any.
Raspberry Pi 4B should now be supported, let me know if you run into issues. I tested it locally with an RPi4B. Thanks for your patience.