Classic CSP is a “model without time” and yet contains time sequence and even a “time-out” or “sliding choice” operator (Roscoe, The Theory and Practice of Concurrency, 2005, p 80). The static occam language and the Transputer processor, both based on finite CSP, have time and other structure that make them a deliberate refinement of classic CSP; but occam is imperative and capable of doing completely general computing tasks. Programs written in occam and run on the Transputer can be proven correct and their behavior characterised down to cycle count. Classic CSP process descriptions of these same programs can also be investigated and proven using CSP techniques, including hiding.

This Fringe presentation, the first of a pair (see “Mathematical Ground Truth”), will introduce these two approaches, using calculated assembly-code response of two-priority T2, T4, or T8 Transputers. We will begin with the n-process rawFIFO and the two-process store/shelf FIFO detailed in author Dickson's book Crawl-Space Computing, p 111–120, using variable timing patterns for external communication. The true timing will be used to make sense of the abstract model of CSP in the real world, with and without hiding of internal channels.

The purpose of the investigation is to illuminate how rigorous conclusions can be drawn with a combination of CSP, occam-to-occam mappings, timing and sequence requirements. As time permits, we will expand the conclusions reached to IoT designs capable of serving multiple external communications and doing content calculations, treated as low-priority, time-consuming and nondeterministic.