Book cover   SVA history and discussion, by Bill Roscoe

SVA, 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. 

An interesting research problem is comparing the effectiveness of the compression strategy uses with other approaches to model checking such as partial order methods.  When is each more effective: can using more than one such technique give extra advantage?  Is there a better compression strategy?

 SVA as presented here should be a good tool for teaching the issues of shared variable programming as well as analysing some  real programs.  It should also provide a core that can be built upon, for example in undergraduate and masters' projects.  We can imagine extending the input language with further features, both relating to general programming constructs and  communication.  Or the technology underlying SVA might be used to develop a corresponding tool for some real programming  language or a subset thereof. 

We hope you find it useful and enjoyable.

Added August 2014: The release of FDR3 meant that a new release of SVA was needed since its command-line functionality was not identical to that of FDR2.  The new version uses the API that is
present in FDR3.1 on. I was helped in this by Tom Gibson-Robinson. We have called this SVA2, but it is functionally almost identical to the original SVA.