search

seL4 / microkit

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

Compatibility Problems with Raspberry Pi 4 #219

Open AhmadSalehEsfahani opened 1 month ago

AhmadSalehEsfahani commented 1 month ago

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?

Ivan-Velickovic commented 1 month ago

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.

AhmadSalehEsfahani commented 1 month ago

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.