The TechGlider

Learning and sharing about Computer Science, programming, research & technology

Jun 27, 2017 - 1 minute read - Comments - update

How to Reason about Correctness of Programs Designed for Non-Volatile Memory?

I recently graduated with a master’s degree in Computer Science from Brown University. My project report that documents the work I did over the last one year is now available on the Brown CS website at

I am making a copy available here as well: PDF.


Traditional storage stack necessitates a separate data format for the persistence of in-memory data structures, requires additional code for conversion to that data format and wastes a lot of CPU time. Upcoming byte-addressable non-volatile memory (NVM) technologies such as memristors or phase change memory offer an opportunity to rethink how code interacts with persistent data. Researchers have come up with a variety of programming models to make effective use of NVM but, unfortunately, it is considered hard to reason about the safety properties provided by these models.

In this report, we look at existing work in a somewhat related field of formal reasoning about the correctness of concurrent software and discuss whether those techniques can be applied to software designed for NVM or persistent memory.

We also document our design of a concurrent graph data structure for non-volatile memory which offers crash-resilience with the help of Atlas programming model.