|
|
|---|
|
|
|
|---|
Booting linux on the
The x86isa model is capable of booting a slightly modified version of Linux. This version of Linux is modified to add support for our timer and TTY devices and a few other minor changes.
The following is a guide explaining how to boot Linux. First we build the modified kernel. Then, we setup a root filesystem for the machine running under the model. Finally, we load these into the model and execute it.
For the sections about building Linux and the rootfs, we assume that you're on a Linux system. The rest of the guide should work on any ACL2 compatible system.
Rather than distributing the entire modified kernel source tree, we've chosen to distribute a patch. We will download and patch the Linux source tree via git. First, clone the Linux source tree from kernel.org.
git clone https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git cd linux
This will clone the Linux source tree into a folder called
git checkout 12214540ad87
Now, we must apply the patch. The patch file is found in the ACL2
source tree in the file
git apply <path to patch file>
Normally, at this point you'd run
Linux supports GCC and LLVM. I'm using
To compile with GCC, run:
make
Using multiple cores can increase build speed. Use
make -j
or
make -j<nprocs>
to use as many threads as you have logical processors or
This will build a
Most modern Linux machines boot by first loading an initramfs as
the filesystem mounted on
On our machine, we choose to use the initramfs as our root
filesystem and don't
While this should work with other Linux distributions, we've tested
the model with Alpine Linux's rootfs. 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
Alpine Linux's rootfs can be downloaded here:
https://alpinelinux.org/downloads/ under the heading "Mini Root
Filesystem". You want the one built for
Once you've downloded the Alpine mini root filesystem, 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 create the
Run the following command (in the directory you extracted the Alpine
rootfs to) to create the
sudo mknod dev/console c 5 3
Next, we need to add a
Any executable you wish to run on the model that works with Alpine
Linux will work. We wish to start
Busybox is an implementation the standard complement of utilities
you'd expect to find on Unix like systems, including
When started, Busybox inspects the contents of
The solution for this is to write a little program which starts
Therefore, we can either setup a musl toolchain and compile with a compatible version of musl or build a statically linked executable. I choose to use a statically linked executable, mainly since I didn't want to setup a musl toolchain, and since I don't want to link in all of glibc, I wrote it in assembly.
You can find the program in
nasm -f elf64 hello-user.S ld hello-user.o -o hello-user
Then copy the
cp <path to hello-user> <path to alpine rootfs>/init
The last step is to create the compressed cpio archive. Run the following command in the alpine rootfs directory:
find . | cpio --quiet -H newc -o | gzip -9 -n > <archive path>.img
Make sure you aren't saving your cpio archive in the alpine rootfs.
Once you've built the kernel and the rootfs, you're ready to run Linux.
While it isn't required, we recommend using the bigmem-asymmetric::bigmem-asymmetric memory model because it gives better performance. See physical-memory-model for more information about the memory models and how to switch.
Run the following in an ACL2 session (assuming you're in the
(include-book "tools/execution/top")
;; This writes out some identity mapped page tables
(init-sys-view #x10000000 x86)
;; Enable peripherals and exception handling
(!enable-peripherals t x86)
(!handle-exceptions t x86)
;; This function serves as our bootloader
(linux-load "<path to kernel bzImage>"
"<path to rootfs archive>"
;; The following is the kernel command line. Unless you
;; know what you're doing, you don't have much reason to
;; touch this
"rootfstype=ramfs console=ttyprintk ignore_loglevel root=/dev/ram0" x86
state)
This will load Linux into the model. Optionally, if you wish to be able to interact with a shell on the machine over a TCP socket, you can run:
(defttag :tty-raw) (include-raw "machine/tty-raw.lsp")
After submitting the second form, the ACL2 session will hang. At this point you can connect to localhost on TCP port 6444 using a program like netcat or socat. For example, you can do this with netcat by executing the following in a shell:
nc localhost 6444
Once you connect, ACL2 should continue. Note: this utility only works in CCL and is unsound. Don't include it in proofs.
Now, all you have to do is start execution. Submit the following form to ACL2:
(x86-run-steps <n> x86)
This will tell ACL2 to execute
As Linux boots, you should see the kernel log being printed in ACL2.
Eventually, once Linux is done starting, it'll start
The modified Linux kernel has support for a block device called
You can mount it like any other drive on a Linux system, but you
may notice that, if your system is configured as we did above,
mount -t devtmpfs none /dev
After doing this, you'll find a