Due: Mon, 04 Apr 2016 23:00:00 -0700

Finish the Z3Py guide and/or the Rosette guide. You may use either tool to finish this assignment.

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`

,
where `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 `R`

; and

2. compute the result using `reciprocal_divide(n, R)`

, which uses multiplication and shift only.

In particular,
`R`

is precomputed as:

and `reciprocal_divide`

is implemented as extracting the high 32
bits of the 64-bit product of `n`

and `R`

:

Take `42 / 3`

as an example:
precomputing `R`

gives `((1ULL << 32) + (3 - 1)) / 3 = 1431655766`

and
`reciprocal_divide(42, 1431655766)`

gives `14`

.
Unfortunately, this optimization is buggy on some `n`

and `k`

,
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.

The paper
*Division by Invariant Integers Using Multiplication*
from PLDI’94 describes a correct optimization that computes `n / k`

for a general `k`

.
This is implemented by Linux kernel’s
commit 809fa972
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 `answers.txt`

.

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.