UNIX programming course

On 21 January 2008 the second term of the academic year 2007/2008 will begin in UCD. Normally I don't notice such dates but now it is a bit special because that's when the first course I'll teach starts. Joe will still be the coordinator as far as the university administration is concerned but I'll be responsible for organizing, planning the content, giving the lectures, and so on. The course is entitled UNIX programming (COMP20060, formerly known as Operating Systems). I will follow the main lines of Joe's curriculum last year. Here's what I'll cover, in various degrees.

1. Introduction to C.
2. The Open Group Base Specifications, the open version of POSIX.
3. Core concepts: multitasking, virtual memory, files.

The course is optional, approximatively 30 students attend it, and they are familiar with Java. My emphasis will be on giving them hands-on experience with the C language. The textbooks are:

1. The C Programming Language, by Kernighan and Ritchie
2. The Practice of Programming, by Kernighan and Pike

The grading is done as follows:

• 40% for the final exam
• 10% for weekly in-class quizzes (that anyone attending the previous lecture should have no difficulty with)
• 20% for a project to be done in a team of two; it will be a command line tool of some sort
• 30% for weekly assignments

The weekly assignments will be judged in a completely objective way. Grading will be done by a computer program and students will know beforehand exactly how that computer program works. Also, students will submit solutions electronically, as many times as they want before the deadline, they will get immediate feedback, and only their best solution will be used for the final grade (with no penalty for multiple submissions or for submitting bad solutions). Nevertheless, the deadline shall be strict. When the deadline expires submissions will be automatically disabled and a sample solution will appear on the website.

When they finish the course, I'd like the students to:

1. feel comfortable using command line in Linux,
2. feel comfortable reading C code written by someone else, and
3. know the main functions of an operating system and its high level architecture.

The advice of the head of school was less content, higher quality. The next steps for me are to:

1. determine more precisely what content I will cover, and
2. code the infrastructure for judging assignments.

Any feedback is welcome, especially from UCD students that might take this course.

Count memory accesses, not operations

Jon Bentley argues in Programming Pearls—a great book—that programmers should have a cost model of the machines they are working on. Recently I had two experiences that really made me feel that "memory is time," as Michal put it. First, I implemented LCS using a n by n matrix. It turned out that this computation took considerable time in the whole program even if it was called for strings of length 10 to 20 on average. Then Michal changed it to use two arrays of length n, and this reduced the running time of the LCS by 40%! The reason is probably that everything now fit in a fast cache. The second story is about strings. I wanted a data structure that allows fast concatenation and subrange extraction. So I tried to do it with persistent balanced trees, which should offer these two operations in logarithmic time. For strings of a few tens of millions of characters it was slower than just using arrays. And the most likely reason is that the space overhead was huge: One needs about 15 times more memory. A few hundred megabytes of memory compared to ten megabytes is a big deal with today's computers.

So I felt like doing a little experiment that I want to share. Copy and paste the following program.

#include <stdio.h>
#define M 100000000
int a[M];

int main() {
  int i; // a counter
  int c; // a number undertaking strange transformations

  i=M, c=71263;
  while (i--) {
    if (i&1) c=3*c+2; else --c;
    a[(c<0?-c:c)%M]=c;   // (*)
  }
  printf("%d\n", a[0]);
  printf("%d\n", c);
}

Compile with optimizations (e.g., gcc -O3 file.c) and time the run (e.g., time ./a.out). Now comment the line (*) and repeat. Now divide the first by the second time and remember the result, which says how slow memory accesses are compared to arithmetic operations.

Oh, I almost forgot! Here is an example of a cost model used in practice.

Sound and Complete

A certain type of researchers value papers based on whether they have a soundness and completeness theorem. I will refer to them as the Cult of the Sound People. In this post I will try to explain in simple terms what soundness and completeness means, what it does not mean, why it is important, and why it is not important. Follow me.

As an example, consider a tool that is supposed to detect bugs in programs. We first define some abstract but precise ideal for what the tool should do. Then we design a real tool and, in the process, we might deviate from the ideal. In this example, the ideal might be the following: If there is any input for which the analyzed program ends with a runtime exception then the tool should tell us that something is wrong; otherwise the tool should be quiet. When you get to implementing the tool you might decide in some cases that some bugs are so hard to find and so unlikely that you are not even going to try. That makes the tool unsound. In other situations you see maybe that a certain usage pattern is almost always a bug but in certain situations, also hard to detect, it is not. So you decide to give a warning always. That makes the tool incomplete. In short, sound means that no bugs are missed, and complete means that correct programs will not make the tool complain about bugs.

To be more precise we consider a language and a set of rules to manipulate propositions in that language. The set of rules is sound if it generates only true propositions when it starts with true propositions. The set of rules (plus a set of propositions known to be true) is complete if it can prove any true proposition.

