Abstract
Establishing adequacy of implementations of software transactional memory (STM) is notoriously non-trivial. Above all, it is difficult to determine the desirable notion of correctness and to define it mathematically. But describing an implementation of STM in a form amenable to mathematical scrutiny and proving it correct with respect to the chosen notion of correctness are also subtle and error-prone tasks.
In this talk, I describe an experiment in this direction. We defined a particular STM implementation for the While language with parallelism and nested transactions in terms of a transactional small-step semantics, stated Guerraoui and Kapalka's opacity for this implementation in terms of simulability of runs in the transactional semantics by runs in a sequential semantics and vice versa for a suitable notion of agreement between configurations in the two semantics, and proved that it holds. We formalized the whole development in the dependently typed programming language Agda.
(Joint work with Andri Saar.)
Short bio
Tarmo Uustalu is a leading researcher at the Institute of Cybernetics in Tallinn, Estonia. He received his PhD degree from the Royal Institute of Technology in Stockholm, Sweden, was a postdoc at the University of Minho in Braga, Portugal. His research interests are in structural proof theory and type theory, functional programming, categorical semantics, program logics and type systems, program verification and analysis. He is the leader of EXCS, the Estonian national center of excellence in computer science 2008-2015, and the general chair of ETAPS 2012.
Resources
This will be shown to users with no Flash or Javascript.
|
