It feels as if the idea of having a formal specification of a processor has turned a corner. Instead of having incomplete specs for parts of some architectures, we now have specs for Arm and RISC-V that are complete enough that you can boot an OS on them and we have complete specs of the x86 instruction set. Instead of having specs that are tied to some particular project/purpose, we have flexible specs that can be used to reason for many different purposes. So this is a great time to hold a workshop for the people working on all the different specs and applications to get together, compare notes and identify future challenges.

Last Friday was the first and hopefully not the last SpISA (pronounced “spicer”) workshop in Portland, Oregon. Historically, formal ISA specs were developed for interactive theorem proving and were usually tied to one particular theorem prover so it was natural that the workshop should be attached to the annual Interactive Theorem Proving conference but only three of the eleven talks involved interactive theorem proving.

The day started with a keynote by Ronak Singhal (Intel) who described the challenges of developing/curating the Intel architecture and teased that they were looking into creating and releasing a formal spec of the x86 architecture where other vendors have paved the way. I had interesting talks in the break about what Intel is doing, the challenges we had at Arm creating, validating and releasing Arm specs, etc.

Shilpi Goel (Centaur) gave a talk about formal verification of instruction execution in their x86 processors and David Russinoff (Arm) talked about verification of floating point units. These were the only hardware verification talks at the workshop - both very cool work!

Sandeep Dasgupta and Andrew Miranti (U. Illinois) gave a talk about their complete x86-64 ISA specification in the K framework and Ben Selfridge (galois) gave a talk about his RISC-V spec written in Haskell. I think that having ISA specs that are not tied to any particular prover is really important.

David Hardin (Collins Aerospace), Freek Verbeek (Virginia Tech.), Samuel Pollard (Oregon State/Sandia) and Joe Hendrix (galois) each talked about various forms of reasoning about binaries (decompilation into logic / symbolic execution / binary lifting).

Shilpi, Joe, Ronak and I took part in a panel discussion. Lots of interesting questions asked by the audience!

Overall, this was a great workshop. Unlike a conference, all the talks seemed very relevant to my work (and others said that they felt the same way). The breaks between talks were long but filled with interesting conversations and it was a great opportunity to talk to others I had not met before but whose work I knew and to learn of others working in the field that I had not heard of. I hope we have another SpISA workshop in the future.