Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Verified Concurrent Programmes: Theory, Tools and Experiments

11-13 June 2013, Microsoft Research, 21 Station Road, Cambridge, CB1 2FB UK

 

Program Co-Chairs:

  • Peter O’Hearn
  • Tony Hoare
  • Mike Gordon 

Sponsors:

  • Microsoft Research (Cambridge); EPSRC (Resource Reasoning Programme Grant)
  • Cambridge University Computer Laboratory

Objectives

We aim to stimulate and focus interest in the development, testing, analysis and verification of concurrent programs, and to advance the state of the art in relevant theories, tools and experiments. This is to be achieved by exchange of news and views, experiences and speculations, plans and prospects among world-leading experts, specialising in various aspects of the problem.

Themes

  • Concurrent program verification (Peter O’Hearn)
  • Concurrent program analysis (Andrey Ribalchenko)
  • Concurrent software engineering tools (Ernie Cohen)
  • Concurrent models of memory (Peter Sewell)
  • Concurrent models in Biology (Jasmin Fisher)

On each theme there will be a scheduled keynote address, with speaker named above. There will also be well-equipped exhibition booths, at which relevant tools will be demonstrated during the ample periods of unscheduled time.

9.30am Tuesday 11th June - Andrey Rybalchenko
Verification of Concurrent Programs by Solving Horn Clauses

We revisit several proof rules for the verification of concurrent programs from the constraint solving perspective.

This perspective yields a uniform approach not only to different proof rules, but can also accommodate proving various kinds of temporal properties. We will also outline difficulties that arise when solving constraints generated for concurrent programs and possible solver optimisations.

Joint work with Ashutosh Gupta, Nuno P. Lopes, and Corneliu Popeea.

2.00pm Tuesday 11th June - Jasmin Fisher
(Con)Current Biology

Biological systems are extremely complex reactive systems. They operate as highly concurrent programs with many entities running in parallel and communicating with each other under various environmental conditions. Understanding how living systems operate in harmony and precision, and how their orchestration is disrupted in diseased states, are key questions in biological and medical research. The complex nature of biological computation requires computer science to adapt some of its well accepted notions of computation. In this talk, I will survey some of these new notions, particularly those relating to concurrency. I will introduce bounded asynchrony, a notion of concurrency tailored to the modelling of biological cell-cell interactions that led to the identification of a molecular-synchronization mechanism operating during cell fate determination. Bounded asynchrony restricts the difference (in terms of number of steps) between communicating processes. I will also introduce dynamic reactive modules (DRM) a language for modelling cell division and cell death, two critical features for biological modelling. DRM define discrete state-transition systems that communicate via shared variables (and not via messages), and uniquely add new computation power as new threads are spawned. These new computational notions, devised for modeling biology, could also be useful for modeling and development of embedded systems, mobile networks, and other applications critically dependent on timing. Moreover, these examples demonstrate how biological concepts are contributing to computer science, and at the same time, shifting current biology to a more computational science, cultivating tight collaborations between experimentalists, computational biologists and computer scientists.

Joint work with Tom Henzinger, Moshe Vardi, Nir Piterman, Dejan Nickovic, Anmol Singh, and Maria Mateescu.

9.30am Wednesday 12th June - Peter Sewell
Minding the Gaps

There are big gaps between the concurrency semantics that we'd like to assume for analysis and verification and the behaviour of actual machines and programming languages when running highly concurrent code. We've made some progress in understanding the latter in the last few years, in work by Alglave, Batty, Maranget, Memarian, Owens, Sarkar, Williams, Zappa Nardelli, and others. In this talk I'll summarise what's now understood and what remains murky, and ask how we can start to build verification techniques that take this into account. I'll also discuss using these precise semantic models to close the cultural gaps between hardware vendors, language implementers, and theorists.

http://www.cl.cam.ac.uk/users/pes20/weakmemory

2.00pm Wednesday 12th June - Ernie Cohen
VCC - An Apology

Seven years ago, we started an ambitious project to verify the functional correctness of industrial software. The most important outputs were VCC (a verifier for concurrent C code) and its accompanying methodology. I’ll explain the rationale behind our design decisions, and some of their unintended consequences

9.30am Thursday 13th June - Tony Hoare
Laws of Programming with Concurrency

The talk starts with a summary of the familiar algebraic properties of choice in a program and of both sequential and concurrent composition. These properties validate the proof rules of Hoare logic (augmented by concurrency), as well as the transition rules of a process algebra (augmented by sequential composition). The laws are then proved true of a simple causal model of the behaviour of programs when executed. The model is generic, and can be particularised to different programming languages, and different notions of correctness. This theoretical result gives hope that any Software Engineering tool that is based on the laws can safely interwork with any other such tool.