• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
          • Building-rootfs
          • Building-linux
          • Introduction
          • Asmtest
          • X86isa-build-instructions
          • Publications
          • Contributors
          • Machine
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Running-linux

    Building-linux

    How to build a patched Linux kernel for the x86isa model.

    The x86isa model is capable of booting a slightly modified Linux kernel, which includes modifications to add support for our timer and tty and removes Linux's dependence on unimplemented peripherals. Here we describe how to obtain a copy of the Linux source, patch it, and build the kernel. We assume you're using a Linux system with a "Linux-style" file system.

    First, we obtain the Linux source via git. Execute the following in a terminal:

    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 linux in your current working directory and then cd into it. Our patch was tested on version v6.12, so we'll checkout that version:

    git checkout v6.12 
    

    Now, we need to patch the kernel. We include the patch at books/projects/x86isa/linux/x86isa-linux.patch in the ACL2 source tree. To apply it run

    git am <path to patch>

    in your copy of the linux source, substituting <path to patch> for the path to the given x86isa-linux.patch file.

    Normally, at this point you'd run make menuconfig to configure the kernel for your machine, but we included a .config file in the patch that configures the kernel to work with the x86isa model, so you don't need to worry too much about the config. However, run

    make olddefconfig 
    

    to update the config with details dependent on your compiler

    Finally, we can compile the kernel. 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 <nprocs> threads to build respectively.

    This will build a bzImage in arch/x86/boot/bzImage, which is the kernel in Linux's bzImage format. This is the file we will load into the model. It also produces a vmlinux file in the root of the Linux source tree, which contains the kernel in ELF format. While this isn't used to boot, it can be useful when debugging.