Scheme: Industry Fellowship
Organisation: University of York
Dates: Sep 2015-Sep 2017
Summary: Since its inception seventy years ago, computer science has revolutionised many aspects of modern life. From scientific research, business, engineering, entertainment, to interpersonal communication, it's hard to think of an unaffected area. Underlying this revolution is *Moore's Law*: since 1960, computing power has roughly doubled every eighteen months. This has driven an extraordinary expansion in what is possible using computers. A few short years can bring a formerly intractable problem within the reach of cheap consumer devices.
Now, however, computing is changing. Limits inherent to the physics of hardware mean that over the last decade the power of an individual processor has plateaued. Instead, modern computers are made up of many processors (`cores') that collaborate on shared tasks. Modern software has to marshal work between cores in a way that is efficient, fair, and bug-free. At the heart of all concurrent systems, handling coordination between cores, are special high-performance *concurrent algorithms*.
I work on verifying these algorithms; that is, guaranteeing they are correct through rigorous applied mathematics. Concurrent algorithms are critical system components, yet the interactions between cores places them amongst the trickiest computing artefacts ever developed. My research is aimed at developing new verification techniques and transferring them to real-world software practice.
The focus of my work is a property called *liveness*. Roughly, an algorithm is live if it is guaranteed to keep doing work -- conversely it is *safe* if it never does anything bad. In the complex dance between interacting cores, un-live algorithms can accidentally block each other's progress, leading them to squander the benefits of concurrency. To do this, I am working on a tool called Starling which can automatically check that software is correct and bug free.