Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Digital systems, linear algebra, introduction to formal proof (resit) (A10101W1)

In the traditional Unix file system model, a regular file consists of file metadata in an inode and an ordered sequence of bytes stored in file data blocks. The inode records the type, owner, permissions, length, timestamps and hard link count, together with the information locating its file data blocks. A small file can use direct file data block addresses; a larger file can additionally use indirect block pointers, whose blocks contain further addresses rather than user data. The final file data block need not be completely occupied.

An inode number identifies an entry in the inode table of this file system; it identifies the file, rather than a particular piece of its contents. A disk block number identifies a fixed-size storage region on the volume. Resolving an inode number first obtains the inode; following its direct or indirect block pointers then finds the required file data block. The two numbers belong to different address spaces, even though the inode table itself occupies disk blocks.

The file-system namespace is rooted at the root file-system directory. Each directory entry associates a local name with an inode number. To resolve a pathname, start at the root for an absolute pathname, or at the process's current file-system directory for a relative pathname, and look up successive components in successive file-system directories. A file-system directory is itself a file with a special interpretation for its data.

The inode table stores file metadata and the information locating contents. The file-system directory structure supplies names and the connections used in pathname lookup. Thus the file is the object represented by its inode, whereas a file name is one entry referring to that object. Two hard links can give the same file two names, possibly in different file-system directories. Renaming a file need not move its contents or change its inode number; after unlinking an open file, a file can temporarily have no names and still be accessible through an existing file descriptor.

Use a block allocation bitmap, one bit per allocatable disk block number, or a free-block list. Allocation removes a free block from the free representation; deallocation inserts it. Reserved file system structures, including the inode table and the free-space representation itself, must never be offered as free file data blocks. Free inodes can be tracked separately by an inode allocation bitmap.

A file data block becomes reusable when the file system has removed its ownership from the file. This happens, for example, when truncation discards that portion of the file, or when the file is finally destroyed. Destruction requires both removal of its last hard link and release of its last live reference: unlinking an open file must not reclaim blocks still needed through an open file description. A memory-mapped file, if supported, also requires its references to be accounted for. The indirect block pointers' own blocks are reclaimed when they are no longer needed.

There are two relevant notions of accessibility. Pathname-accessible files are those reached from the root through valid directory entries, subject to permissions; their allocated blocks are found through their inodes. Already-open files can additionally remain accessible through file descriptors even after their last names disappear. Allocated file system structures and blocks pinned by an operation must also be excluded from allocation. A block allocation bitmap must therefore describe actual allocation, rather than merely the blocks of currently named regular files.

One processor can still run several processes and be interrupted. Updating ownership and the free-space representation must therefore be serialized with respect to competing operations, for example through an appropriate kernel critical section. Persistence across a crash additionally requires file-system crash consistency, such as ordered updates or file-system journaling.

The hard link count in an inode duplicates information recoverable by counting directory entries that refer to its inode number. Keeping the count makes the last-name test fast: a hard link removal need not search every file-system directory. A file-system consistency checker can independently recount the references and compare the result with the stored value.

Likewise, a block allocation bitmap summarizes ownership information recoverable from allocated inodes, their file data blocks, their indirect block pointers, and reserved file system structures. This summary makes allocation efficient and supplies an independent consistency check against multiply allocated or lost blocks. Replicated superblock information is another possible form of data redundancy, helping recovery if one copy is damaged. These examples have distinct benefits: a cached count or allocation summary saves work, while an independent or replicated representation helps detect or repair corruption. Consistent updating is essential; redundancy alone does not make a file system crash-safe.

A file descriptor table belongs to a process: its small nonnegative integer indices are file descriptors, and each occupied entry points to an open file description. It also holds descriptor-specific information, such as whether the descriptor closes on a successful program replacement. There is one logical file descriptor table per process in the traditional model; implementations can let processes explicitly share one.

The system-wide open file table, called the file pointer table here, contains open file descriptions. Each entry records an opening's access mode, current file offset, reference count and reference to an in-memory inode. Duplicated file descriptors, including inherited ones, can refer to the same open file description and therefore share its file offset. Independent opens of the same file normally create separate open file descriptions and separate offsets. There is one logical system-wide open file table, with many entries.

