SVA
history and
discussion, by Bill
RoscoeSVA, or Shared Variable Analyser, has its origins in my desire to explain shared variable concurrency to Oxford undergraduates who had already learned CSP. The question at the start of Chapter 18 of UCS about Hyman's and Peterson's algorithms was asked every year as a tutorial exercise to second-year students. It was obvious that one could create CSP models of these programs and check on FDR whether they did in fact achieve mutual exclusion. These would be based on Hoare's concept of running parallel processes representing variables with other processes representing the control state of the threads.
It rapidly became apparent that one could, in fact, translate any program in a simple shared variable language in this way. I therefore wrote a "compiler" to do this. The most obvious form of such a compiler would have been a program written in a third language that input code written in something like SVL and output code in CSPM that could be run through FDR. Instead, as a demonstration of the power of the functional sublanguage of CSPM, I wrote the compiler in CSPM itself. The lack of conventional input, output and string functionality in CSPM meant that the obvious model would not work. My original compiler's "input" was a pre-parsed program from a subset of SVL (which, in the absence of a parser, meant programming in a CSPM data type). Instead of outputting the CSP translation of the SVL, one would run the program-plus-compiler on FDR, creating a CSP simulation of the object program. This work was reported in a 2001 paper.
It proved an effective tool for me to use, but the input language peculiarities were always likely to put off others.
David Hopkins took on the task of making SVA usable for his 2006/7 third-year undergraduate project. He created the GUI and counter-example analyser much as you see them now, together with an ASCII form of SVL which would parse naturally to the input language of the original compiler. The project also involved experimenting with priority and a fore-runner of the Overseers described in Section 19.5, as well as an approximation to the general proof of the bakery algorithm now given in Chapter 19. This work was reported in a short paper.
I had originally intended to write a chapter of UCS about the version of SVA resulting from Hopkins's project, but a desire to tidy up the code quickly led to more. During a sabbatical visit to Adelaide in December 2008 and January 2009, and subsequently back in Oxford, I re-wrote just about the whole compiler and added substantial extra functionality. The most obvious additions are proper arrays, the use of compression, dirty variables as described in Section 19.1, and the support for checking refinement between program fragments. So now, of course, there are two chapters.
The use of compression, in particular, transforms the effectiveness of SVA since on many problems it reduces the state space by several orders of magnitude. This is the most general class of examples I have found for FDR where compression just about always produces excellent results. I believe that this approach makes SVA highly competitive with other analysis tools for reasoning about the limit syntax that it presently supports.