Formal design techniques in the implementation of concurrency
Davis Shepherd · Formal Methods · 1991
Describes the design of the INMOS H-1 processor. This is a high performance implementation of the transputer currently under design. The H-1 will support a full implementation of OCCAM where communication with other processors is achieved by multiplexing messages from 'virtual channels' down the physical link channels. Such multiplexing is achieved through packetising the message and adding header information to indicate the ultimate destination of the packet. These packets are routed through a network by routing switches. Each packet is transmitted as a sequence of bytes with each byte being handshaken. On top of this byte level protocol is a packet level protocol which handshakes each packet across the network. >