Compositional Reasoning for Computer ProgramsMathematical reasoning has the potential to provide much needed guarantees about what computer programs do. It is important that the reasoning is compositional. Compositional reasoning means that we consider each program component (such as a program fragment, a library function or a concurrent thread) in isolation without having knowledge of the program context (such as the rest of the code, a client program using the library or the environment thread) in which it will be placed. It means that the reasoning scales and can therefore be applied to industrial code. This talk presents a mathematical theory of views for reasoning compositionally about sequential and concurrent programs. A program’s view provides abstract partial knowledge of the current state of the machine and the program’s right to change that state. Views can be composed as long as their knowledge and rights do not conflict. The theory of views is simple but highly applicable; traditional concurrent reasoning methods such as rely-guarantee and Owicki-Gries, modern methods centering on separation logic, and many type theories can all be seen to fit within this theory. In this talk I will demonstrate these ideas by reasoning about simple algorithms including the Sieve of Eratosthenes, fine-grained list-locking algorithms and concurrent tree algorithms.
The venue is the London Mathematical Society, De Morgan 57-58 Russell Square, London WC1B 4HS
Refreshments will be available from 5.30pm. The seminar is free of charge and open to everyone. If you would like to attend, please register at computerscience@lms.ac.uk.