Mechanical Verification of Non-blocking Concurrent Algorithms
Speaker: Dr Lindsay Groves, School of Mathematical and Computing Sciences, Victoria University of Wellington,
When: 2003-07-03 10:00:00
Venue: 78-420
Host: Ian Hayes
Abstract:Non-blocking algorithms allow concurrent access to shared data
structures without using any form of locking or mutual exclusion,
and are considered to be important for the development of large
scale concurrent and distributed systems. This talk will outline
our work on mechanical verification of a non-blocking implementation
of double-ended queues, using a sophisticated doubly-linked list
representation. The verification is based on simulation between
Input Output Automata, and is being mechanised using PVS. Our
initial proof attempt revealed a subtle bug in a previously
published algorithm, and the proof of the corrected algorithm
requires a combination of forward and backward simulations. The
talk will provide an overview of the project, and will not assume
familiarity with the particular formalism used.
This is join work with Simon Doherty and Ray Nickson (School of
Mathematical and Computing Sciences, Victoria University of
Wellington), and Mark Moir (Scalable Synchronization Research Group,
Sun Microsystems Laboratories, Boston).
Biography:(biography unavailable)
Type: ITEE Systems and Software Engineering Seminar
Contact:Ian Hayes, seminar host (Ian.Hayes@itee.uq.edu.au)
or Guido Governatori (ITEE seminar co-ordinator)
(guido@itee.uq.edu.au)