Checking Robustness to Weak Persistency Models
PSan
Based on Jaaru, it detects Robustness (PM) violation and suggests fixes like where to insert fences and flushes.
Like Jaaru, it is dynamic and does not explore all execution and interleaving of threads.
Two modes can be used to generate some execution: Random v.s. Model Checking modes.
The basic idea is: given a specific execution, PSan assumes it is run in Strict Persistency. Then based on the value read in post-crash recovery routine, it adjusts the interval where the crash should happen (still assuming Strict Persistency). If all the intervals are unsatisfiable, then non-robustness is proved.
See the example below:
Experiments
PSan is efficient when run.
In the original paper, the experiments on benchmarks are run such that 10,000 executions are generated and analyzed.
PSan Artifact: Checking Robustness to Weak Persistency Models (PSan Artifact)
On Github: uci-plrg/psan-vagrant
Results: PSan Bug Report - Google 表格