/cc @TheLortex may be a nicer boot.S and link script. However, a bug persists. I think this layout solve the issue about bss nicely. The remaining bug is about the Sys.argv.(0) and its usage. Indeed, a main.ml such as:

let () = Format.printf "Hello %s!" Sys.argv.(0)

But this code does not show anything:

let () = Format.printf "Hello %S!" Sys.argv.(0)

Main changes

In this PR, the 64 interrupts referenced in the BCM2711 ARM Peripherals manual (6.2.4. VideoCore interrupts) are mapped to signals. Sys.set_signal can be used to setup a handler on one particular interrupt line. Currently, the interrupt process is the following:

• signal_init is called to register a handler to the kernel
• an interrupt is thrown, jump to the handler in the kernel, which in turn jumps to the handler in nolibc/signal.c
• handler dispatch the interruption to the ocaml runtime
• interruption returns, but they stay globally disabled
• at some point, the signal handler is called by OCaml
• the signal handler acknowledges the interrupt and enables them back globally.

Idea

Maybe it's possible to disable only the triggered interruption, but that would mean that double interruptions could occur, I don't know how OCaml handles that (what happens if another signal is triggered while handling a signal ?)

Miscellanous changes

kernel_old=1 is used because otherwise some breaking configuration is done in the interrupt controller (see https://github.com/raspberrypi/tools/blob/13474ee775d0c5ec8a7da4fb0a9fa84187abfc87/armstubs/armstub8.S#L214). I wanted to dune build caml/libnolibc.a and did some fixes for that.

With a deep look, the help of @TheLortex and @pitag-ha. many beers and a MirageOS retreat, we figure out that the compilation of variadic arguments with GCC 11 and GCC 12 produces a bad assembly for a RPi4. At least, that the only real difference we noticed.

For interrupts ID >= 32, the OCaml signal handler wouldn't be called.

That's because 1 << sig is a 32-bit value, it equals to zero when overflowing. Instead we have to do 1L << sig to work with a 64-bit value and get the correct behavior.

It seems that since GCC 11, the compilateur is able to use some 128 bits registers and they are specially used on variadic arguments. Even if we allowed the RPi4 to use these registers, we are trapped by a non-aligned access. We enforce GCC to produce this assembly code and be sure that everything is aligned.

I believe that on the real world operating system, such behavior are trapped and fixed(?) by the kernel.

Changes:

• build system: add dune
• interrupts: add a default handler that prints the exception register
• change default exception level to EL1 (kernel)
• mmu: add a flat mapping to enable cache

Currently, our unikernel is available at 0x0 into our image and we specify to the firmware that we use the old memory layout with kernel_old=1. However, from an @palainp's advise, it will be nice to have a reserved area before the kernel where it will be "safe" to manipulate the NULL pointer (which will be equal to 0x0).

I'm fine with the same memcpy+memmove as the ones in ocaml-freestanding/nolibc. My current testing is:

$ opam pin
gilbraltar.~dev                   git  git+https://github.com/palainp/gilbraltar#nolibc
gilbraltar-linux.~dev             git  git+https://github.com/palainp/gilbraltar#nolibc
gilbraltar-toolchain.~dev         git  git+https://github.com/palainp/gilbraltar#nolibc
mirage-console-gilbraltar.~dev    git  git+https://github.com/palainp/gilbraltar#nolibc
mirage-gilbraltar.~dev            git  git+https://github.com/palainp/gilbraltar#nolibc
$ dune clean && dune build kernel8.img
$ md5sum kernel8.img 
8a83b4fe753409c01e298cd0beb3a6e3  kernel8.img
$ sudo mount /dev/mmcblk0p1 /mnt/
$ cat /mnt/config.txt 
core_freq_min=500
#enable_uart=1
kernel_old=1
$ sudo cp kernel8.img /mnt/
$ sudo umount /mnt
$ sudo minicom -D /dev/ttyUSB0 -b 115200
 _____ _ _ _           _ _                                                      
|   __|_| | |_ ___ ___| | |_ ___ ___                                            
|  |  | | | . |  _| .'| |  _| .'|  _|                                           
|_____|_|_|___|_| |__,|_|_| |__,|_|                                             
EL:1                                                                            
Interrupts: up                                                                  
MMU: ON                                                                         
RPi4: Memory map: 752 MB addressable:                                           
RPi4:   reserved @ (0x0 - 0xffffffffffffffff)                                   
RPi4:       text @ (0x0 - 0x40e5f)                                              
RPi4:     rodata @ (0x40e60 - 0x4738f)                                          
RPi4:       data @ (0x47390 - 0x1012f4f)                                        
RPi4:       heap >= 0x1013000 < stack < 0x2f000000                              
Hello World from OCaml!                                                         
IRQ                                                                             

So, any idea what the other cores should be doing while one is executing one MirageOS unikernel?

One idea would be to have one unikernel per CPU - thus a dedicated network unikernel etc. -- but then there needs to be some communication channel between the unikernels (shared memory? who'd set this up?). I'm thinking mostly in terms of muen policy and channels (i.e. decided at compile time, not at runtime, where code is executed and which communication is setup).

What do you think?

a mirage-gilbraltar, as a mirage-solo5 should exists and we should extend targets inside the mirage/mirage project. However, I think we must implement yield before to be able to launch lwt.