The system-wide in-memory inode table caches the inodes currently needed, including shared file metadata, locking and reference information. Its identity key must include the file system as well as the inode number when several volumes are mounted. There is one logical system-wide active inode table, distinct from the persistent inode table stored on each volume. These are logical organizations, not requirements for a single contiguous array in memory.

For a CMOS inverter, connect one PMOS transistor from the positive supply $V_{DD}$ to the output and one NMOS transistor from the output to ground; drive both gates with the input $x$. When $x=0$, the PMOS transistor conducts and the NMOS transistor is off; when $x=1$, the reverse holds. Thus the output is $\neg x$, using two transistors.

For a four-input NAND gate, use four NMOS transistors in series between the output and ground, with gates $a,b,c,d$. Use four PMOS transistors in parallel between $V_{DD}$ and the output, with the same gate signals. The pull-down network conducts exactly when all four inputs are one; the pull-up network conducts whenever at least one input is zero. HenceAs usual for static CMOS, tie the NMOS transistor bodies to ground and the PMOS transistor bodies to $V_{DD}$.

Each parenthesized pair in the given Boolean function tests equality of two input bits:This is logical equivalence, or the two-input XNOR gate function. Thus $z$ is one whenever either input pair agrees. Generate the four complemented inputs with four inverters, and define the following NAND gate outputs:Feed these four outputs into a single four-input NAND gate. De Morgan's laws giveHere juxtaposition denotes logical conjunction. The construction uses only inverters, two-input NAND gates and one four-input NAND gate, as required.

The four CMOS inverters use $4\cdot 2$ transistors, the four two-input NAND gates use $4\cdot 4$, and the four-input NAND gate uses $8$. Therefore this particular design uses

A more economical static CMOS design follows from factoring the condition for $z=0$. The output is low exactly when both input pairs disagree:Generate $\neg a,\neg b,\neg c,\neg d$ with four CMOS inverters. Write $n(x)$ or $p(x)$ for an NMOS transistor or PMOS transistor whose gate receives $x$. In the following network expressions, a dash means a series connection and $\parallel$ means a parallel connection.

Connect this eight-device pull-down network between $z$ and ground:The first parallel module conducts exactly when $a\ne c$ and the second exactly when $b\ne d$. Their series connection therefore conducts precisely when $z$ should be zero.

By complementary CMOS network duality, connect this eight-device pull-up network between $V_{DD}$ and $z$:A PMOS transistor conducts when its gate is zero. Consequently the first upper branch conducts when $(\neg a\vee c)\wedge (a\vee \neg c)$, namely $a=c$; the second conducts when $b=d$. Their parallel connection gives the required logical disjunction. For every stable binary input, exactly one of the pull-up network and pull-down network conducts.

The figure labels each MOSFET channel by its gate signal; the four input CMOS inverters are additional to the devices drawn.

The custom CMOS circuit uses eight NMOS transistors and eight PMOS transistors in the output networks, plus eight transistors in the four input CMOS inverters:The complementary types give an actively driven output at either supply rail. An NMOS transistor provides a strong connection to ground; a PMOS transistor provides a strong connection to $V_{DD}$. An NMOS transistor used alone to pass a high level loses gate overdrive as the output rises, giving a threshold-degraded high level; the complementary problem affects a PMOS transistor passing a low level. Complementary networks avoid these degraded levels and, ideally, have no direct supply-to-ground conducting path for a stable input. Physical leakage and switching current remain, but a resistive load and its continuous static current are unnecessary.

In the pictured single-cycle MIPS architecture, RegDst selects the write address of the register file: zero selects instruction bits $20\dots 16$, the rt field used by a load; one selects bits $15\dots 11$, the rd field used by an MIPS R-type instruction. RegWrite enables the clocked write to the selected processor register.

ALUSrc selects the second ALU input: zero uses the second register file read output, while one uses the sign-extended 16-bit immediate field. The zero signal is produced by the ALU, rather than being an opcode-decoder output: it is one exactly when the ALU result is zero. During beq, the ALU subtracts its operands, so zero tests equality. The diagram combines it with Branch to select the branch target instead of $PC+4$.

