Formal derivation of concurrent algorithms
Speaker: Brijesh Dongol, ITEE
When: 2005-06-10 10:00:00
Venue: 78-420
Host: Ian Hayes
Abstract:In this seminar, we discuss the method of Feijen and van Gasteren
for deriving concurrent programs, a newly developed logic of
progress for the Owicki-Gries formalism and future directions
regarding formal derivation of concurrent non-blocking data
structures. The logic of Owicki-Gries is a popular choice for the
formal verification of concurrent programs. Recently, Feijen and van
Gasteren have described how the logic of Owicki-Gries can be used as
a basis for their construction. Unfortunately, Owicki-Gries' logic
does not have a way of reasoning about progress. This fact is
reflected in Feijen-van Gasteren, as only safety concerns are
formally addressed.
We have recently developed a logic of progress for the Owicki-Gries
formalism. Labelled statements, program counters, and modified wlp
rules have been introduced, which allow us to adapt the leads-to
rules of UNITY to fit the Owicki-Gries formalism. The main benefit
of this is that derivations that give equal consideration to both
safety and progress are now possible.
The algorithms derived using the approach make atomicity assumptions
which implementation languages such as Java cannot
guarantee. Atomicity can be simulated using locks and blocking
mechanisms, but this introduces other problems such as deadlock,
poor efficiency and priority inversion. Another approach to
synchronisation is via non-blocking algorithms where atomic
non-blocking compare-and-swap primitives are used to achieve
correctness. This solves many of the problems regarding lock-based
algorithms, and tends to be more practical. Our focus is on the
derivation of non-blocking algorithms and their progress properties.
Biography:(biography unavailable)
Type: Ph.D confirmation
Contact:Ian Hayes, seminar host (ianh@itee.uq.edu.au)
or Guido Governatori (ITEE seminar co-ordinator)
(guido@itee.uq.edu.au)