Verifying Concurrent Data Structures for Trustworthy Systems

This project aims to develop a framework for specifying and verifying concurrent data structures running on hardware with weak memory in the proof assistant Isabelle/HOL, focussing on the inclusion of weak memory models and the needs of a multicore extension of seL4. The main issues over the earlier sequential verification of the uniprocessor kernel are handling parallel execution of the kernel itself on multiple processors, and the complications that arise due to the weak memory models, which give rise to out-of-order execution. The project also considers concurrent user software running on arbitrary Oss.The specification language to be used for specifying and verification should be based on existing technology, such as COMPLX 1 and the language used in 2. CDSs include both blocking (locking) data structures and non-blocking structures, such as read-copy-update data structures and locking mechanisms, such as ticket lock and CLH lock.