Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 1 / c

Use byte addresses, so adjacent 32-bit array elements are four bytes apart. The following MIPS instructions include harmless sll $zero,$zero,0 instructions in every branch delay slot; the second load is followed by another independent instruction before its value is consumed, also accommodating an early MIPS architecture with a load-use delay. All mnemonics here denote individual machine instructions.

        beq   $t3,$zero,done  # n=0: do not access any array
        sll   $zero,$zero,0
loop:
        lw    $t4,0($t0)      # current a element
        lw    $t5,0($t1)      # current b element
        addiu $t0,$t0,4       # advance a; also separates lw from its use
        subu  $t6,$t4,$t5     # current difference, modulo 2^32
        sw    $t6,0($t2)      # store current c element
        addiu $t1,$t1,4
        addiu $t2,$t2,4
        addiu $t3,$t3,-1      # one fewer element remains
        bne   $t3,$zero,loop
        sll   $zero,$zero,0
done:

A loop invariant at the head of the loop, after

k

completed iterations, is that the three addresses point to elements

k

, the count is

n - k

, and every output element before

k

equals the corresponding difference. One iteration reads element

k

, stores its difference and advances to

k + 1

, preserving the loop invariant. The remaining count is a nonnegative loop variant decreasing by one, so the loop ends with

k = n

The code uses subu to avoid signed-overflow traps: the suffix does not restrict the operands to unsigned values. Its precise result is

c_{i} \equiv a_{i} - b_{i} (mod 2^{32}) (0 \leq i < n) .

(1)

For representable signed differences this is exactly

c_{i} = a_{i} - b_{i}

. If trapping signed arithmetic is required instead, use sub and assume all differences are representable. The arrays must occupy valid word-aligned storage with no address wrap; the usual separate output array avoids overwriting unread inputs.

ii

 0  0

Solution

 0  0

Make the code a leaf procedure called array_diff, copy the four argument processor registers into the temporaries used above, and replace the final label by a return. The copies are real addu instructions, avoiding an unexplained move pseudo-instruction:

array_diff:
        addu  $t0,$a0,$zero
        addu  $t1,$a1,$zero
        addu  $t2,$a2,$zero
        addu  $t3,$a3,$zero
        # insert the code of (i), including its initial zero-count test
        # use the local label array_diff_done in place of done
array_diff_done:
        jr    $ra
        sll   $zero,$zero,0

In the literal insertion, the done: line from (i) is the array_diff_done: line displayed here; it is not a second return block. Under the usual calling convention, temporary processor registers are caller-saved. This procedure calls no other procedure and changes no saved processor registers, so it needs no stack frame or saved return address.

For a 32-bit constant

K

, define

H_{K} = ⌊ K / 2^{16} ⌋

and

L_{K} = K mod 2^{16}

using its unsigned binary representation. Load it with lui followed by ori; both are single MIPS instructions. For base addresses

A, B, C

and count

N

, the main program is:

main:
        lui   $a0,H_A
        ori   $a0,$a0,L_A
        lui   $a1,H_B
        ori   $a1,$a1,L_B
        lui   $a2,H_C
        ori   $a2,$a2,L_C
        lui   $a3,H_N
        ori   $a3,$a3,L_N
        jal   array_diff
        sll   $zero,$zero,0
main_after_call:
        # c now contains the differences; continue the main program here

Here each H_... and L_... is an assembler-time numeric constant, not an executed operation. lui places the high half and clears the low half; ori inserts the low half without sign extension. Thus

(H_{K} ≪ 16) OR L_{K} = K .

(1)

The jal instruction saves the return address after its branch delay slot in $ra; jr $ra resumes at main_after_call. A main routine that itself needs to return to a caller must save its incoming $ra before jal and restore it afterwards.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 1 / c

i

Solution

ii

Solution

 Ancestors (11)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Digital systems, linear algebra, introduction to formal proof / 1 / c

i

Solution

ii

Solution

 Ancestors (11)

 Discussion (0)  Subscribe (1) New discussion

 Articles by others on the same topic (0)

 Discussion (0) New discussion