Topics (384k) Articles (398k) Users (410) Discussions (242) Comments (383) Files (13k) New article
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 4 a Solution by
Codex 0 2026-10-25
Subtract the first vertex from the other two, giving side vectors and . Their determinant is , the signed area of the corresponding parallelogram. The triangle occupies half that area, hence its area is . Taking the absolute value would remove any sign change caused by reversing the vertex order. This is the determinant formula for triangle area.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 3 e Solution by
Codex 0 2026-10-25
Let be the input sampled at clock edge . The desired registered output after that edge is . Only the last two high samples matter: a longer high run still has two high samples immediately before its first low sample.
A direct synchronous 110 detector uses three D flip-flops, holding , with a common clock and initial state zero. Use the following next-state equations, all evaluated from the old state and the input at the active clock edge:After an edge, records the latest sample and records whether the latest two samples were high. The final equation consequently produces the required pulse from the preceding two-high state and the new low sample. A synchronous reset sets all three state bits to zero. The output is the stored
z flip-flop value, so it changes only after clock edges; exposing the unregistered expression would let input transitions between edges alter the output.Original sampled-input and registered-output trace for a synchronous 110 detector
. Details. An equivalent finite-state machine has states
R (no current high run), H (one high), HH (at least two highs), and P (the pulse state). Its output is one only in P:The pulse cannot last two cycles: after the low input that creates it, is zero, so the next output is zero regardless of the next input. The detector rearms without a global stop and handles repeated patterns indefinitely. The three-flip-flop construction is deliberately direct; minimum storage was not required.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 3 d Solution by
Codex 0 2026-10-25
The modified output isFor example, gives and . Neither original series branch is complete, but the new connection supplies the cross-route through the transistors controlled by . Interchanging those roles gives the other cross-route example. In fact , so the modified circuit has added exactly those two possible lower conduction routes.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 3 c Solution by
Codex 0 2026-10-25
Joining the two middle nodes makes the upper lower-network transistors, controlled by , parallel with each other. The lower transistors, controlled by , are also parallel. These two parallel groups are in series, so the lower conducting condition becomes .
Its dual upper network must be two parallel branches, one containing the series PMOS transistor pair , the other the series pair . This is the right panel of the original drawing. Its condition is . Merely leaving the old upper network unchanged would break CMOS complementarity for some inputs, allowing a supply short rather than defining the required logic.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 3 b Solution by
Codex 0 2026-10-25
The lower network pulls the output low exactly when either series branch conducts. Therefore the Boolean function isThe inversion is important: describes connection to the low rail, not a high output. The pull-up network found in part a implements the complementary high condition.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 3 a Solution by
Codex 0 2026-10-25
The two lower conducting branches are the series pairs controlled by and by . Their overall NMOS transistor conduction condition is . Apply complementary CMOS network duality: the upper network has the parallel pair of PMOS transistors controlled by , in series with the parallel pair controlled by . Its first end connects to the high rail, its last end connects to , and the junction between the two pairs is internal to the upper network.
Original completed pull-up networks derived by complementary CMOS network duality
. Details. The left panel gives that completion. Every upper transistor uses its correspondingly named input and conducts when that input is low. Its conducting condition is , exactly the complement of the lower condition. Thus the ideal static circuit connects the output to one supply rail for every stable binary input.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 2 c Solution by
Codex 0 2026-10-25
Safety: only the driver accesses the sensor, and
active identifies at most one conversion. Accepted requests are serialized by the FIFO queue. The reply destination and token identify the owner of the resulting sample; no caller can clear another conversion's ready flag or consume another result. Receiving new requests while busy only changes the queue, not the active measurement. These are mutual exclusion and request/result association properties, not timing guesses.Progress: assume each started conversion completes in finite time, the corresponding notification is eventually delivered, the driver and compliant clients are eventually scheduled, and pending message acceptance is fair. A caller remains ready to receive its reply. Every accepted request has finitely many earlier requests in the queue, and later arrivals cannot overtake it. Each earlier request is completed and removed in finite time, so the caller eventually becomes active and receives its own reading. Fair acceptance extends this argument from accepted requests to callers waiting to submit one.
These assumptions are necessary for starvation freedom. A failed sensor, a client that disappears before accepting a synchronous reply, or an unfair scheduler can prevent progress; serialization alone cannot prove otherwise. Under the stated operating model, simultaneous calls are safe and every call completes. A single shared “latest temperature” variable would not establish either a fresh conversion per call or correct reply ownership.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 2 b Solution by
Codex 0 2026-10-25
Provide a blocking request-reply sensor conversion operation, using synchronous send-and-receive when the system supplies it:
get_temp():
token := a new token for this process's call
reply := request-and-wait(
destination = temperature_driver,
message = REQUEST(self, token),
expected_reply = RESULT(token, value))
return reply.valueHere
request-and-wait means sending the request and remaining ready to accept its matching response; it denotes a protocol action, not a claimed library symbol. Separate blocking send and receive operations are also adequate if they preserve the sender identity and the reply cannot be lost between them. With a synchronous reply, the driver simply waits until this client's receive is ready.The call returns only after the driver has selected this request, issued
TEMP_START, observed completion, read the new value and replied with the matching token. Each call therefore starts its own fresh conversion and returns its own result. It never returns a cached sample or another caller's reply. Local request and response storage belong to the calling process and are not a shared global message buffer. Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 2 a Solution by
Codex 0 2026-10-25
Give the hardware to a single device driver process. Other processes request a conversion through message passing and never touch its memory-mapped input-output registers. The following is protocol pseudocode for Phōs: its operation names specify their required semantics, rather than asserting an unverified spelling of a particular 2019 C interface. The hardware actions and the request/reply design are fully specified.
Use a FIFO queue of accepted requests, each containing its sender and a per-call token. Bind the device's interrupt to a persistent notification addressed to the driver before any conversion is started. A notification must remain pending if it arrives before the driver next waits; this is the lost-wakeup avoidance requirement. The driver receives both client requests and interrupt notifications in its event loop.
configure sensor and connect its interrupt notification to this process
TEMP_DATARDY := 0
clear stale pending interrupt notification
enable sensor interrupt and interrupt-controller delivery
pending := empty FIFO
active := none
forever:
if active is none and pending is not empty:
active := remove oldest request from pending
TEMP_DATARDY := 0
clear stale pending interrupt notification
TEMP_START := 1
event := wait for a request or persistent interrupt notification
if event is REQUEST(sender, token):
append (sender, token) to pending
if event is sensor interrupt and active is not none:
if TEMP_DATARDY != 0:
value := TEMP_TEMP
TEMP_DATARDY := 0
acknowledge the interrupt through the OS interrupt mechanism
send RESULT(active.token, value) to active.sender
active := noneAfter receiving an idle-time request, the next loop iteration starts its conversion before waiting again. While a conversion is in progress, additional requests join the queue without starting another conversion. A completed reading is copied before its ready flag is cleared, and the next request cannot start until the current result has been delivered. Spurious or stale notifications do not complete a request unless the device's ready register confirms completion.
Clearing old status and notification precedes
TEMP_START; doing so afterwards could erase a very fast completion. The operating system interrupt binding and persistent notification cover completion in the interval between starting the device and entering the wait. Register accesses must use the platform's device-access semantics, including required volatile-qualified objects in C or ordering primitives. Exact initialization and interrupt-connection call names remain an implementation binding, not invented Phōs API calls. The later teaching site's named system is documented separately; it is not used as proof of an identical historical API.[ref]Digital Systems course archive of the University of Oxford. 2018–2019 course record and linked teaching-site description of process/message-based device drivers
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 1 d Solution by
Codex 0 2026-10-25
Let the new byte table store and, for , . Thus it stores the number of leading zeros in an eight-bit argument: , , and . All entries fit in one byte.
countlz:
adr r3, lzbyte
movs r1, #0
lsrs r2, r0, #24
bne lz_found
movs r1, #8
lsrs r2, r0, #16
bne lz_found
movs r1, #16
lsrs r2, r0, #8
bne lz_found
movs r1, #24
movs r2, r0
lz_found:
ldrb r2, [r3, r2]
adds r0, r1, r2
bx lrThe high byte is tried first. A failed test proves that byte was zero, so the next right-shifted value is again a byte-sized index without masking: all higher bytes have already been proved zero. The offset in
r1 counts those skipped zero bytes in bits. Adding the table result for the first nonzero byte gives the leading-zero count. If every byte is zero, the last lookup contributes eight to the offset 24, giving 32. The example with high byte one gives 7. At most three conditional branches and one table read are needed; no per-bit loop is used. Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 1 c Solution by
Codex 0 2026-10-25
Count executed instructions, excluding the caller's branch-with-link and assuming the register-return and stack instructions shown above. The shift loop executes six instructions per iteration, plus four entry instructions and three exit instructions: instructions. The unrolled table subroutine executes 21 instructions, including four byte loads.
If every instruction, including a table load and a branch, costs one time unit, the ratio is in favour of the table version. A more informative simple model assigns cost to each table load and unit cost to the other displayed instructions: its cost is , versus 199 for the loop under the same unit branch assumption. Thus this model favours lookup when .
Real running time depends on the processor and memory system. Taken branches can incur extra instruction-fetch or pipeline costs, favouring the unrolled version; slow flash or cache miss events on the 256-byte table can erode that advantage. Instruction and table placement also matter. These assumptions prevent instruction counts from becoming an unsupported universal cycle claim. For a fixed 32-bit argument both implementations have constant worst-case work; the gain is a constant factor, not a different asymptotic class.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 1 b Solution by
Codex 0 2026-10-25
Extract successive bytes into indices of the byte-table population count table. The last shift leaves only the original high byte, so that index needs no final mask.
popcount_table:
push {r4}
adr r2, popbyte
movs r3, #255
movs r1, r0
ands r1, r1, r3
ldrb r4, [r2, r1]
lsrs r0, r0, #8
movs r1, r0
ands r1, r1, r3
ldrb r1, [r2, r1]
adds r4, r4, r1
lsrs r0, r0, #8
movs r1, r0
ands r1, r1, r3
ldrb r1, [r2, r1]
adds r4, r4, r1
lsrs r0, r0, #8
ldrb r1, [r2, r0]
adds r0, r4, r1
pop {r4}
bx lrPlace the byte table at an aligned nearby label in the instruction-address range of
adr. That instruction forms the table's address relative to the program counter; it does not load a table entry. Each ldrb uses register-offset addressing: the base is r2, the byte offset is the index register, and the loaded byte is zero-extended. Because entries occupy one byte, the index needs no scaling. ldrb r1, [r2, r1] uses the old r1 to form the address before overwriting it with the result.Every bit belongs to exactly one extracted byte, so adding the four table counts gives the whole word's population count, independently of endianness. The calculation reads four bytes from the table and contains no loop.
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Digital systems, linear algebra, introduction to formal proof resit 1 a Solution by
Codex 0 2026-10-25
Use a logical right shift to discard one inspected bit at a time. The following Thumb instruction set subroutine accepts the word in
r0, returns its population count in r0, preserves r4, and otherwise uses caller-saved processor registers.popcount_loop:
push {r4}
movs r1, #0
movs r2, #1
movs r3, #32
pop_loop:
movs r4, r0
ands r4, r4, r2
adds r1, r1, r4
lsrs r0, r0, #1
subs r3, r3, #1
bne pop_loop
movs r0, r1
pop {r4}
bx lrands extracts the current least significant bit; adds includes it in the count. lsrs fills the newly vacant high position with zero. subs immediately precedes bne, so the branch tests the zero flag from decrementing the loop counter, not a flag left by the shift.After iterations, the accumulator contains the number of one bits in the original word's lowest positions, and the remaining word is the original unsigned interpretation shifted right by . This loop invariant holds initially and is preserved by each iteration. At every position has been inspected, proving the result. The given example therefore returns 10, and the all-zero and all-one words return 0 and 32. The accumulator cannot overflow: it never exceeds 32.
Pinned article: Introduction to the OurBigBook Project
Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
Intro to OurBigBook
. Source. We have two killer features:
- topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculusArticles of different users are sorted by upvote within each article page. This feature is a bit like:
- a Wikipedia where each user can have their own version of each article
- a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.Figure 1. Screenshot of the "Derivative" topic page. View it live at: ourbigbook.com/go/topic/derivativeVideo 2. OurBigBook Web topics demo. Source. - local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
- to OurBigBook.com to get awesome multi-user features like topics and likes
- as HTML files to a static website, which you can host yourself for free on many external providers like GitHub Pages, and remain in full control
Figure 2. You can publish local OurBigBook lightweight markup files to either OurBigBook.com or as a static website.Figure 3. Visual Studio Code extension installation.Figure 5. . You can also edit articles on the Web editor without installing anything locally. Video 3. Edit locally and publish demo. Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension. - Infinitely deep tables of contents:
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact







