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 [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