研究
编程语言和工具实验室
Memory Fairness
在弱内存环境下，应该如何限制无限期执行？ 在这种情况下，并发的程序何时会终止？ 我们的项目正是要回答这样的问题。
即使是最简单的共享内存并发程序在顺序一致性下的有效性属性，如终止，通常也需要对调度器进行一些公平性假设。 在弱内存模型下，线程公平性的标准概念是不够的，还需要一个额外的公平性属性，即内存公平性。 在这个项目中，我们提出了在 SC、x86-TSO、RA 和 StrongCOH 等操作性和声明性内存模型中的内存公平性定义，并研究了它们在模型检查和低级同步的并发程序的终止检查中的应用。