Jade Alglave

Extending Arm’s consistency model to account for Arm’s Virtual Memory System Architecture

A consistency model describes the rules a concurrent system must respect, for example, what value a given read instruction is allowed to see. Arm’s consistency model is written in the domain-specific language cat. A consistency model written in cat can be executed and experimented with using the herd tool.

In this talk, I will present the work done by my team on modelling Arm’s Virtual Memory System Architecture: how we extended the cat model to include orderings necessary to programs manipulating page tables, as well as the herd tool, and the testing tools diy and litmus.

This model has been reviewed and ratified by Arm’s Memory Model Review Board, and is now part of the Arm Architecture Reference Manual.  

back to overview

Watch Recording
Speaker Image
 

Biography

Jade Alglave works in the area of concurrency, more precisely consistency models. Together with Luc Maranget, she designed and developed a domain-specific language called cat to write executable and formal consistency model. Models for various systems have been written in cat, including the Linux kernel and the Arm architecture. Jade leads an engineering team at Arm which maintains and enhance the Arm cat model and companion tools to execute and test the model.
Footer

Imprint / Privacy