2
$\begingroup$

I was reading an assembly procedure that needed to align addresses on 4 bytes boundary for performance reasons so it has used the next statement that i formulated as a theorem to be proven.

Let $s$ be an integer that is not a multiple of 4 ($s \% 4 \neq 0$). $m$, the first next multiple of 4 such that $m \gt s$ is obtained using the following formula, where the operands are expressed in base 2 (Binary): $m = s + (\lnot s \land 11)$ ($\lnot a$ will return the 2's complement of $a$).

How to prove that ?

$\endgroup$
4
  • $\begingroup$ @dkaeae Yes. I made a mistake i forgot to tell that the negation $\lnot$ will actually return the 2's complement of its operand (The Intel's x86 neg instruction). $\endgroup$ – Karim Manaouil Mar 15 '19 at 17:05
  • $\begingroup$ Yes, but it still doesn't work. Now if $s = 1$, then $m = 3$. $\endgroup$ – dkaeae Mar 15 '19 at 17:07
  • $\begingroup$ In fact, $\text{and}(a, 3)$ yields a number strictly smaller than $4$ for any $a$. $\endgroup$ – dkaeae Mar 15 '19 at 17:08
  • $\begingroup$ @dkaeae Damn man, i feel too dumb. That is actually the distance that is needed to reach the next multiple of 4. God, sorry for this spaghetti i made. I just corrected the formula, take a look. $\endgroup$ – Karim Manaouil Mar 15 '19 at 17:43
1
$\begingroup$

Suppose that $s = 4a+b$, where $0 \leq b < 4$; by assumption, $b \neq 0$. If the numbers are $n$ bit long, then $\lnot s = 2^n - s = 4(2^{n-2}-a) + (4-b)$. Since $b \neq 0$, the last two bits of $\lnot s$ will be $4-b \in \{1,2,3\}$. Therefore $(\lnot s) \land (11)_2 = 4-b$. Adding this to $s$, we get $4a+b+4-b = 4(a+1)$.

$\endgroup$
3
  • $\begingroup$ Oh great, that's so beautifully done. I really missed the idea that $\lnot s = 2^n - s$ . That was the key for proving it. Thanks professor. The thing that puzzles me is how did the programmer knew about such a fact ?! Is it something that could be intuitively figured out and later be proved ? for example, the fact that $and(n, 3)$ always gives you the distance to the previous multiple of 4 is easy to notice and then prove. But this one is really tricky. What do you think professor @Yuval Filmus, is it a known technique for the people that work on assembly level ? $\endgroup$ – Karim Manaouil Mar 15 '19 at 22:55
  • $\begingroup$ It's really impossible to say. Such tricks probably get discovered and rediscovered many times, and then spread around. You can also compute the next multiple using (s&~3)+4, something I just thought about. I'm probably not the first person figuring this one out either. $\endgroup$ – Yuval Filmus Mar 15 '19 at 23:14
  • $\begingroup$ Yes, i see your point professor. Thanks again. $\endgroup$ – Karim Manaouil Mar 15 '19 at 23:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.