j.alglave@ucl.ac.uk

Prof. Jade Alglave FREng

Since March 2018, I am also working at Arm, where I lead the Arm Architecture Formal Team. The team looks after, amongst other things:

• the Concurrency Model
• the Architecture Specification Language
• the Architecture Speaks

Publications

• Puss In Boots: on formalizing Arm's Virtual Memory System Architecture (in IEEE Micro 2024)
• Armed cats: formal concurrency modelling at Arm (in TOPLAS 2021)
• Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel (in ASPLOS 2018)
• Don't sit on the fence: a static analysis approach to automatic fence insertion (journal version of CAV 2014, in TOPLAS 2017)
• Ogre and Pythia: an invariance proof method for weak consistency models (in POPL 2017)
• Syntax and semantics of LISA (on Arxiv, 2016)
• Syntax and semantics of cat (on Arxiv, 2016)
• Modelling of Architectures: Choose your own adventure in herding cats (in SFM 2015)
• GPU concurrency: weak behaviours and programming assumptions (in ASPLOS 2015)
• Don't sit on the fence: a static analysis approach to automatic fence insertion (in CAV 2014)
• Herding cats: modelling, simulation, testing, and data-mining for weak memory (in TOPLAS 2014)
• Weakness is a virtue (position paper, in EC² 2013)
• Partial Orders for Efficient Bounded Model Checking of Concurrent Software (in CAV 2013)
• Software Verification for Weak Memory via Program Transformation (in ESOP 2013)
• A Formal Hierarchy of Weak Memory Models (in FMSD 2012, Volume 41, Number 2)
• An Axiomatic Memory Model for Power Multiprocessors (in CAV 2012)
• Synchronising C/C++ and Power (in PLDI 2012)
• Fences in Weak Memory Models (Extended Version) (journal version of CAV 2010, in FMSD 2012, Volume 40, Number 2)
• Soundness of Data Flow Analyses for Weak Memory Models (in APLAS 2011)
• Making Software Verification Tools Really Work (invited paper, in ATVA 2011)
• Stability in Weak Memory Models (in CAV 2011)
• Understanding Power Multiprocessors (in PLDI 2011)
• Litmus: Running Tests Against Hardware (in TACAS 2011)
• Fences in Weak Memory Models (in CAV 2010)
• Relaxed Memory Models Must Be Rigorous (in EC² 2009)
• The Semantics of x86-CC Multiprocessor Machine Code (in POPL 2009)
• The Semantics of Power and ARM Multiprocessor Machine Code (in DAMP 2009)

Software

The diy+herd tool suite

• herd: a generic simulator that takes as input a memory model defined in our home-made DSL (.cat).
• diy and litmus: a tool suite for generating and running tests in PowerPC and x86 assembly against hardware.
• offence: a tool for enforcing stability to x86 and Power assembly programs, i.e. the program has nothing but SC executions.

Software analysis

• musketeer: a tool for placing synchronisation in C code (e.g. memcached).
• mole: a tool looking for weak memory cycles in C code (e.g. Debian packages).
• CBMC: an extension of CBMC that handles weak memory via partial orders.
• goto-instrument: a tool for transforming a C program so that the transformed program's SC executions are all the executions the initial program could have on a weak architecture.

Coq developments

• Coq development associated to the TOPLAS 2014 paper
• Coq development associated to the ESOP 2013 paper
• Coq development associated to the CAV 2011 paper
• Coq development associated to the CAV 2010 and FMSD 2012 papers

Ph.D. Thesis

Here is the manuscript.

818 Pumpkin

• C'est bon la salade !
• J'aime le mardi !
• Ceci n'est pas la page web de Samuel Mimram.