# Making ThinkFinger Faster

Some time ago, I have installed and configured ThinkFinger, a driver for the fingerprint-readers found in most IBM/Lenovo Thinkpads, including my Lenovo X61 Tablet. Although it worked well, it was very slow! I had to wait 5 to 10 seconds for the prompt to show, then a bit more before I could swipe my finger or write my password, and then a bit more for the password to be accepted.

To make my world a better place to live, I have downloaded the development version of the driver and tried to figure out why it was being so slow. It turns out that in the library that is used to communicate with the fingerprint-reader, there was a call to the function usb_bulk_read that was taking too long. I have tried to find some official documentation about this function, but all I could find was how not to document a function (seriously, what is the role of the parameter timeout? and is it measured in seconds? milliseconds?).

Anyway, I have changed the value of the USB_TIMEOUT constant from 5000 to 5 and the fingerprint-reader is much, much better! In detail, here is the patch:

Index: libthinkfinger/libthinkfinger.c
===================================================================
--- libthinkfinger/libthinkfinger.c     (revision 118)
+++ libthinkfinger/libthinkfinger.c     (working copy)
@@ -35,7 +35,7 @@

#define USB_VENDOR_ID     0x0483
#define USB_PRODUCT_ID    0x2016
-#define USB_TIMEOUT       5000
+#define USB_TIMEOUT       5
#define USB_WR_EP         0x02
#define USB_RD_EP         0x81
#define DEFAULT_BULK_SIZE 0x40


I am not sure why this works and what are the implications, but all the tests I did were satisfactory. If you know more about this problem, please let me know! I would be more than happy to understand why the USB_TIMEOUT constant seems to be acting as a time-wait delay, rather than as a timeout in the following call (line 324, libthinkfinger/libthinkfinger.c):

usb_retval = usb_bulk_read (tf->usb_dev_handle, USB_RD_EP, bytes,
size, USB_TIMEOUT);


(I think it is strange that I haven’t found anyone complaining about the same problem. Nevertheless, I’ve decided to publish this post anyway, in case someone runs into the same problem.)

Update (2009/07/31): I’ve upload a patched SRC RPM: thinkfinger-0.3-9.jff.src.rpm. Please note that I have added the patch to Fedora’s SRC RPM.

# Sir Tony Hoare on the future of Computing Science

Sir Tony Hoare on the future of Computing Science (CACM, March 2009):

I expect the future to be as wonderful as the past has been. There’s still an enormous amount of interesting work to do. As far as the fundamental science is concerned, we still certainly do not know how to prove programs correct. We need a lot of steady progress in this area, which one can foresee, and a lot of breakthroughs where people suddenly find there’s a simple way to do something that everybody hitherto has thought to be far too difficult.

# A Calculational Proof of the Handshaking Lemma

UPDATE (2011/09/20): This post was superseded by An improved proof of the handshaking lemma.

In graph theory, the degree of a vertex $A$, $\fapp{d}{A}$, is the number of edges incident with the vertex $A$, counting loops twice. So, considering Graph 0 below, we have $\fapp{d}{A}=3$, $\fapp{d}{B}=3$, $\fapp{d}{C}=1$, $\fapp{d}{D}=3$, and $\fapp{d}{E}=2$.

Graph 0: Example of an undirected graph with five nodes

A well-known property is that every undirected graph contains an even number of vertices with odd degree. The result first appeared in Euler’s 1736 paper on the Seven Bridges of Königsberg and is also known as the handshaking lemma (that’s because another way of formulating the property is that the number of people that have shaken hands an odd number of times is even).

As we can easily verify, Graph 0 satisfies this property. There are four vertices with odd degree ($A$,$B$, $C$, and $D$), and 4, of course, is an even number.

Although the proof of this property is simple, I have never seen it proved in a calculational and goal-oriented way. My aim with this post is to show you a development of a goal-oriented proof.

# Multiples in the Fibonacci series

I found the following problem on K. Rustan M. Leino’s puzzles page:

[Carroll Morgan told me this puzzle.]

Prove that for any positive K, every Kth number in the Fibonacci sequence is a multiple of the Kth number in the Fibonacci sequence.

More formally, for any natural number n, let F(n) denote Fibonacci number n. That is, F(0) = 0, F(1) = 1, and F(n+2) = F(n+1) + F(n). Prove that for any positive K and natural n, F(n*K) is a multiple of F(K).

This problem caught my attention, because it looks like a good example for using a result that I have derived last year. My result gives a reasonable sufficient condition for showing that a function distributes over the greatest common divisor and shows that the Fibonacci function satisfies the condition.

In fact, using the property that the Fibonacci function distributes over the greatest common divisor, we can solve this problem very easily. Using $\fapp{fib}{n}$ to denote the Fibonacci number $n$, $m{\nabla}n$ to denote the greatest common divisor of $m$ and $n$, and $\setminus$ to denote the division relation, a possible proof is:

$\beginproof \pexp{\text{\fapp{fib}{(n{\times}k)} is a multiple of \fapp{fib}{k}}} \hint{=}{definition} \pexp{\fapp{fib}{k} \setminus \fapp{fib}{(n{\times}k)}} \hint{=}{rewrite in terms of \nabla} \pexp{\fapp{fib}{k} ~\nabla~ \fapp{fib}{(n{\times}k)} ~=~ \fapp{fib}{k}} \hint{=}{fib distributes over \nabla} \pexp{\fapp{fib}{(k{\nabla}(n{\times}k))} = \fapp{fib}{k}} \hint{=}{k{\nabla}(n{\times}k) = k} \pexp{\fapp{fib}{k} = \fapp{fib}{k}} \hint{=}{reflexivity} \pexp{true~~.} \endproof$

The crucial step is clearly the one where we apply the distributivity property. Distributivity properties are very important, because they allow us to rewrite expressions in a way that prioritizes the function that has the most relevant properties. In the example above we could not simplify $\fapp{fib}{k}$ nor $\fapp{fib}{(n{\times}k)}$, but applying the distributivity property prioritised the $\nabla$ operator — and we know how to simplify $k{\nabla}(n{\times}k)$. Furthermore, in practice, distributivity properties reduce to simple syntactic manipulations, thus reducing the introduction of error and simplifying the verification of our arguments.

(Now that I think about it, perhaps it would be a good idea to write a note on distributivity properties, summarizing their importance and their relation with symbol dynamics.)