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 2026-10-25
View more
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 iterations, the loop invariant is that r2 contains the first elements' sum, r0 points to element , and r1 is . 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 and , so it fits. For longer arrays that overflow, these instructions compute the sum modulo ; 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]
Read the full article
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 / b / Solution 2026-10-25
View more
Let the stored bits be and let . The sign extension performed by ldrsh keeps output bit equal to for , and sets every output bit to . 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
(1)
The last expression is exactly the original signed 16-bit value. The equality uses the finite geometric series . In particular, simply inserting zero bits would be wrong for a negative halfword: its unsigned interpretation differs from its signed value by .
Read the full article