Practical Experiences Constructing Working Virtual Machines

The Instruction Set Architecture (ISA) of a computing machine is the definition of the binary instructions, registers, and memory space visible to an executing program. Despite there being many ISAs in existence, all share a set of core properties which have been tailored to their particular applications. An abstract model may capture these generic properties and be subsequently rened to a particular machine: this is a task to which the Event-B formal notation is well suited. The motivation for the work is the systematic specication of the ISA’s behavior for all possible instruction sequences loaded into the machine, whether part of a correct program or an erroneous one. The constructed model consists of two parts: a generic description of properties common to most ISAs, and renement to particular ISAs. The generic part is incrementally constructed from a very trivial initial model, and the second part constructs a particular ISA from this. The complete renement process is demonstrated by the creation and testing of Virtual Machines automatically generated as C source code via a translation tool, which was developed as part of the project. The technique is demonstrated by refinement to the MIDAS (Microprocessor Instruction and Data Abstraction System) ISA specification. MIDAS is a specication capable of executing binary images compiled from the C language. It is intended to be representative of typical microprocessor ISAs, but using a minimal number of dened instructions in order to make a complete renement practical. There are two variants: a stack-based machine and a randomly accessible register array machine. The two variants employ the same instruction codes, the differences being limited to register file behavior. Compiler tool chains for each variant have been developed. Some numbers: the MIDAS ISAs have thirty four instructions; their complete renements consist of over thirty steps, expanding a single initial event to over one hundred for each variant. This process involves the discharging of nearly ve thousand proof obligations. Automatic translation yields over four thousand lines of C source code for each variant. This presentation will give an overview of the MIDAS project as an example of a model renement of sucient scale, depth and detail to be suitable for automatic translation into a usable executable. The place of Event-B model construction within a wider development process is described. Various scaling issues are discussed, including editing and manipulation of Event-B notation via the user interface, discharging of the vast number of proof obligations, and the practical limits of Rodin as an Eclipse/Java platform. The modeling techniques used to mitigate some of these scaling issues are described, and promising emerging or proposed Event-B features highlighted. Suggestions for possible future enhancements are made.