Assignment: SMT

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.

Division by constants

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:

	uint64_t k64 = (uint64_t)k;
	return (uint32_t)(((UINT64_C(1) << 32) + (k64 - 1)) / k64);

and reciprocal_divide is implemented as extracting the high 32 bits of the 64-bit product of n and R:

uint32_t reciprocal_divide(uint32_t n, uint32_t R)
{
	return (uint32_t)(((uint64_t)n * (uint64_t)R) >> 32);
}

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.

Figure 10-45 of Hacker’s Delight describes the following optimization that computes n / k for the k = 3 case:

uint32_t divu3(uint32_t n)
{
	uint32_t r = (0x55555555 * n + (n >> 1) - (n >> 3)) >> 30;
	return (n - r) * 0xaaaaaaab;
}

Write up your answers to the questions, along with any code or proof, in a plain text file named answers.txt.

Network diagnosis

Hash collision generation