The Worm Ouroboros

Here's a quick question: can the behaviour of the following bit of C code depend upon the semantics of the Python programming language?

1 2 3 4 5 6 7

int sum(size_t len, char *array) { int total = 0; for (int i = 0; i < len; i++) { total += array[i]; } return total; }

Now, the very fact that I am asking this question probably makes you suspicious. (This suspicion is correct and natural, and incidentally also indicates that you basically understand Derrida's critique of the metaphysics of presence.) Luckily, as lecturers go, I'm a very generous grader: I'll accept both no and yes as answer!

The "no" answer is easy enough to explain: the C language specification defines an (informal) abstract machine, and the behaviour of the sum function can be explained entirely in terms of that abstract machine. Python never shows up in this semantics, so how on Earth could it possibly be relevant to the behaviour of this code?

To get to "yes", let's look at another bit of C code (please forgive the total lack of error handling, as well as the absence of all includes):

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19

int foo(char *filename) { int fd = open("foo.txt", O_RDONLY); // open a file struct stat s; fstat(fd, &s); // we only want s.size // // memory-mapped IO (every time, I remember Perlis epigram 11) // char *array = (char *) mmap(NULL, s.size, PROT_READ, MAP_SHARED, fd, 0); // // Now we can add up the byte values: int total = sum(s.size, array); // // We're done with the file now. munmap(array, s.size); close(fd); return total; }

This function will open a file "foo.txt", and then will get the file's size using fstat, and then use that size information to call mmap, mapping that file into memory, storing the start pointer at array. Then we'll call sum to total the bytes of the array. But note that:

1. The semantics of array depend on the semantics of the file system.
2. The file system might be a user-mode file system, implemented using something like FUSE or WinFsp.
3. You could (and various people have) written user-mode filesystems to expose a Mercurial repository as a file system.
4. Mercurial is implemented in Python.

Let me emphasize: on a modern computer, a pointer dereference could very lead to the execution of Python code. Indeed, seeing an assembly listing, like this one:

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17

sum: test edi, edi jle .L4 mov rdx, rsi lea eax, [rdi-1] lea rsi, [rsi+1+rax] mov eax, 0 .L3: movsx ecx, BYTE PTR [rdx] add eax, ecx add rdx, 1 cmp rdx, rsi jne .L3 rep ret .L4: mov eax, 0 ret

offers no guarantee that anything "close to the metal" will actually happen. This is the normal state of affairs, which is almost certainly true about every computer upon which this article is being read. (If it's not, you've probably somehow compiled your browser into a kernel module, which is security-wise an incredibly reckless thing to do.)

You might wonder, what's the moral of this story? Actually, there isn't a moral -- instead, there's a question. Namely, how can we prove that this kind of thing is a sensible thing to do, ever? The key intellectual difficulty is that the rationale for for why this kind of program can work appears to be circular.

In general, the easy case of abstraction is when things build up in layers. We start with a piece of hardware, and on this hardware we run an operating system, which (by running in kernel mode to access various hardware primitives) implements address space virtualization. Since user-moder code can never touch the hardware primitives to manipulate things like page tables, we can conclude (assuming the implementation of virtual memory is correct) that the virtual memory abstraction is seamless -- user code can't tell (without relying on OS calls or side-channels like timing) how memory is implemented.

However, what memory-mapped IO and user-mode file systems let you do is to move part of the implementation of the memory abstraction into user space. Now the correctness of the Python implementation depends upon the correctness of the virtual memory, but the correctness of the virtual memory abstraction depends upon the correctness of the Python implementation!

If A implies B, and B implies A, then we are not licensed to conclude tha A and B hold. (This is because it's bad reasoning! Since false implies itself and false implies everything, if this principle were true in general then everything would be true.) And yet: something very close to this kind of reasoning is essential for building systems from modular components, or even writing concurrent algorithms. (We call it rely-guarantee, usually.)