		Search-engine friendly clone of the ACL2 documentation.

Model-validation

Virtualization-for-validation

Validating the model by comparing its behavior with a virtual machine

Our virtualization based model validation tool works by loading the state of the machine into KVM, Linux's hardware accelerated virtualization API. This means using it requires a Linux system with support for hardware accelerated virtualization. This has been tested on Intel processors with VMX and (very minimally) on QEMU with its tiny code generator (TCG) backend.

This tool, at a high level, consists of a C program and some ACL2 functions. We use the function dump-virtualizable-state to dump the model's state into a file. Then, we run the C program, which loads the model state from the file into a KVM virtual machine and opens a socket. Then, we call the validate-insts function, which connects to the socket causing the virtual machine to execute some instructions, executes the model until the instruction pointer matches the VM, and then compares the GPRs and RIP.

It should be noted that this tool is very rough around the edges. It was built quickly to help track down bugs when attempting to get Linux to boot on the model. Additionally, it only works in the system-view mode, though if you have userspace Linux binary that you wish to use to test, you can do it by booting-linux and then running the program under Linux on the model. Of course, this won't catch bugs that only occur in app-view. This tool also requires including raw lisp and is unsound. It also requires using CCL.

Before using this tool, you should probably read virtualization-for-validation-limitations. Additionally, if you encounter issues, debugging tips are documented at virtualization-for-validation-debugging.

To use this tool, first compile the C program in books/projects/x86isa/virtualization/main.c with the flag -DVALIDATE (without it, the program simply executes a few instructions and logs some information). Since this uses Linux kernel APIs, to compile it you may need to make sure you have kernel headers installed. These can usually be downloaded from your Linux distribution's package manager. Refer the to the documentation of the Linux distribution you are using for help with this.

Next, open ACL2 and include the model. Get it into whatever initial state you wish to use. Then, include the virtualization/top book and call dump-virtualizable-state passing it the filename you wish to save to, the x86 stobj, and state. Then, run the C program you compiled, making sure the file you just saved is in your current working directory and called state.virt. To use it, you need to make sure you have permissions to open the /dev/kvm device.

Finally, in ACL2, execute validate-insts passing it the number of iterations (number of comparisons with the VM and model) you wish to execute and the x86 stobj. This will continue executing instructions until one of the following is met:

The number of iterations has been exhausted.
In the last iteration, we executed 30 instructions, but we weren't able to get to the same instruction pointer value as the VM.
In the last iteration, we found a difference between the GPRs of the model and the GPRs of the VM.

Subtopics

Virtualization-for-validation-debugging: Some tips on debugging the virtualization based validation tool.
Virtualization-for-validation-limitations: A note regarding the limitations of our virtualization based validation scheme.
Dump-virtualizable-state: Write the a subset of the model state to a file in a format that can be read by our virtualization-for-validation tools.
Write-virtualizable-mem: Write the memory to a channel.
Validate-insts: Validate the model until we have done n iterations.
Run-until-rip-or-n: Execute the model until we reach the given rip address or have executed n instructions.
Validate-inst: Handles a single back and forth with the C program over the socket. Smashed in raw lisp.
Write-val1
Write-bytes