Run the following two MIPS instruction tests separately from externally prepared states, and inspect the register file after the indicated instruction. External preparation is useful in a manufacturing test: code that initializes processor registers through the very control line being tested need not work. Assume the one potentially faulty line is RegDst; all other lines work normally.

For the first test, preset $t0=7, $t1=5, $t2=99, and executeThe encoded rt is $t1, while rd is $t2. A healthy line or a line stuck at one writes 12 into $t2. A line stuck at zero instead writes 12 into $t1, leaving $t2=99.

For the second test, preset $t3=4, $s0=L, and the aligned memory word at $L$ to 37, then executeThe zero immediate makes instruction bits $15\dots 11$ zero. A healthy line or a line stuck at zero writes 37 into $t3; a line stuck at one attempts to write the MIPS zero register, leaving $t3=4. The MIPS zero register ignores attempted writes. Thus, recording the first test's $t2 and the second test's $t3,

A writing MIPS instruction distinguishes a line stuck at zero. With $t0=7, $t1=5, $t2=99, executeA healthy line or a line stuck at one produces $t2=12; a line stuck at zero leaves $t2=99.

To distinguish normal operation from stuck at one, execute a normally nonwriting MIPS instruction. The following functional test uses the usual concrete controller choice MemToReg=0 during sw, selecting the ALU result on the write-data bus. Prepare $t0=37 and $s0=L-16384, for an aligned writable address $L\ne 37$, then executeThe ALU computes $L$. Here rt is register 8 ($t0), and immediate $16384=0x4000$ also puts 8 into bits $15\dots 11$. Thus either value of the otherwise irrelevant RegDst selects $t0. With a healthy RegWrite, $t0 remains 37. With RegWrite stuck at one and the specified write-data selection, the unwanted register file write changes $t0 to $L$. Combining the two independent observations gives

Controller qualification. The source diagram does not specify values of otherwise irrelevant control outputs during a store. MemToReg is a don't-care condition when RegWrite=0; its chosen implementation matters when that enable line is faulty. The functional test above explicitly fixes this convention instead of assuming that all implementations resolve it identically. A manufacturing fixture can also observe the register file write-enable directly while executing add followed by sw: the expected pairs are $(1,0)$ normally, $(0,0)$ stuck at zero, and $(1,1)$ stuck at one. This second observation does not depend on unused write-data controls or on whether an unwanted write happens to repeat an old value.

Again use independent externally initialized MIPS instruction tests. First preset $t0=7, $t1=5, and executeThe normal result, also obtained with ALUSrc stuck at zero, is 12. If the line is stuck at one, the second ALU operand is the sign-extended low 16 instruction bits. For this exact instruction they encode rd=10, shift amount zero and function $0x20$, giving $0x5020=20512$. The erroneous result is therefore $7+20512=20519$.

For the second test, preset $s0=L, $t3=4, memory at $L$ to 37 and memory at $L+4$ to 99, with both words valid and aligned. ExecuteNormally, and with ALUSrc stuck at one, the address is $L+0$ and the result is 37. With the line stuck at zero, the second ALU operand is the old $t3=4, so the load reads 99 from $L+4$. Thus

Execute this MIPS instruction fragment twice, once with equal operands and once with unequal operands, and observe whether its conditional branch is taken:Use $t0=7,$t1=7 for the first test and $t0=7,$t1=8 for the second. All padding instructions are explicit harmless MIPS instructions. In the pictured single-cycle model, the next program counter after beq is either hit or the sequential address. The branch target is deliberately different from the next sequential instruction. The extra padding also keeps a branch delay slot harmless if a test fixture uses an implementation with one, although the pictured model itself has none.

A healthy zero line reports the first subtraction as zero and the second as nonzero. A line stuck at zero prevents both branches, while a line stuck at one forces both branches. ThereforeObserve the branch decision or execution trace itself; an alleged unconditional beq used to skip result-recording code would also be affected by the fault.

The register file in this datapath supplies both read ports combinationally for whatever read addresses the instruction fields present. Reading a processor register is harmless, and a result that the current MIPS instruction does not need can simply be ignored. Only writes require an explicit enable because writes change architectural state. There is consequently no functional need for RegRead in this design.

