Semantics Club 27 04 2001
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  and  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.
 R. Stata, M. Abadi: A type system for Java bytecode subroutines. POPL'98
 S. Katsumata, A. Ohori: Proof-directed de-compilation of low-level code. ESOP'01