I (CLJ) have done some work on embedding a specification of each Transputer instruction in the Transterpreter source code. This is is mostly to serve my own needs at this stage (thesis), but could be useful in general. A branch of the TVM currently contains sourcecode which is marked up using something which is easy to parse, where the most interesting bit is perhaps the statetransition diagrams which I have included. These are not a formal spec, but should give an idea of how each instruction changes the state of the virtual machine.

A natural extension of this is the specification of the instructions in a formal notation (Z, B, ...). This would be a lot more work, and the current effort tries to present the currently executable specification of the Transterpreter/Transputer/occam-pi VM which can be used and understood by others.

Since it does not look like it is possible to upload attachments to this wiki, i have put a sample (primary instructions) up: vmdef.pdf. This is generated from the Transterpreter source code and renders the little state transition language into prettyish little diagrams.

An instruction might look like this (vmdef.pdf page: 12 logical - 14 physical):

/* 0xE_ - stnl - store non-local */

/** DESCRIPTION
 *
 * This instruction stores a value into a slot addressed by using the A
 * register as a base and the operand register as an offset. The value which is
 * to be stored in memory is located in the B register.
 */

/** STATE
 * (assumes (= (|| areg byteselectmask) 0))
 * (areg (in (str base)) (out creg))
 * (breg (in (str value)) (out undefined))
 * (creg (out undefined))
 * (oreg (in (str offset)) (out 0))
 * (iptr (out nextinst))
 * (mem (out (writemem (+wordsize areg oreg) breg)))
 */

void ins_stnl()
{
  /* Put value in breg into mem(areg + oreg) */
  write_mem(pooter_plus((POOTER)areg, oreg), breg);

  /* Pop the stack */
  STACK(creg, UNDEFINE(breg), UNDEFINE(creg));

  CLEAR(oreg);
}

ExtractingTransterpreterAnnotations (last edited 2006-10-03 19:20:40 by clj3)