Peter Landin Annual Semantics Seminar: 6 December 2010, 5pm, Covent Garden, London -- speaker: Prof. John Reynolds

Peter Landin Annual Semantics Seminar

6 December 2010

BCS London Offices

First Floor, The Davidson Building
5 Southampton Street
London
WC2E 7HA

http://www.bcs.org/upload/pdf/london-office-guide.pdf

Introduction
----------------

Peter Landin (1930--2009) was a pioneer whose ideas underpin modern computing.
In the the 1950s and 1960s, Landin showed that programs could be defined in
terms of mathematical functions, translated into functional expressions in
the lambda calculus, and their meaning calculated with an abstract mathematical
machine. Compiler writers and designers of modern-day programming languages
alike owe much to Landin's pioneering work.

Each year, a leading figure in the area of semantics will pay tribute
to Landin's contribution to computing through a public seminar. The first
such seminar will be delivered by Professor John Reynolds (Queen Mary,
University of London, Imperial College and Carnegie Mellon University).
Professor Cliff Jones (Newcastle University) will introduce and chair
the seminar.

Immediately before the seminar, a rare film of a lecture Peter Landin gave at
the Science Museum in 2001 will be replayed.

Programme
-----------------

5pm Coffee
5:25pm Welcome and Introduction (Prof. Cliff Jones)
5.35pm Film of Peter Landin talk at the Science Museum, 2001
5.55pm Introduction to seminar
6pm Peter Landin Semantics Seminar:

Toward a Grainless Semantics for Shared-Variable Concurrency
(Prof. John Reynolds)

7.15pm Close (Prof. Cliff Jones)
7.20pm - 8.20pm Drinks Reception

Registration
-----------------

If you would like to attend, please email Paul.Boca@googlemail.com by
3 December.

Seminar details
-----------------------

TOWARD A GRAINLESS SEMANTICS FOR SHARED-VARIABLE CONCURRENCY

Prof. John C. Reynolds
Queen Mary, University of London
Imperial College
Carnegie Mellon University

Conventional semantics for shared-variable concurrency suffers from the
"grain of time" problem, i.e., the necessity of specifying a default
level of atomicity. We propose a semantics that avoids such a choice
by regarding all interference that is not controlled by explicit
synchronization as catastrophic. It is based on three principles:

- Operations have duration and can overlap one another
during execution.

- If two overlapping operations touch the same location, the
meaning of the program execution is ``wrong''.

- If, from a given starting state, execution of a program can
give "wrong", then no other possibilities need be considered.

In our current approach, instead of trace sets, we use trace trees, in
which we separate nondeterminism and branching.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

tl;dr

so that's an approach to races, but doesn't rule out deadlock?

Deadlock isn't modelled by wrong...

...it's modeled by infinite traces that make no progress. Note that this isn't a program analysis or verification methodology; it's a semantics.

Presently, most approaches to giving semantics to current languages require you to specify what the atomic operations are. (This is the "grain size".) The trouble with this is that it ties the specification of a language too closely to the hardware -- Intel and ARM can and do change their mind about what you can consider atomic as processor technology evolves. Furthermore, specifying grain sizes can force you to nail down implementation details that you may want to keep open (for instance, whether implementations box floats).

In informal prose specs (such as in the POSIX threads), people sometimes say that the language's semantics are only defined for data-race-free programs. The idea is that if a program ensures that all possible concurrent accesses are guarded by synchronization, then it doesn't matter what operations are atomic. And if the language deliberately doesn't specify what racy programs do, then whatever the hardware actually does is okay.

This is a nice idea, but making it both mathematical and tractable is quite tricky -- I know John has been working on it for a number of years.