Why separation logic is the bee's knees, and why you should care

Advanced Programming and Formal Aspects of Computing Specialist Group event

Thursday 8th December 2005, 6.00 pm

The Davidson Building, 5 Southampton Street, London, WC2 7HA. The nearest underground station is Covent Garden.

Professor Richard Bornat, Middlesex University.

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.

Free, but to gain admission please e-mail your name to our Vice-Chairman, Dr Frank Martin, at - f.martin@londonmet.ac.uk.

CPD Value:
Half unit

View the slides for this event (PDF - 449kb)