Northern Concurrency Workshop

Wednesday, 25 November 2009

Northern Concurrency Workshop

I am just back from the Northern Concurrency Workshop, which was organised by Joey Coleman at Newcastle University.

It was a really, really fun event. The talks were largely dominated by separation logic, which I am only just getting into, so I would say I understood less than 30% of the speakers’ words. Nevertheless, most of the other 70% sounded tantalisingly interesting even though it was over my head! I gave a more practical talk on applying model checking to multicore programs with DMA.

What I liked about the workshop is that despite some pretty big names in concurrency theory being present, the atmosphere was very relaxed. There was a lot of friendly discussion; it really did have the feel of a workshop, rather than just a series of talks.

The standout presentation for me was “Verifying malloc”, given by John Wickerson from University of Cambridge. It was really well explained, and so obviously of practical importance.

It is expected that there will be another one in Cambridge in September 2010, so I look forward to that!

Posted by Ally Donaldson at 11:19 No comments:

Having trouble getting the Murphi verifier to compile?

Tuesday, 1 December 2009

Having trouble getting the Murphi verifier to compile?
I’ve spent quite a bit of time today getting the Murphi verification tool to compile. I thought I’d write down how I did it in case this is of use to others.
First, I found that the version here did not compile due to flex/yacc errors. I don’t know how to solve these, but luckily the version here (which has the same version number!) didn’t present those problems.

Instead, it gave me this error:
error.C:58:20: error: stream.h: No such file or directory
In file included from mu.h:441,
from error.C:56:

It seems that stream.h comes from the days before C++ include files didn’t finish with “.h”. This header file has been deprecated for some time, but it seems that with gcc 4.3.3, which I have, it is not even provided.

It turns out that GCC 4.2.2 comes with a folder called “backward”, that has “stream.h” and related header files. Armed with these files (which I provide online), I was able to get Murphi to compile OK by changing one line in the makefile from:

CFLAGS = -O4 # options for g++


CFLAGS = -O4 -I /home/scratch/gcc4.2.2_backward/backward # options for g++

(this is where I put the “backward” files).

Happy Murphi-ing!

Posted by Ally Donaldson at 14:31 No comments:

Academic Responsibilities

Doctoral supervision

With Codeplay, I am recruiting for a Ph.D. student to work at Imperial College, London, on Language and Compiler Support for Efficient Programming of Heterogeneous Multi-core Systems. If you’re interested in this project then more details are available.

I am industrial supervisor for an Eng.D. and a Ph.D. student:

Haitham Fattah: Automatic parallelisation of C++ applications using FPGAs. Academic supervisor: Wim Vanderbauwhede. Institution: Institute for System Level Integration (Eng.D.)
Paul Kier: Multi-core compilers for scientific computing. Academic supervisor: Paul Cockshott. Institution: University of Glasgow (Ph.D.)
Reviewing and event organisation

I have reviewed papers for the following international journals:

ACM Transactions on Design Automation of Electronic Systems
Acta Informatica

The Cell Processor: a Compiler Challenge. Guest lecture for Compilers honours course at the University of Glasgow, 5th February 2008.
The Cell Processor: a Compiler Challenge. Guest lecture for Advances in Programming Languages honours course at the University of Edinburgh, 10th March 2008.
Abstract Data Types and Binary Trees. Lectures delivered as part of Data Structures and Algorithms 2nd year course at the University of Glasgow, October 2006.


Tutor for CS1P module (introduction to imperative programming, problem solving and design), 1st year course at the University of Glasgow, 2003-2006 (also demonstrator 2002-2003)
Tutor for CS1Q module (introduction to HCI, databases and systems), 1st year course at the University of Glasgow, 2003-2006 (also demonstrator 2002-2003)
Demonstrator for Introduction to C, 3rd year course at the University of Glasgow, 2003-2006

Tutor on the Top-up programme, organised by the University of Glasgow as part of the GOALS project.
Demonstrator for Royal Institute of Great Britian mathematics master-classes for secondary school pupils, hosted by the Department of Mathematics at the University of Glasgow.