ITEE seminar: Dr Lindsay Groves, 10.00AM, Thu 03 Jul 2003

Mechanical Verification of Non-blocking Concurrent Algorithms

Speaker: Dr Lindsay Groves, School of Mathematical and Computing Sciences, Victoria University of Wellington, New Zealand

When: 10.00AM, Thursday 03 Jul 2003

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)

ITEE seminar web page: http://www.itee.uq.edu.au/~seminar

[All seminars]