++程序可以通过简单顺序推理来验证多线程程序的可靠性

理论计算机科学电子笔记174（2007）23-47www.elsevier.com/locate/entcs主流多线程程序可靠模块验证的简单顺序推理方法Bart Jacobs，Jan Smans，Frank Piessens1，2DistriNet，部门比利时鲁汶大学计算机科学Wolfram Schulte3Microsoft ResearchRedmond，WA，USA摘要由于对象别名、数据竞争和死锁的非局部性质，对多线程面向对象程序的推理是困难的。我们提出了一个编程模型，防止数据竞争和死锁，并支持本地推理存在对象别名和并发。我们的编程模型建立在多线程和同步原语的基础上，因为它们存在于当前的主流语言中。根据我们的模型开发的Java或C#程序可以通过风格化的注释进行注释，以明确地使用模型。我们表明，这样的注释程序可以正式验证，以符合编程模型。换句话说，如果带注释的程序经过验证，则可以保证底层Java或C#程序没有数据竞争和死锁，并且是可靠的在本地推理程序行为。我们的方法支持不可变对象以及静态字段和静态初始化器。我们已经在Spec#编程系统的自定义构建中为根据我们的模型开发的程序实现了验证器，并在案例研究中验证了我们的方法关键词：别名，类初始化，并发，数据竞争，死锁，不可变对象，局部推理，模块化推理，所有权，验证条件生成1介绍用Java或C#等主流语言编写正确的多线程软件是出了名的困难。对象别名、数据竞争和死锁的非局部性质使得很难推断此类程序的正确性1巴特·雅各布斯和扬·斯曼斯是科学研究基金的研究助理-佛兰德斯（F.W.O.- Vlaanderen）（比利时）。2电子邮件：{bartj，jans，frank}@ cs.kuleuven.be3电子邮件：microsoft.com1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.00524B. Jacobs等/理论计算机科学电子笔记174（2007）23此外，开发人员对并发性所做的许多假设都是不明确的。例如，在Java中，许多对象不打算由多个线程使用，因此在访问它们的字段之前没有必要执行同步。其他对象旨在与其他线程共享，并且访问应该同步，通常使用锁。但是，程序文本并没有明确说明对象是否打算共享，因此，编译器或其他静态分析工具实际上不可能验证锁定是否正确执行我们提出了一个类似Java语言的并发编程模型，并设计了一组程序注释，使编程模型的使用显式。例如，开发人员可以注释他的代码，以明确表示对象是否打算与其他线程共享。这些注释为静态分析工具提供了足够的信息，以验证锁定是否正确执行：共享对象必须在使用前锁定，非共享对象只能由创建线程访问。 此外，验证可以模块化完成，因此验证可以扩展到大型程序。还有其他几种方法可以验证多线程代码的竞争和死锁自由。它们的范围从生成验证条件[6，8，10，17，1，18]到类型系统[5，9]。（相关工作的概述见第8我们的方法是独特的，因为它围绕保护不变量而构建，它允许对多线程代码进行顺序推理。因此，本文的贡献如下：• 我们提出了一个编程模型和一组注释并发编程类Java语言。• 遵循我们的编程模型可以确保没有数据竞争和死锁。• 生成的验证条件允许对程序行为进行合理的本地推理。请注意，在本文中，我们忽略了空解引用检查以避免混乱，尽管我们的原型完全支持它。• 我们已经将验证器原型化为Spec#编程系统的自定义构建[4，2]，特别是它的顺序程序验证器• 通过一个案例研究，我们表明该模型是可用的，在实践中，注释开销是可以接受的。[ 12 ][14 ][15][16][17][18]它通过直接支持平台标准的锁定原语，防止死锁，增加对不可变对象的支持，以及报告使用原型实现获得的经验来改进[12]。它通过添加对静态字段和静态初始化器的支持来改进[14]。正如[12]和[14]所做的那样，它构建并扩展了Spec#编程方法[3]，该方法可以在顺序程序中对对象不变量进行合理的推理。本文其余部分的结构如下。 我们介绍方法论分三步第2节的模型可以防止各个字段上的低级别数据竞争。第3节增加了死锁预防。最后的模型，增加了预防B. Jacobs等/理论计算机科学电子笔记174（2007）2325在由多个对象组成的数据结构上的竞争，在第4节中介绍。每一节由三个小节组成，分别阐述了编程模型、程序注释和静态验证规则。其余部分讨论不可变对象，我们的方法静态字段和静态初始化器，经验，和相关的工作，并Ocherer一个结论。2防止数据竞争当多个线程同时访问同一个变量，并且这些访问中至少有一个是写访问时，就会发生数据竞争开发人员可以通过将互斥锁与每个数据结构相关联并确保线程仅在持有相关联的锁时才访问数据结构来保护多个线程并发访问的数据结构。然而，诸如Java和C#的主流编程语言不强制线程在访问数据结构之前获取任何锁，并且它们不强制锁与数据结构一致地相关联。防止数据竞争的一个简单策略是在访问前锁定每个对象虽然这种方法是安全的，但在实践中很少使用，因为它会导致严重的性能损失，冗长，并且容易出现死锁。相反，标准做法是只锁定在多个线程之间有效共享的对象。然而，很难根据程序文本区分共享对象（应该被锁定）和非共享对象。因此，编译器无法强制执行锁定规则，其中共享对象只能在锁定时访问，而无需额外的注释。另一个复杂的事实是，方法的实现可能假设对象已经被其调用者锁定。 因此，实施 将访问共享对象的字段，而不首先锁定对象。在这种情况下，仅仅指示哪些对象是共享的是不成立的。方法的实现者还应该在方法契约中明确地假设调用线程在本节中，我们将描述一个简单的编程模型版本，该模型处理共享对象字段上的数据竞争。后面的部分将进一步开发这个模型，以处理多对象数据结构上的死锁和高级竞争2.1编程模型我们在Java的上下文中描述了我们的编程模型，但它同样适用于C#和其他类似的语言。在我们的编程模型中，对共享对象的访问是使用Java的synchronized语句同步的只 有 当 没 有 其 他 线 程 在 synchronized （ o ） 块 内 执 行 时 ， 线 程 才 可 以 进 入synchronized（o在本文的其余部分，我们使用以下术语来指代Java26B. Jacobs等/理论计算机科学电子笔记174（2007）23--我们说它释放了o请注意，与术语所暗示的相反，当一个线程锁定一个对象时，Java语言会阻止其他线程锁定该对象，但不会阻止其他线程访问该对象这是拟议方法所要解决的主要问题。当一个线程持有一个对象的锁时一个重要的术语点如下：当线程t在线程锁定o之前可能会经过一段时间，特别是如果另一个线程保持o事实上，如果另一个线程从不解锁o，t就永远不会锁定o。这种区别很重要，因为我们的编程模型对尝试锁定对象。我们的编程模型通过确保没有两个线程同时访问给定对象来防止数据竞争。具体地说，它在概念上将每个线程t与访问集t. A相关联，访问集t.A是其字段线程允许在给定点进行读或写，并且该模型确保没有两个线程的访问集相交。访问集可以在创建对象、共享对象、创建线程或线程进入或退出同步块时增长和收缩。请注意，这些访问集在运行时并不存在：我们使用它们来解释编程模型，并实现静态验证。• 对象创建。当一个线程创建一个新对象时，该对象被添加到创建线程的访问集中。这意味着构造函数可以初始化对象的字段，而无需首先获取锁。这也意味着单线程程序可以正常工作：如果只有一个线程，它会创建所有对象，并且可以在不锁定的情况下访问它们。• 对象共享。除了访问集之外，我们的模型还将每个运行时状态与全局共享集S相关联。我们称S中的对象为共享的，称S的补集中的对象为非共享的。 共享集，像访问集一样，是概念性的：它在运行时不存在，但用于解释模型和实现验证。新对象最初是非共享的。创建线程以外的线程不允许访问其字段。此外，不允许任何线程尝试锁定非共享对象：我们的编程模型不允许synchronized（o）.操作，除非O是共享的。在我们的编程模型中，不打算共享的对象永远不会被锁定。如果在代码中的某个点，开发人员希望使对象可用于并发访问，他必须通过注释（共享o注释）。从这一点开始，对象o被共享，线程可以尝试获取对象的锁。当对象被共享时，该对象将从创建线程的访问集中移除并添加到共享集中。如果在此转换之后，任何线程（包括创建线程）希望访问该对象，则必须首先获取其锁。一旦被共享，对象就永远不能恢复到非共享状态。B. Jacobs等/理论计算机科学电子笔记174（2007）2327• 创建线程。启动一个新线程会将线程主方法的接收器对象（即Java中的Runnable对象，或.NET Framework中的ThreadStart委托实例的目标对象）的可访问性从启动线程转移否则，将不允许线程此外，前提条件要求此接收方对象是非共享的。 作为结果，保持了线程访问集中的共享对象也被该线程锁定的不变式• 获取和释放锁。当一个对象被共享时，它将从创建线程的访问集中删除，并添加到共享集中。由于该对象现在不属于任何线程的访问集，因此不允许任何线程访问它。要获得对这样一个共享对象的访问，线程必须首先锁定该对象。当一个线程获得一个对象的锁时，该对象被添加到该线程的访问集中在同步块的持续时间如图1所示，对象可以处于以下三种状态之一：未共享、自由（未被任何线程锁定并被共享）或锁定（被某个线程锁定并被共享）。最初，对象是非共享的。 有些对象最终会转换到共享状态（在开发人员指定的程序点）。在此转换之后，对象不再是任何线程的访问集的一部分，并且被称为自由。要访问一个自由对象，它必须首先被锁定，将其状态更改为锁定，并将该对象添加到锁定线程的访问集中。解除锁定对象会将其从访问权限集中删除，并使其再次成为自由让我们总结一下。线程只允许访问其相应访问集中的对象。一个线程的访问集包括所有它持有锁的对象，它已经创建但还没有共享的对象，以及线程的主方法的接收器对象（如果线程还没有共享这个对象）。我们的编程模型通过确保访问集永不相交来防止数据竞争2.2程序注释在本节中，我们通过以下方式详细说明我们的方法所需的注释：如图2所示。该示例由一个程序组成，该程序观察来自不同来源的事件，并记录观察到的事件总数。由于计数由多个线程更新，因此除非采取预防措施，否则它会受到数据竞争的影响。我们的做法确保不可能在我们的原型实现中（参见第7节），注释被写成风格化的注释。但为了提高可读性，本文采用了一种语言综合语法.图2所示的程序是一个Java程序，增加了许多注释（由灰色背景表示）。更具体地说，使用了三种注释：共享命令，共享修改器和方法契约。此外，：=表示赋值和=相等。• share命令使非共享对象可用于并发访问28B. Jacobs等/理论计算机科学电子笔记174（2007）23Fig. 1. 物体的三种状态多线程。在该示例中，计数器对象在所有会话之间共享。• 字段和参数可以使用共享修饰符进行注释，表示它们只能保存共享对象。Session的字段计数器是具有共享修改器的字段的示例。• 需要方法契约来使模块化验证成为可能。 它们由前置条件和后置条件组成。一个前提条件声明了方法实现对当前线程的访问集（表示为tid .A）和全局共享集的假设例如，start方法的前提条件要求访问集为空。后置条件声明访问集和共享集的属性。例如，Session注意我们的注释是完全可擦除的，也就是说，它们对程序的执行没有任何示例程序是正确同步的，注释使我们的静态验证器能够证明这一点。我们将在下一节讨论如何做到这一点。如果开发人员忘记在run方法中写入synchronized块，程序将不再正确同步。具体来说，就是进入柜台。方法run中的count违反了编程模型，因为对象counter不在线程2.2.1线程创建为了验证示例，我们还需要所有库方法的方法契约 程序使用的如图3所示。图3所示的方法契约对编程模型中有关线程创建的规则进行了编码• Thread构造函数要求其参数是调用线程的访问集的一部分，并且是非共享的。构造函数从访问集中删除Runnable对象，并将其与Thread对象关联。实际上，构造函数• 当方法start被调用时，一个新的线程被启动，Runnable对象B. Jacobs等/理论计算机科学电子笔记174（2007）2329requirestid.A=tid;确保this∈tid.A∈this/∈S;要求计数器∈S;需要tid.A={this}this/∈S;publicintfindDuplicate（）{{}}classSessionimplementsRunnable{共享计数器;intsourceId;Session（Counter counter，intsourceId）这个。int count：=count;这个sourceId：=sourceId;}公共voidrun（）public voidrun（）{//等待来自源sourceId的事件（未显示）publicvoid run（）{柜台计数++;}}}}班级计划{static voidstart（）{Counter counter：=newCounter（）;股票柜台newThread（new Session（counter，1））. 开始（）;newThread（new Session（counter，2））. 开始（）;}}图二.示例程序说明第2节的方法。程控仪提供的注释显示在灰色背景上。确保this∈tid.A∈this/∈S;30B. Jacobs等/理论计算机科学电子笔记174（2007）23要求这个∈tid.A;确保this∈tid.A∈this/∈S;requiresrunnable∈tid.Arunnable/∈S;public interfaceRunnable{voidrun（）;}public classThread{publicThread（Runnable）{... 个 文件夹public voidstart（）{... 个 文件夹}图三. 图2中程序使用的库方法的契约。将与Thread对象关联的新线程插入到新线程的访问集中。方法run2.3静态验证我们已经在前面的章节中非正式地解释了我们的编程模型。在本节中，我们正式定义了模型，并展示了如何在模块化（即，每方法）方式。我们如下进行：一个用我们的注释丰富的程序P被翻译成一个用断言和经典方法契约丰富的验证时程序PJ这种翻译定义了我们的注释的语义，并且是我们的编程模型的形式定义：根据我们的模型，原始注释程序P是正确的，当且仅当翻译后的程序PJ关于其断言和经典方法契约是正确的。为了检查翻译的程序PJ是否正确，我们使用现有的单线程程序自动程序验证器。我们的实验表明（第7节），最先进的验证器能够以这种方式验证现实的程序本文的贡献在于注释语法的设计（对于多线程特定的注释）和注释程序的翻译;我们使用现有的技术[2]进行顺序程序验证。翻译涉及两件事。在第一步中，我们将两个仅用于验证的变量（所谓的幽灵变量）插入到程序中，以跟踪执行验证所需的状态。ghost变量tid.A表示当前线程然后，在第二步中，原始程序的每个方法都被翻译，使得翻译后的方法可以被模块化地验证。开发人员在注释中编写的方法契约是需要tid.A={this}this/∈S;B. Jacobs等/理论计算机科学电子笔记174（2007）2331第一步中引入的幽灵状态。开发人员编写的代码和其他注释被转换为验证时代码和验证者的证明义务（编写为断言）。图4显示了代码和注释转换的本质。它是2.1节中介绍的编程模型规则的形式化。我们忽略了对象引用可以为空以减少混乱的事实。同步块的验证时代码包括一个破坏操作，该操作为被锁定对象的所有字段分配一个任意值。此外，它还包括一个由任意超集替换共享集的破坏操作。 这反映了其他线程或许，这一次，他们改变了这个世界。源程序分配和验证时间分配分别显示为：=和←o：=newC;o←newC;假设o/∈S;tid.A←tid.A{o};x：=o.f;asserto∈tid.A;x←f;o.f：=x;asserto∈tid.A;如果（f被声明为共享的）断言x∈S;o.f←x;分享断言o∈tid.A;断言o/∈S;tid.A←tid.A\{o};tid.S←tid.S{o};同步的，同步的断 言 o∈S; 断言o/∈ A;破坏o。（c）tid.A←tid.A{o};Btid.A←tid.A\{o};图四、 将源程序命令转换为验证时命令。3用于防止第2节的方法可以防止数据竞争，但不能防止死锁。在本节中，我们将介绍防止死锁的方法在本文中，我们将死锁定义为一个线程循环，每个线程都在等待下一个线程释放某个锁。从形式上讲，死锁是一个线程序列t0，...，t n-1和对象序列o0，.，on-1使得t i持有o i的锁，并试图获取o（i +1）mod n的锁。陷入死锁的线程将永远被卡住开发人员避免死锁的典型方法是在所有共享对象上定义偏序，并允许线程仅在对象少于线程已持有锁的所有对象时才尝试获取对象有不同的共同策略来定义这样的偏序。第一个是静态地定义顺序这种方法在共享的32B. Jacobs等/理论计算机科学电子笔记174（2007）231M1n我J对象保护全局资源：代码必须以静态定义的顺序获取这些资源。 第二种策略是根据一些所涉及的对象。例如，定义账户之间的转账操作，可以按照账号的顺序锁定两个账户，从而在锁定账户对象时避免死锁在某些情况下，特定模块的开发人员可能只希望对锁定顺序施加部分约束，或者可能希望对一组对象进行抽象。例如，Subject-Observer模式中Subject类的开发人员可能希望指定Observers应该在锁定Subject之前锁定，而不是相反。换句话说，在死锁预防排序中，所有Observer都在Subject之上。3.1编程模型我们的编程模型旨在支持上述所有三种场景。开发人员可以通过锁定级别的中介来指示他想要的顺序。锁级别是新原语类型（仅为验证目的而存在）锁级别的值。 可以使用构造函数在给定的现有锁级别在（{1A，...，I A}，{I B，...， I B}），其中0 ≤ m，n，假设每个指定的下限低于每个指定的上限;形式上，对于每个1 ≤i≤m和1 ≤j≤n，l A

下载后可阅读完整内容，剩余1页未读，立即下载