gazagnaire.org
Example mirage-eio unikernels
xen/two-domain: run the interrupt self-test before the shared-page exchange
Each domain calls R.irq_selftest once at boot, demonstrating the GICv3
interrupt subsystem in a dom0less domU. Boot-verified: both domains report the
SGI handler FIRED.
author
Thomas Gazagnaire
date
(Jul 18, 2026, 8:35 AM UTC)
commit
b06d8a79
b06d8a797d67142dce32b21372202198a1ce442f
parent
bae54dab
bae54dabb0e49d4b7274aa27d51d1cc4ea5b5074
+19
-1
+9
bin/xen/two-domain/README.md
+9
bin/xen/two-domain/README.md
···
22
22
boots both domains -- no hand-written device tree, no raw qemu:
23
23
24
24
```
25
+
(d2) [irq] SGI self-test: FIRED (interrupt path works)
26
+
(d1) [irq] SGI self-test: FIRED (interrupt path works)
25
27
(d2) [round 1/10] shared counter now 1 -- the peer's writes are visible
26
28
(d1) [round 1/10] shared counter now 3 -- the peer's writes are visible
27
29
(d2) [round 2/10] shared counter now 2 -- the peer's writes are visible
···
29
31
(d2) ==== done: shared counter reached 18 > 10 rounds -- the two domains share one page ====
30
32
(d1) ==== done: shared counter reached 20 > 10 rounds -- the two domains share one page ====
31
33
```
34
+
35
+
Each domain first runs an interrupt self-test (`R.irq_selftest`): it installs an
36
+
AArch64 exception vector table, brings up the GICv3 CPU interface and
37
+
redistributor, sends itself a software-generated interrupt, and confirms the IRQ
38
+
handler ran -- the machinery a guest needs to wake on a device interrupt instead
39
+
of polling, since Xen/ARM injects device IRQs through the vGIC (there is no
40
+
`bind_pirq` path to an event channel on ARM). The counter exchange then follows.
32
41
33
42
Both domains run the same image (`unikernel.xen`, linked at the standard guest
34
43
RAM base `0x40000000` where Xen maps each domain's static memory) and need no
+10
-1
bin/xen/two-domain/unikernel.ml
+10
-1
bin/xen/two-domain/unikernel.ml
···
15
15
mapping ONE host page instead reach about 2*[rounds], because each sees the
16
16
other's writes. The port (10) and the shared page's guest address are
17
17
conventions the host device tree and the runner (cmd_run) agree on, since a
18
-
fully static domain gets no dynamically generated tree of its own. *)
18
+
fully static domain gets no dynamically generated tree of its own.
19
+
20
+
Before the exchange, each domain runs {!R.irq_selftest} once: it installs an
21
+
exception vector table, brings up the GICv3 CPU interface and redistributor,
22
+
sends itself a software interrupt, and confirms the handler ran -- the
23
+
interrupt machinery a guest needs to wake on a device IRQ (Xen/ARM injects
24
+
those through the vGIC) instead of polling. *)
19
25
20
26
module R = Mirage_eio_xen_hypercalls.Runtime
21
27
···
39
45
(* Map shared_info (the event-channel pending bitmap lives there) and the
40
46
grant table, as any PV guest does at boot. *)
41
47
if R.boot_identity () <> 0 then failwith "boot_identity: boot mapping failed";
48
+
Printf.printf "[irq] SGI self-test: %s\n%!"
49
+
(if R.irq_selftest () then "FIRED (interrupt path works)"
50
+
else "no interrupt (timed out)");
42
51
(* The one host page Xen maps into both domains (xen,static-shm): the counter
43
52
lives in its first four bytes. *)
44
53
let shared = R.shared_region ~gpa:shm_gpa ~len:shm_len in