Lindsay's Concurrency Projects


Most work on concurrency has been based on the use of mechanisms such as locks and critical regions to ensure that concurrent processes don't interfere with each other during crucial updates to shared data. This approach has severe limitations which become prohibitive in large scale concurrent systems. An alternative being explored by various researchers is the use of lock-free or non-blocking algorithms which do not use locks, but instead rely only on the use of hardware primitives such as Compare and Swap to atomically test and update shared variables. Such algorithms are very subtle and notoriously hard to get right, so it is important to be able to formally verify their correctness. I am involved in work with Sun Microsystems, Boston, aimed at developing techniques for formally verifying non-blocking algorithms, especially non-blocking implementations of shared data structures such as queues. Our approach is based on Input-Output Autoamat (developed by Nancy Lyndh at MIT) and the PVS theorem prover (developed at SRI International).

The following are some examples of possible projects in this area:

This is joint work with Sun Microsystems, Boston, funded by Sun.