Control-flow semantics for assembly-level data-flow graphs

Abstract. As part of a larger project, we have built a declarative assembly language that enables us to specify multiple code paths to compute particular quantities, giving the instruction scheduler more flexibility in balancing execution resources for superscalar execution. Since the key design points for this language are to only describe data flow, have built-in facilities for redundancies, and still have code that looks like assembler, by virtue of consisting mainly of assembly instructions, we are basing the theoretical foundations on data-flow graph theory, and have to accommodate also relational aspects. Using functorial semantics into a Kleene category of “hyper-paths”, we formally capture the data-flow-with-choice aspects of this language and its implementation, providing also the framework for the necessary correctness proofs.