Today I Learned

Some of the things I've learned every day since Oct 10, 2016

164: Instruction Pipelining

Instruction pipelining is a technique for increasing the throughput of a computer processor by executing instructions in parallel rather than sequentially.

Suppose you have several tasks to perform which each consist of stages s_1, \dots, s_n and each of these stages uses different resources than the others. One approach to completing a series of such tasks would be to complete one entirely before moving on to the next one, but since each stage of a task uses different resources, this approach leaves most resources sitting idle for unnecessary periods of time. To take advantage of this idleness, you can instead wait until stage 1 of task 1 is done, move it on to stage 2, and then while that is going just start task 2 on stage 1 using the stage 1 resources which are now available, continuing indefinitely in this manner.

A picture makes this idea clearer:


One sees that ideally, pipelining would increase the throughput of a processor by a factor of n, where n is the number of stages to an instruction. However, actually implementing pipelining is much more complicated than this abstraction, and the complications involved actually increase the latency of each individual instruction. Despite this increase in latency, if well-implemented pipelining still increases throughput by a significant factor. In fact, being clever about pipelining is usually the single most important factor in determining the CPI (cycles per instruction) of a processor.


163: Iron Law of Performance

In the study of computation, the Iron Law of Performance refers to the equation

\frac{\text{time}}{\text{program}} = \frac{\text{time}}{\text{cycle}} \cdot \frac{\text{cycles}}{\text{instruction}} \cdot \frac{\text{instructions}}{\text{program}},

which is just a way of roughly compartmentalizing the factors involved in determining how long it takes a program to execute.

While the first 2 terms depend on the instruction set architecture (ISA), microarchitecture, and base hardware technology involved, the 3rd depends mostly on things like the source code, the language the source code is written in, and the way the code is compiled.

162: Most Subsets of a Countable Structure Aren’t Definable Over a Finite Subset

Suppose \mathcal{M} is an \mathcal{L}-structure with universe M which is countably infinite, and suppose N is a finite subset of M. Recall that a subset X of M^p is definable over N iff there exists an \mathcal{L} formula \varphi and tuple (b_1, \dots, b_q) \in N^q such that

X = \{(a_1, \dots, a_p) \in M^p : \mathcal{M} \vDash \varphi(a_1, \dots, a_p, b_1, \dots, b_q)\}.

Suppose The set of subsets of M is a classic example of an uncountable set. However, there are only countably many \mathcal{L}-formulas and countably many tuples of any size from N, so it follows that there are at most countably many N-definable subsets of M. This means almost all subsets of M will be undefinable over any given finite subset N \subseteq M.

161: Elementary Substructures (Logic)

Suppose \mathcal{L} is a first-order language and \mathcal{M, N} are \mathcal{L}-structures with \mathcal{M} \subseteq \mathcal{N}. Then we say \mathcal{M} is an elementary substructure of \mathcal{N} if and only if for any \mathcal{L}-formula \varphi,

\mathcal{M} \vDash \varphi (a_1, \dots, a_k) \Leftrightarrow \mathcal{N} \vDash \varphi (a_1, \dots, a_k)

for a_i \in M. To denote this, we write \mathcal{M} \preceq \mathcal{N}.

160: Soak Testing (Software)

In software development, soak testing is a form of load testing where a system is exposed to some ‘normal’ (anticipated) load for a relatively long period of time to expose issues that would develop under these circumstances. For instance, certain problems like memory leaks in a system under normal usage might take a long time to have noticeable effects. The period of time required or desired varies depending on specifics, but some companies have been known to perform soak tests up to several months long. (Contrasting with the rapid deployment cycles of many systems.)

Ideally, one would be able to vary the load on the system in order to better simulate the fluctuations that it would encounter in deployment, instead of just using a flat average expected load. If this isn’t possible, one might instead set the flat load to one that’s higher than expected in order to get a better simulation. (“Passed tests give you no information.”)

159: Term Substitution (Logic)