The data-memory read interface has an explicit MemRead enable. Non-load MIPS instructions can present irrelevant or invalid addresses at the memory address input; an external memory transaction should not be initiated merely because those bits happen to be present. An explicit enable also permits interfaces with memory-mapped input-output, where a read can have a side effect. It can reduce unnecessary activity even for ordinary memory.This is a distinction in the supplied datapath, rather than a universal physical prohibition: other register files can have read enables, and an ideal side-effect-free memory can be modeled with continuous reads.

Source gap / TODO: the original printed page 4, confirmed visually, omits the unknown vector. It literally equates a $3\times 3$ matrix with a $3\times 1$ vector, so it does not define a well-formed system of linear equations. The following answer is conditional on the usual intended interpretation $A\mathbf{x}=(1,k^2,k{)}^T$; the missing factor is not present in the source.

Under that interpretation, the rows satisfy $r_1-2r_2+r_3=0$. Applying this linear relation to the right-hand side gives the necessary consistency conditionIt is sufficient too: the upper-left $2\times 2$ minor has determinant $4-9=-5\ne 0$, so the first two rows are linearly independent. The third row is $2r_2-r_1$, and imposes precisely the condition already found. ThereforeFor completeness, setting $x_3=t$ givesand direct substitution satisfies all three linear equations exactly for those two values of $k$. An unconditional answer to the malformed printed equality awaits a source correction.

Apply flow conservation at the four junctions, using the directions in the original diagram:The total external inflow and outflow are both 250 cars per hour. Accordingly one of these linear equations is redundant. Put $F_2=t$. Successive substitution yieldsin cars per hour. The nonnegativity restriction expresses clockwise traffic on every arc. Conversely, every $t\ge 0$ gives nonnegative flows satisfying all four conservation equations, so this is the whole physically allowable family. Increasing $t$ adds a common network circulation around the roundabout without changing any external inflow or outflow.

Since $F_1=200+t$ and $t\ge 0$, its minimum is attained at $t=0$:Zero flow on the $B\to C$ arc is allowed; no strictly positive lower bound was specified.

A scalar $\lambda$ is an eigenvalue of an $n\times n$ matrix $P$ if there is a nonzero vector $\mathbf{v}$ such thatAny such vector is an eigenvector corresponding to $\lambda$. The requirement that an eigenvector be nonzero is essential: the zero vector would satisfy the equation for every scalar and would convey no information.

Use the state order Tall, Medium, Short and column probability distributions, so that ${\mathbf{p}}_{n+1}=P{\mathbf{p}}_n$. The $j$th column records the child's probability distribution given parent state $j$. Thus the transition matrix isEvery entry is nonnegative and every column sums to one. This convention also gives the requested property $P^T(1,1,1{)}^T=(1,1,1{)}^T$. A row-distribution convention would use the transposed transition matrix consistently instead. The stated Markov chain is the mathematical model to analyze; no additional biological assumptions are needed.

Condition on the intermediate parent's height and use the Markov property. The three mutually exclusive paths through Tall, Medium and Short contributeEquivalently, this is entry $(3,1)$ of the matrix power $P^2$. Hence

For $1=(1,1,1{)}^T$, the entries of $P^{T}1$ are the column sums of $P$. Henceso $1$ is an eigenvalue of $P^T$, with eigenvector $1$.

The determinant is unchanged by matrix transposition, soThus $P-I$ has a nontrivial null space, givingThe same argument with $\lambda I$ shows that a matrix and its transpose have the same characteristic polynomial. It does not say that they have the same eigenvectors: here $P1=(0.9,1.2,0.9{)}^T\ne 1$.

Find a stationary distribution $\mathbf{\pi }=(u,v,w{)}^T$ from $P\mathbf{\pi }=\mathbf{\pi }$ and $u+v+w=1$. The first two independent linear equations areThey give $u=9w/8$ and $v=7w/4$. Normalization gives $w=8/31$, hence

