A prototype computer implemented in the project area of a Logic Engine. Consists of a processor, storage manager, and a dual ported memory organized to implement a data heap. All components except the system bus were derived using the DDD transformation system. The test system is a codesign environment in which the hardware can be tested against its own executable specification

purpose: research
dates: 1994-present
students: Bob Burger, B. Bose, M. Tuna, K. Rath, S. Pullela
engineering: Willie Hunt
faculty: S D Johnson
information: IUCS TR413 TR544

The Schemachine project is an ongoing study in formal methods for systems. It was implemented using the DDD transformation system from a virtual machine specif ication taken from the textbook Essentials of Programming Languages (Friedman , Wand and Haynes, McGraw-Hill, 1992). Part of the testing regime involves runni ng the specification model on a PC and comparing its behavior with the derived implementation. For example, the garbage collection component on the prototype w as tested by executing the Scheme model of the surrounding system with a softwar e interface to the hardware heap implementation. All the software for modeling, testing, and deriving the implementation is written in Scheme.

The technologies used in the prototype include standard DRAM memory SIMMs, PLD d evices (programmable logic arrays) and Actel FPGA devices (field programmable, non-reconfigurable gate arrays). The prototype's scale is around 8000 logic gates (a conventional measure not directly related to the hardware technology). In denser technologies, the prototype would easily fit into a single chip, although functionally it would make more sense to use three chips.

The detail at the right shows principal components of the prototype. The processor executes object code compiled from Scheme programs. The specification for this processor is a virtual machine extracted from a definitional interpreter in a systematic and rigorous fashion. The storage manager consists of three processes, a garbage collector that runs as a coroutine to the processor, an allocator that coordinates storage use and reclamation, and a "trailer" process that runs in parallel with the processor.

The storage manager and processor were formally derived in the DDD system and are correct with respect to their specification models (assuming DDD is correctly implemented. Testing of the realization has revealed no observed discrepancies.

The system bus is specially designed for a heap based mutator/collector system. It is a high performance bus, relative to the speed of its DRAM (dynamic random access memory technology), running the inner loop of the collector at about 160% of standard memory speed.

Further work on the prototype includes:

  1. Verifying system level properties; for example, proving that the collector and processor do no interfere with each other.
  2. Proving the system bus correct with an automatic tool, such as a model checker.
  3. Proving the algorithms from which the hardware is derived are correct.
  4. Revising the specification to conform more closely to rigorously developed compi ler descriptions
  5. Developing new transformations to make the derivation more automatic.
  6. Incorporating new architectural features.