Wolfram Kahl, Christopher K. Anand, Jacques Carette
pp. 147-160 in
I. Düntsch, W. McCaull, M. Winter (eds.)
8th International Conference on Relational Methods in Computer
Science (RelMiCS 8) and 3rd International Workshop on Applications
of Kleene Algebra, St. Catherines, Ontario, Canada, Feb. 22--26, 2005,
LNCS
3929, Springer-Verlag, 2006.
(.bib)
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.