To justify the limit using the assumptions, distinct eigenvalues give an eigenbasis, over the complex numbers if necessary. Choose $\mathbf{\pi }$ as the eigenvector for 1 and let ${\mathbf{v}}_2,{\mathbf{v}}_3$ correspond to the other eigenvalues ${\lambda }_2,{\lambda }_3$. Expand the initial probability distribution asSince $1^{T}P=1^T$, each ${\lambda }_j\ne 1$ satisfiesMultiplying the expansion by $1^T$ therefore gives $\alpha =1$. It follows thatbecause $|{\lambda }_2|,|{\lambda }_3|<1$. The components of the limiting probability distribution are approximately $0.2903,0.4516,0.2581$.

For a real $m\times n$ matrix $A$, the row space is the linear span of its rows in ${\mathbb{R}}^n$. The column space is the linear span of its columns in ${\mathbb{R}}^m$, equivalently $\{A\mathbf{x}:\mathbf{x}\in {\mathbb{R}}^n\}$. The null space isThe matrix rank is the dimension of the column space, which equals the dimension of the row space. In particular,The last equality is the rank-nullity theorem.

Denote the five rows by $r_1,\dots ,r_5$. They satisfyThus $r_2,r_3,r_4$ span the row space. They are linearly independent: in a linear combination $\alpha r_2+\beta r_3+\gamma r_4=0$, coordinate 1 gives $\alpha =0$, coordinate 2 then gives $\beta =0$, and coordinate 4 gives $\gamma =0$. ThereforeAs an alternative basis, the nonzero rows of the reduced row echelon form are

Let $c_1,\dots ,c_4$ be the original columns. The first three are linearly independent: restricting them to rows 2, 3 and 4 gives the triangular matrixwhose determinant is one. Also $c_4=c_1-c_2+c_3$, so a basis for the column space isThese are columns of the original matrix. Taking columns of its reduced row echelon form would generally give the wrong column space.

The reduced row echelon form gives $x_1+x_4=0$, $x_2-x_4=0$, and $x_3+x_4=0$. With free parameter $x_4=t$,The displayed nonzero vector therefore forms a basis for the null space:This agrees with the rank-nullity theorem: there are four columns and matrix rank three.

The second, third and fourth linear equations giveSetting $x_4=t$ yields $x_3=-1-t$, $x_2=1+t$ and $x_1=1-t$. The first linear equation then gives $(1-t)+(1+t)+(-1-t)+t=1$, and the fifth gives $(1-t)+t=1$, so both remaining conditions hold for every real $t$. ConsequentlyThis is a particular solution plus the whole null space, an affine line in a vector space of solutions. The derivation both produces solutions and shows that none have been omitted.

The implication introduction rule opens a subproof under a temporary assumption $\varphi$, derives $\psi$, then performs assumption discharge to conclude $\varphi \to \psi$. The negation introduction rule instead derives logical falsity $\perp$ under a temporary assumption $\varphi$, discharges it, and concludes $\neg \varphi$:The rectangular boxes delimit these subproofs and the scope of their temporary assumptions. A line depending on the boxed temporary assumption cannot simply be used outside the box. The relevant introduction rule exports the indicated logical implication or negation; other surrounding assumptions $\Gamma$ stay in force.

Write $H=(P\wedge Q)\vee (P\wedge R)$ and $K=P\wedge (Q\vee R)$. In the following natural deduction derivations, brackets name temporary assumptions, and cited ranges specify the subproofs discharged. The abbreviations $\wedge E,\wedge I,\vee E,\vee I$ denote the corresponding conjunction elimination rule, conjunction introduction rule, disjunction elimination rule and disjunction introduction rule.

First use the disjunction elimination rule backwards: split the premise into two cases and build the whole conclusion in each case.

Alternatively, use the conjunction introduction rule backwards on the conclusion. First obtain $P$ by cases, then obtain $Q\vee R$ by a second case analysis, and finally combine the results:

The first proof goal transformation starts with case analysis; the second starts by splitting a conjunction goal. Counting only actual applications of the printed inference rules, both use nine steps: the first has four $\wedge E$, two $\vee I$, two $\wedge I$ and one $\vee E$; the second has four $\wedge E$, two $\vee I$, one $\wedge I$ and two $\vee E$. The extra case analysis in the second exactly replaces one conjunction construction. If assumption lines are counted as well, the second display has two more lines because it opens four case subproofs rather than two. Thus the apparent difference in display length need not be a difference in inference count.

