After a first successful boot, I want to understand how the files fit together. There is source code, an ELF, a system description, and a bootable image. Each answers a different question about the program I am trying to run.
The Microkit/QEMU setup note gets the tools working. This note is about reading the configuration that connects them.
Start with the Program Image
An ELF is an input to the system build. It contains the compiled program, but the program's file name alone tells me little about the environment in which it will execute.
I read the system description alongside the code. Microkit's public tutorial introduces this XML file by connecting a protection domain to its program image. It also explains the execution context, address space, and capabilities associated with a domain. Upstream introduction.
That gives me a useful reading habit: whenever I find a program image, I look for the corresponding configuration entry.
Read a Small Description First
Here is an illustrative fragment:
<system>
<protection_domain name="sample">
<program_image path="sample.elf" />
</protection_domain>
</system>
This is a structure example. It assumes that sample.elf has been built for the intended target; the fragment is not a complete build recipe.
There are two names worth separating. sample names the protection domain in the description. sample.elf names the executable input. Keeping those distinct makes it easier to follow a build error back to either a configuration reference or a missing artifact.
The versioned Microkit manual defines the elements and attributes. I keep that reference open when reading an unfamiliar description rather than inferring syntax from a diagram.
Follow the Inputs Through the Build
I find this small inventory useful:
| Item | Question it answers |
|---|---|
| Program source | What behavior am I compiling? |
| Program ELF | Which executable file does the description reference? |
| System description | Which programs and resources are configured together? |
| Selected SDK board and configuration | Which target assumptions does the build use? |
| Generated image | Which output will the emulator or bootloader load? |
When a build fails, this list helps narrow the next question. An absent ELF and an unsupported configuration attribute need different fixes, even though both can stop image generation.
Treat Resource Declarations as Part of the Program
A larger description can introduce memory mappings and communication channels. Those declarations affect how the application can behave, so I review their changes alongside changes to the C code. The manual is the reference for their exact meaning in the selected SDK release.
For a first reading, I write a plain-language annotation beside each declaration: which program it concerns, which resource it names, and why the program needs it. An entry I cannot explain becomes a question to resolve before adding another component.
A Small Reading Exercise
Open the public hello example from the setup note. Find its ELF reference, locate that file in the build directory, and follow the image-generation command that consumes the description.
Then explain the path from source to boot image in a few sentences. Being able to describe that path makes the next configuration change easier to review and debug.