Non-blocking concurrent algorithms, such as the Herlihy-Wing queue, allow processes to run concurrently without stopping. The verification of such algorithms are particularly challenging and interesting. Linearisability is a well-known correctness condition for concurrent algorithms. For algorithms such as the Herlihy-Wing queue, establishing whether or not linearisability holds is difficult, as it depends on the future behaviour of the components. A recent approach was devised which allows such algorithms to be verified by considering the previous behaviour of components, instead of the future.
This project will investigate this technique further, by applying the ideas to model checking. The goal will be to model an algorithm such as the Herlihy-Wing queue or other similar problems in a model checking input language and then devise appropriate verification conditions, which utilise the idea of relying on previous states on the trace. The project will evaluate the effectiveness of the approach on different algorithms.
Requirements: The project can be adapted to 12 or 24 unit projects, including Honours and Masters projects. Students should have an interest and some understanding of formal methods and logic concepts. Feel free to arrange a chat with Nisansala Yatapanage (nisansala.yatapanage@anu.edu.au) to discuss your suitability and the details of the project, to decide whether it would interest you.