Proof: Flexible Copy Example

Here we present a program and prove that it copies a set (or array) of numbers to a different location in memory. More precisely, we show that

Let's prove the following theorem:

if the following are true:

the PC at time 0 = 0
instruction #0 is load dst=7 addr=5 imm=0
instruction #1 is store src=7 addr=6 imm=0
instruction #2 is addi dst=5 src=5 imm=1
instruction #3 is addi dst=6 src=6 imm=1
instruction #4 is addi dst=4 src=4 imm=1
instruction #5 is beq left=3 right=4 imm=1
instruction #6 is jump imm=0
value of cell 3 at time 0 = 3
value of cell 4 at time 0 = 0
value of cell 5 at time 0 = 8
value of cell 6 at time 0 = 12
value of cell 8 at time 0 = 24
value of cell 9 at time 0 = 31
value of cell 10 at time 0 = 45

then value of cell 14 at time 20 = 45

Cell #3 specifies the number of values to copy. Cell #5 indicates where the source array begins. Cell #6 indicates where the destination array begins.

Together, these cells indicate that we want to copy cells 8, 9, and 10 to cells 12, 13, 14.

By specifying these parameters in memory, we don't have to change the instructions when we have a longer or shorter array or the array is in a different location. We can just update memory cells 3, 5, and 6.

Instructions

Memory Cells

Program Counter	Time
0	0

LW Computer Simulator

Instruction #0 copies cell #8 to cell #7. The source is the value stored in cell #5 (8) plus the imm (0).

Instruction #1 copies cell #7 to cell #12. The destination is the value stored in cell #6 (12) plus the imm (0).

Notice how the computer first copied cell #8 to #7, then again from #7 to #12. Cell #7 is a "work area" cell where the program temporarily stores the value before it is copied to the actual destination.

Why don't we just copy cell #8 directly to cell #12? We could do that with addi dst=12 src=8 imm=0, for example. But let's suppose that some time later, we want to copy values again, but the source the source starts somewhere else, say, cell #18. Then we need to change the ADDI instruction src to 18. But we prefer to keep the instructions the same, if possible, so that we can easily reuse them. For instance, the copy instrcutions might be part of a larger program that jumps to the copy instructions many times with different source arrays and/or destinations.

Then how about using a single LOAD instruction with dst=12? Then the source can change in memory, but the destination is still specified in the instruction, so the destination cannot change without changing the instruction. This is more flexible than ADDI, but not flexible enough.

Similarly, using a single STORE instruction means that the destination is flexible, but not the source.

Thus we use both LOAD and STORE instructions. Using LOAD allows the source to be specified in memory. The destination, cell #7, is in the instruction. Then, the STORE instruction uses cell #7 as the source. Using the STORE instruction allows the destination to be spcified in memory.

After a value is copied to the destination, we increment the source (cell #5) and destination (cell #6) by one, so that the next time the LOAD and STORE instructions run, the next value in the array (31) will be copied. We also increment the counter (#4) to remember how many values have been copied.

The BEQ instruction checks whether we've copied values enough times. If so, the program jumps to the end. If not, instruction #6 runs, and the computer jumps back to instruction #0. The result is a loop that copies 1 value at each iteration.

Proof:

View as a tree | View dependent proofs | Try proving it

Given

1	the PC at time 0 = 0
2	instruction #0 is `load dst=7 addr=5 imm=0`
3	instruction #1 is `store src=7 addr=6 imm=0`
4	instruction #2 is `addi dst=5 src=5 imm=1`
5	instruction #3 is `addi dst=6 src=6 imm=1`
6	instruction #4 is `addi dst=4 src=4 imm=1`
7	instruction #5 is `beq left=3 right=4 imm=1`
8	instruction #6 is `jump imm=0`
9	value of cell 3 at time 0 = 3
10	value of cell 4 at time 0 = 0
11	value of cell 5 at time 0 = 8
12	value of cell 6 at time 0 = 12
13	value of cell 8 at time 0 = 24
14	value of cell 9 at time 0 = 31
15	value of cell 10 at time 0 = 45

Proof Table

Comments

Please log in to add comments