[Apologies if you receive multiple copies of this announcement]
BCS-FACS Evening Seminar
Joint event with the BCS Advanced Programming Group
Why separation logic is the bee's knees, and why you should care
Professor Richard Bornat
Middlesex University
8 December 2005
start time: 6pm
BCS London Offices
First Floor
The Davidson Building
5 Southampton Street
London WC2E 7HA
Long ago (in 1968, or maybe it was 1965) E.W. Dijkstra sorted out
concurrency _so far as programming methodology is concerned_. He laid
down conditions of what we now recognise as _separation_ between
threads (processes) and their associated variables, and conditions
for action on shared variables. But it remained _methodology_: that
is, pious words without formal content. Nobody, so far, has been able
to build a programming tool, like a compiler or an IDE, which can
help programmers write concurrent programs.
Recent developments have made things much worse. The inept, one could
reasonably say idiotic, introduction of concurrent programming
primitives to the masses through Java has collided with the now
almost universal use of pointers (aka references) in programming.
Pointers are another problem. Hoare logic, our only means of talking
about programs precisely up to now, can't really do pointers. If you
don't see the problem, here's a fact to choke on: every Swing Java
program (that is, every Java program with a GUI, which is every Java
program) runs 8 to 14 threads that _the programmer has no notion of_.
It's impossible to tell which thread you are in in a Java program,
and _it matters_: some program actions work in some threads, and
others simply and silently do not. Deadlock is a frequent problem.
Well, folks, there is good news. Separation logic is a reworking of
Hoare logic which deals with pointers, and concurrency, and pointers-
and-concurrency. We can give _completely formal_ descriptions of
popular and intricate concurrent algorithms and even of some hoary
old concurrency chestnuts. We have not yet built a tool because we
are at the beginning of the business of overturning computer science.
But overturned it will be (again!) and this time (again!) it will
matter.
If you are healthily cynical of the chances of a version of Hoare
logic making a blind bit of difference to anything at all, given its
spectacular failure to do _anything_ much that was worthwhile in its
heyday in the 1970s and 1980s, bring your scepticism along to the
meeting and I shall demolish it.
Oh, and did I say the talk would be funny? It will be.
Refreshments will be served from 5.15pm
The seminar is free of charge and open to everyone. If you would
like to attend, please email Paul Boca[[log in to unmask]] by
>>> 5 December 2005 <<<. Pre-registration is required, as security
at the BCS Offices is tight.
Location of venue:
http://www.bcs.org/NR/rdonlyres/B5872B38-3FBB-46E8-9CE7-6F43212E1198/0/londonss.jpg
BCS Advanced programming website:
http://www.bcs.org.uk/siggroup/advprog/
BCS-FACS website:
http://www.bcs-facs.org
BCS-FACS Evening Seminars website:
http://www.bcs-facs.org/events/EveningSeminars
