Bob Reversible ISA - Semantic

The semantics of Bob amounts to what we can do with instructions, and how the given model behaves.

The model

After executing an instruction we update the model = (pc,br,dir) as thus

# model update
if dir = 0 then
    if br = 0 then pc := pc + 1
    else pc := pc + br
else
    if br = 0 then pc := pc - 1
    else pc := pc - br

The model is not reset after updated. For example the br register needs be reset if a jump has been performed. Or else the program counter will jump ahead resulting in undefined behavior. This is often done placing a branch right at the target of a given jump. For example

label0:
    BRA     label1
    #some code
label1:
    BRA     label0
    # more code

The internal stack

Besides the memory that is visible to the programmer, an internal stack is maintained. This stack is not visible to the programmer. Each frame is a list of keys and values. Thus a key can be present several times with different values. In this version of Bob the internal stack is only used for storing arguments when doing CALL or RCALL.

Instructions

In general all instructions must have an inverse. Some instructions, like multiplication, takes 3 arguments, a destination and two source registers, where the result of evaluating the instruction on the two source registers is XOR'ed into the destination register. Such instructions are self-inverse since they essentially are a XOR instruction. All branch instructions are self-inverse since the way they modify state is automatically inverted in backward execution as of the model described above.

The types of arguments are as thus:

Register are prefixed with $, for example $reg1
Immediate values are just integers, for example 123
Memory references are in [], for example [mem_a]
Variable types are prefixed with # followed by the allowed types, for example #reg,mem

SWAP

The swap instruction swaps the values of two registers. The inverse of SWAP is itself, that is it is self inverse.

SWAP $reg1 $reg2

ADD

The add instruction adds the values of two registers and stores the result in the first. The inverse of ADD is SUB.

ADD $dest $source

ADD1

The add1 instruction adds 1 to the destination register. It has SUB1 as inverse.

ADD1 $dest

SUB

Subtracts the values of the two registers. The inverse is ADD.

SUB $dest $source

SUB1

Subtracts one from destination register. The inverse is ADD1.

SUB1 $dest

MUL

Multiply the two source registers and XOR the result into the destination register. This instruction is self-inverse.

MUL $dest $s1 $s2

MUL2

Multiplies the destination register with 2. The inverse is DIV2.

MUL2 $dest

DIV

Divides the two source registers and XOR the result into the destination register. This instruction is self-inverse.

DIV $dest $s1 $s2

DIV2

Divides the source with 2. The inverse is MUL2.

DIV2 $dest

NEG

Stores 0 minus the value of the destination register in the destination register. This is the same as the additive inverse on integers. This instruction is self-inverse.

NEG $dest

MOD

XOR the result of $s1 modulo $s2 into the destination register. This instruction is self-inverse.

MOD $dest $s1 $s2

XOR

XOR the value of the source register into the destination register. This instruction is self-inverse.

XOR $dest $source

XORI

As with XOR, though the source here is an integer. This instruction is self-inverse. It is quite central as it is the only way to move integers into register.

XORI $dest 1234

AND

Bit wise ∧s the two source registers and stores the result in the destination register. This instructions is self inverse.

AND $dest $s1 $s2

OR

Bit wise ∨s the two source registers and stores the result in the destination register. Self-inverse.

OR $dest $s1 $s2

EXCH

Exchanges the value of the register given as the first argument with what resides at the memory location of the value of register given as second argument. This instruction is self-inverse. It is the only way to directly move values in and out of memory.

EXCH $reg1 $reg2

PUSH

Adds 1 to $spointer. Then exchanges the value of given register into what resides at $spointer in memory. This instruction has POP as inverse. This is essentially a x86 push, though it exchanges values instead of moving them.

PUSH $reg1

POP

Exchanges the value of given register into what resides at $spointer in memory. Then subtracts 1 from $spointer. This instruction has PUSH as inverse. This is essentially a x86 pop, though it exchanges values instead of moving them.

POP $reg1

CALL

First of all the br register is calculated based on the target label. Then one of two things can happen:

