Consistency and Persistency: Ensuring Correctness of Concurrent Programs on Non-Volatile Memories
Tidsperiod: 2020-12-01 till 2024-11-30
Projektledare: Parosh Abdulla
Budget: 5 312 000 SEK
Nonvolatile memories (NVRAMs)} offer the best of two worlds, namely the low latency of DRAM, and the persistency of long term storage.They provide direct access to data in the same way as DRAM, but allow programs to recover from system failures. An important task for programmers when using NVRAMs is to ensure correct recoverability, i.e., that the program returns to a consistent state after a failure. Naively, one would think that correct recoverability would be easy. This is, however, not true, since the state of the NVRAM may not be consistent with the program view. The reason is that write operations persist (i.e., become durable) in an order which may differ from the order in which they are issued by the program.The operation reorderings give rise to a memory persistency model that prescribes the order in which operations may persist.In this project, we will develop methods for the verification of concurrent programs in the presence of persistency.To analyze concurrent program behaviors operating on NVRAMs, we need also to take into consideration the memory consistency model that defines the semantics of the program running on the processor.The goal of the project is to develop methods, algorithms, and tools for the verification of programs running on systems that exhibit behaviors conforming to both persistency and consistency.