Due: Mon, 04 Apr 2016 23:00:00 -0700
The Jitk paper from OSDI’14
(Figure 11; Section 3.2.2) describes an incorrect optimization in the Linux kernel.
Consider unsigned integer division
n / k,
n is a 32-bit unsigned integer and
k is a 32-bit unsigned constant.
The incorrect optimization tries to avoid division on the critical path
using two steps:
1. precompute a 32-bit unsigned integer
2. compute the result using
reciprocal_divide(n, R), which uses multiplication and shift only.
R is precomputed as:
reciprocal_divide is implemented as extracting the high 32
bits of the 64-bit product of
42 / 3 as an example:
((1ULL << 32) + (3 - 1)) / 3 = 1431655766 and
reciprocal_divide(42, 1431655766) gives
Unfortunately, this optimization is buggy on some
as described by commit aee636c4.
Is this optimization correct for
k = 3?
If so, prove it. If not, find a counter example.
Figure 10-45 of Hacker’s Delight
describes the following optimization that computes
n / k for the
k = 3 case:
Is this optimization correct? If so, prove it. If not, find a counter example.
Division by Invariant Integers Using Multiplication
from PLDI’94 describes a correct optimization that computes
n / k for a general
This is implemented by Linux kernel’s
to fix the earlier bug.
In this commit correct? Verify its correctness or find a counter example.
As a reference, see similar optimizations and proofs in CompCert.
Write up your answers to the questions,
along with any code or proof,
in a plain text file named
Design and implement a network diagnosis tool that resembles Anteater from SIGCOMM’11 using SMT. Your tool should work for a network as shown in Figure 3 of the paper, for example, to find loops in a network. You may design an input file format or hard-code the input in code.
Use SMT to generate MD4 hash collisions. You may find the following references useful.