If br != 0, what resides in register $arg0 ... $arg3 is pushed onto the internal stack, and the first 4 elements of the list given as second argument is placed in registers $arg0 ... $arg3. If less than 4 arguments are given, 0 is placed in the respective register. If more than 4 are given, the rest is ignored.
Else the internal stack is popped, and each value is reinserted into their respective registers. Note that br == 0 implies that the br register has been reset, and thus we are returning from a call.

This instruction is self-inverse.

CALL label ($reg1,...)

RCALL

Almost the same as CALL. This instruction differs in that the dir register is set to 1, and that the br register is set to 0 - calculated_br. The execution details of this instruction are opposite of the semantics of the model: we want to make a jump and then invert the dir register. But in our model the position tuple is updated after executing a given instruction. To overcome for this we use the additive inverse of the calculated br register. Self-inverse.

RCALL label ($reg1,...)

SWBR

Exchanges the value of the br register with given register. Self-inverse.

SWBR $reg1

SWRET

Exact same as SWBR. This had been included in order to give a more informative name. It is often used when constructing procedures.

SWRET $reg1

BRA

With this instruction and unconditional jump to the given label is made.

BRA label

RBRA

The same as BRA, though after instruction execution the dir register is inverted. This is done in the way described for RCALL.

RBRA label

BZ

Branch on equal to 0.

BZ #reg,mem label

BNZ

Branch on not equal to 0.

BNZ #reg,mem label

BEQ

Branch on equal.

BEQ #reg,mem #reg,mem label

BNEQ

Branch on not equal.

BNEQ #reg,mem #reg,mem label

BGT

Branch on greater than.

BGT #reg,mem #reg,mem label

BGEQ

Branch on greater than or equal to.

BGEQ #reg,mem #reg,mem label

BLT

Branch on less than.

BLT #reg,mem #reg,mem label

BLEQ

Branch on less than or equal to.

BLEQ #reg,mem #reg,mem label

STOP

Stop execution. This instruction results in a success on status.

STOP

NOP

Similar to the x86 instruction of the same name. It does nothing, execution just passes on according to the position.

NOP

Compound code translation

For compound code we use a set of templates. The CALL, RCALL and the SWRET is made as to accommodate these templates.

Procedures

These are constructed as thus

# template for procedure
proc_top:
    BRA     proc_bot
    POP     $raddr
proc:
    SWRET   $raddr
    NEG     $raddr
    PUSH    $raddr
    # procedure code
proc_bot:
    BRA     proc_top

As can be seen: every time we jump to some label, we need to reset the br register. Or else we keep jumping resulting in undefined behavior. The return address resides in $raddr - this is pushed right ahead accommodating for possible recursion.

Conditional statements

Figure 1: Flowchart of reversible if-conditions

Reversible statements needs an exit condition so we in case of backwards execution can decide path taken. This condition is called fi. This is illustrated in Figure 1.

The template for a conditional statement is as thus


if_top:
    BGEZ    $if if_else
    #code for then
if_then:
    BRA     if_bot
if_else:
    BRA     if_top
    # code for else
if_bot:
    BGEZ    $fi if_then

In the code the first condition is inverted, that is if the value of $if is less than 0, then do the then branch.

Loops

Figure 2: Flowchart of reversible for-loop

As with conditional statements loops need an exit condition. This is illustrated in Figure 2.


loop_top:
    BGEZ    $entry loop
    # code for do
loop_do:
    BLZ     $exit loop_bot
    # code for loop
loop:
    BRA     loop_top
loop_bot:
    BRA     loop_do

Again the top branch checking entry is inverted.

Compare Operators

If we need to evaluate a compare operator (⊕ = [ >,<,≥≤,=,≠ ]), we can do so as illustrated in Figure 3. This results in the following code where we need to zero-clear the registers we have used.


c_top_pre:
    BGT     $r1 $r2 c_true_pre
c_false_pre:
    BRA     c_bot_pre
c_true_pre:
    BRA     c_top_pre
    XORI    $res 1
c_bot_pre:
    BLE     $r1 $r2 c_false_pre

# Code that can use $res in condition

c_bot_post:
    BLE     $r1 $r2 c_false_pre
c_true_post:
    BRA     c_top_pre
    XORI    $res 1
c_false_post:
    BRA     c_bot_pre
c_top_post:
    BGT     $r1 $r2 c_true_pre

Here post-code is in order to zero-clear registers after use.

Semantics