拥有一种静态检查互斥锁正确性的语言是否明智？IE，
var m
var x guarded_by(m)
func f1() {
lock(m)
x = 42
unlock(m)
}
func f2() {
x = 42 // error, accessing x w/o holding its mutex
}
func f3() assumes_locked(m) {
x = 42
}
func b1() {
f3() // error
}
func b2() {
lock(m)
f3()
unlock(m)
}
正如 delnan 在评论中所说，“互斥正确性”可能意味着很多事情。 从您的评论中，听起来您在谈论竞争条件检测，这对我来说很方便，因为这是我本科论文的主题:-)¹您想知道 (1) 是否可行，(2)如果这样做是明智的，以及 (3) 如果这样做了。与任何静态分析（包括像这样的轻量级类型或效果系统之类的分析）一样，前两个问题归结为四件事：
请注意，由于停止问题（及其更一般的大兄弟赖斯定理），我们永远无法获得 1 和 2 的 100% 准确度。例如，大多数类型系统² 的目标是稳健性和可用性（#1 和 #3）；也就是说，它们的目标是易于使用，同时不允许类型不安全的程序，并试图仅排除不切实际的类型安全程序。（他们的拥护者，像我一样，会声称他们在这个目标上大体上是成功的。）
您的示例似乎正在尝试最大化可用性（＃3）：您提供了最少的注释，这与您希望程序员无论如何都会想到的内容相对应，然后需要进行检查来检查它们的分析。整体方案听起来非常类似于RaceFreeJava (Abadi et al., 2006)。RaceFreeJava 是 Java 的扩展，其中：
ghost锁）进行参数化；guarded_by注释，指定哪些锁必须保护它们；和requires注释，指定必须持有哪些锁才能调用它们。正如您可能已经猜到的那样，这个想法是每个字段都有一个关联的锁，每次访问该字段时都必须持有该锁；分析会跟踪每个程序点持有哪些锁，如果在其锁不在当前锁集中时访问变量，则会报告错误。ghost使用锁定参数，这会变得更加微妙；例如，你可以有
class RunningTotals<ghost Object m> {
private int sum = 0 guarded_by m;
private int product = 1 guarded_by m;
public void include(int x) requires m {
sum += x;
product *= x;
}
public int getSum() requires m {
return sum;
}
public int getProduct() requires m {
return product;
}
}
现在我可以将一个RunningTotals对象嵌入到其他对象中，并用' 锁o保护它，这很方便；o但是，分析之后需要注意到底是哪个锁m。另外，请注意，其中的方法RunningTotals 无法同步m，因为m不在范围内，并且只是类型级别ghost；同步必须由客户端处理。与我们声明锁参数化类的方式类似，RaceFreeJava 的另一个特性是声明thread_local类的能力。这些类永远不允许在线程之间共享，因此不需要用锁保护它们的字段。
正如您在评论中指出的那样，通常无法确定程序是否正确使用这些注释，特别是因为 Java 允许您在任意表达式上进行同步。为了理智， RaceFreeJava 将同步限制为最终表达式；然后，就像所有类似类型的注释一样，它使用保守的语法检查锁标识。阿巴迪等人。发现大多数正确的程序都可以通过这种方式成功检查。因此，它们强烈地依赖于健全性（实际上，分析是声音模数他们放入的一些逃生舱口）和可用性，以牺牲完整性为代价。为了检查可用性——这与完整性密切相关，因为太多的虚假警告使静态分析几乎无法使用——Abadi 等人。还写了一个工具（rccjava) 用于检查这些注解并进行少量注解推断，还使用它来构建更大的工具 ( Houdini/rcc) 以执行更多推断。在评估这些（表 I-IV）时，他们发现了真正的错误，没有太多必要的注释或虚假警告。但是，请注意它并不完美。这个分析会抱怨一些有效的Java程序。
因为我有一种长篇大论的自然倾向，而且因为（正如我所提到的）我为此写了我的本科论文，我还将讨论其他一些分析，但在我看来，RaceFreeJava 可能是最相关的. 如果你想直接跳到最后，本节之后有一个总结。
Boyapati 等人提出的另一种基于类型系统的分析。（2002 年）。这种类型的系统检测竞争条件和死锁，但使用不同的技术；它基于所有权类型，它跟踪允许哪些线程访问哪些变量；只有在持有其所有者的锁时才能访问变量。同样，方法可以注释需要accesses或需要locks。为了检查死锁，Boyapati 等人。还添加了锁定级别的概念，它将所有锁按部分顺序放置。通过确保始终按此顺序获取锁，可以自动排除死锁。同样，该算法是合理的（尽管不幸省略了证明）但并不完整，并且试图可用。为此，他们必须做大量的推理工作，因为写下注释的工作量太大了。
还有其他不是类型系统的分析。这些必须对程序的执行进行建模，而不仅仅是执行语法检查，并且通常倾向于既不健全也不完整，但通过不需要注释（即使它们允许它们）并尝试报告有用的错误。 RacerX (Engler and Ashcraft, 2003)在某种意义上做到了这一点，它通过生成足够的静态信息来近似运行动态 Lockset 类型的算法，例如 Eraser (Savage et al., 1997) 使用的算法。 这需要大量的调整，因为静态逼近运行时检查器并不容易，而且 Lockset 已经是实际情况的逼近。RacerX 还使用高度调整的约束传播方法执行死锁检查，其中约束是锁定顺序。Engler 和 Ashcraft 设法使用 RacerX 在真实操作系统中发现了一些错误，尽管他们确实会得到误报并找到良性竞争（表 5）。
根据设计，RacerX 没有处理的一件事是别名信息：知道两个引用何时指向相同的值。这对于并发代码很重要；考虑以下仿C：
// Thread 1:
acquire(superman_lock);
*superman_bank_account += 100; // Saved Metropolis and got rewarded!
release(superman_lock);
// Thread 2:
acquire(clark_kent_lock);
*clark_kent_bank_account -= 100; // More bills...
release(clark_kent_lock);
假设superman_lock和clark_kent_lock是不同的，知道这段代码是否安全需要知道是否superman_bank_account与 相同clark_kent_bank_account。这是一件非常难以弄清楚的事情！
Chord算法 (Naik et al., 2006) ³ 是一种不同的全程序竞争检测器，它有一个别名检测器作为关键步骤；然而，我们又遇到了赖斯定理，这样的分析不可能既可靠又完整。 和弦轨道可能是混叠信息（等同于绝对未混叠信息），因此是不健全的。
所以。您想知道三件事：您的方案 (1) 是否可行，(2) 合理，以及 (3) 在现实世界中是否可行？所有这些分析都表明这是一个完全明智且可能的想法；RaceFreeJava 尤其证明了您拥有的注释想法非常接近经过验证的健全类型系统。但是，我不知道有什么语言内置了这个功能。我相信我在这里引用的每篇论文都实现了他们的算法，但我根本没有看这些工具是否可以免费获得、商业上可用、比特腐烂，正在积极开发中，或者什么。当然，现实世界的静态分析确实存在。例如，Coverity 的（商业）静态分析器发现，除其他外，竞争条件和死锁。它们确实有缺点，即可能对好的代码产生虚假的抱怨，或者对不好的代码没有抱怨，但这与领域有关，在实践中通常不是一个大问题。
¹好吧，无论如何，动态竞争条件检测。这一切都意味着我是从我当时写的相关工作部分抄来的，这特别方便！这也意味着这可能缺少最近的发展（我在 2011-2012 学年写了论文）。相关地，这意味着我已经有一段时间没有考虑所有这些了，所以上面可能存在严重缺失的引文或（希望是小的）错误；如果有人注意到这样的事情，请告诉我或编辑这篇文章！
² 最明智的类型系统，Haskell 党派说 :-) 例如，C 根本不在乎，Java取得了大部分的成功，但由于向下转换和 (*shudder*) 之类的事情，不得不求助于动态检查数组协方差。
³ 抱歉 ACM 数字图书馆链接；我找不到这篇论文的免费 PDF 版本，但我确实找到了 PostScript 版本。
Mayur Naik、Alex Aiken 和 John Whaley。“Java 的有效静态竞争检测”。在2006 年 ACM SIGPLAN 编程语言设计和实现 (PLDI) 会议论文集中，第 41 卷，2006 年，第 308-319 页。可在 ACM 数字图书馆和作为 PostScript 文件获得。