Emulating PVS on M1 macs

[Tanner Slagel]

All,

I recently had to figure out how to get PVS running on M1 macs by emulating lubuntu using Qemu. Here are the steps: 

1) Get Qemu (https://www.qemu.org/): You can do this through brew:

brew install qemu

2) Get a Lubuntu iso file (or other lightweight Linux distribution):  https://lubuntu.me/ 

3) Make an .qcow file that will be your virtual machine image:

qemu-img create -f qcow2 <name>.qcow2 20G

The 20G represents the maximum amount of disc space the image can take up (it will ended up being 6-7 Gigabits in my case

4) In the attached lubuntu_vm.sh file, input the name of the lubuntu iso file next to the -cdrom option, and the name of your .qcow2 file next to the -hda option (where there are <>). You may also change the -M parameter to decide how much memory you emulation will get. It is currently set to 4G - this worked well on a M1 macbook air with 8G memory.

5) In the same direcotry as the .qcow2 image and lubuntu .iso file, run the script:
(to make executable):
chmod +x ./lubunt_vm.sh

(then to run)
./lubuntu_vm.sh

6) This will open up an emulation and you will be prompted to install lubuntu. Install lubuntu and close the emulation when completed. You will not need the iso now, so remove the -cdrom <name>.iso from the lubuntu_vm.sh script.

7) To start do ./lubuntu_vm.sh again and lubuntu will start up! From here you can install PVS however you please (the vscode route or through SRI's PVS webpage).

8) Fun note: you may send files from your machine to the emulation by using scp from your machine's terminal:

scp -P 2222 <filename> <username in emulated machine>@localhost:/home/<username in emulated machine>

this will send <filename> to the directory /home/<username in emulated machine> in your emulated machine. 

9) Note: The lightweight Linux distribution is essential - this emulation does not run super quickly, and when we tried this using ubuntu it was painfully slow. Even on lubuntu, typechecking while importing a large library is slow (analysis@top for example). Emacs runs faster than VScode-PVS, but typechecking is still slower than a PVS user would like. 

Have fun! Questions and comments are welcome. This solution was something Rohan Isaac (https://www.linkedin.com/in/rohanisaac) and myself came up with (mostly Rohan). He does not do FM, but someone should really convince him. 

sincerely,

Tanner

[Paolo Masci]

Tanner, thank you for sharing these instructions!

For those of you that want to use PVS on M1 Macs, please be aware that the execution of PVS in Qemu can be *really* slow, for example typechecking any non-trivial theory may take 10-20 minutes in PVS Emacs, and several hours in vscode-pvs.

With SRI we are working on a new release of PVS that can run natively on M1 Macs (and future Apple silicon processors).

Progress is a bit slower than expected, but we are getting there!

Thanks,

Paolo

[Julin S]

That difference between pvs on emacs and vs code is quite large.

Is it because it's running in vm?

Or would there be such significant difference between the two anyway?

[Paolo Masci]

They are both slow because of the emulation with Qemu.

The difference in the performance is probably due to the different APIs used by vscode-pvs and pvs-emacs to interact with the core modules of pvs (vscode-pvs uses a server component, pvs emacs uses a Lisp interface).

Without Qemu, both vscode-pvs and pvs-emacs are much faster, and vscode-pvs is generally faster than pvs-emacs (because of the server component).

If some of you have M1 Macs, could you please try to use a Virtual Box VM with Linux and check if you are able to install and run vscode-pvs and/or pvs-emacs?

If you have already tried this option, please share your experiences.

I don't have access to an M1 Mac for now so I can't perform this test. 

Thanks,

Paolo