UKRI Future Leader fellowship (October 2021 – September 2025)
Modern society depends on accessing and storing vast quantities of data, at ever-increasing speeds. To meet our conflicting desiderata of fast and durable (persistent) data, the cutting-edge non-volatile memory (NVM) technology provides fast, byte-addressable access at a performance comparable to DRAM, while ensuring persistence across crashes as with hard disks. NVM is expected to lead to substantial changes in how we manage storage in software, the huge performance gains of NVM are difficult to exploit correctly (without programming bugs).
The objective of my fellowship, PERSEVERE, is to develop the scientific and engineering underpinnings necessary for safe and ubiquitous NVM adoption in modern computing through rigorous, mathematical foundations. Specifically, as part of this fellowship I will:
UKRI VeTSS (UK Research Institute in Verified Trustworthy Software Systems) (April 2020 – March 2021)
Non-volatile memory (NVM) is fast becoming mainstream, and with it comes the need to write programs that exploit it correctly and efficiently. To verify the correctness of such programs, we need formal models of how CPUs interact with NVM, answering questions such as: which stores are guaranteed to persist across crashes? And in what order do they persist? Previous work by the PIs has devised putative models; this project seeks to validate those models empirically against main- stream architectures such as Armv8 and Intel-x86. Key challenges include generating test cases that are capable of revealing the persistency behaviour of CPUs, and detecting which stores become per- sistent without continually power-cycling the CPU.