		Search-engine friendly clone of the ACL2 documentation.

X86isa

Running-linux

Running Linux on the x86isa model.

The x86isa model is capable of running 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.

To run Linux, you need to certify the books, as described in x86isa-build-instructions. If you wish to interact with the model over a TCP socket, you need to use ACL2 built with Clozure Common Lisp (CCL). You must also obtain a Linux kernel image and a rootfs (root filesystem) image. We provide instructions to build your own in building-linux and building-rootfs and provide images available to download here with the following SHA512 checksums (available at books/projects/x86isa/linux/artifacts.sha512 in the ACL2 source tree):

00233a202564befedfeee50822fd3b4ef1fc64196bfda38b9382687005d1c2744d9e4a704efb9c5aa3f4aafcffc6c0d1fe71e7ad3eaafe591af681afbaca0144  alpine-gcc.img
9bc9b816ac751c569db4ba17f27c3d9c0ffbd1fb34e4fe129f4fc2b70a572a01e753c564e87cc3eea6f0f82b6d6595f1772ea7d310ba65290dcf86b2a45339aa  alpine.img
05545c7c38547cb8c86968853cd0b2292407764bb0f3924116de19ff5d3059904b148886eff48b13871418b1cf49ecc68d16043444d0e59397086271372626f3  bzImage
859f8d7c67e32183988ae7c8fbe973e537b9e731820b3ff8c26b1f2c3f871cb961c76e5ab1f59f5e58dfc03f1332398f2f07dfe1578918cb0fdb17c89a38f87d  vmlinux

The provided bzImage is the kernel in Linux's bzImage format, which is what we'll use to boot. vmlinux is the kernel provided in ELF format, which isn't used to boot, but useful for debugging. We provide two rootfs images, alpine.img, which contains Alpine Linux's rootfs with just the software that comes with Alpine Linux and alpine-gcc.img, which is Alpine Linux's rootfs with GCC installed.

While it isn't required, we recommend using the bigmem-asymmetric::bigmem-asymmetric memory model because it gives better performance. See physical-memory-model. You can execute the following in ACL2, before doing anything else, to switch:

(include-book "centaur/bigmems/bigmem-asymmetric/bigmem-asymmetric" :dir :system)
(attach-stobj bigmem::mem bigmem-asymmetric::mem)

To load Linux, run the following in an ACL2 session (assuming you're in the books/projects/x86isa directory in the ACL2 source tree):

(include-book "tools/execution/top") 
;; This writes out some identity mapped page tables 
(init-sys-view #xF0000000 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 socat. Execute the following in a shell:

socat file:`tty`,rawer tcp-connect: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 <n> instructions. Booting Linux takes on the order of 600 million instructions. I usually just put in some large number (though you probably want to keep it a fixnum).

As Linux boots, you should see the kernel log being printed in ACL2. Eventually, once Linux is done starting, it'll start /init. The stdout of /init will be printed to the kernel log. If you're using tty-raw.lsp, you'll be able to interact with it over the socket.

The modified Linux kernel has support for a block device called blkx86isa. This device is essentially a view into the gigabyte of physical memory at address 0x100000000. This could be useful for transfering files into and out of the Linux system running in the model. You can mount it like any other drive on a Linux system.

To measure the performance of booting Linux on the x86isa model (running on your specific machine), add code the form

(defun run-model-count-steps (n x86) 
  (declare (xargs :mode :program 
                  :stobjs (x86))) 
  (b* (((when (equal (cpl x86) 3)) (mv n x86)) 
       (x86 (x86-fetch-decode-execute x86))) 
    (run-model-count-steps (1+ n) x86))) 
 
(defun run-model-measure-speed (x86 state) 
  (declare (xargs :mode :program 
                  :stobjs (x86 state))) 
  (b* (((mv start state) (get-real-time state)) 
       ((mv steps x86) (run-model-count-steps 0 x86)) 
       ((mv end state) (get-real-time state)) 
       (duration (round (- end start) 1)) 
       (steps-per-second (round steps duration)) 
       (- (cw "~%~ 
               Time: ~x0 seconds~%~ 
               Steps: ~x1~%~ 
               Speed: ~x2 steps/second~%~%" 
              duration steps steps-per-second))) 
    (mv x86 state)))

The first function runs the model until we enter privilege lever 3, which corresponds to user mode; that is, we execute Linux until it drops into user mode to run init. The second function measures the time elapsed and divides the number of instructions (i.e. steps) by that time, to obtain the average number of instructions per second.

Run the code above with

(run-model-measure-speed x86 state)

This may take a while. At the end, it will print time elapsed, number of instructions, and average number of instructions per second, surrounded by blank lines for readability.

Subtopics

Building-rootfs: How to build a rootfs (root filesystem) image for running Linux on the x86isa model.
Building-linux: How to build a patched Linux kernel for the x86isa model.