Semantics Club 27 04 2001

Type systems for explicit forwarding

Lennart Beringer

Abstract

I will talk about an approach for reasoning about the flow of operands in processors with register-bypassing. In these architectures, instructions forward operands through queues instead of writing them to registers.
I will consider a small assembly language where the decision how the queues are used is made at compile time (explicit forwarding). Aiming at analysing the forwarding behaviour by type-checking, I will describe two simple SOS models of execution. These correspond to the sequential instruction set architecture (ISA) definition of a processor and distributed execution in a super-scalar implementation.
Using a notation based on linear logic, types describe the effect of instruction execution on operand queue configurations. By proving the type systems sound for the execution models, we eliminate various run-time hazards such as operand queue mismatch, lack of operands, non-determinism and deadlock.
The types are in effect similar to those used in [1] and [2] for reasoning about the JVM operand stack, abstracting from the order of operands. Time permitting I will expand on this similarity and talk about a resulting translation from JVM code into our language.

[1] R. Stata, M. Abadi: A type system for Java bytecode subroutines. POPL'98
[2] S. Katsumata, A. Ohori: Proof-directed de-compilation of low-level code. ESOP'01