理论计算机科学电子笔记162（2006）317-321www.elsevier.com/locate/entcs过程演算：开始的结束？（从思想实验到实验语义学）彼得·休厄尔英国剑桥大学计算机实验室摘要本说明从过程演算的角度出发，介绍了在对真实世界的TCP和UDP网络协议进行研究建模过程中所吸取的经验教训。保留字：进程演算，TCP，实验语义进程演算的一个早期驱动力是希望建立并发的基本演算，足以表达许多现象和例子，并扮演类似于函数计算的lambda演算的角色。然而，回顾过去25年，研究已经产生了数量惊人的非确定性和并发系统模型。有数以百计的演算和等价物，许多配备了复杂的证明技术或模型检查算法.在这个各种各样的模型中，通常不可能重用证明技术、工具和元理论。这是一场令人震惊的灾难还是一次巨大的成功？也许两者都有无论如何，回想起来，这并不令人惊讶。并发性在计算机系统的许多层面上都是关键，从低级硬件到全球互联网-但早期的讨论往往没有任何特定的基础。相反，为了挑出一般概念，它经常通过思维实验进行，例如在众所周知的自动售货机上。后来的模型扩散解决了各种各样的现象（同步，命名，时间，地点，概率等），由许多不同的应用程序（通信协议、安全协议、并发和分布式编程语言、生物信息学、控制系统等等）推动。从这个角度来看，我们当然不应该以涵盖所有现象的单一演算为目标-相反，我们可以将这25年来最重要的产品视为操作性的习惯用法和技术的剧目。1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.033318P. Sewell/Electronic Notes in Theoretical Computer Science 162（2006）317语义，建模和推理，可以很容易地应用在新的情况下。我在本说明中说明了这些想法，并从模拟现实世界的TCP和UDP网络协议中吸取了一些教训。这项工作直接开始于进程演算领域，特别是20世纪90年代后期的分布式进程演算：πl，Join，dpi，Nomadic π，Ambient，Dπ，Seal，Box-π，Kell等，这些演算旨在为分布式计算建模，但它们缺乏一个详细和准确的模型，可以在现实世界的网络中发生部分故障-分布的基本方面之一当人们查看TCP/IP的真实协议时，会发现一个复杂的情况。有一些官方标准（RFC和POSIX）很好地描述了连线格式和接口类型，但只使用非正式和不完整的散文来描述系统的行为。另一方面，存在通用实现的事实上的标准。这些代码非常复杂（BSD中有15000行多线程C代码），并且由于部署的基础，几乎是不可变的。在2000-2005年的工作中我们开发了TCP、UDP、TCP的相关部分和数学上严格的Sockets API的行为的事后详细，可读，准确，并涵盖了广泛的使用。为此，我们主要依赖于一种新的实验语义方法：将常见的实现视为受（白盒和黑盒）实际实验影响的工件，与早期的思想实验形成对比。我们：(i) 工作在通用逻辑（高阶逻辑）的表达能力，和通用证明助理（HOL）的严谨性;(ii) 开发语言习惯用法（在高阶逻辑中）来编写规范：具有非确定性的操作语义、时间、系统调用、一元关系编程等;(iii) 写了一个特殊用途的符号模型检查器，在HOL之上编程;(iv) 我用它来验证规范对几千个真实世界的跟踪，从FreeBSD 4.6该特性的主要部分是主机LTSh−lb→lh J，其中h J为主机状态，对单个机器的操作系统和网卡的相关部分进行建模，lbl是套接字API或有线接口上的交互，或者是内部（τ）或时间通道（dur）转换。tid·bind（fd，isJ，psJ）tid·v118>TCPH>：UDP协议IP套接字API线接口msg msgP. Sewell/Electronic Notes in Theoretical Computer Science 162（2006）317319这是一个巨大的数学人工制品。来自HOL的Typical，大量注释：类型定义等。Sockets API规则（148条规则）160页;消息规则（46条规则）75页。准确吗？合理的情况是：对于UDP，2603个跟踪中有2526个（97.04%）成功（BSD、Linux和WinXP）;对于TCP：1095个跟踪中有1004个（91.7%）成功（BSD）。这些迹集被设计为提供良好的覆盖，但当然它们并不完整（系统具有复杂且无限的状态空间）。是否可用？(i) 作为参考文档（现在）(ii) 用于对其他协议栈进行高质量的自动一致性测试（需要更多工作）(iii) 用于描述方案的拟议变更(iv) 作为证明分布式算法的可执行描述的基础例如，Michael Compton在Isabelle中证明了Stenning算法的OCaml实现的性质(v) 而且，最重要的是，如果我们能做到这一点，我们应该能够为未来的协议进行设计时规范，并进行自动一致性测试。w.r.t.这些规格。最后，回到我们的主题，它是一个过程演算吗？1是和否。对于这项工作：• 我们发现在顶层使用进程演算结构是很方便的：整个网络被建模为一个并行的定时标记传输系统的组合，对主机和传输中的消息进行建模（我们不是在对IP路由拓扑进行建模）。• 另一方面，协议端点的内部细节最好用另一种方式来指定它们有一个可扩展的内部结构：它们的状态是特定HOL类型的值（用记录、有限映射等构建），而没有任何内部平行组合。• 顶层并行组合有一个特定的同步代数，有一些二进制和一些多路同步，以及几个不同步的标签。• 主人LTS自然是接受的。与许多演算（以及按钮推动的思想实验）形成鲜明对比的是，主机的系统调用接口可以拒绝线程对套接字调用的调用，或者网络接口可以拒绝让IP数据包通过，这是没有意义的顶层组成不可能出现僵局• 协议（及其用户）依赖于时间属性，但我们使用紧急行动的概念，而不是一些最大进度属性。某些行动-1CCS，CSP，ACP，.. . 、TCP？320P. Sewell/Electronic Notes in Theoretical Computer Science 162（2006）317例如来自主机网络接口的分组的输出可能变得紧急，从而防止时间流逝直到它们发生。接受性意味着这不会引入病理性死锁;在截止时间上适当的灵活性意味着模型确实涵盖了现实世界系统的时间行为。• 大量的语义几乎是194个SOS规则的集合，每个描述一个概念上不同的交互的细节。只有少数涉及过渡前提。将系统行为切片到这些规则中是我们工作的重要组成部分。• 不需要名字生成• 我们使用我们的符号模型检查器将主机LTS的跟踪与捕获的真实世界的跟踪相关联;我们没有进行任何过程等价或一致性推理，也没有使用非平凡模态逻辑。我们不希望从这些点过度概括，这些点只涉及一个相当特殊的工作线，但与传统的过程演算的相似性和对比是有趣的。最后，一些结论：• 为了使这一点有用，我们必须处理真实的东西，没有实质性的理想化（TCP没有一个简单的• 我们需要一种实验性的语义学方法，这也许是早期按钮机器思维实验的一个遥远的春天。• 需要认真注意建模问题• 在表达逻辑中与通用证明助手一起工作是至关重要的。• 针对数学规范的自动化测试是非常强大的• 过程演算为操作语义学、建模和推理提供了一整套习惯用法和技术，可以很容易地应用于新的情况。确认本说明基于与Steve Bishop、Matthew Fairbairn、Michael Norrish、MichaelSmith和Keith Wansbrough的联合工作。 我们感谢英国皇家学会大学研究奖学金（ Sewell ） 、 圣 凯 瑟 琳 大 学 海 勒 研 究 奖 学 金 （ Wansbrough ） 、 EPSRC 赠 款GR/N24872广域编程：语言、语义和基础设施设计、EPSRC赠款EP/C510712NETSEM：真实系统的严格语义、EC FET-GC项目IST-2001-33234 PEPITO对等计算：实施和理论、CMI UROP实习支持（Smith）和EC专题网络IST-2001- 38957APPSEM 2的支持澳大利亚国家信息和通信技术由澳大利亚政府的支持澳大利亚能力倡议资助P. Sewell/Electronic Notes in Theoretical Computer Science 162（2006）317321引用[1] Steven Bishop ， Matthew Fairbairn ， Michael Norrish ， Peter Sewell ， Michael Smith 和 KeithWansbrough。逻辑工程：TCP实现的HOL规范和符号评估测试。《2006年公共财产法会议记录》（查尔斯顿），2006年1月。[2] Steven Bishop ， Matthew Fairbairn ， Michael Norrish ， Peter Sewell ， Michael Smith 和 KeithWansbrough。网络协议的严格规范和一致性测试技术，适用于TCP、UDP和套接字。2005年SIGCOMM会议记录（费城），2005年8月。[3] Steven Bishop ， Matthew Fairbairn ， Michael Norrish ， Peter Sewell ， Michael Smith 和 KeithWansbrough。TCP、UDP和Sockets：严格且经过实验验证的行为规范。第1卷：概述。技术报告UCAM-CL-TR-624，计算机实验室，剑桥大学，2005年3月。88页。[4] Steven Bishop ， Matthew Fairbairn ， Michael Norrish ， Peter Sewell ， Michael Smith 和 KeithWansbrough。TCP、UDP和Sockets：严格且经过实验验证的行为规范。第二卷：规格。技术报告UCAM-CL-TR-625，计算机实验室，剑桥大学，2005年3月。386页。[5] 迈克尔·诺里什彼得·休厄尔和基思·旺斯布罗严格性对你有好处，而且可行：关于C和UDP套接字的形式处理的建议。第10届ACM SIGOPS欧洲研讨会论文集（圣艾米隆），第49-53页，2002年9月[6] Keith Wansbrough，Michael Norrish，Peter Sewell，and Andrei Serjantov.定时UDP：套接字、线程和故障的ESOP 2002会议录：第11届欧洲编程研讨会（格勒诺布尔），LNCS 2305，第278-294页，2002年4月[7] 安德烈·瑟扬托夫，彼得·休厄尔，基思·旺斯布罗。UDP演算：真实网络的严格语义。在TACS 2001会议录：计算机软件的理论方面（仙台），LNCS 2215，第535-559页[8] 安德烈·瑟扬托夫，彼得·休厄尔，基思·旺斯布罗。UDP演算：真实网络的严格语义技术报告UCAM-CL-TR-515，计算机实验室，剑桥大学，2001年7月。iv+70页。[9] 迈克尔·康普顿Stenning的协议在UDP中实现，并在Isabelle中验证。 在Proc.11th CATS，Computing：TheAustralasian Theory Symposium，第21
我的内容管理
展开
