Instruction sequences with indirect jumps

TL;DR

This paper analyzes instruction sequences with direct and various kinds of indirect jump instructions, defining their semantics via translation into sequences without indirect jumps and modeling their behavior through interaction with memory devices.

Contribution

It introduces formal semantics for different kinds of indirect jump instructions by translating them into direct jump sequences and models their execution behavior with memory interactions.

Findings

Semantic definitions for various indirect jump instructions

Translation methods from indirect to direct jump programs

Behavioral modeling via memory device interaction

Abstract

We study sequential programs that are instruction sequences with direct and indirect jump instructions. The intuition is that indirect jump instructions are jump instructions where the position of the instruction to jump to is the content of some memory cell. We consider several kinds of indirect jump instructions. For each kind, we define the meaning of programs with indirect jump instructions of that kind by means of a translation into programs without indirect jump instructions. For each kind, the intended behaviour of a program with indirect jump instructions of that kind under execution is the behaviour of the translated program under execution on interaction with some memory device.