Semantics for Persistent Memory


Non-volatile memory (NVM) is emerging as a technology that may significantly impact the computing landscape in the near future. NVM ensures durability of data across power failures (i.e., as hard drives do) at a performance close to that of conventional volatile memory (RAM). Nevertheless, NVM is quite difficult to use correctly because of data caches: the writes do not persist to memory immediately when performed by a program and may further be reordered. In order to ensure that writes are propagated to memory in the correct order and that all writes have persisted to memory, the programmers have to use special barrier and cache flushing instructions.

This project is primarily concerned with the formalization of the semantics of such instructions and their interaction with the weak consistency model followed by each architecture. In addition, we develop correctness conditions for programs running over persistent memory and techniques to prove such programs correct.



Imprint | Data protection