The classical proof by contradiction rule, also called reductio ad absurdum, iswith assumption discharge of the displayed $\neg \varphi$. It differs from the negation introduction rule by concluding $\varphi$ from a contradictory assumption of its negation.

To derive double-negation elimination using this rule, start with $\neg \neg \varphi$, assume $\neg \varphi$, and apply the negation elimination rule to those two formulas:No double-negation elimination occurs inside this derivation, so the argument is not circular.

Put $F=(\neg P)\to Q$ and $G=(\neg P)\to \neg Q$. Use the printed implication elimination rule, negation elimination rule, negation introduction rule, double-negation elimination and implication introduction rule:Line 1 is the given premise; the argument actually establishes the conclusion without needing it, since line 2 supplies its own copy of $F$. Introducing and discharging this separate temporary assumption preserves the exact printed conclusion.

First obtain $A$ by a double-negation elimination, then obtain $\neg B$ by the negation introduction rule. The following natural deduction proof uses only the printed rules, with $\perp E$ denoting the logical falsity elimination rule:Reiteration only reuses an available line within its scope. In particular, the unused temporary assumption on line 11 is legitimately discharged by the implication introduction rule.

Apply the negation introduction rule to an assumed existential statement and the existential quantifier elimination rule with a fresh witness $u$:The eigenvariable condition holds: $u$ is absent from the surrounding premise, the existential assumption and the exported conclusion $\perp$. Its local assumption is discharged before the final negation introduction rule.

The dot after $\forall x$ gives it scope over the following implication: read the premise as $H=\forall x(P(x)\to Q(x))$. Choose a fresh arbitrary eigenvariable $u$. A natural deduction proof isAt line 6, $u$ is free in no undischarged assumption, so the universal quantifier introduction rule is valid.

The proposed variant is not derivable in a sound first-order logic. For a countermodel, use the two-element domain $\{0,1\}$, interpret both predicates $P,Q$ as $\{0\}$, and assign the free variable $x$ the value 0. Then $\forall x(P(x)\to Q(x))$ is true, as is $P(x)$ under the assignment, but $\forall xQ(x)$ is false at element 1. The premise's bound $x$ and the conclusion's free $x$ have different scopes.Attempting to generalize from $Q(x)$ in the variant would violate the eigenvariable condition, because $x$ remains free in the undischarged assumption $P(x)$.

Let $H=\forall x\forall y(S(x,y)\vee \neg S(x,y))$ and abbreviateAssume $\exists bB(b)$ and eliminate the existential quantifier using a fresh eigenvariable $u$. Inside that subproof, specialize $B(u)$ at $p=u$. Write $s=S(u,u)$. The premise $H$ supplies $s\vee \neg s$, so a disjunction elimination rule finishes the contradiction:Line 7 abbreviates two consecutive universal quantifier elimination rule applications; no new rule is used. The fresh witness $u$ is absent from $H$, the assumed existential statement and the exported $\perp$, so the existential quantifier elimination rule satisfies its eigenvariable condition. This is the self-application behind the barber paradox, written entirely with the supplied rules.

The equality introduction rule is reflexivity, with no premise. The equality elimination rule is substitution of equal first-order terms into a first-order formula:The indicated substitution must be capture-avoiding substitution in first-order logic: the first-order terms must be free for the replaced variable. One can designate a particular argument occurrence by choosing $\varphi (v)$ appropriately; the rule does not demand replacing every occurrence of an identical-looking term in a formula.

For transitivity of first-order equality, take $\varphi (v)$ to be $T_1=v$. The equality elimination rule applied to $T_2=T_3$ and $\varphi (T_2)$ givesFor symmetry of first-order equality, first obtain $T_1=T_1$ by the equality introduction rule. Now take $\psi (v)$ to be $v=T_1$ and substitute using $T_1=T_2$:These choices of formula show exactly which occurrence is replaced, so neither argument assumes the property it is establishing.

Choose fresh arbitrary eigenvariables $u,v$. Under $u=v$, use the equality elimination rule to transport $P(u)$ to $P(v)$. For the reverse direction, first derive $v=u$ by the symmetry derivation above. In full natural deduction form:All temporary assumptions are discharged before either universal quantifier introduction rule application, so both eigenvariable conditions hold. No premises remain: