PhD scholarship: Verifying compiler optimization passes

Summary

Enrolment status New students
Student type Domestic students, International students
Level of study Higher Degree by Research
Study area Engineering and Computing
HDR funding type Living stipend scholarship
Scholarship value $40,000 per annum tax-free for three years, with the possibility of two 6-month extensions at the standard RTP rate ($28,092 per annum, indexed annually) in approved circumstances
Opening date 10 March 2020
Closing date 30 June 2020

Description

These two PhD scholarships are part of a new project funded by Oracle Labs Australia to model and verify sophisticated compiler optimisations in the Graal Java compiler. Graal is a high-performance polyglot virtual machine (VM) that not only supports JVM-based languages such as Java, Scala, Kotlin and Groovy, and LLVM-based languages like C and C++, but also more dynamic languages like Python and JavaScript. The GraalVM compiler is widely used for high-performance applications by many large companies such as Twitter, Red Hat and Alibaba.

Compilers are an essential ingredient of the computing base. Software developers need to be able to trust their compilers because an error in a compiler can manifest as erroneous generated code for any of the myriad of programs it compiles. The traditional approach to compiler verification is testing, but this cannot cover all cases and hence can only show the presence of errors, not their absence.  The gold standard for producing trusted software is mechanized formal verification by theorem provers.  This research project focuses on verifying optimization passes of the Graal compiler, using the Isabelle interactive theorem prover.

Verification of a compiler is a complex, time-intensive task that requires expertise in formal semantics, verification methods, mechanized theorem-proving technology, and of course compilers. Fortunately, compilers are organized into multiple passes, thus enabling the verification process to be structured to match the passes, and allowing one to build up a verified compiler pass-by-pass.  Our project is focusing on modelling the Graal Intermediate Representation (IR), which is a sophisticated graph structure, and then verifying several key optimisation passes of the open-source Graal compiler.  If you are interested in working with cutting-edge compiler technology and doing a PhD as part of this project, we invite you to join our team.

Eligibility

To be eligible, you must meet the entry requirements for a higher degree by research.

Applications are closed.

Before you get started

If this scholarship has rules, download and read them.

How to apply

To apply for admission and scholarship, follow the link on the upper right of this page. There is no separate application for scholarship because you will have the opportunity to request scholarship consideration on the application for admission.

Before submitting an application you should:

When you apply, please ensure that under the scholarships and collaborative study section you:

  1. Select ‘My higher degree is not collaborative’
  2. Select 'I am applying for, or have been awarded a scholarship or sponsorship'.
  3. Select ‘Other’, then ‘Research Project Scholarship’ and type in ‘COMPILER OPTIMIZATIONin the 'Name of scholarship' field.

See an example of what you have to do

Learn more about applying for a higher degree by research at UQ

The information you provide in your application is collected for the purposes of (1) assessing your eligibility for this scholarship, (2) selecting scholarship recipients, and (3) administration of the scholarship.  The University of Queensland will disclose the information you provide to Oracle Labs Australia for the stated purposes. The University will not otherwise disclose the information to a third party without your consent, unless such disclosure is authorised or required by law.  For further information, please refer to the University’s Privacy Management Policy at http://ppl.app.uq.edu.au/content/1.60.02-privacy-management

Selection criteria

Required selection criteria:

  • An honours or research masters degree in computer science;
  • Some knowledge of compilers and intermediate representations;
  • Expertise in logic and discrete mathematics.

Desirable selection criteria:

  • Experience with formal semantics of programming languages;
  • Experience with theorem provers, especially interactive theorem provers;
  • Experience with program analysis, such as static analysis tools or algorithms.
Applications are closed.

Contact

Associate Professor Mark Utting
+61 7 3365 3310
Applications are closed.

Terms and conditions

Read the policy on UQ Research Scholarships.

A domestic part-time student with carer’s responsibilities, a medical condition or a disability, which prevents them from studying full time may be eligible for scholarship consideration, on a case by case basis.

Applications are closed.