It is notoriously difficult to ensure that concurrent programs have been designed correctly. Compared to sequential programs, concurrent programs can exhibit behaviour that a programmer may not have anticipated. Rely/guarantee reasoning is a compositional program reasoning method for concurrent programs. There are many interesting areas of research to explore, such as:
- Exploring the relationship between rely/guarantee reasoning and linearisability. While rely/guarantee is usually a top-down approach starting from the abstract specification, linearisability is a bottom-up approach, but understanding how these two techniques intersect is an open problem.
- Developing approaches for modelling and verifying concurrent algorithms without locks (non-blocking algorithms). These types of problems are particularly challenging.
- Comparing the different types of concurrency approaches, e.g. separation logic and rely/guarantee reasoning, to understand the fundamental properties of concurrency.
- Incorporating temporal logic into rely/guarantee approaches, to enable properties to be expressed involving the future and past.
Requirements
These projects are suitable for any level, from Bachelor research projects and Honours to PhD projects. You will need an ability to reason about logic, and completion of a course on discrete mathematics, including logic and set theory, e.g. MATH1005 at ANU. Previous experience with concurrent programming is beneficial but not required. Previous knowledge of Hoare logic, such as covered in COMP1600 at ANU, is also useful. PhD students should have a strong background in areas such as mathematics, logic, formal methods and software engineering.
Depending on your level, background and interests, the project could be on a more theoretical side, such as developing the theory and exploring the fundamental concepts, or practical, such as involving theorem proving or investigating particular algorithms, or a combination of both.
Scholarships are available for PhD students.
Contact
If you’re interested in this area, contact Dr. Nisansala Yatapanage.