Ale*_*lec 5 concurrency mutex language-design
使用静态检查互斥锁正确性的语言是否明智？也就是说,
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)
}
Ant*_*sky 11
正如Delnan在评论中所说,"互斥正确性"可能意味着各种各样的事情. 从你的评论中,听起来你正在谈论竞争条件检测,这对我来说很方便,因为这是我本科毕业论文的主题:-)¹你想知道(1)这是否可行,(2)如果这是明智的,(3)如果这样做.与任何静态分析一样(包括像这样的轻量级类型或效果系统),前两个问题归结为四个方面:
请注意,由于停止问题(以及更为一般的大兄弟Rice's定理),我们永远无法获得1和2的100%准确度.例如,大多数类型的系统²旨在确保可靠性和可用性(#1和#3); 也就是说,它们旨在易于使用,同时不允许任何类型不安全的程序,并试图排除不切实际的类型安全程序.(他们的支持者,像我一样,会声称他们通常在这个目标上取得了成功.)
您的示例似乎是在尝试最大化可用性(#3):您提供了最少的注释,这些注释与您希望程序员在任何时候都会想到的相对应,然后需要进行分析来检查它们.总体方案听起来与RaceFreeJava非常相似(Abadi等,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和Ashcraft,2003)在某种意义上通过生成足够的静态信息来近似运行动态Lockset类型算法(例如Eraser使用的算法)(Savage等,1997). 这需要大量的调整,因为静态地近似运行时检查器并不容易,并且Lockset已经是实际事实的近似值.RacerX还使用高度调整的约束传播方法执行死锁检查,其中约束是锁定顺序.Engler和Ashcraft设法使用RacerX在实际操作系统中找到一些错误,尽管他们确实得到了误报并找到了良性竞赛(表5).
根据设计,RacerX无法处理的一件事是别名信息:知道两个引用何时指向相同的值.这对并发代码很重要; 考虑以下faux-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.这是一件非常难以理解的事情!
的和弦算法(Naik等人,2006) ³是具有一个别名检测器作为关键步骤不同的整个程序的竞争检测器; 但是,我们再次遇到赖斯的定理,这样的分析既不健全也不完整. 和弦跟踪可能是别名的信息(相当于,肯定是非混淆的信息),因此是不健全的.
所以.你想知道三件事:你的方案(1)可能,(2)合理,(3)在现实世界中完成吗？所有这些分析表明这是一个非常明智和可能的想法; RaceFreeJava特别证明了你所拥有的注释思想非常靠近经过验证的声音类型系统.但是,我不知道有任何内置的语言.我相信我在这里引用的每篇论文都实现了他们的算法,但是我没有全神贯注地看看这些工具是否可以免费获得,商业上可用,有问题,在积极的发展,或什么.然而,当然,确实存在现实世界的静态分析; 例如,Coverity的(商业)静态分析仪在许多其他事情中发现竞争条件和僵局.它们确实存在缺点,即可能会出现关于良好代码的虚假投诉,或者没有关于不良代码的投诉,但这种情况来自于领域,而且在实践中通常不是一个大问题.
¹好吧,动态竞争条件检测,无论如何.这一切都意味着我正在从我当时写的相关工作部分中捏造,这特别方便!这也意味着可能缺少特别是最近的发展(我在2011-2012学年写了这篇论文).相关地,这意味着自从我考虑所有这一切以来已经有一段时间了,因此可能会出现以下错误的引用或(希望是小的)错误; 如果有人注意到这样的事情,请让我知道或只是编辑这篇文章!
²大多数敏感类型的系统,Haskell党员说:-) C根本不在乎,例如,Java 大部分都在那里,但由于像向下转换和(*颤抖*)这样的东西,它必须求助于动态检查阵列协方差.
³抱歉ACM数字图书馆链接; 我找不到本文的免费PDF版本,但我确实找到了PostScript版本.
Mayur Naik,Alex Aiken和John Whaley."Java的有效静态竞争检测." 在对程序设计语言的设计与实现(PLDI)2006年ACM SIGPLAN会议论文集,41卷,2006年,第308-319.可在ACM数字图书馆和PostScript文件中找到.