Notation In a language \mathcal{L}, where \tau (x_1, \dots, x_n) is a term with free variables from x_1, \dots, x_n and \tau _1 , \dots, \tau _n are terms, let

\tau(x_1, \dots, x_n ; \tau _1, \dots, \tau _n)

denote the term resulting by simultaneously swapping every instance of x_i in \tau for \tau _i.

Further, let \nu be a map from the variables of our language to elements of an \mathcal{L}-structure \mathcal{M}, and \bar{\nu} be its natural extension to a map from terms to elements of \mathcal{M}.

Then we have that

\bar{\nu}(\tau(x_1, \dots, x_n ; \tau _1, \dots, \tau _n)) = \tau(\bar{\nu}(\tau_1), \dots, \bar{\nu}(\tau _n)).

That is, terms “behave well” under substitution.

158: Stress Testing (Software Development)

In software testing, stress testing is generally testing software by subjecting it to a ‘heavier load’ than it would ordinarily be expected to encounter during ‘normal’ usage. It differs from load testing in that its focus is less on controlled variations in load and more on chaotic, unpredictable causes of stress to a system.

This can be advantageous because it’s not always possible to forsee all the different circumstances in which the software may be used in the future. For instance:

  • Operating systems and middleware will eventually have to support software which hasn’t even been written yet.
  • Users may run the software on systems with less computational resources than those on which the software was tested in development.

In some cases, stress testing over a short period of time can also serve as a good simulation of ‘normal’ use over a long period of time, potentially exposing bugs with effects that take time to become noticeable. Additionally, stress testing is good for finding concurrency problems like race conditions and deadlocks.

157: Dijkstra’s and Negative Weights

Dijkstra’s algorithm, commonly used to find the path of minimum weight to any given node from a starting node in a weighted graph, does not work if negative weights are allowed.

Intuitively, the reason is that Dijkstra’s makes the assumption while working through the graph that paths can only become ‘heavier’, and so while visiting a node does not consider neighbors which themselves have already been visited. For instance, consider running the algorithm on the following graph with A as the starting node:



The algorithm will look at as a neighbor of A and set its minimum known distance to 2. It will then look at B and set its to 5. It will then move on to visit C without any changes since C has no neighbors. It will then visit B, but will not consider the edge from to C because C has already been visited. So the algorithm will wrongly conclude that the shortest path to C from A is 2, not -5.

One adaptation which does work on certain types of graphs with negative weights is Johnson’s algorithm, which itself uses Dijkstra’s as a subroutine.


156: Expanding a Finitely Satisfiable L-Theory

Let T be a finitely satisfiable \mathcal{L}-theory and \phi an \mathcal{L}-sentence. Then either T \cup \{\phi\} or T \cup \{ \neg \phi\} is finitely satisfiable, with the or obviously being exclusive.

Proof If T \cup \{\phi\} is not finitely satisfiable, then there is a finite subset \Delta thereof for which \Delta \vDash \neg \phi. In fact, it must be that \Delta \subseteq T. Let \Sigma be a finite subset of T. Since \Delta \cup \Sigma is a finite subset of T it is satisfiable, and we also have that \Sigma \cup \Delta \vDash \neg \phi, so we have that \Sigma \cup \{\neg \phi \} is satisfiable. Thus T \cup \{\neg \phi\} is finitely satisfiable.

This fact can be used to expand a finitely satisfiable theory to a maximal finitely satisfiable theory, one element at a time.

155: Inclusive Logics, Free Logics

Informally, an inclusive logic is a logic which allows models with empty domains, whereas for instance classical first-order logic makes the assumption/requirement that a model have a nonempty domain. An example of this difference is that in classical first-order logic, the sentence

\forall x \phi \rightarrow \exists x \phi

is a tautology, while in an inclusive logic it isn’t because the subformula \forall x \phi could be vacuously satisfied.

Inclusive logics are part of a larger class of logics called free logics, which in general are just logics which make less existential assumptions than classical logics.