A Semantic Foundation for Persistent Programming

Non-volatile memory (NVM) is an emerging technology that provides orders of magnitude faster access to persistent storage (which preserves its contents after a crash or a power failure) than hard disks.

While NVM is expected to radically change how we manage storage in applications, its programming model is standing on very shaky foundations.The persistency semantics of the mainstream architectures is very unclear and full of counterintuitive behaviours.

As a result, writing correct NVM programs is extremely difficult: there is no support for persistent programming in programming languages nor any techniques for testing and verifying their correct recovery from crashes.PERSIST will develop a solid mathematical basis for determining the possible outcomes of persistent programs and reasoning about their correctness.

More specifically, it will produce:(1) formal empirically-validated persistency models for mainstream hardware architectures,(2) formal efficient persistency models for mainstream programming languages,(3) firmly-grounded higher-level abstractions to ease persistent programming, and(4) the first effective testing and verification techniques for persistent programs.