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

Use the AAPCS32 convention: r0 holds the input address, r1 the length, and r0 receives the result. The following Thumb instruction set assembly language uses only scratch processor registers, so no callee-saved registers need saving. Assume the array is valid, halfword-aligned, and has nonnegative length; for the mathematical sum assume it fits a signed 32-bit two's complement integer.

.syntax unified
.thumb
.thumb_func
sum16:
    movs r2, #0             @ accumulated sum
    cmp  r1, #0
    ble  .Ldone             @ empty array; also returns 0 if n < 0
.Lloop:
    movs r3, #0             @ Thumb signed load needs a register offset
    ldrsh r3, [r0, r3]      @ signed halfword at a; offset read before r3 changes
    adds r2, r2, r3         @ include this signed value
    adds r0, r0, #2         @ advance by one short, not one byte
    subs r1, r1, #1         @ one fewer element remains
    bne  .Lloop
.Ldone:
    movs r0, r2             @ result register
    bx   lr                 @ leaf routine: lr was not overwritten

After

j

iterations, the loop invariant is that r2 contains the first

j

elements' sum, r0 points to element

j

, and r1 is

n - j

. The sign extension in ldrsh supplies the correct signed addend. One iteration preserves this loop invariant, and the decreasing remaining length proves algorithm termination. For the seven-element calls, the sum lies between

- 229376

and

229369

, so it fits. For longer arrays that overflow, these instructions compute the sum modulo

2^{32}

; that is not a claim about defined signed C programming language overflow behavior. The operand forms are those of the paper's reference sheet.^[ref]

b

 0  0

Solution

 0  0

Let the stored bits be

b_{15}, \dots, b_{0}

and let

s = b_{15}

. The sign extension performed by ldrsh keeps output bit

i

equal to

b_{i}

for

0 \leq i \leq 15

, and sets every output bit

16 \leq i \leq 31

s

. Thus a nonnegative halfword gets sixteen leading zero bits, while a negative halfword gets sixteen leading one bits.

Its signed 32-bit two's complement value is

- s 2^{31} + s \sum_{i = 16}^{30} 2^{i} + \sum_{i = 0}^{15} b_{i} 2^{i} = - s 2^{16} + s 2^{15} + \sum_{i = 0}^{14} b_{i} 2^{i} = - s 2^{15} + i = 0 \sum 14 b_{i} 2^{i} .

(1)

The last expression is exactly the original signed 16-bit value. The equality uses the finite geometric series

\sum_{i = 16}^{30} 2^{i} = 2^{31} - 2^{16}

. In particular, simply inserting zero bits would be wrong for a negative halfword: its unsigned interpretation differs from its signed value by

2^{16}

c

 0  0

Solution

 0  0

Keep total in the callee-saved register r4, and the first returned sum in the callee-saved register r5. Suppose the surrounding function has made an aligned stack frame with the local seven-halfword array at the current sp, occupying fourteen bytes in a sixteen-byte slot. One possible frame setup is push {r4,r5,r6,lr} followed by sub sp,sp,#16; the earlier code initializes total, regular, and special before this fragment.

    ldr  r0, =regular       @ assembler literal load of the global array address
    movs r1, #7
    bl   sum16
    movs r5, r0             @ first sum must survive the next call

    add  r0, sp, #0         @ current frame's local special array
    movs r1, #7
    bl   sum16
    muls r0, r5, r0         @ second sum times first sum
    adds r4, r4, r0         @ update total

The AAPCS32 permits each call to overwrite r0–r3, r12, and condition flags, but requires preservation of r4–r8, r10, r11, and sp. Thus both r4 and r5 remain valid even if sum16 is replaced by another conforming implementation. bl changes the link processor register lr, so the enclosing function saves its own return address in its prologue. Its epilogue can use add sp,sp,#16 and pop {r4,r5,r6,pc}. The frame uses thirty-two bytes in total, preserving the required eight-byte stack pointer alignment at both calls.^[ref]

The two calls may be evaluated in this order. Assume the product and final addition fit the signed 32-bit result expected by the source program; unlike each individual seven-element sum, their product need not fit. The assembly language operations retain their low 32 bits if this assumption fails, whereas signed integer overflow in the C programming language has different semantics.

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

a

Solution

b

Solution

c

Solution

 Ancestors (10)

 Discussion (0)

 Articles by others on the same topic (0)

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

 Discussion (0)  Subscribe (1)

 Discussion (0)