A Formal Semantics of Exposed Datapath Architectures with Buffered Processing Units

Synchronous control asynchronous dataflow (SCAD) architectures are a new kind of exposed datapath processor architectures which reveal all of their processing units (PU) and datapaths to the compiler to increase the use of instruction-level parallelism (ILP). They employ FIFO buffers at the input and output ports of their PUs, consuming operands and producing results similar to dataflow computers. Because the arrival of operands triggers the execution of instructions, SCAD architectures only need a single type of instruction that transports data from output buffers to input buffers. Among other advantages, this allows a simple integration of application-specific PUs, since a PU may implement in principle any function that can be realized with reasonable hardware without changing the instruction set. However, simply allowing any computable function for PUs introduces problems: Because of the asynchronous nature of data moves and operation execution, not all functions yield scheduling-independent, deterministic results. In this paper, we therefore first describe an operational semantics for SCAD architectures which enables formal reasoning about the underlying model of computation. Then, we create an equivalent model using well-known dataflow process networks. From this model, the desired restrictions for functions can then be derived, giving a configurable and sound class of SCAD architectures. Finally, we discuss further restrictions that should be applied and propose a notion for well-structured SCAD machine code.