Prospective students
Part 4 project ideas 2016

Programming languages, compilers, and architectures
Auckland logo

Research interests

  1. Programming language design
  2. Formal semantics
  3. Theorem proving, especially equivallence of programming language semantics
  4. Compiler optimizations, especially in LLVM
  5. Real-time systems, especially using satisfiability modulo theories to generate automatic schedulers
  6. Last but not least, I also develop processor architectures, especially for real-time and safety critical Globally Asynchronous Locally Synchoronous (GALS) programming languages.

Teaching in 2015

  • COMPSYS 302 -- Software practice
  • COMPSYS 725 -- Computer Networks
  • COMPSYS 723 -- Embedded Systems
  • COMPSYS 705 -- Formal methods

Prospective students -- part-4 or ME-studies/ME/PhD

For students good in C++

  • Implementing on the fly array of structure to structure of array conversion in LLVM -- this should improve vectorization
  • Blocking and strip-mining very long vectors in LLVM -- should result in better cache locality and the bypass LLVM's not very good lowering phase to x86 and x86_64

For students good in functional programming (Ocaml/Haskell)

  • Parallelize compilation of Cgals -- the current compiler takes too long to compile very large programs

For students good in hardware design (VHDL)

  • Implement the real-time analyzable Network on Chip (NoC) protocol and associated hardware support for Cgals programs

Projects and software releases


SystemJ (COMPSYS students will learn more about in COMPSYS-704) is a GALS programming language, which supports programming very large distributed and complex software systems. It makes programming multi-core concurrency and distributed memory concurrent programs a breeze. SystemJ is not released under an open source license. But, if you want to try it see here.


Cgals is the evolution of SystemJ programming language towards hard real-time and safety critical systems. You can read more about Cgals here and here. The compiler is released under MIT license and its source code is here. The opam package of the compiler is going to be released soon, which should significantly reduce the installation burden.

Equivalence of micro-step and natural (macro-step) semantics

Unfortunately, the compiler for SystemJ and Cgals is not the same. SystemJ compiler described here uses micro-step semantics for efficient compilation. Cgals on the other hand uses finite state machines (FSMs). FSM based compilation is easier to verify both: for functional properties and real-time properties, it also gives better results, e.g., tighter real-time bounds. This project aims to prove the equivalence of micro-step semantics of SystemJ compiler and the FSM semantics of Cgals, including support for data computations, in Coq theorem prover. A translator is then automatically extracted from Coq, which can translate from micro-steps to macro-steps (FSMs) and vice-versa. This is work in progress and the Coq proof-scripts are available here.

Opam software repo

For getting the below listed packages do this: opam repo -k http add testing && opam update

Older projects and software see here

Emacs powered