In the example above the (unspecified) language is something capable of saying "the program (enclose program here) does not produce run-time exceptions." The tool is basically a set of rules that tries to prove such statements. A sound tool will prove such a statement only if the statement is correct; a complete tool will prove such a statement if the statement is true.

The language and the rules should be precise enough so that meta-proofs about them can be done. To take an example, consider boolean expressions that use the (associative) operators \/ and /\ with operands being variables (x, y, ...) and constants (0, 1). An example proposition in this language is a\/(b/\0). Is this `true'? Don't confuse `true' as used earlier with the constant 1 in this particular language! In fact, most people say `valid' for what I named `true' earlier just to avoid the confusion with 1 (which some people call `true'). OK, I hope you're not too confused about this terminology mambo-jumbo. Anyway, the idea is that we need some definition of when a proposition is valid/true/OK. In the case of this language the tradition is to say that you get the answer 1 whatever constants you substitute for variables and then evaluate according to the usual rules to compute \/ and /\ between constants. This definition also gives an algorithm to decide whether a proposition is true. But for more complicated languages it may be possible to have a definition but not an algorithm! In particular, whenever you say "for all real numbers x, property (insert property here) must hold," you are potentially in trouble because the trivial algorithm of iterating over all real numbers... does not exist. There are way to many real numbers, there's more of them than natural numbers.

Anyway, it's probably clear by now that whenever possible it is desirable to have sound and complete algorithms, sets of rules, tools, and so on. It should also be clear that you can't claim something to be sound or complete unless the language and the set of rules are formal enough to allow meta-proofs about them. In particular the ideal of "not producing run-time exceptions" needs to be complemented with a mathematical definition of what the program does when it is run, the so-called semantics of the language.

Even if such mathematical definitions exist, the tool is proven sound (or complete) with respect to those rules. It is still possible to have a program crash even if the tool says that won't happen because... the interpreter that actually runs the program does not correspond to the mathematical definitions of the semantics of the language. Some more proofs are needed. Even worse, even if the interpreter is proven correct with respect with those rules, well, we might have a malfunctioning DRAM and the program can still go wrong. Does this mean the battle is lost? Does it mean we should stop coming up with all these proofs that do nothing?

Of course not! A program that was proven correct has much less chances of being wrong than one that was not. (Folklore fact: Proven programs need testing.) And a program that was certified as bug free by a program that was proven to be correct has even less chances of being wrong. And if it is run by an interpreter (or, what do they say these days? ah, virtual machine) that was proven to be correct then the chances of being wrong are even less. And... well you get the idea. All we do with these proofs and meta proofs is considerably reducing the chances of programs going wrong. But there is some effort involved in this proving and the challenge is to find a sweet-spot. When does proving become more of a time-consuming sport and a self-justifying contemplation than something really useful?

If you would develop a tool like the one described here would you strive for soundness? Completeness? Both? Would you do the same if the goal is to obtain a tool that is useful to programmers in the industry and that makes them more efficient?

1, 2, 3, \infty

Since the time of Greek philosophy, scholars have prided themselves on their ability to understand something about infinity; and it has become traditional in some circles to regard finite things as essentially trivial, too limited to be of any interest. It is hard to debunk such a notion, since there are no accepted standards for demonstrating that something is interesting, especially when something finite is compared with something transcendent. Yet I believe that the climate of thought is changing, since finite objects are proving to be such fascinating objects of study.

Donald E. Knuth, Mathematics and Computer Science: Coping with Finiteness, 1976

Interdisciplinary research

I am a PhD student in the Systems Research Group (SRG) at the University College Dublin. The groups contains people working on pervasive computing, vizualization, and software verification. SRG is part of the Complex and Adaptive Systems Laboratory, which includes geologists, mathematicians, electrical engineers, and who knows what else. The point of putting all of us under one roof is to foster interdisciplinary research. In fact, at the last week's SRG Away Day we have been encouraged to engage strangers into conversation during lunch. I am a rather introvert person so I find such an action to be quite odd but, oh well, maybe I'll try.

What is an SRG Away Day you ask? It is like a team building trip, except it is less fun. It happens every six months somewhere in Dublin. We start with the Three Minute Madness. Each PhD student is supposed to condense six months of work in three minutes and then say a bit about future plans. Then the lecturers start preaching on some random subjects, such as "have a publication goal!" and "try to engage in interdisciplinary research!". The whole thing is quite boring. Then we go on a pub crawl. Or not — in case you have a deadline the next day.

Anyway, after my three minutes talk Aaron asked how do the things I do help with my PhD. I talked about three things I've done during the last six months: FreeBoogie, reachability analysis for annotated code, and edit and verify. In those two seconds I was formulating an answer to Aaron's question I might have well come up with the subject of my PhD thesis — the efficiency of software verification tools.