The aim of the workshop is to bring together concurrency experts and researchers working on program analysis/verification. The goal of the workshop is to understand what properties of concurrent algorithms should be verified (e.g. linearizability, lock-freedom), how important they are in practice, and to what extent can these properties be verified automatically with existing tools.
The algorithm designers will benefit by learning what tools exist, and how useful would these tools be in their research. Similarly the verification researchers should get more intuition about concurrency, weak memory models, etc., and will find out what properties do the algorithm designers really care about.
We aim to compile a list of the algorithms that have been verified already and a set of challenge verification problems.
Topics of interest include:
· Techniques for verifying safety properties, such as memory safety, absence of memory leaks, linearizability, etc.
· Techniques for verifying liveness properties such as lock-freedom, wait-freedom, absence of starvation, etc.
· Techniques for dealing with relaxed memory models
· Alternative correctness properties
We are particularly interested in:
· Automatic or semi-automatic verifications of blocking and non-blocking concurrent algorithms
· Challenge verification problems
· Feedback on how tools can assist during the development of a new algorithms
· Hagit Attiya on concurrent algorithms
· Peter OHearn on concurrent separation logic
· Shaz Qadeer on model checking
· Eran Yahav on shape analysis
· Mooly Sagiv, Tel-Aviv University, email: msagiv [at] acm [dot] org
· Viktor Vafeiadis, Microsoft Research Cambridge, email: viktorva [at] microsoft [dot] com
Participation to the workshop is by invitation only. If you are interested in attending, please email the workshop organisers as soon as possible.
· Hagit Attiya. A mile-high view of concurrent algorithms. [PPT]
· Peter OHearn. Concurrent separation logic. [PDF]
· Matthew Parkinson. Marriage of rely/guarantee and separation logic. [PDF]
· Shaz Qadeer. Verifying concurrent programs by model checking. [PPTX] [PDF]
· Eran Yahav. Shape analysis for concurrent programs. [PPTX]
· Richard Banach. Protocol-centric verification of isolated and not-so-isolated protocols. [PDF]
· Sebastian Burckhardt. Checking memory model safety of programs. [PPTX] [PPT]
· Tim Harris. Five challenges in defining the semantics of atomic blocks. [PPTX] [PDF]
· Alexey Gotsman. Proving wait-freedom, lock-freedom, obstruction-freedom.
· Roman Manevich. Shape analysis for fine-grained concurrency. [PPT]
· Maged Michael. Experiences developing concurrent algorithms. [PPT]
· Cosmin Oancea. Dynamic analysis for optimising software thread-level speculation. [PPT]
· Jaroslav Sevcik. Validity of program transformations in the Java memory model. [PDF]
· Vasu Singh. Model checking transactional memories. [PPT]
· Armando Solar-Lezama & Chris Jones. Sketching concurrent data structures. [PDF]
· Philippas Tsigas. Lock-free data sharing. [PDF]
· Viktor Vafeiadis. Shape-value abstraction for verifying linearizability. [PPTX] [PDF]
· Martin Vechev. Computer-assisted construction of linearizable algorithms. [PPT]
Thursday, 1st May
2008.
|
08:30 09:00 |
Tea/coffee |
|
09:00 10:30 |
Introduction Hagit Attiya A mile-high view of concurrent algorithms (70min) |
|
10:30 11:00 |
Tea/coffee |
|
11:00 12:30 |
Peter OHearn Concurrent separation logic (60min) Matthew Parkinson Marriage of rely/guarantee and separation logic (30min) |
|
12:30 13:30 |
Lunch |
|
13:30 15:30 |
Shaz Qadeer Model checking (60min) Eran Yahav Shape analysis for concurrent programs (60min) |
|
15:30 16:00 |
Tea/coffee |
|
16:00 18:00 |
Viktor Vafeiadis Shape-value abstraction for verifying linearizability (20min) Maged Michael Experiences developing concurrent algorithms (20min) Discussion |
|
19:00 |
Drinks reception & dinner at New Hall,
Cambridge |
Friday, 2nd May
2008.
|
08:30 09:00 |
Tea/coffee |
|
09:00 10:30 |
Philippas Tsigas Lock-free data sharing (20min) Richard Banach Protocol-centric verification of isolated and not-so-isolated protocols (20min) Vasu Singh Model checking transactional memories (20min) Tim Harris Challenges in defining the semantics of STM (20min) |
|
10:30 11:00 |
Tea/coffee |
|
11:00 12:30 |
Peter Sewell Formal semantics of weak memory models (20min) Jaroslav Sevcik Validity of program transformations in the Java memory model (20min) Sebastian Burckhardt Checking memory model safety of programs (20min) Discussion |
|
12:30 13:30 |
Lunch |
|
13:30 15:30 |
Alexey Gotsman Proving wait-freedom, lock-freedom, obstruction-freedom (20min) Roman Manevich HeDec (20min) Martin Vechev Computer-assisted construction of linearizable algorithms (20min) Armando Solar-Lezama/Chris Jones Sketching concurrent data structures (20min) Cosmin Oancea Dynamic analysis for optimising software thread-level speculation (20min) |
|
15:30 16:00 |
Tea/coffee |
|
16:00 17:30 |
Discussion & concluding remarks |
Topics for discussion:
· What correctness conditions should be verified? How important are they?
· What kinds of tools do concurrent algorithm designers want? What about developers?
· How long is one willing to spend on verifying/testing a new concurrent algorithm?
· How to reason about programs executing in a weak memory model?
· Challenge problems (e.g. algorithms to be verified, bugs to be found, etc.)
·
Address:
Microsoft Research Cambridge
Roger Needham Building
7 JJ Thompson Avenue
Cambridge CB3 0FD
UK