		Search-engine friendly clone of the ACL2 documentation.

Running-linux

Building-rootfs

How to build a rootfs (root filesystem) image for running Linux on the x86isa model.

Most modern Linux machines boot by first loading an initramfs as the file system mounted on /. This, as the name suggests, is an initial file system which resides in RAM. The kernel then starts /init, which mounts the "real" root file system, usually from a disk. Then it uses the pivot_root syscall to make it the new /. This allows Linux to dynamicly link in the appropriate kernel modules from the initramfs, including disk and file system drivers necessary to mount the "real" disk.

On our machine, we choose to use the initramfs as our root file system and don't pivot_root. This makes it so that we don't have to use a disk device to boot. Linux requires the initramfs to be a (potentially compressed) cpio archive.

We assume you're following this using a Linux system with a "Linux-style" file system. While this should work with other Linux distributions, we've tested the model with Alpine Linux's rootfs (version 3.21, the latest as of writing). We chose this distribution because it is small, making it easy to quickly recreate the cpio archive as needed when testing and because they provide a download link on their website for a tarball of their rootfs, rather than having to bootstrap the rootfs using a tool like Arch Linux's pacstrap.

Alpine Linux version 3.21 for x86_64 can be downloaded here. From that page, download the file alpine-minirootfs-3.21.0-x86_64.tar.gz.

Once you've downloded the Alpine mini root file system, do the following to extract it:

mkdir alpine 
cd alpine 
# Note: the Alpine tarball will extract into your current directory, 
# so you should create a directory to contain the files, as shown 
# above 
tar xvf <downloaded Alpine tarball path>

Now, we need to add an init script. This is what the kernel will start once it is done booting. We provide the following simple init script:

#!/bin/busybox sh

mount -t devtmpfs none /dev
mount -t proc proc /proc
mount -t sysfs sysfs /sys

hostname x86isa-linux
export HOME=/root

exec sh -l

at books/projects/x86isa/linux/init in the ACL2 source tree. It mounts some file systems that are expected to be present by many programs, sets the system hostname and the HOME environment variable, and then starts a login shell for us to use. Copy it to the root of your alpine rootfs and make sure it has executable permissions.

If you wish to install additional software, you can chroot into your alpine rootfs and install your software like usual.

The last step is to create the cpio archive. We'll use libarchive's implementation of tar, which in addition to tar, supports a number of archive formats, including cpio. On Linux systems, it's usually installed as bsdtar. Run the following command in the alpine rootfs directory to create your rootfs image:

bsdtar --format newc --uid 0 --gid 0 -cvf <archive path>.img *

Make sure you aren't saving your archive in the rootfs directory. Once that is done you should have a cpio archive <archive path>.img containing your rootfs, which can be used to boot Linux.