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:

• Construct a tool to animate concurrent algorithms, allowing the user to step through a concurrent execution observing the program state, or to perform a random execution to show typical behaviour.

• Experiment with recently developed tools for analysing concurrent programs so see how well they perform in analysing non-blocking algoriths.

• Compare different concurrent algorithms that have been proposed for a particular task and attempt to improve on them. A suitable task would be non-blocking implementations of priority queues.

• Attempt to verify some published concurrent algorithm(s).

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