基于对象的图形文法模型检查和自动代码生成：并行应用程序的功能验证和性能测试

理论计算机科学电子笔记184（2007）113-131www.elsevier.com/locate/entcs用基于对象的图文法建模的并行应用程序的代码生成1F'abioPasini，2，3FernandoL. Dotti4Faculdade deInforma'tic aPontif<$ıciaUniversidadeCatoo<$licadoRioGrandedoSulPorto Alegre，Brazil摘要在并行应用程序的开发过程中，除了能够分析性能方面之外，还非常希望能够尽早确保功能属性。确保并行应用程序模型的功能属性可以带来重要的节省，因为它减少了应用程序开发和调试所花费的时间。在这个方向上，模型检查和自动代码生成可以在开发过程中用作补充工具，从而可以分析系统行为并快速生成相应的代码。在本文中，我们提出了使用基于对象的图形文法（OBGG）的规范的并行应用程序。OBGG是一种形式化的可视化语言，适合于描述基于异步消息传递的并发系统。使用OBGG描述的模型可以通过模型检查进行验证。在此基础上，提出了一种基于MPI（消息传递接口）的OBGG模型到C代码的转换方法，该方法适合于集群环境。为了说明这一贡献，在OBGG中对一个示例并行应用程序进行了建模;通过模型检查证明了模型的功能特性;给出了C/MPI相应的模型，并给出了性能测试结果的翻译模型进行了讨论，并与一个类似的C/MPI应用程序的手建立关键词：图文法，并行编程，MPI，模型检测。1介绍并发系统可以表现出难以预测的行为。即使当所提出的算法解决方案激发了高度的信心时，有时不容易避免的竞争条件和死锁等方面也可能是潜在的 破坏系统功能在并行应用程序的开发过程中，与任何并发应用程序一样，人们必须关注系统的正确性及其性能1IQ-Mobile（CNPq-CNR）和DACHIA（FAPERGS/IB-BMBF）项目2作者部分由HP-Brasil/PUCRS协议赞助。3电子邮件地址：fpasini@inf.pucrs.br4电子邮件：fldotti@inf.pucrs.br1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.03.018114F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113（这通常是并行应用程序构建者关注的焦点）。确保并行应用程序模型的正确性，除了增加结果的可靠性之外，在经济上也很重要，因为它减少了测试所花费的集群的计算时间（这是一种昂贵的资源）集群是高性能并行机，其架构基于一组独立的工作站，通过低延迟通信网络互连，用作并行应用程序的执行平台。每个站都有一个本地存储器，只有本地处理器可以访问。大多数分布式内存计算机的并行应用程序构建器使用MPI（消息传递接口）[15]。MPI是用于使用分布式存储器计算机（例如集群）的应用的标准消息传递接口。MPI库是可移植的，目前允许用FORTRAN、C和C++语言编写程序。 它不支持容错，并假设存在无错误通信。根据这种编程范式，所有的并行性都是显式的，即程序员负责识别应用程序的并行部分，并显式地将它们映射到通信进程或线程。开发并行编程工具的几种尝试使用抽象来降低编程的复杂程度，帮助用户快速开发程序，避免许多编程错误。这些工具中的大多数专注于生成代表各种并发进程及其通信的代码，用户使用顺序代码片段填充生成的代码[12]。这些环境/工具中的一些还支持通过模拟或性能测试来分析开发中基于对象的图形语法（OBGG）[5]是一种形式化的可视化语言，适用于基于消息传递的异步分布式系统。通过定义可能的状态变化的规则声明，非确定性是隐含的，并且支持非确定性。提供的少量抽象和基于对象的风格使它相对容易学习。 由于少数建筑 及其形式语义，OBGG模型可以通过翻译到PROMELA [4][11]进行模型检查，PROMELA是SPIN模型检查器的输入语言[8]。在本文中，我们提出了使用OBGG的并行应用程序模型的建设和转换步骤，从OBGG模型生成C/MPI实现。其中一个论点是允许使用具有隐式并行性的语言来指定并行应用程序，从而提高设计者的抽象级别。另一个论点是将开发中的并行应用程序作为OBGG模型进行模型检查的可能性，然后可以直接将其转换为C/MPI实现。这些想法是illustrated与一个简单的并行应用程序，它是在OBGG中定义的，模型检查的一些属性，有其C/MPI代码生成通过建议的翻译，并在集群上执行，生成性能图形进行了讨论。本文档的组织如下：第2节讨论了与并行编程和并行程序生成相关的方面;第3节介绍了OBGG语言以及使用该语言的示例。检查的属性F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113115对于这个例子，也在第3节中讨论。在第4节中，介绍了从OBGG到C/MPI的转换，然后给出了示例应用程序的性能结果。最后，在第5节中对结论和未来的工作进行了评论。2并行编程并行编程在许多方面不同于顺序系统的编程，大多数开发人员首先接触的模型。平行过程状态之间可能的插入是难以预测的， 传统的串行算法调试技术难以识别问题源。此外，考虑到expertation- tion平台和通信系统之间的差异，编程错误是非常常见的。并行程序中的三种主要错误被识别出来[9]：(i) 语义错误：这些错误是由程序员对所使用的并行计算模型以及如何将其应用于手头问题的错误理解引起的。例如，错误常常是由于误解了进程间内存共享的语义和所用并行编程语言的语义;(ii) 实现错误：这些错误的发生是因为并行程序增加了复杂性，如进程启动、通信和同步。 典型的错误包括不正确地打包/解包消息或创建死锁场景;(iii) 性能错误：这些错误是由于缺乏关于并行和并发成本的直觉或经验而导致的。例如，这类错误包括并行执行细粒度的程序段，或者限制并发的糟糕同步选择前两种类型的错误通常会导致程序不正确地执行，或者使其无法生成可执行文件。第三个源通常导致程序正确运行，但在与顺序解决方案兼容时性能增益很差。使用自动代码生成工具可以防止前两个问题，一旦它使用户不必使用特定的语言方面或通信库。第三个错误可以通过代码生成器的专业化来最小化，以便在开发过程中引导用户使用更合适的模型并行编程的标准以多种形式存在了大约二十年，例如设计模式[14] [17]，骨架和模板[13]。 插件和模板提供具有并行代码的结构，其中用户引入应用程序相关代码。设计模式基本上是对常用代码片段Frameworks工具[13]是使用图形语言来建模并行应用程序的第一个作品之一。生成的系统由通过RPC（远程过程调用）进行通信的模块组成，使用的语言是C。116F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113操作构造器基于数据流程图，用符号表示模型中的数据划分或分组、调度和同步。模型中使用的顶点具有可变的语义，边表示通信信道。因此，（异构网络计算环境）[1]是一个图形化的并行编程环境，使用PVM [16]作为通信平台。顶点表示用户提供的顺序例程和/或顶点之间的数据流控制。未标记的边表示通信信道。工具Code（面向计算的显示环境）[2]提供了使用MPI和PVM的代码生成。与HeNCE工具一样，还有数据处理和控制顶点。顶点可以有多个通信通道，边标签定义了用于消息传递的通道。DPnDP（Design Patterns and Distributed Processes）[14]使用可参数化的设计模式作为并行编程的可扩展库。应用程序是使用一个或多个设计模式构建的，它们可以与其他代码片段结合使用低级别的通信原语。新的设计模式可以逐渐添加到系统中，使其具有可扩展性。工 具 CO2P3S （ Correct Object-Oriented Pattern-based Parallel ProgrammingSystem）[17]使用设计模式生成Java代码。 所使用的建模语言表示应用程序的拓扑结构。 该工具具有用于监视的资源-允许进程之间的处理和通信，允许用户修改模型并搜索更好的负载平衡。另外，一个名为MetaCO2P3S的模式编辑器也与这个环境相关联.这些工具中使用的图形建模语言针对用户需求进行了详细说明，提供了描述所需系统的机制，但在许多情况下（如[13]和[17]），语言语义的形式化定义 并没有提出。3基于对象的图文法Graph Grammars [7]是一种自然的方式来表达复杂的情况，其中被分析的系统可以被描述为一个图，动态方面可以通过语法规则图文法由以下组成(i) 类型图，表示系统中允许的顶点和边(ii) 初始图，表示系统的初始状态，(iii) 描述系统中可能发生的更改的一组规则在[5]中，提出了一种称为OBGG的图文法的限制形式。OBGG是一种基于对象的语言，适用于异步消息传递系统的规范在OBGG中，系统由称为对象的自治实体组成。对象具有内部状态，并通过异步消息传递进行通信在OBGG系统中，状态被描述为一个图形，其中对象和消息被塑造为顶点。对象F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113117形状像顶点。图1展示了OBGG对象的模型。 从图形上看，一个对象有一个包含其名称（图1中的Obj N），类标识符（i）和属性集的矩形符号。 同一级别的学生同一个类标识符。预定义数据类型的属性列在矩形内（例如atr A），引用其他对象的属性（例如atr B）具有绑定到其他对象的边的符号，或者在规则和类型图的情况下绑定到类标识符。属 性 可 以 是 基 本 数 据 类 型 （ 如 整 数 、 字 节 、 字 节 ） 或 抽 象 数 据 类 型（ADT）。用户定义的ADT可以在OBGG模型中使用，但有一些限制：（i）用户定义的数据类型的正确性必须由用户保证;（ii）对用户定义的数据类型的操作必须是原子的，即它们在规则应用期间完成。例如，它们不能留下任何已创建的线程或挂起的处理，例如接收响应5。图1.OBGG对象的模型对象的行为对应于接收消息时执行的操作。这样的动作可以改变对象的内部状态和/或导致发送发送给其他对象和/或自身。在图形上，消息具有多边形的形式，如图1中的消息Msg。消息只能有一个对象作为目的地，并且可以有预定义类型（例如parA）或其他对象（例如parB）的参数值。消息的目的地由箭头给出，消息参数由将这些参数绑定到消息多边形的线给出。基于对象的系统可以由属于不同类的对象组成。在OBGG中，每个类都使用类型图来定义。 类的类型图（参见图2）确定该类的任何实例可以接收和发送的类属性和消息（以及消息初始图描述了在期望的初始模型情况下必须存在的所有对象、消息和属性值。所有具有属性和消息的对象都是类型图中定义的类的实例。对象实例化可以从初始图静态完成，也可以通过执行创建新对象的规则作为初始图的示例，参见图3。例3.1为了说明这种形式主义的使用，我们采用了一个OBGG模型，用于一个主从系统，实现了一个类似蒙特卡罗的方法来计算π的值。该方法包括：(i) 在边长为s的正方形上内接一个圆（圆的半径为s/2）;(ii) 在正方形内部生成n个5更具体地 说 ， 对于这项工作，他们可能不会调用MPI通信接口进行任何操作。118F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113(iii) k是正方形内同时也在圆内的点的个数(iv) 计算π4×kn。观察到生成的点越多，近似越好。一个好的随机算法会在一个域内生成一个均匀的点分布。 如果使用一个坏的随机发生器，得到的值将不会足够接近π。因此，根据随机化点的集合（即取决于所使用的随机数生成器），可能存在最终值不是π的良好近似的模型计算。我们将为一个主人和三个奴隶建立模型。图2显示了Master和Slave类的类型图。 对象可以接收的消息指向对象，对象生成的消息在每个类型图的右侧表示，指向它们被发送到的对象类标识符图2.对于主对象和从对象，键入Graph图3. 初始图形。在类型图中，对其他对象的引用也链接到类标识符，因为它是对象Master中的引用sl1、sl2和sl3以及对象mst中的引用的情况F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113119→····奴隶在OBGG中，计算系统状态规则定义了对象类的行为在a graph图grammar语法，a rule规则r：LC发生如下：R指定系统中的一个状态变化，在规则L左侧的所有项目必须存在于系统的当前状态中，以使得规则应用成为可能C，如果存在的话，是一个关于其左边属性的等式，并且只有当这个条件为真时，该规则才能被应用保留映射r中从L映射到R的所有项;所有未从L映射到R的项都从当前状态消失;• 所有在R中而不在L中的项都被添加到图中在OBGG语言中，一个类的规则出现在被接收的一条信息的左侧。每一条规则都指定了该类中的任何对象对接收到这样的消息的反应在规则的右侧，此消息将被使用，对象的属性可以更改值，并且可以生成新消息。同一规则中描述的所有操作都发生在一个原子步骤中。对可能的规则应用的识别称为匹配。每条规则只描述一条消息的处理一个对象可以发送消息到另一个对象，只有当存在至少一个引用的目的地在右手边的规则。该引用可以是对象的属性或传入消息的参数OBGG规则允许表示并发性和非确定性。同时适用是指在同一情况下，当这些规则不发生冲突时，适用一个以上规则的可能性。 两条规则相互冲突， 它们消费或修改相同的项目。并发可以发生在不同的对象（外部竞争）或同一个对象（内部竞争-当同一个对象可以在图的同一状态中应用多个规则时）。这种非决定性表现在适用规则的选择上。如果在一种情况下可以应用多个规则，则非确定性地选择其中一个来执行。例3.2图4和图5分别给出了前面定义的Master和Slave类的规则。表示法ObjectNameRuleName将用作所呈现规则的Master Start是系统中应用的第一条规则。它消耗消息Start并为每个Slave发送一个Start消息，在n中指示Slave必须随机生成多少个点，在s中指示要使用的正方形的大小。主接收规则表示主接收消息InsPoints时的行为，累计每个从计算的圆内的点数。接收到来自从机的最后一条消息（规则Master Done）后，Master最终计算π的近似值。 选择之间的分歧120F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113图4. 主对象的规则。主接收和主完成的比较是由每个规则的关联保护进行的对于Slave Start规则，在出现Start消息时，Slave在total属性中设置要生成的对的数量，并在square side值中设置 此外，它将第一个坐标对作为点消息的参数发送给自己。之后，Slave会持续消耗P点，计算该点是否属于圆周（内部属性），并更新生成的消息总数（完成属性）。当最后一条消息被处理时，它执行Slave Done，向Master发送圆内的点的总数函数newM ath（）、ins（s，x，y）和rand（s）在OBGG模型外部定义，使用以下M ath抽象数据类型。抽象数据类型数学：运营：Mathnew Math（）;调用ADT。int ins（s， x， y）;函数ins（s，x，y）确定点（x，y）是否属于内接于边长为s的正方形的半径为s/2的圆周。此函数返回1（一）点包含在圆内的情况或返回0（零）F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113121图5. 从属对象的规则。否则，请执行以下操作。奥索特 rand（随机限值）;返回小于或等于limit的数字。intn（intn，intn）;随机化边长为s的正方形内的一组n个点，返回内接于该正方形的半径为s/2的圆内所提出的ADT的相应实现必须遵守前面提到的限制。函数rand eval（）将在4.7节中使用。已经使用OBGG开发了一系列案例研究，例如移动代码应用程序[5];基于拉的故障检测器[6]和读者和作家问题[11]等。 少量的结构使语言易于学习，基于对象的风格使重用和可扩展性变得容易。3.1模型检测为了对OBGG模型进行模型检查，所有的模型元素（对象、消息、规则和参数）都被转换成PROMELA结构，从而允许使用SPIN[8]验证者。关于OBGG-PROMELA翻译的更多细节可以在[4]中找到，包括原始OBGG模型和翻译模型之间语义兼容性的正式证明。 SPIN模型检查器支持对线性时序逻辑（Linear Temporal Logic，LTL）中描述的属性进行验证。在[4] [11]中，提出了如何使用LTL指定OBGG模型的属性，考虑到122F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113↑↑||↑||↑||↑如[10]中所描述的事件的定义。 OBGG开发环境[3] 允许编辑OBGG模型并将模型自动转换为PROMELA。此外，SPIN生成的反例（当模型违反LTL规范时）可以转换为OBGG抽象，这样反例就可以使用OBGG模型而不是PROMELA生成的模型来解释。这个特性为开发人员保持了相同的抽象级别。在本节中，我们将讨论所提出的模型要证明的性质。由于生成的状态空间，模型将使用三个Slave和一个Master进行验证，每个Slave将仅生成四个点。以下属性将在LTL中形式化并检查模型：(i)系统终止：最终模型将生成一个结果，在此之后，不再应用任何规则(ii) 响应：从机总是响应请求;(iii) 收敛：存在（至少一个）导致可接受结果的计算。下面我们使用SPIN语法来表示LTL属性。 此外，我们使用 [10]在《易经》中，有这样的说法。 事件被写入事件，并表示状态从非活动到活动的改变，或者（！事件X事件）。事件通常用于表示OBGG模型规则的应用。[10]还介绍了可以与事件概念一起使用的属性模式。这种模式的用法是针对所讨论的属性的(i) 系统终止：Master Done是计算π的最终值的规则。 因此，我们必须证明这个规则被应用，并且在应用之后没有其他规则被应用。为了证明这条规则是适用的，我们有：(1)<>（↑主完成）结果是真的。 表明在其应用之后没有其他规则被应用在模型中，我们有：(2)[]（↑大师完成→[]！↑任何规则）其中：↑任何规则=（↑主开始||↑主接收||主机完成从机启动从机继续从机完成这个公式是一个事件后缺席的模式，如[10]所示。这里，在Master Done之后没有任何事件，这导致真。(ii) 响应：每次应用Slave Start规则时，总是会出现Slave Done关联的.(3)<>↑从机启动→<>（↑从机启动<>↑从机完成）此公式是事件（从机启动）后存在（从机完成的模式[10]结果是真的。同样，重要的是要记住，这一步假设函数ins（）和rand（）是正确的。这些功能是手动翻译的。在PROMELA模型中，rand（）总是返回相同的0值，而ins（）可能不确定地返回1或0。这种抽象用于缩小状态空间，并且不修改给定系统的含义，）F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113123↑ ↑ ≤≤≈ × ×÷因为ins（）的结果定义了点是否属于圆周。(iii) 收敛性：模型的收敛性可以用分辨率来表示。在预期的时间间隔内。然而，由于模型检查过程将考虑生成的随机点的所有组合，因此将存在所有点都落在圆之外的计算，因此不会收敛。另一方面，会有收敛的计算。可以通过模型检验来证明现有的计算是收敛的。使用LTL，证明收敛是可能的，我们努力证明该模型将永远不会收敛。 结果是模型收敛的轨迹。 该方法收敛的频率取决于实际实现中采用的随机数生成器的质量。为该物业验证的LTL公式为：(4)【】！（↑Master Done P i）其中：主完成Pi=主完成&&（3， 0结果3， 4）这个公式是一个全局不存在事件的模式[10]，正如预期的那样，结果为false。关于这方面，验证工具的一个局限性是缺乏对浮点变量的支持。对于句子验证，将模型修改为π1000（四）Kn）在规则Master Done中使用的操作，并测试结果在区间（3000，3400）内的收敛性。随着随机点数量的增加，该间隔可以缩小。4翻译OBGG -C/MPI表1给出了GBBO和C/MPI环境中发现的OBGGC/MPI基本单位对象过程单元形成初始图系统调用对象初始化动静态静态沟通方式消息传递消息传递非决定论规则伪随机函数同意对象内部/对象之间进程/线程之间表1比较OBGG和C/MPI。OBGG模型由通过消息传递进行交互的各种并发对象组成。因此，很自然地将OBGG对象映射到进程，并将OBGG对象之间的消息传递通信映射到进程之间的消息传递。OBGG所描述的非确定性可以嵌入到进程处理传入消息动态对象创建可以是124F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113∈通过动态过程创建支持。OBGG的初始图可以映射到并行应用程序的初始（主）进程在下面的章节中，我们将详细讨论这些方面。 互补地我们还讨论了在执行结束时的资源重新分配问题 正如争论所产生的实现的语义保留一样4.1OBGG过程翻译过程的第一步是将每个对象映射到一个单独的进程（称为OBGG进程）中，使系统中不同进程的规则并行执行成为可能（对象之间的并行性-外部竞争）。要考虑的另一个方面与模型支持的消息数量有关。OBGG状态图（在理论上）拥有无限数量的消息。这个特性是用一个链表（Lin）来表示的，用来存储每个OBGG进程已经收到但尚未处理的消息。因此，实际实现的限制是可用内存。此外，任何消息都可以在任何时候被消息发送到的对象使用。这决定了规则的选择和执行机制。一旦Lin存储了对象的所有输入消息，就可以计算出给定时刻的所有匹配消息规则。这如下进行：对于Lin中的每个输入消息Mi，考虑消费该类型消息并且能够被应用的所有规则（条件保持），构建列表Ri。为每个消息生成的每个配对（M i，R i）存储在列表（L个匹配）中，从该列表中随机选择配对（M i，R），其中RR i。所指示的消息从L in中移除并被消费，从而触发相关联的规则。规则应用程序可以修改OBGG进程内的属性值和/或生成一个或多个消息。以与接收到的消息类似的方式，在应用规则之后，将生成的消息插入列表Lout中，将发送操作留给后面的步骤。这个选择是为了采用Lout还带来了其他优势，这些优势将在下一节中讨论从上面可以看出，在OBGG过程中执行的基本算法可以分为八个主要步骤：1. 接收消息Mi;2. 包括Mi在Lin中;3.在生成L个匹配时评估L;4. 从L个匹配中随机选择一对（Mi，R）;5. 从L中取出Mi;6. 应用规则R，消费Mi并生成（或不生成）新消息;7. 将生成的消息插入Lout;8. 把L里的所有信息都发出去在下面的部分中，将更详细地介绍用于转换模式的元素，从而使这种基本算法F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113125可用的源代码。4.1.1 OBGG过程代码根据OBGG形式主义，消息传递的所有操作（发送或接收）都是非阻塞的。这意味着没有进程发送/接收消息将停止等待通信完成。MPI操作器包含阻塞和非阻塞通信原语，但是非阻塞调用语义并不简单。因此，采用了阻塞原语为了打破发送和接收进程之间的同步，在OBGG进程中使用三个不同的线程来接收、处理和发送消息。这些线程将分别被称为接收器，评估和验证。根据前面介绍的基本算法，Receiver与步骤1和2的执行相关联，Evaluate执行步骤3到7，而Receiver执行步骤4。8.这种策略使得实现更模块化的程序成为可能，使得生成的代码更容易理解，易读性和维护作为补充，OBGG对象的属性被映射到相应OBGG过程的局部变量。目标语言（C）中可用的基本数据类型可以在OBGG规范中使用。也可以使用遵循已经讨论过的限制的用户定义的4.2OBGG消息使用C数据结构将OBGG消息转换为MPI消息。这些结构由基本的数据类型组成，如char，int和numeroat。MPI消息是使用由库存储的打包原语逐场构造的这样的消息必须按照生成的Receiver代码以相同的顺序解包在翻译生成的数据结构中，第一个字段包含相应消息类型的标识。其他字段（如果存在）与消息中的每个当前参数相关。在该呈现的翻译模式中，生成的系统仅使用一种类型的数据结构来进行翻译。所有消息，它是系统中所有允许的消息参数的超集。采用的另一个重要限制是消息参数的限制仅基于打包/解包原语支持的基本数据类型。因此，在OBGG系统的建模期间，不允许发送复杂的数据结构（即列表），除非用户在发送之前提供将这些结构转换为原始数据类型的操作，以及在接收之后在对应规则中使用的反向操作6当使用非阻塞原语时，用户发出一个发送请求，并且必须显式地编程发送过程，以便与通信平台重 复 测 试 发送操作是 否 完成。126F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）1134.3OBGG规则一旦匹配算法识别出要执行的规则，OBGG过程执行以下步骤：(i) Construct消息（删除Mi将其传递给规则代码内的缓冲器(ii) 如有必要，更新OBGG流程内部属性(iii)生成消息，将它们插入临时列表7Ltemp。发往应用规则的进程的消息直接插入到L中。(iv) 将Ltemp添加到Lout的末尾。4.4初始图初始图定义了从系统一开始就处于活动状态的所有实例，以及与这些实例相关联的每个属性的值，包括对象之间的关系。初始图的另一个功能是定义每个对象的初始消息对象属性值的定义 这些值在接收任何消息之前都是固定的，所以匹配机制不会发现对象处于不一致的状态。 在代码生成和编译之后，将获得的二进制代码复制到集群节点，并通过系统调用启动进程。所有消息的生成和发送都是由一个名为INIT的特殊进程完成的。要遵循的发送顺序是非确定性定义的。 在发送完所有消息后，INIT充当其余进程之间的协调器，这将在下一节中由于MPI库的限制，4.5系统终止在OBGG中，对象的终止没有显式表示。当不再有可能的匹配时，系统停止处理。然而，显式进程终止在实际系统中是必要的，例如，释放集群的资源。因此，为了考虑系统终止，从而能够释放资源，我们必须以某种方式检测到在代表OBGG对象的分布式进程中没有更多的匹配可能。当检测到这种情况时，则发出信号并终止各种过程。在执行初始化过程之后，由INIT进程协调分布式终止的标识7.避免了连续锁定和解锁L，以确保数据一致性。使用一个临时列表使Lout更容易被编译器使用。F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113127在完全异步的设置中，这个问题类似于投票协议。然而，在我们的翻译模型中，我们可以假设某些通信特性，并避免大量的消息。下面描述用于检测终止的分布式协议。 它使用三个控制消息：R、B和C。 每个参与者进程的行为和INIT（协调器）的行为如下所示。参与者行为：• ThreadEvaluate负责在输入缓冲器中搜索消息并识别匹配项。如果此线程没有为缓冲器中的所有消息标识任何匹配项，或者缓冲器为空，则它将阻塞，直到有新消息收到了。一旦Evaluate被阻塞了一段时间，一个控制消息（B），用信号通知阻塞状态，目的地为INIT，被附加到Lout，并最终由UART发送。• 在Evaluate块之后，DIR定期将OBGG进程块状态（使用C消息）确认为INIT。• 当OBGG进程收到消息时，再次评估匹配测试，如果成功，立即发出信号以INIT重新激活（使用R消息）。如果没有找到匹配，则OBGG进程在再次通知至少一次阻塞状态之前不会去确认其阻塞状态（C）INIT（协调器）进程的行为• 在INIT保存的视图中，每个进程都可以处于以下三种状态之一：（R），阻塞（B）我们的确认阻塞（C）。• 当协调器首先检测到一个视图时，如果处于状态C，则存在可能的终止情况。• 然后协调员等待每个参与者的立即确认（C）。只有在所有进程都确认了它们的状态C一秒钟，并且在前一个视图中所有进程也处于状态C之后，的特征。• INIT过程视图的所有其他配置对于终止无效。• 当INIT检测到上述终止情况时，它向所有参与者发送控制消息Killmesg，通知进程可以完成和释放资源。该协议基于所有通信都是同步的这一事实，即确保每个其他进程从给定进程接收控制消息的顺序是发送顺序。该协议应确保没有检测到错误终止，即，如果至少一个进程仍处于活动中，则协调器将不会在两个后续视图中两次在（C）中具有所有进程。为了更好地理解协议，假设所有过程都在（C）中，只有一个过程在状态（R）中。现在假设正在运行的进程向一个进程发送数据消息（M），然后使用INIT阻塞（B），并在一段时间后确认128F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113（三）封锁状态。此时，INIT拥有（C）中的所有进程，并且对于错误终止检测，INIT将需要再次确认每个进程。由于消息（M）被保证在发送进程发送（B）和（C）到INIT之前被传递到另一个进程，所以另一个进程将不会确认消息（M）。（C）在这一点之后初始化，但发送（R）或（B）消息，这取决于消息（M）的匹配或不匹配（分别）。因此，将不会检测到（错误）终止。4.6关于翻译的生成的代码应该按照OBGG语义运行。确保这种行为需要一个正式的证明，证明生成的代码的语义与相应的OBGG模型的语义是等价的。这种形式化的证明依赖于编程语言和通信平台的形式化语义，而这是不可用的。因此，在本节中，我们认为OBGG模型的主要特征保留在生成的源代码中。讨论的主要方面是：(i) 并发性：对象之间的并发性通过表示对象的各个进程的并行执行考虑到对象内并发性，在OBGG中，可以并行地应用非冲突规则。我们目前的映射并不代表同时应用非冲突规则的可能性。这会带来太多的开销，因为必须复制左侧属性的状态， 每个活动规则和线程都必须动态创建。但是，该实现确实表示了OBGG对象的所有可能的可达状态。 由于选择执行规则的算法是非确定性的，因此生成的系统表示规则应用的所有潜在序列和从初始状态开始的所有可能状态。这与[4]中讨论的OBGG-PROMELA翻译(ii) 非确定性：如描述由对象执行的步骤的算法中所述，匹配的计算考虑输入缓冲器中的所有消息，并且对于每个消息，所有可能的规则（消息可以由多个规则处理）。 从所有启用的规则应用程序中随机选择。 在所有启用的规则中的这种随机选择表示OBGG模型的非确定性行为。(iii) 无序通信：使用与上述相同的参数（非确定性），没有与消息消费相关联的顺序(iv) 异步通信：一个对象的规则评估活动不会因为发送消息而停止。消息传输在单独的线程上执行。(v) 封装：表示对象的属性成为进程的内部变量。改变这些属性的唯一方法是通过应用对象(vi) 反应性：仅当接收到特定消息（并且F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113129满足关于对象的属性和消息的参数的特定条件）。因此，只有在处理消息时，对象的内部状态才会发生变化。4.7性能测量在本节中，我们将介绍从第3节中介绍的模型生成的并行应用程序的性能测量。并行应用程序在CPAD8集群中执行，该集群由16个通过快速以太网网络互连的双Pentium III站（550 MHz，256 MB-Ram）组成。对于模型执行，每个进程使用一个集群节点图6.a的图形比较了生成的应用程序与手动生成的程序（称为基本程序）的执行时间，改变了从属进程的数量并占用了系统的总执行时间。基本程序有一个主-从逻辑拓扑结构和主和从之间的通信是类似于第3节中考虑的模型。此外，函数randeval（）在base的Slave进程中用于图6.原始Pi模型、基本算法和改进Pi模型的性能可以观察到，由生成的代码获得的执行时间大约是从基本程序获得的执行时间的八倍。这是因为在Slave的OBGG模型中，在Slave Continue规则中，有一条消息发送到Slave本身，用于模拟顺序行为。如果我们将这种顺序行为建模为抽象数据类型功能的一部分，避免消息传递，那么与程序基础相比，生成的应用程序的性能将如图6. b所示图7显示了在此执行中使用的Slave修改后的规则请注意，现在所有的点生成和评估都由函数rand eval（）完成尽管生成的应用程序的性能低于基本程序，但应该注意到模型的可伸缩性与 基本程序;即添加更多进程不会导致意外的性能损失。8CPAD - Centro de Pesquisa em Alto Desempenho或高性能研究中心-是PUCRS和HP-巴西之间的合作项目。130F. Pasini，F.L.Dotti/Electronic Notes in Theoretical Computer Science 184（2007）113图7.奴隶的模式性能差异的原因有很多。而在基础程序上，只需要一个MPI调用来传输消息（仅包含一个整数值），在生成的应用程序中涉及许多MPI调用：一个用于打包每个参数，一个用于发送，最后一个用于每个参数的解包调用。 此外，由于OBGG行为，消息的（链接）列表必须被操纵，并且每次必须选择应用规则时，都要在该输入列表中的所有消息上计算匹配。 此外，必须考虑的是，这种性能损失是由于更抽象的建模形式主义，它导致了非确定性和隐式并行。5结论和今后的工作这项工作提出了使用OBGG模型的并行应用程序，以及从OBGG模型，产生相应的C代码的MPI平台。这种从OBGG到C/MPI的转换在许多方面都遵循了从OBGG到PROMELA的现有转换的相同思想[4]，这也是基于流程和通信渠道。如本文所述，翻译步骤很简单，可以自动化。这种转换的一个实现是一个电流表。应将结果集成到现有环境中，以用于OBGG模型的版本[3]。第4.7节中的转换模型的性能显示了对OBGG提供的抽象进行优化的影响翻译的某些方面正在调查中，以便更好地发挥作用。例如，在当前的翻译中，整个模型只定义了一种MPI消息类型。在消息参数方面，此MPI消息是所有OBGG消息的超集，导致额外的处理和通信开销。下一个优化是生成各种MPI消息类型，OBGG模型的每种消息类型都有一个。在优化中投资的另一个主题是每个对象的内部算法。更具体地说，匹配计算机制可以受益于细化技术，以便识别输入缓冲器中特定消息的候选规则。最后，应进行更多的案例研究，以显示其适用性的OBGG的并行应用程序，以及分析所生成的应用程序的行为，并可能提高这里提出的翻译