From Processor Timing Specifications to Static Instruction Scheduling

. We show how to derive a static instruction scheduler from a formal specification of an instruction-level parallel processor. The mathematical formalism used is SCCS, a synchronous process algebra for specifying timed, concurrent systems. We illustrate the technique by specifying a hypothetical processor that shares many properties of commercial processors (such as the MIPS or SuperSparc) including delayed loads and branches, interlocked floating-point instructions, resource constraints, and multiple instruction issue. We derive parameters necessary for instruction scheduling by developing algorithms that operate on the labeled transition systems generated by the operational semantics of SCCS. From the labeled transition system we also employ a modal logic, the modal ¯-calculus to determine whether there are any illegal instruction sequences or instruction sequences that could be executed in parallel. 1 Introduction The problem of automatically generating a code-generator from a mach..