没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记162(2006)209-215www.elsevier.com/locate/entcs为什么总是CSP?Tony Hoare微软研究有限公司摘要最初的沟通顺序过程理论模型的灵感来自于Milner、Scott和Dijkstra的成果。它是在米尔纳的通信系统微积分出版的时候开发的。为什么CSP与CCS不同?ESPRIT基础研究行动“CONCUR”汇集了三个原始并发演算的支持者:ACP,CCS和CSP。人们希望我们能开发出一种统一的微积分,并同意采用它。我们到底为什么失败了?我想和你们分享一下我在25年前思考这些问题的方式。从那时起,进行了许多出色的比较研究。因此,我们现在可以看到,如何才能最好地统一这些理论,而不同化它们的独特特征或损害它们的独特优点。保留字:CCS,CSP,互模拟,细化,撤回,统一理论。进程代数(Process algebra)是计算机科学的一个分支,它研究进程的数学模型,这些进程被视为与其他类似的代理及其共同的环境连续动作和交互的代理。代理人可以是真实的对象(甚至是人),也可以是人工制品,可能体现在计算机硬件或软件系统中。在过去的四分之一世纪中,已经构建和探索了许多不同的过程演算;其中许多过程演算的灵感来自于Milner在CCS上的原始工作,而其他过程演算显然更多地基于CSP。在这篇文章中,我想非正式地解释并激发这两种传统相互偏离的方式。但首先,我必须强调,整个范围内的相似性远比它们的差异性更重要。因此,在我的结论中,我建议现在是时候统一这两种建模风格了,以便使实践工程师能够利用它们互补优势的组合如果它们一开始就不不同,这是不可能的。原始过程和操作符CCS最初设计的一个主要目标是发现和编纂一组最小的基本原始代理和操作员,它们能够结合1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2006.01.031210T. Hoare/Electronic Notes in Theoretical Computer Science 162(2006)209描述了在研究并发代理人的相互作用时遇到的所有特征现象原语的最小化是所有科学分支的一个基本目标;在过程代数中,它还有一个额外的优点,即它简化了在所选微积分中可描述的所有主体的属性的归纳证明。CCS当然已经实现了它的目标,并且随后研究的各种有用的运算符都可以用CCS原语来定义。从一开始,CSP就对更广泛的有用运算符更感兴趣,而不考虑它们中的哪一个可能被选为原语。实践中的数学家通常有几十个运算符,他们并不关心哪一个是原始的。在CSP的标准版本中定义了近12种结构化运算符;它们的定义受到构建复杂计算机系统的设计者和实现者例如,CSP包括熟悉的顺序组合操作符这是有用的,因为它使系统能够被分割成单独实现和理解的组件当它们被顺序地组合时,它们的执行被保证是时间上不相交的,在这个意义上,一个的活动完全在另一个的活动之前发生。因此,世界上所有的资源都在操作数之间无声地传递,没有任何实现的开销并发计算机系统的设计通常涉及顺序结构和并发结构的微妙相互作用,理论家的注意力对它们都有好处。基于CCS的理论倾向于忽视顺序组成,完全合理的理由是,可以很容易地构建出并行的组合和同步。选择CSP操作符的另一个标准是尽可能独立地探索并发编程的重要特性。例如,CSP将选择的两个概念分开:一个是由过程的外部环境做出的选择,另一个是非确定性选择的纯粹形式,它是内部的,不能被环境所影响类似地,CSP并发组合的基本操作符避免隐藏其操作数之间的内部交互。因此,并发组合的某些动作可能被计划为需要来自三个或更多个过程的同步参与。隐藏被定义为一个单独的操作符,因此其属性可以独立于并发性进行研究。因此,主CSP并发组合运算符具有非常简单的定义,并且允许结合性、交换性等的简单证明。其他有用的并发形式(交织、链接和锁步同步)都可以用以下术语来定义:的主要运营商。此外,终端的多路同步√1998年, )自动实现同步终止顺序流程.最后,并发操作符不会引入非确定性。这一系列的免费午餐给人的感觉是,数学真的对我们有利。特别是在建模和模型检查的实际应用中,随后的工作揭示了多路同步的非凡表现力决定算子定义细节的一个最终标准是,它能导出优美而有用的定理。甚至定义本身也应该是T. Hoare/Electronic Notes in Theoretical Computer Science 162(2006)209211优雅,当以所选择的定义风格表达时。因此,CCS的算子有优雅的操作定义,而CSP算子有相当优雅的指称定义。但CSP愿意将其定义复杂化,以改善算子的代数性质。例如,CSP将并行组合子定义为严格的,因为任何一个操作数的活锁都会将整个系统还原为活锁。准确性需要在外延定义中增加一个条款。有实际的论据支持这一点,因为它使任意的优先级被分配给进程,而不需要保证逻辑的正确性。但最初的动机是简化代数和范式。严格-对于使进程链接操作符>>具有关联性,也需要ness最后,需要建立与操作语义的形式对应,把错综复杂的公平性问题放在一边。在CONCUR项目的时候,我认为命名、代数和操作定义的精心组合是支持采用CSP统一角色的有力论据。基本判断所有的过程演算都提供了一种方法来证明一个过程与一个规范的一致性,这个规范是在同一个演算的符号中表达的。这是有价值的,当规范比它的实现更清楚或更简单地表达实现的额外效率通常会引入复杂性和模糊性,这就是证明正确性的必要性。CCS的正确性关系要求进程及其规范通过互模拟的对称等价关系来关联。互模拟有一个优雅的共归纳定义,它验证了简单和卓越的证明。利用模型检测的基本算法,可以自动高效地构造互模拟证明。通过等价关系定义正确性意味着一个规范及其实现在微积分本身中必须是本质上不可区分的。CSP更一般地根据排序关系来定义正确性,称为细化。细化直接定义为对进程与其环境一起执行时的行为的观察正确实现的观察结果必须包含在其规范所描述的观察结果中,因此也是其规范所允许的观察结果。包含是一种不对称关系。意图是,一个规范可能是相当抽象的,并且有许多可区分的正确实现,所有这些都可以被证明是对它的细化;实现细节的选择仍然很重要,但可以故意推迟到设计轨迹的后期,甚至可以作为执行的任意结果原则上,CSP的精化关系在机械计算上不如CCS的互模拟有效但在实践中,这个问题已经被克服。FDR的设计者,CSP模型检查器,在开始证明实现的正确性之前,利用CSP代数将规范简化为规范形式。原则上,这种减少引入了高复杂性,但不幸的是,212T. Hoare/Electronic Notes in Theoretical Computer Science 162(2006)209自然的规范通常比实现简单,并且整体性能非常高。CSP不坚持任何特定的符号来表示其规格。对系统所需观测的任何数学上合理的描述都可以作为它的抽象规范,这种抽象规范可以与微积分中表达的更具体的规范自由地混合。如果一个过程不满足它的规范,那么当这个过程被执行时,总是有可能找到一个可观察的证据来证明这一事实。CCS规范也可以用Hennessy和Milner设计的更具表现力的逻辑来表达。它更有表现力,因为它包括连接和否定,除了多种模态和固定点。它的语义由CCS模型公理化地定义,而不是由与具体行为观察的关系定义在像CSP这样的基于观测的理论中,选择哪些观测是相关的是至关重要的。显然,假定过程与其最终环境之间的相互作用是可观察的是合理的。在CSP中,过程内部状态的某些精心选择的属性也被认为是可观察的。这种选择主要取决于并发系统设计者的需要如果一个理论不能模拟一个无因律,那么就不可能用这个理论来证明它的不存在。特别是,当一个进程显然已经停止了与环境的交互时,重要的是要区分原因:在某些情况下,这可能不是一个进程,因为进程已经成功地完成了所有的任务;在其他情况下,也许进程无法继续,因为它在与环境的通信中陷入僵局;或者最糟糕的是,也许进程正在进行一个无限的内部计算,有时称为活锁。免于死锁和免于活锁通常被归类为活性属性,需要更复杂的证明方法。CSP通过引入特殊的符号(拒绝和勾号)来表示这些现象,从而将它们转化为安全属性。 因此,CSP区分了三个不执 行 任 何 操 作 的 基 本 进 程 ( STOP 、 SKIP 和 CHAOS ) , 而 CCS 只 处 理 一 个(NIL)。CCS的许多发展现在认识到需要观察而不是相互作用;它们现在通常被称为倒钩。即使是CCS的原始版本也引入了一个这样的特殊非交互作用,即沉默事件τ,代表一个过程的内部转换或计算步骤。 作为单个原语,这是一个很好的选择,因为它可以用来定义许多其他的兴趣概念,包括内部非决定论,稳定状态,拒绝和分歧。CSP倾向于将这些其他更专业的概念与每个概念隔离开来进行其他的,有点武断地拒绝了沉默的事件τ。变化CCS的另一个主要初始目标是为构建和探索一系列相关过程演算提供基础。选择一个标准-T. Hoare/Electronic Notes in Theoretical Computer Science 162(2006)209213可以根据每个特定应用的需要进行计算。它是一个基础,在这个意义上,所有的范围的演算必须被约束,以满足所有的基本属性和等价,这是有效的CCS本身。为了保持尽可能广泛的应用范围,有强烈的动机将CCS互模拟可证明的定律集限定为一个明显的基本最小值。CSP追求完全相反的目标-验证尽可能多的方程。额外的方程在推理计算机系统设计和实现的正确性方面可能是有用的;额外的方程在优化计算机硬件或软件中执行的过程设计方面也是有用的对方程数量的主要限制是需要保持行为良好的计算机系统与容易发生特定故障(如死锁和发散)的计算机系统之间的区别。CCS在它的另一个原始目标上取得了巨大的成功--为开发大量其他类似的过程计算提供一种模式和方法。每个演算都从它自己的操作符和原始过程的语法选择开始。语义的递归定义是通过转换规则或结构化操作语义给出的。这为实际实现提供了指导,并支持程序员尝试调试程序的操作直觉。最后,一个等价关系,通常基于(和弱于)互模拟,定义在语法形式,其中一个过程可以表达。两个这样的语法形式是等同的,如果它们可以被证明是等价的,在所有的情况下表示的符号;平等的证明这使得重要的平等概念变得有些脆弱:语法或转换规则中最轻微的变化可能需要重新进行许多证明。这并没有被证明是一个严重的缺点,因为对新过程演算的研究通常从头开始,没有太多地重新使用早期演算的具体定义和定理CCS开创的定义原则是非常强大的,因为它保证了这样定义的数学对象总是存在的。对于CSP,原始过程或算子的每个定义都被约束为满足或保持观测模型上的某些健康条件例如,如果一个过程参与了一个长序列的相互作用,那么一定有一段时间,它被观察到参与了其中一些较短的子序列这由跟踪集的prefix闭包的健康状况表示健康条件的作用很像物理学中的守恒或对称原理,因为它们为微积分中表达的陈述、定义和假设提供了快速的可行性检验。然而,伴随每个定义的额外证明义务是额外的工作,通常不受计算机科学家欢迎。CSP运算符定义的另一个限制是它必须是单调的,在这个意义上,它保留了其操作数的细化顺序。 这是必要的,以确保复杂系统的组件可以安全地细化,结果可以组合以满足原始规范。然而,它允许递归被著名的214T. Hoare/Electronic Notes in Theoretical Computer Science 162(2006)209塔斯基-纳斯特建筑公司每一个定义都应该伴随着一个证明的义务,这可能是对基于CSP的理论范围相当狭窄的一种解释。值域成员之间的关系与经典数学中所熟悉的关系相似例如,标准CSP的故障和跟踪模型是通过简单地从观测集合中省略分歧和/或拒绝而导出的。所有在标准理论中有效的方程(以及更多的方程)在约化理论中仍然有效,并且不需要再次证明。其他更专业的演算是通过标准演算的组成部分的专业化而获得的例如,通信信道上的输出是一种特定类型的交互,被建模为由信道名称和消息内容组成的对。然后,输入被建模为沿着特定通道的所有可能消息中的外部选择。因此,从输出器到输入器的成功同步通信是通过并行组合的通常定义实现的CSP模型的证明方法与经典离散数学中的方法完全相同,涉及集合、序列和映射等标准概念。CCS的证明方法是高度创新的,涉及语法定义、操作语义、递归、归纳和共归纳等技术;这些显然仍然属于计算机科学的范畴。在这些证明风格之间的选择绝对是个人品味的问题。在纯数学家中也可以发现类似的二分法,他们常常几乎是根据天生的天性把自己归类为分析家或代数学家。许多人强烈喜欢一种风格,并发现很难改变。显然,数学本身从这种风格的多样性中获益匪浅, 我希望这篇文章已经论证了多样性给这项研究带来了同等的价值在进程代数的狭窄领域中。CCS和CSP似乎占据了几乎所有频谱的极端在所有随后探索的进程演算中,CCS定义了一组最小的原语和运算符,以及一组最小的方程,而CSP探索了一系列广泛的概念,这些概念在并发系统设计中被证明是有用的。从广义上讲,在所有已经探索过的过程演算的变体中,CCS和CSP仍然占据着极端的位置。理论的统一极值的存在对于数学家探索它们之间的整个变化范围是一个很大的优势。在实际应用中,它也具有优势,这在极端情况下自然是最大的。如果强行过早地同化这两种结石,这些优势很容易丧失。如果CONCUR项目成功地实现了其最初的目标,进程代数将是一个贫穷的研究领域。但我们能为实践做些什么呢- 工程师谁希望结合优势,在每一个极端发现?幸运的是,数学家们很清楚如何做到这一点。T. Hoare/Electronic Notes in Theoretical Computer Science 162(2006)209215通过将一种理论的对象映射到另一种理论的对象上,同时保留重要的结构属性。在进程代数的情况下,我认为这些映射是Scott收缩。这些都是伽罗瓦联系的简单例子,它们本身也是范畴映射的简单例子。我自己的研究方法表明,转换系统的CSP本质上是一个子集的通用转换系统的CCS。在这个子集中,相互细化与互模拟相同,细化与模拟相同。此外,还有一个收缩,它将CCS的每个过程投影到CSP子集中最接近的近似值上。收回由CCS中标准的那种转换规则定义。CSP过程的所有健康条件都可以通过它们是收缩的不动点的陈述来表达。因此,可以使用互模拟在CCS中进行定义和证明,并通过收缩将结果直接投影到CSP中。事实上,有一个完整的撤回链,将CCS的各个版本相互联系起来,并与CSP的各个版本联系起来。有一种回缩将互模拟映射到弱互模拟,还有一种回缩引入了代表分歧、拒绝和痕迹的倒钩。通过组成这些撤回的适当子集,可以在这些不同的结石之间移动,根据哪一个对手头的任务最有利这是一个结论,不需要我们作出任何判断是否子集优于完整的集合,反之亦然。这些发现是在与何继峰的密切合作下完成的,为的是实现编程理论统一的长期目标
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- 京瓷TASKalfa系列维修手册:安全与操作指南
- 小波变换在视频压缩中的应用
- Microsoft OfficeXP详解:WordXP、ExcelXP和PowerPointXP
- 雀巢在线媒介投放策划:门户网站与广告效果分析
- 用友NC-V56供应链功能升级详解(84页)
- 计算机病毒与防御策略探索
- 企业网NAT技术实践:2022年部署互联网出口策略
- 软件测试面试必备:概念、原则与常见问题解析
- 2022年Windows IIS服务器内外网配置详解与Serv-U FTP服务器安装
- 中国联通:企业级ICT转型与创新实践
- C#图形图像编程深入解析:GDI+与多媒体应用
- Xilinx AXI Interconnect v2.1用户指南
- DIY编程电缆全攻略:接口类型与自制指南
- 电脑维护与硬盘数据恢复指南
- 计算机网络技术专业剖析:人才培养与改革
- 量化多因子指数增强策略:微观视角的实证分析
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)