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
by 5 December 2005. Pre-registration is required, as security
at the BCS Offices is tight Pre-registration is required, as security at the BCS Offices
is tight.
