Principal investigator: Steven D. Johnson , Indiana University
An HTML version of this white paper can be found at http://www.cs.indiana.edu/hmg/schemachine-wp.htm
A very rough draft of a project description can be found at http://www.cs.indiana.edu/hmg/schemachine.ps.Z
Under MIPS funding we developed the Digital Design Derivation system to mechanize the transformation of functional specifications into stream networks from which hardware is synthesized. The Scheme programming language has served as the executable formal language on which this design algebra is performed, as well as for implementing DDD. In keeping with the style of research from which this work evolved, one of our continuing case studies has been the derivation of a hardware system for executing compiled Scheme. We have completed a working prototype that includes a high performance storage reclamation system for a standard Scheme heap and the hardware realization (excluding floating point) of a byte-code interpreter for compiled Scheme.
Four of the five major components of this system were derived using DDD. However, a number of outstanding verification problems remain to be solved before the entire system could be called formally correct. Completion of this work is the focus of the proposed project. There are four tactical goals in verification: proving of coherence and noninterference among the major components, verifying the manually designed memory interface, and a correlating two levels of timing. When completed, this will be the most advanced case study yet in formal system specification and verification.
Within the scope of MIPS/DA, this case study advances formal methods as applied to higher levels of system design. It is a coherent---albeit still academic---problem linking the highest levels of abstraction (a mathematical language specification) to realistic hardware architecture. From this perspective, the most important results of the work are the insights it contributes to conceptual aspects of system design. Continued implementation of the formalism, through DDD, results in a reasoning tool that addresses higher levels of specification than are presently seen in practice. We believe this work will help light the way for the next generation of design automation for systems.
There are also two strategic goals in methodology: linking this prototype with the VLISP compiler derivation for Scheme (( Lisp and Symbolic Computation 8(1/2), March 1995) and redirecting the derivation toward a Java implementation.
The roots of line of research lie in the programming methodology espoused in the text books Scheme and the Art of Programming and Essentials of Programming Languages . The prototype's CPU specification comes straight from Chapter 12 of "EoPL", making it a first cousin, though the influence of Mitchell Wand, of VLISP's virtual machine. Within the scope of CCR, we believe that a coherent notion of "programming" must demonstrably transcend distinctions of hardware and software, This need is manifesting itself now in network programming, distributed and embedded software, and co-design. Thus, while a compiler derivation such as VLISP demonstrates the depth of the methodology our redirection from native-code target machine to dedicated hardware contributes to demonstrating its breadth.
This project is on the frontier of formal-methods experimentation in system design. It has already produced potentially useful artifacts. Although the components of our Scheme machine are not as complex as their commercial counterparts, the system-level verification problems are realistic. Furthermore, the CPU and the self-managing heap are viable for embedded, design-critical applications, especially when coupled with the rigorously developed VLISP Scheme compiler.
Application of these tools and techniques to the Java virtual machine is quite possible. We are particularly interested in the partitioning problem raised by JavaVM's object manipulation instructions, which define the boundary between a hardware core and the network system in which it is embedded. We do not know whether transformations now supported by the DDD system can tackle this decomposition or not, but it exemplifies the level of system design that we want to address in our research.
We have designed a three-year project involving two research assistants, a .25FTE electrical engineer, and six months of summer support for the PI. Although the necessary instrumentation is in place for the continuing prototyping effort, workstation upgrades must be scheduled to maintain the research environment.
If commercial interest arises for the products of this research, collaboration could be arranged with a start-up company of graduates in design derivation research having expertise in the formal reasoning tools and experience in the case study.