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++

to

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
Constraints
Teaching
Lecturing:

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.

Tutoring:

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
Miscellaneous:

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.

Publications and Talks

All the downloadable papers below are in pdf format. In some cases the presentations associated with conference/workshop papers are available in power point format.

If you have trouble downloading any of these papers, or are keen to see one of the papers currently under review then feel free to email me.

Submitted articles
A. Lokhmotov, A.F. Donaldson, P. Keir, A. Richards Parallel Scopes. Submitted November 2009 to International Journal of Parallel Programming.
A.F. Donaldson, S.J. Gay Type Inference and Strong Static Type Checking for Promela. Submitted September 2009 to Science of Computer Programming.
Thesis
A.F. Donaldson Automatic Techniques for Detecting and Exploiting Symmetry in Model Checking. PhD Thesis, University of Glasgow. June 2007.
Edited volumes
A.F. Donaldson, P. Gregory and K. Petrie (Eds.) Symmetry in Constraint Satisfaction Problems, Part III of F. Benhamou, N. Jussien and B. O’Sullivan (Eds.): Trends in Constraint Programming. ISTE, 2007.
A.F. Donaldson, P. Gregory and K. Petrie (Eds.) Proceedings of the 6th International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon’06), Nantes, France, September 2006.
A.F. Donaldson and P. Gregory (Eds.) Proceedings of Almost-Symmetry in Search, a SymNet funded workshop, New Lanark, January 2005. University of Glasgow, Department of Computing Science Technical Report No. TR-2005-201, May 2005.
Papers published in journals or conference/workshop proceedings
T. Wahl, A.F. Donaldson Replication and Abstraction: Symmetry in Automated Formal Verification. Symmetry, 2(2):799-847, 2010.
A.F. Donaldson, D. Kroening, P. Ruemmer Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors. To appear in Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’10), Paphos, Cyprus, March 2010. Lecture Notes in Computer Science. In November, I gave a talk on this work at the Northern Concurrency Workshop, slides are available.
A.F. Donaldson, U. Dolinsky, A. Richards, G. Russell Automatic Offloading of C++ for the Cell BE Processor: a Case Study Using Offload. In Proceedings of the 2010 International Workshop on Multi-Core Computing Systems (MuCoCoS’10), Krakow, Poland, February 2010, pages 901-906. IEEE Computer Society.
P. Cooper, U. Dolinsky, A.F. Donaldson, A. Richards, C. Riley, G. Russell Offload – Automating Code Migration to Heterogeneous Multicore Systems. In Proceedings of the 5th International Conference on High Performance and Embedded Architectures and Compilers (HiPEAC’10), Pisa, Italy, January 2010. Lecture Notes in Computer Science 5952:337-352.
A.F. Donaldson, A. Miller On the Constructive Orbit Problem. Annals of Mathematics and Artificial Intelligence, published online December 2009.
A.F. Donaldson, A. Miller, D. Parker Language-level Symmetry Reduction for Probabilistic Model Checking. In Proceedings of the 6th International Conference on the Quantitative Evaluation of Systems (QEST’09), Budapest, Hungary, September 2009, pages 289-298. IEEE Computer Society. Extended version including proofs.
A.F. Donaldson Vector Symmetry Reduction. In M. Calder and A. Miller (Eds.): Proceedings of the 8th International Workshop on Automated Verification of Critical Systems (AVoCS’08), Glasgow, UK, October 2008. Electronic Notes in Theoretical Computer Science 250(2):3-18.
L. Howes, A. Lokhmotov, A.F. Donaldson, P.H.J. Kelly Towards Metaprogramming for Parallel Systems on a Chip. In Proceedings of the 3rd Workshop on Highly Parallel Processing on a Chip (HPPC’09), Delft, The Netherlands, August 2009. To appear in Lecture Notes in Computer Science.
L. Howes, A. Lokhmotov, A.F. Donaldson, P.H.J. Kelly Deriving Efficient Data Movement From Decoupled Access/Execute Specifications. In André Seznec et al. (Eds.): Proceedings of the 4th International Conference on High Performance and Embedded Architectures and Compilers (HiPEAC’09), Pahpos, Cyprus, January 2009. Lecture Notes in Computer Science 5409:168-182.
A.F. Donaldson, A. Miller Automatic Symmetry Detection for Promela. Journal of Automated Reasoning, 41(3-4):251-293, 2008.
G. Russell, A.F. Donaldson, P. Sheppard Tackling Online Game Development Problems with a Novel Network Scripting Language. In Proceedings of the 7th ACM SIGCOMM Workshop on Network and Systems Support for Games (NetGames’08), Worcester, USA, October 2008, pages 85-90. ACM.
A.F. Donaldson, P. Keir, A. Lokhmotov Compile-time and Run-time Issues in an Auto-parallelisation System for the Cell BE Processor. In Eduardo César et al. (Eds.): EuroPar 2008 Workshops (the paper was presented at the 2nd Workshop on Highly Parallel Processing on a Chip (HPPC’08), Las Palmas de Gran Canaria, Spain, August 2008). Lecture Notes in Computer Science 5415:163-173.
A.F. Donaldson, C. Riley, A. Lokhmotov, A. Cook Auto-parallelisation of Sieve C++ Programs. In Luc Bouge et al. (Eds.): EuroPar 2007 Workshops (the paper was presented at the Euro-Par Workshop on Highly Parallel Processing on a Chip (HPPC’07), Rennes, France, August 2007). Lecture Notes in Computer Science 4854:18-27. Also presented at the 4th HiPEAC Industrial Workshop on Compilers and Architectures, Cambridge, UK, November 2007.
D. Bosnacki, A.F. Donaldson, M. Leuschel and T. Massart Efficient Approximate Verification of Promela via Symmetry Markers. In K.S. Namjoshi et al. (Eds.): Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA’07), Tokyo, Japan, October 2007. Lecture Notes in Computer Science 4762:300-315.
A.F. Donaldson, A. Miller and D. Parker GRIP: Generic Representatives in PRISM. In Proceedings of the 4th International Conference on the Quantitative Evaluation of Systems (QEST’07), Edinburgh, UK, September 2007, pages 115-116. IEEE Computer Society.
A.F. Donaldson and A. Miller Extending Symmetry Reduction Techniques to a Realistic Model of Computation. In S. Merz and T. Nipkow (Eds.): Proceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS’06), Nancy, France, September 2006. Electronic Notes in Theoretical Computer Science 185:63-76.
A. Miller, M. Calder and A.F. Donaldson A Template-based Approach for the Generation of Abstractable and Reducible Models of Featured Networks. Computer Networks 51(2):439-455, 2007.
A. Miller, A.F. Donaldson and M. Calder Symmetry in Temporal Logic Model Checking. ACM Computing Surveys 38(3): Article 8, 2006.
A.F. Donaldson and A. Miller Symmetry Reduction for Probabilistic Model Checking Using Generic Representatives. In S. Graf and W. Zhang (Eds.): Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA’06), Beijing, China, October 2006. Lecture Notes in Computer Science 4218:9-23.
A.F. Donaldson and A. Miller Exact and Approximate Strategies for Symmetry Reduction in Model Checking. In J. Misra, T. Nipkow and E. Sekerinski (Eds.): Proceedings of the 14th International Symposium on Formal Methods (FM’06), Hamilton, Canada, August 2006. Lecture Notes in Computer Science 4085:541-556.
A.F. Donaldson and A. Miller A Computational Group Theoretic Symmetry Reduction Package for the SPIN Model Checker. In M. Johnson and V. Vene (Eds.): Proceedings of the 11th International Conference on Algebraic Methodology and Software Technology (AMAST’06), Kuressaare, Estonia, July 2006. Lecture Notes in Computer Science 4019:374-380.
A.F. Donaldson and S.J. Gay ETCH: An Enhanced Type Checking Tool for Promela. In P. Godefroid (Ed.): Proceedings of the 12th International SPIN Workshop on Model Checking Software (SPIN’05), San Francisco, USA, August 2005. Lecture Notes in Computer Science 3693:226-271.
A.F. Donaldson and A. Miller Automatic Symmetry Detection for Model Checking Using Computational Group Theory. In J. Fitzgerald, I.J. Hayes and A. Tarlecki (Eds.): Proceedings of the 13th International Symposium on Formal Methods (FM’05), Newcastle, UK, July 2005. Lecture Notes in Computer Science 3582:481-480. Slides.
A.F. Donaldson, A. Miller and M. Calder SPIN-to-GRAPE: A Tool for Analysing Symmetry in Promela Models. In I. Ulidowski (Ed.): Proceedings of the 6th AMAST Workshop on Real-Time Systems (ARTS’04), Stirling, UK, July 2004. Electronic Notes in Theoretical Computer Science 139(1):3-23. Appendix. Slides.
A.F. Donaldson, A. Miller and M. Calder Finding Symmetry in Models of Concurrent Systems by Static Channel Diagram Analysis. In M. Huth (Ed.): Proceedings of the 4th International Workshop on Automated Verification of Critical Systems (AVoCS’04), London, UK, September 2004. Electronic Notes in Theoretical Computer Science 128(6):161-177, 2005. Appendix. Slides.
Papers and extended abstracts appearing in unpublished conference/workshop proceedings
U. Dolinsky, A. Richards, G. Russell, C. Riley, A.F. Donaldson Offloading Parallel Code on Heterogeneous Multicores: A Case Study using Intel Threading Building Blocks on Cell . In Proceedings of the 4th Many-Core and Reconfigurable Supercomputing Conference (MRSC’10). Rome, Italy, March 2010.
A.F. Donaldson, P. Ruemmer, D. Kroening Analysing DMA Races in Multicore Software. In Proceedings of the 3rd Workshop on Programming Language Approaches to Concurrency and Communication-Centric Software (PLACES’10). Paphos, Cyprus, March 2010.
U. Dolinsky, A. Richards, G. Russell, A.F. Donaldson Offloading Code to Heterogeneous Multi-core. In Proceedings of the 2nd Swedish Workshop on Multi-Core Computing (MCC’09). Uppsala, Sweden, November 2009.
L. Howes, A. Lokhmotov, P.H.J. Kelly, A.F. Donaldson Decoupled Access/Execute Specifications for GPGPU-Accelerated Systems (extended abstract). Proceedings of the 2009 Symposium on Application Accelerators in High Performance Computing (SAAHPC’09), Urbana, USA, July 2009.
L. Howes, A. Lokhmotov, P. Kelley, A. Donaldson Automating Generation of Data Movement Code for Parallel Architectures with Distributed Memories (extended abstract). Proceedings of the 5th HiPEAC Industrial Workshop, Barcelona, Spain, June 2008. Slides
A. Lokhmotov, A.F. Donaldson, A. Mycroft, C. Riley Strict and Relaxed Sieving for Multi-Core Programming. In Proceedings of the 1st Workshop on Programmability Issues for Multi-Core Computers (MULTIPROG’08), Goteborg, Sweden, January 2008.
A. Miller and A. Donaldson Symmetry Reduction Methods for Model Checking (extended abstract for Alice Miller’s invited talk). In Proceedings of the 14th Workshop on Automated Reasoning (ARW’07), London, UK, April 2007.
A.F. Donaldson and A. Miller Symmetry Reduction Techniques for Explicit State Model Checking. In I.P. Gent, S. Linton and K. Petrie (Eds.): Proceedings of the 1st International Symmetry Conference (ISC’07), Edinburgh, UK, January 2007, pages 41-45.
A.F. Donaldson and A. Miller Evaluating a Formal Methods Technique via Student Assessed Exercises. In R. Boute and J. Oliveira (Eds.): Proceedings of Formal Methods in the Teaching Lab, a workshop at the Formal Methods 2006 Symposium, Hamilton, Canada, August 2006, pages 93-100.
A.F. Donaldson and A. Williamson Pen-based Input of UML Activity Diagrams for Business Process Modelling. In J. Read and P. Gray (Eds.): Proceedings of Improving and Assessing Pen-based Input Techniques, a workshop at the HCI 2005 Conference, Edinburgh, UK, September 2005, pages 31-38. Slides.
A.F. Donaldson and A. Miller Symmetry Reduction for Probabilistic Systems (extended abstract). In Proceedings of the 12th Workshop on Automated Reasoning (ARW’05), Edinburgh, UK, July 2005, pages 17-18. Slides.
A.F. Donaldson and A. Miller Automatic Symmetry Detection Techniques for Model Checking (extended abstract). In Proceedings of the EPSRC Postgraduate Research Conference in Electronics, Photonics, Communications & Networks, and Computing Science (PREP’05), Lancaster, UK, March/April 2005, pages 138-139. Slides.
A. Donaldson, A. Miller and M. Calder Comparing the Use of Symmetry in Constraint Processing and Model Checking. In W. Harvey and Z. Kiziltan (Eds.): Proceedings of the 4th International Workshop on Symmetry and Constraint Satisfaction Problems (SymCon’04), Toronto, Canada, September 2004, pages 18-25. Appendix. Slides.
Short abstracts
A. Donaldson General Techniques for Symmetry Reduction in Model Checking. In Report on the 22nd British Colloquium for Theoretical Computer Science (BCTCS’06), Swansea, UK, April 2006. Bulletin of the European Association for Theoretical Computer Science 89, pages 193-194.
A. Donaldson Investigating Structural Symmetries in Models of Concurrent Systems. In Report on the 20th British Colloquium for Theoretical Computer Science (BCTCS’04), Pitlochry, UK, April 2004. Bulletin of the European Association for Theoretical Computer Science 85, page 201. Slides (jointly awarded BCS-FACS prize for best student presentation).
Technical reports
A. Miller and A. Donaldson Property Preservation in Quotient Structures. Technical Report TR-2008-270, Department of Computing Science, University of Glasgow, 2008.
Selected talks
These will be available sometime.

research interests

My research interests are

  • formal verification,
  • particularly model checking,
  • verification of source code
  • type-checking;
  • compilers
  • multi-core programming, and s
  • software performance optimization.

I plan to write some more about each area here, but for now, check out my publications.