K框架：基于重写的编程语言设计与形式化分析工具支持【论文总结】

可在www.sciencedirect.com在线获取理论计算机科学电子笔记304（2014）3-56www.elsevier.com/locate/entcsK概述和SIMPLE案例研究GrigoreRos，u1伊利诺伊大学香槟分校TraianFlorinS，erb jujanut，Boga2University Alexandru Ioan Cuza of Ias， i摘要本文概述了基于语义的程序设计语言设计和形式化分析的工具支持的K框架K提供了一个方便的符号，用于模块化地定义编程语言的语法和语义，以及一系列基于这些的工具，包括解析器和解释器。还讨论了一个案例研究，即K定义的动态和静态语义的SIMPLE，一个非平凡的命令式编程语言。本文中讨论的材料是在K'11研讨会的特邀演讲中提出的关键词：编程语言，基于重写的语义，K1引言由第一作者于2003年引入[40]，用于教授编程语言课程，并从那时起不断改进和发展，K框架[43，52]是一种基于重写的编程语言定义框架，它汇集了现有框架的优点（表达性，模块化，并发性和简单性），同时避免了它们的弱点。 K框架包括（1）K技术，它可以并且已经被用来定义现实生活中的编程语言，如Java，C和Scheme，以及程序分析工具（参见第5节和那里的参考文献），以及（2）K重写，一种重写语义，允许K定义捕获真正的资源共享并发。为了给编程语言构造赋予语义，K框架依赖于计算结构、配置和K规则。计算结构，更简单地称为计算，并激发了名称第1grosu@illinois.edu2traian.serbanuta@info.uaic.rohttp://dx.doi.org/10.1016/j.entcs.2014.05.0021571-0661/© 2014 Elsevier B. V.保留所有权利。4G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）3框架是计算任务的序列，其中每个计算任务是可能扩展的语言语法上的一个项;计算通常用于处理定义的编程语言的顺序片段和各种语言构造的求值策略运行程序的配置K规则通过只指定配置中需要的内容和明确识别哪些更改来区分自己;因此，它们比常规重写规则更简洁，更模块化，更并发。如果忽略其并发语义，K可以被视为重写逻辑[31]中的一个符号，与大多数其他语义框架相同，例如自然（或大步）语义，（小步）SOS，模块SOS，具有评估上下文的约简语义等[55]。然而，与上面列举的这些其他语义框架不同，K不能在重写逻辑中被容易地逐步捕获，因为它增强了并发性，这在图重写的思想中得到了最好的描述[43，52]。我们将只关注K框架的基本方面，而不是它的具体实现;本卷中包含的KPrimer [53]提供了当前实现的更深入的视图因此，我们并不坚持在下面的内容中对K定义进行特定于实现的注释。相反，我们建议对实现细节感兴趣的读者参考K工具的当前发行版（可从k-framework.org获得），在那里可以找到后续K定义的注释版本。此外，我们也不坚持K的可执行性方面，也就是说，一个定义的基本方面使它（有效地）可执行。在本文中，我们仅限于纯理论和高层次的K在第2节中介绍的K框架的概述是由SIMPLE的动态（第3节）和静态（第4节）语义的完整文字定义补充的，SIMPLE是一种命令式编程范式的非平凡编程语言这些部分展示了框架的表达能力和模块性，并提供了令人信服的证据，证明K可以扩展到更大的语言。参考其他研究项目利用K在实现他们的目标是在第5节。第6节结束。2K框架概述在这里，我们给出了K的概述，重点是它的整体能力和目标。正如人们所预料的那样，一个相对较新的和积极使用的框架经常由于用户的请求/投诉而发生变化。K也不例外。在本节中，我们还将重点介绍最近的发展，符号和术语。我们将尝试在适当的地方证明我们的设计决策是正确的，因为我们相信其他语义框架设计者可能需要采取类似或相关的决策。对于K的更技术性（但更老）的介绍，我们请读者参考[43]。第3节和第4节讨论SIMPLE编程语言及其类型系统的完整K定义G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）35两者都是K工具发行版的一部分，我们也将在本节中使用它来说明KK是一种基于上下文不敏感项重写的编程语言定义框架K建立在以下三个主要思想之上：(i) 将语法扁平化为特殊的计算结构，称为简单计算，其中包括抽象语法，并让人想起归约语义中的重新聚焦[14]与评估上下文[20]，延续[39]以及单子中的计算[34]。(ii) 将执行程序的状态或配置表示为标记单元的潜在嵌套结构。这让人想起化学抽象机（CHAM）中的解决方案[10]。K重写规则（下面解释）然后迭代地转换这样的配置，从保存原始程序的配置开始，以保存结果的配置结束(iii) 使用K重写规则为语言结构赋予语义，通常为每个语言结构提供少量独立规则K的精确语义是根据图重写直觉给出的，以便正确地产生真正的并发语言语义（更多细节见2.5节此外，K规则分为结构和计算，前者的作用只是重新安排配置，这让人想起重写逻辑K还带来了一系列语义创新和实际需求所决定的符号。例如，K规则被认为是事务，说明什么是只读的，什么是读和写的，什么是不相关的。这允许真正的并发，即使在共享的存在。此外，配置抽象机制允许定义既紧凑又模块化，当配置改变时，通常不需要改变现有规则。2.1案例研究：SIMPLE语言在本文中，我们将使用SIMPLE语言的定义来介绍和K，我们在这里简要描述。SIMPLE旨在成为一种教学和研究语言，它抓住了命令式编程范式的本质，并扩展了命令式语言中经常遇到的几个功能程序由一组全局变量声明和函数定义组成。与C一样，函数定义不能嵌套，每个程序必须有一个名为main的函数，当程序执行时调用。为了使它更有趣，并突出K• 多维数组和数组引用。数组计算为数组引用，它是一个特殊值，包含位置（数组元素的起始位置）和数组大小;数组的元素可以是6G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）3--数组引用自身（特别是当数组是多维的时候）。数组引用是普通的值，所以它们可以被赋值给变量，并被函数传递/接收。• 函数和函数值。函数可以有零个或多个参数，并且可以使用return语句突然返回。SIMPLE遵循按值调用的参数传递风格，具有静态作用域。函数名计算为函数抽象，函数抽象是语言中的普通值，如数组引用。• 与当地人一起街区SIMPLE变量可以在任何地方声明，它们的作用域是从它们的声明位置到封闭块的末尾• 输入/输出。表达式read（）计算输入缓冲器中的下一个值，语句print（e）计算e并将其值输出到输出缓冲器。输入和输出缓冲器是值的列表。• 例外. SIMPLE有参数异常（作为异常抛出的值可以被捕获和绑定）。• 通过动态线程创建/终止和同步实现并发。可以生成一个线程来执行任何语句。派生线程在创建时与其父线程共享其线程可以通过join命令同步，该命令阻塞当前线程直到加入的线程完成，通过可获取和释放的可重入锁，以及通过rendezvous命令。2.2K语言、演算或系统的K语法，以及它们的语义所需的额外语法，是使用上下文无关文法（context-free grammar，CFG）定义的，或者等价地，使用mix fix表示法编写的代数签名（即，操作名称包括下划线““作为参数占位符）[ 23，22，12 ]。我们可以根据需要从代数世界中借用任何感兴趣的结构。在本文中，我们使用List{Nonterminal，terminal}来表示对应于非终结符元素的终结符分隔列表的非终结符;例如，List{Exp，@}代表表达式的@分隔列表 当它是逗号时，我们跳过终端;例如，List{Exp}代表逗号分隔的表达式列表在本文和一般的K中如果一个人喜欢一个不同的单位，那么一个人应该提到它作为一个额外的参数列表，例如，列出Exp、@、nil等语法定义和语法分析是一个非常困难的话题，在过去的几十年里已经得到了广泛的研究和实现。K的实现可能会利用现有的技术和工具来定义语法和解析。然而，在其核心，K实际上根本不关心具体的语法。更准确地说，K的语法目前由一个语法计算结构的K类，或Complex-just计算3，即，当放在正确的上下文中时，具有计算能力的结构3.K的句法可以扩展到K以外的其他句法范畴。目前有几K项目，似乎需要这样的扩展，但在这里我们限制自己的最小设置。G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）37与另一个语法类别KLabel一起，用于抽象语法树标签：K：：=KLabel（List{K}）| List{K, a}(generic)KLabel：：= 0 | 1 | 2 | ··· | while（_）_|我的天|··· （语言特定）一种编程语言、微积分或系统语法，包括常量（如原始值），通过简单的关联，最终被视为一组K标签一个唯一的K标签，每个生产和丢弃所有的具体句法类别。这样，任何程序或程序片段都可以被视为（出于语义原因）K抽象语法树（KAST），其节点是K个标签，叶子是“·”默认情况下，我们在选择标签名称时遵循mix fix标记哲学[23，22，12]，但可以自由使用任何命名约定。例如，使用我们的约定，SIMPLE程序的片段= x- 1;}_-_（x（·），1（·）"。KAST表示法在理论和实践上都很方便。从理论上讲，它允许人们给那些需要访问整个语言语法的构造（如替换或代码生成）提供独立于语言的模块化语义，只需简单地根据KAST给出它们的语义，从而不必担心具体的语言语法。实际上，它提供了一种统一的方法来分离语法关注点和语义关注点，将具体语法到KAST的K工具可以（并且确实[53]）提供比K标签集更用户友好的方法来定义语言语法。除了如上所述将语言/演算/系统语法捕获为KAST结构之外，K语法类别还提供任务序列化列表构造，写为如果t1，t2，...，t n是计算，那么t1at2a···at n可以被认为是由t1和t2组成的计算。. ，然后是tn。正如在2.4节中所看到的，例如，如果s1，s2∈K是对应于SIMPLE中两个语句的KAST，那么顺序组合的语义将把“s 1 s 2“简化类似地，如果e1，e2∈K是对应于SIMPLE中两个表达式的KAST，那么定义加法求值策略的重写规则将允许表达式“e 1 + e 2“非确定性地重写为“e 1 a Q + e 2“或“e 2 a e 1+ Q“，其中+ Q和Q +是为此目的专门添加的两个新K标签（换句话说，Q是标签名称的一部分，而不是显式的其他评估策略也是可能的，并且很容易想象，以及让人想起重新聚焦[14]的技术，以支持定义评估上下文。2.3K配置编程语言语义通常由语法驱动，但它通常需要额外的语义数据，以便正确捕获每个语言构造的所需语义这样的数据可以包括将程序变量映射到存储器位置的程序环境，将存储器位置映射到值的存储，8G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）3Fig. 1. SIMPLE的K构形用于函数和异常的一个或多个栈、线程的多集合（或包）、与每个线程相关联的一组保持的锁等等。这样的列表、集合、多集合和映射结构是公知的代数结构，许多论文描述了将它们定义为代数或逻辑结构的各种方式（参见，例如，[35]和Maude[12]手册）。为了区分不同的语义成分，在K中，当我们将它们构造在一起时，我们将这些单元只不过是构造器，它采用所需的结构并产生一个配置项。例如，一个名为store的单元格可以定义为一个操作商店：地图→CfgItem其中Map是从自然数到整数的映射单元格可以嵌套。我们不坚持如何定义配置，因为K的不同实现/实现/编码可以选择不同的表示和符号。重要的一点是，配置，无论多么复杂，都可以被定义为适当的代数规范。此外，K假设这样的配置在语义规则给出之前就被预先定义了，因为程序配置的结构是赋予K模块性的一个重要方面（如下一节所讨论的）。接下来我们非正式地讨论SIMPLE语言的K配置，如图1所示。回想一下2.1节，SIMPLE有突然终止、异常、动态线程、锁同步和内存共享以及输入/输出的函数。 它的配置包括一个顶层单元T，它包含一个线程单元，一个全局环境映射单元genv，它将全局变量和函数名映射到它们的位置，一个共享存储映射单元存储，它将每个位置映射到某个值，一个集单元忙着保存锁，G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）39已被线程获取但尚未被线程释放，一个set cellterminated，保存已经终止的线程的唯一标识符（join所需），输入和输出列表cell，以及一个nextLoccell，保存指示下一个可用位置的自然数。与小型语言不同，在SIMPLE中，我们更喜欢显式地管理内存。nextLoc中的位置计数器模拟存储中的实际物理线程单元包含程序中每个现有线程的一个线程在任何给定的时刻，可能存在零个、一个或多个线程单元。每个线程单元包含一个计算单元k，一个控制单元，它包含跳转到程序执行中某些感兴趣的点所需的各种控制结构，一个本地环境映射单元env，它将线程本地变量映射到存储中的位置，最后a包含映射单元，它指示线程已经获取了哪些锁，到目前为止还没有释放，以及每个锁已经获取了多少次而没有被释放（SIMPLE控制单元当前只包含两个子单元，一个函数堆栈fstack是一个列表，一个异常堆栈xstack也是一个列表。可以在控制单元中添加更多的控制结构，诸如用于循环的中断/继续的栈等，如果语言扩展了更多的控制改变结构。请注意，除了k之外的所有单元也被初始化，因为它们包含相应排序的基项。第k个单元格用要执行的程序（的KAST）初始化，如$PGM占位符所示，后面跟着执行任务（其语义将在第3节中给出）。K中的配置声明以紧凑和直观的方式同时做几件事：(i) 它为配置定义了一个代数签名，如本节第一段所述;(ii) 它告诉如何初始化配置;(iii) 它为具体化语义重写规则提供了基础，由于模块化的原因，可以更加抽象，如下一节所示K的实现可以选择不同的方式来定义配置，以及其他方式来初始化它们。例如，我们当前的实现使用XML来分隔单元格（例如，<线程>.& lt;/threads>），它允许用户通过自定义$PGM-like占位符进一步初始化配置，甚至允许将某些单元连接到标准输入/输出，以便在执行K定义时获得真实的解释器[53]。K为定义复杂的配置提供了支持，但这并不意味着K的定义总是要使用它，甚至K也不鼓励基于环境的语义。例如，为了定义一个语言或演算的纯语法的、基于替换的语义，我们只需要一个用$ PGM初始化的单细胞配置。读者可以参考K工具发行版中的几个基于替代的定义。10G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）32.4K规则如2.3节所示，通过将目标程序放置在指定位置并使用其声明的内容初始化任何其他单元来初始化配置从这里开始，K重写规则给出了语言语义（非确定性和并发）匹配和应用，潜在地生成目标程序的任何可能的行为。K中有两种类型的规则，即结构规则和计算规则。直观的结构化规则分解并最终将准备好处理的任务推到计算的顶部（或左侧）。然后，语义规则告诉如何处理原子任务。换句话说，结构规则不算作可观察的步骤，而计算规则算作可观察的步骤。两者之间的形式语义差异将在2.5节中讨论。除非明确标记为结构规则我们首先讨论结构K规则的一个重要类别，加热/冷却规则。我们对这些规则的术语来自化学抽象机（CHAM）[10]。人们可以自由地使用不同的箭头来特别地加热/冷却或一般地用于结构规则，例如~或z，而不是CHAM中的类似于X的箭头例如，在我们当前的K加热/冷却规则的作用是根据所需的评估策略重新安排计算，以便将这种结构化过程的总体效果是，与具有评估上下文的归约语义不同[20]，K中的重写不需要是上下文敏感的。例如，考虑SIMPLE中的加法运算，它是不确定的。然后，我们为它添加两对可逆结构规则，即规则E1+E2E1aQ+E2[结构]规则E1aQ+ E2E1+E2[结构]规则E1+E2E2a E1+Q[结构]规则E2a E1+QE1+E2[结构]请注意，我们对规则使用了二维表示法，重写规则的左项这个符号是一个更一般的原理的例子，稍后会解释第一条和第三条规则是说，我们可以在任何时候通过第二条和第四条规则说，我们可以在任何时候通过插入将其激烈的争论重新纳入其背景。这样，我们可以非确定性地探索所有可能的顺序，其中两个参数的总和可以减少（所有的评估交织）。G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）311编写上面的规则有两个问题。首先，编写这样的规则是乏味的，无聊的和容易出错的。为了解决这个问题，在K中，我们采用了一个简单而直观的语法注释：语法Exp：：=Exp+Exp[严格]与句法结构相关联的如果希望一个构造只在它的某些参数中严格，那么应该在“strict”属性后面的括号有时需要按照给定的顺序（比如从左到右）计算构造的参数。然后可以使用属性“seqstrict”（来自sequentially strict）而不是“strict”。不难看出，所有这些都可以很容易地转化为如上所示的结构加热/冷却规则例如，如果sum构造被注释为“seqstrict”，那么上面的最后两个规则V1+E2E2a V1+Q[结构]规则E2a V1+QV1+E2[结构]编写上述加热/冷却规则的第二个问题是，它们不能立即执行，因为它们会导致不可终止。这类似于说明某些构造的可交换性的规则如果天真地执行可能导致非终止性同样的，项重写理论允许重写模公理，如交换性（和结合性，幂等性等）。重写引擎提供了实现它的决策过程，在K理论中，我们假设用计算规则重写以结构规则为模发生，并且K的实现提供了处理结构规则的算法或过程。这些程序超出了本文件的范围。我们只提到，如果一个人愿意用（一些）非确定性来换取性能，那么他可以通过添加附加条件来打破如上所述的加热/冷却规则的循环，即加热的表达式总是非值（例如，第一条规则中的E1），并且冷却表达式总是一个值（例如，第二条规则中的E1更一般地说，我们可以像上面那样根据加热/冷却结构规则来指定任何评估上下文例如，在SIMPLE的定义中，考虑以下K求值上下文，为了计算数组元素的左值，我们需要计算该元素的索引（这里A在数组表达式中的范围）：C上下文左值（A[Q]）这个上下文可以用以下两个结构规则来表示：12G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）3规则左值（A[E]）E为左值（A[Q]）[结构]规则E为左值（A[Q]）左值（A[E]）[结构]注意：在约简语义中，上面的求值上下文将使用形式为“Cxt：：= lvalue（A（Cxt））”的语法声明来 这样的评估上下文的声明然后被自动转换成如上所述的加热/冷却规则。加热/冷却规则不限于仅通过常规评估上下文来定义评估例如，受实际需求的刺激，当前的K工具允许用户还指定C上下文I*Q当I/=Int0时C上下文Q. M当QKsuperC上下文++Q左值（Q）上面的第一个上下文指出，乘法运算的第二个参数仅在第一个参数的值不同于零时才被计算（因为人们可能希望给乘法一个短路语义，第二个声明成员访问表达式中的对象在与super不同时被求值（因为super成员访问是静态解析的，所以它们具有不同的语义）。上面的第三个上下文声明更特殊，它使用了K它基本上是说，当计算增量结构的参数时，它应该用左值结构包装包装器的作用是允许对正在计算的表达式进行特殊处理。这正是在l值的情况下所需要的，因为我们想要“几乎”评估表达式（可以是变量，数组元素，对象字段），但一旦我们计算位置就停止了。上述三种情况对应的加热规则分别为规则I*EEaI*Q当我Int0规则E. MEaQ。M当EKsuper规则++E左值（E）a++Q[结构][结构][结构]相应的冷却规则与上述规则相反。特别要注意的是，也就是说，这个包装器应该只具有上下文意义，用于改变语义，但由它保留。在某种意义上，这些包装器实际上提供了本地类型的评估上下文。人们可以设计其他类似的符号，并且K工具很可能在未来会包含新的或不同的符号。这里的要点是，加热/冷却规则是非常强大的，在定义复杂的评估策略时赋予K灵活性并不是所有的结构规则都需要像上面这样的加热/冷却规则。有时G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）313我们希望将一些语言构造去糖为其他构造或内建的K构造，并且我们不希望这样的步骤是可观察的。例如，人们可能想将“for”循环脱糖语言设计者可能不希望这样的结构规则是可逆的。事实上，使所有结构规则可逆可能会在语言中产生不受欢迎的非确定性计算规则许多K规则，特别是那些计算性的规则，涉及不止一个细胞。例如，SIMPLE的变量查找规则（如下所示）从k单元格中获取要查找的程序变量，然后从env单元格中获取其位置，然后访问存储单元格中该位置处的值，最后将程序变量重写为该值。因此，大量的配置结构需要在变量查找规则中指定，最终只有一小部分结构发生变化，而其余部分保持不变。传统的左-右形式的重写规则有两个缺点，一个是实践上的，一个是理论上的。在实践方面，我们必须在规则的左侧和右侧术语中提到整个配置上下文，这是乏味的，容易出错的，并且是非模块化的。在理论方面，这样的规则强制执行并发的交错语义，其中可能需要真正的并发语义;例如，读取存储中相同位置的两个线程将必须交错，仅仅是因为对应的变量查找规则实例的左侧重叠。K通过引入一种用于编写重写规则的就地样式来解决这些问题，我们将在下面讨论，并且它的语义不基于转换到传统规则，我们将在2.5节中简要讨论。下面是SIMPLE中变量查找的K规则规则KXV店L→VenvX›→L因此，配置上下文仅被提及一次，并且改变的部分被下划线，下面写有改变传统的规则左-右是一种特殊的K规则，其中整个左项都加下划线，右项在下面（就像上面显示的结构规则上述规则中还有两个额外的K-特异性方面需要讨论。首先，请注意所涉及的细胞要么是圆形的，要么是侧面撕裂的撕裂的单元格一侧意味着它可能包含更多的数据，但这些数据是无关紧要的。例如，要查找的变量X需要首先出现在计算单元k中，但其余的计算上下文是无关紧要的。类似地，环境中剩余的绑定以及存储中剩余的位置也是无关紧要的。我们假设映射的定义是键→值对的集合。在上述规则中要注意的第二个K-特异性方面是配置上下文不匹配。事实上，如图1中SIMPLE的配置所示，单元存储并不位于与k和env相同的单元中，因此这三个单元不能像查找规则所规定的那样匹配在一起这条规则利用了K14G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）3配置抽象机制（以前称为上下文转换[43]），它允许我们只指定每个规则中所需的单元格，其余的配置上下文从定义的配置中推断出来（例如，图1中的SIMPLE）。这种抽象的配置规则上下文的具体化基于几个原则和标准，这些原则和标准有助于消除可能的具体规则之间的歧义。他们在[43]中进行了充分的讨论这里我们只提到其中之一，即局部性原理，它指出配置将完成，使得将添加最小数量的单元这确保了在多线程SIMPLE程序中，上述规则中的单元格k和env不会被分配给不同的线程单元格。虽然这与配置结构一致，但将它们放在同一个线程配置抽象的动机来自于实际需要 对于模块化语言语义，更确切地说，是在配置变化下所需的模块化。随着新功能被添加到编程语言中，它的配置往往会多次改变其结构。例如，在SIMPLE的情况下，很自然地从它的非并发片段开始（为了首先关注顺序语言结构），其中不包括线程和线程单元，它们现在的内部单元与现在共享的单元处于同一顶层。然后，上面的查找规则按原样匹配，因为它的三个单元格位于单元格结构中的同一级别。当我们添加线程时，我们意识到我们需要一个更结构化的配置，所以我们重新组织它，如图1所示。在传统的结构操作语义（SOS）中，配置结构的改变需要重新访问所有现有的规则，这是非常不方便的。模块化SOS [36]解决了SOS的这个问题，当配置由一组可扩展的（非嵌套的）语义单元组成时，允许规则只从配置中抓取需要的那些单元。K进一步推动了这一想法，允许同样的事情也发生在细胞边界上。这样，当线程被添加到SIMPLE语言中时，我们就不必改变变量查找的规则。作为上述抽象能力的基础的总体原则，以及K的大部分设计一般来说，一直是以下内容当语言被扩展时，我们写在规则中的所有内容都可能对我们不利框架能为我们自动推断的越多越好。非正式地，上述单元和配置抽象可以被认为是K在实现方面，可以静态或动态地应用此规则完成过程。在我们当前基于转换到Maude [53]的实现中，我们静态地应用它们;例如，上述K规则转化为常规重写规则：RULEthreads（thread（k（XaK）env（X›→L，Env）Thread）Threads）store（L›→V，Store）⇒threads（thread（k（VaK）env（X›→L，Env）Thread）Threads）store（L›→V，Store）K、Env、Thread、Threads和Store是对应于撕裂的单元格框架变量。我们目前的K工具利用Maude的优势，如其多集和上下文无关的重写。其他后端可能需要更复杂的翻译。G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）315例如，一个人可能需要完成配置上下文一直到顶部（如果目标语言不支持上下文不敏感重写），或者向保存映射，集合或多集合的单元格添加左右框架（当多集合重写不可用时）。在本节的剩余部分，我们将讨论另外两个K规则，它们也是SIMPLE的语义的一部分，它们说明了K的配置抽象的另外两个特征前者的动机是需要动态地向配置中添加新的单元实例，而后者的动机是需要匹配驻留在同一单元的不同实例中的项。让我们首先考虑给出线程生成语义的规则：规则·箱包线程KSenvEnvID不新鲜时（T）生成线程在将子线程添加到线程池时，将生成表达式求值为fresh（thread）标识符T;回想一下，“·“是K中任何集合数据类型的单位，它读取“nothing”。 派生线程被赋予其父线程的环境，但没有提到派生线程中的其他单元。但是，请注意，派生的线程单元格是撕裂的。 这告诉K用默认单元格和它们的默认内容填充缺失的部分，如配置中所定义的。 这也是为什么在定义配置时要求用户提供默认单元格内容的另一个原因（另一个原因是初始化配置）。下一个规则给出了集合同步的语义，说明下一个语句是相同值集合同步请求的两个线程可以丢弃它们的集合语句并继续执行：规则K第五集合点·KK第五集合点·K[会合]K如何知道上面的两个k单元格应该出现在两个不同的线程中，而不是同一个线程中同样，图1中定义的配置告诉我们如何消除这条规则的歧义：线程单元被声明为具有其多重性“*"，这意味着在执行语义期间的任何给定时刻，我们可能在线程单元内有零个，一个或多个没有其他单元格具有多重性“*"，因此上述规则匹配配置的唯一方法是 对于两个k个单元格，每个单元格出现在线程单元格内。K此外，由于K的语义是通过重写给出的，因此会合规则需要匹配两个不同的小区，这需要线程k环境产卵S环境T16G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）3在施加之前至少两根线已经到达了一个连接点2.5K的语义K的语义是根据变迁系统给出的。任何K定义都可以被看作是一个转换系统的生成器，每个转换系统对应于所定义语言中的每个程序。正如预期的那样，这些转换系统的状态由程序配置给出，转换由计算规则的实例给出。结构规则不产生转换，它们的作用是在结构上重新排列配置，以便计算规则匹配和应用。不太明显的是，K允许（但不强制）多个规则实例并发地应用于给定的配置，作为同一转换的一部分，即使它们重叠;唯一的限制是不允许一个规则实例重写另一个并发规则实例需要访问的子项。这让人想起事务的工作方式：允许并发读取，但不允许读/写或写/写并发。目前，我们让K相反，我们更愿意把它看作是我们目前在K工具中实现它的方式，即静态去糖的语法糖。 我们这样做有几个原因：第一，配置抽象对最终的转换系统没有影响，它的作用是简单地调整规则以适应预期的配置;第二，它为我们和其他人赢得了时间，以更好地理解，评估和收敛配置抽象在其完全的一般性中应该意味着什么;最后，也许是相关的，配置抽象现在似乎很难以算法以外的任何其他方式形式化。因此，配置抽象的严格形式化目前只能给我们带来很少或根本没有好处，因此不值得付出代价。K规则描述了如何通过改变术语的某些部分来转换术语K与标准项重写共享匹配替换的思想，但是每个Krule还指定模式的哪一部分是只读的。接下来让我们正式定义K规则的概念和所需的并发K语义。给定一个签名和一个（可能无限的）变量集X，令T（X）表示具有来自X的变量的X项的论域。给定W ={Q1，.，Qn}，命名为接触变量s，或孔s，一个W-接触变量r_n（X）（假设X <$ W=r_n）是一个项k∈T_n（X<$W），其中W中的每个变量只出现一次. 具有n元组t =（t1，.，t n），写作k [t]或k [t1，...，t n]，是项k[t1/Q1，.，t n/Qn]。我们可以把t看作一个替换t：W →T（X），定义为t（Qi）=ti，在这种情况下k[t] =t（k）。在下面的内容中，我们固定一个签名和一组变量X。定义2.1[43，54，52]K规则ρ：k[LR]是一个三元组，其中：k是W-上下文其中W是k的洞;k可以被认为是ρ的“只读”部分或“局部”上下文; L，R：W → T（X）分别将W中的每个洞与原始项和其替换项相L，R可以被认为是ρ的当W={Q1，···，Qn}且L（Qi）=1i且R（Qi）=ri时，我们可以写为：G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）317k[ l1r1，...，Ln] 的一种Rn而不是k[LR]，因为孔是隐式的，不需要提及。W中的变量仅用于标识k中重写发生的位置;在实践中，我们通常使用上面的紧凑表示法，即在要重写的子项下面加下划线，并在下面写上它们的替换项。它包含了所有需要的语法类别，即语言语法、配置语法、辅助操作等。我们可以关联到任何K规则ρ：k[LR]常规重写规则K2R（ρ）：L（k）→R（k）。例如，在我们当前的K实现中使用了这种翻译（通过翻译为Maude;参见2.6节）。虽然这种转换降低了资源共享的并发性（因为只有在规则不重叠的情况下才允许重写逻辑中规则的并发应用），但在许多情况下它是可以接受的。相反，给定常规重写规则τ：左→右，我们可以生成一个明显的（零共享）K规则R2K（τ）：Q[左]。 基于这个理由，权我们有时会使用传统我不知道你在说什么。如果τ是重写逻辑规则，则nt−→τtJ表示二进制重写由τ生成的关系，即：t通过τ的一个实例重写为tJ。像往常一样，τ∗τ−→是f −→的恢复和过渡。并发K重写关系的定义比传统的并发项重写关系更复杂。这是因为我们希望它尽可能地并发，因此K中定义的并发语言或演算不仅具有重写逻辑的标准并发语义，禁止并发兑换之间的重叠，而是通过允许兑换之间的重叠来实现更大的并发性，只要重叠只发生在只读部分。这意味着两个或多个并发重写可以同时共享状态的某些公共部分实现上述目标的关键是要考虑K规则的特性，即它们明确表示哪些部分是共享的，哪些部分是重写的。非冲突K规则被期望可能被并发地应用，像事务一样，其中“非冲突”规则意味着它们中的任何一个都不会重写被另一个访问（共享或写入）的项的部分。我们目前根据图重写（双推出方法）定义了K我们建议感兴趣的读者参考[54，52]以了解详细信息。这里相关的是，可以定义一个K并发重写关系，它捕获了上面所需的规则作为事务的非正式语义;我们将其表示为”而不是“。18G. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）3J···n1ρ∗我如果cfg是一个SIMPLE配置项（在图1中的签名之后），包含两个线程，它们的计算分别从变量x和y开始，因此需要查找，那么查找规则的两个实例（参见2.4节）可以同时应用，x和y的两个实例可以在一个步骤中重写为它们的存储值;也就是说，如果cfg请注意，当查找的K规则被认为是传统的重写规则时（如在K2R映射中），这 是不 可 能的 ： 两个 规则 实 例在 存 储单 元 上重 叠 ，因 此它 们 需要 交 错产 生cfgcfgxcfg'或cfg cfg y cfg'，其中cfg x是仅用其值替换第一个线程中的x的此外，当x和y是相同的（共享的）变量时，由于两个规则实例读取但不改变对应于x的存储位置（读/读访问），cfg“>cfg另一方面，如果一个线程读另一个线程写（见第3节中的变量赋值规则）同一个变量，那么这两个访问不允许并发进行，它们需要交错。如果读变量和写变量是不同的，那么这两个访问可以并发进行ρ++ρK在一个并发步骤中使用规则ρ1，. . .，ρn：意味着t可以定理2.2[54，52]设ρ，ρ1，. ......、 ρ n不一定是不同的K规则。K2R（ρ）JρJ完备性：如果t −→ t，则t> t。ρJK2R（ρ）J如果t> t，则t −→ t。ρ1+···+ρnJ可串行化性：如果t不存在，则存在的n是项st0，· · ·，tn的等式，使得t0= t，t n= tJ，且t i−1<$> t i。完整性意味着任何使用重写逻辑的步骤也可以使用K重写。合理性指出，使用K重写进行的任何非并发步骤对应于零个、一个或多个重写逻辑步骤;这是由于要重写的项被表示为K中的图，并且需要零个、一个或多个项重写步骤来模仿图重写步骤（当重写部分不可达时为零）。可串行性是指并发重写关系<$>除了重写关系→之外不会到达任何其他项：它只是在可能更少的步骤中到达它们。从实践的角度来看，上述定理告诉我们，在许多情况下，使用K2R映射将K规则转换为传统的重写规则是翻译过程中唯一丢失的是原始K定义中可用的真正并发量。然而，请注意，大多数编程语言的语义框架本质上都遵循交织哲学，因此“失去一些真正的并发性”甚至不能在这些框架中表达出来。然而，我们相信，随着大规模并行架构的发展，最大化语义框架的真正并发能力将越来越受欢迎，因此K不会对w.r.t.它对并发性的理论支持。也就是说，认为KG. R os u，T. F. Serbanuta/ElectronicNotesinTheoreticalComputerScience304（2014）319SSS联合 例如，取相同的t，u和t如上所述，但=t。图二. 与程序相关联的状态空间。意识到，或者谁不想进入图重写