Свойства живучести, например прекращение выполнения, даже самых простых параллельно выполняемых программ с использованием общей памяти в условиях последовательной согласованности обычно требуют некоторых предположений относительно справедливости планировщика. В слабых моделях памяти стандартные представления о справедливости потоков недостаточны, и необходимо дополнительное свойство — справедливость памяти. В рамках этого проекта мы предлагаем определения справедливости памяти в условиях таких моделей оперативной и декларативной памяти, как SC, x86-TSO, RA и StrongCOH, и исследуем возможность их применения для проверки моделей, а также проверки прекращения выполнения параллельно выполняемых программ с низкоуровневой синхронизацией.

• Репозиторий проекта