管旭东导师尤晋元上海交大计算机科学与工程系分布计算

1、鲁棒灰箱演算的类型系统和代数性质研究博士生：管旭东导师：尤晋元上海交大计算机科学与工程系分布计算技术中心2002 . 6博士论文答辩2002-6. 1 .博士论文答辩 - 鲁棒灰箱演算内容提要1. 论文的背景2. 灰箱演算，研究ROAM的原因3. 演化类型系统4. ROAM的进程等价性5. 演算的翻译及证明6. 总结论文的创新处2002-62博士论文答辩 - 鲁棒灰箱演算论文的背景移动计算硬件移动、软件移动网络的广域化、全球化从技术到理论支持从程序设计理论（programming language theory）角度寻求支持并发(concurrency)、分布(distribution)、移动

2、(mobility)概念的核心模型（CCS,CSP,join,ambient,seal,.）目标：作为支持全球性移动计算编程语言的理论基础2002-63博士论文答辩 - 鲁棒灰箱演算相关研究领域本论文有关灰箱演算（ambient calculus）的研究工作，属于：程序设计理论（并发、分布、移动）进程代数相关研究领域：OS (distributed/mobile): OS support for Java and mobile agent technologyTCS: type theory and semanticsSecurity - Wide area network, software

3、 mobility2002-64博士论文答辩 - 鲁棒灰箱演算灰箱演算的相关工作支持分布、移动的形式化模型，除了Ambient, 还有：dist: Sekiguchi,et.al., 1997, U.TokyoD: Henessey, et.al., 1998, U. Sussex1l : Amadio, 1997Distributed-: Sewell, 1998, CambridgeD-join: Fournet, et.al., 1996, INRIASeal: Vitek, et.al, 1999, U. Purdue.2002-65博士论文答辩 - 鲁棒灰箱演算内容提要1. 论文的背

4、景2. 灰箱演算，研究ROAM的原因3. 演化类型系统4. ROAM的进程等价性5. pi演算的翻译及证明6. 总结论文的创新处2002-66博士论文答辩 - 鲁棒灰箱演算MA在提出后迅速成为研究热点 Cardelli & Gordon: “Mobile Ambients”Digital Research = Microsoft Research会议：FoSSaCS98期刊：Theoretical Computer Science, 2000后续研究：Ambient有关的研究论文：50多篇FoSSaCS98的引用数：200左右 (/cardelli98mobile.html， 2002-05)

5、 (SCI引用数: 50左右)欧盟：2002启动FET-Global Comp.计划2002-67博士论文答辩 - 鲁棒灰箱演算MA用三个原语来描述移动计算csmailout cs . in lib . Body | libopen maillibopen mailcsout cs . in lib . Bodymail2002-68博士论文答辩 - 鲁棒灰箱演算out 使一个灰箱移出其父灰箱libopen mailcsout cs . in lib . Bodymaillibin lib . Bodymailopen mailcs2002-69博士论文答辩 - 鲁棒灰箱演算in 使一个灰箱移

6、进另一个同层灰箱csin lib . Bodymaillibopen mailBodymaillibopen mailcs2002-610博士论文答辩 - 鲁棒灰箱演算open 用来打开一个灰箱Bodymaillibopen mailcsBodylibcs2002-611博士论文答辩 - 鲁棒灰箱演算防火墙跨越体现了MA的安全性(page72)Agent = mopen k . k QFirewall = ( w)(wkout w . in m . in w| open m . open k . P)Agent | Firewall * ( w)(wP | Q )防火墙的一般形式： ( w)(

7、w )授信代理(Agent)跨越防火墙(Firewall)：( m k k )(Agent | Firewall) ( w m k k)(wP | Q )2002-612博士论文答辩 - 鲁棒灰箱演算防火墙跨越前后的等价性推导(GC99)( m k k ) (Agent | Firewall) ( m k k w) (mopen k . k Q| kin w | wopen m . open k . P) ( m k k w) (wmk Q | open m . open k . P) ( m k k w) (wk Q | open k . P) ( m k k w) (wQ | P)= (

8、m k k ) (mopen k . k Q | ( w)(wkout w . in m . in w | open m . open k . P) | wopen m . open k . P) ( m k k w) (mopen k . k Q | kin m . in w ( m k k w) (mk Q| in w | wopen m . open k . P)通过约束实现并发、移动进程行为的确定性2002-613博士论文答辩 - 鲁棒灰箱演算MA存在强干扰问题一旦失去约束，进程行为将不可预测！wormin m . open m . 后果：m的约束将限制其在防火墙外的功能以取消对m的约

9、束为例：mkQ| in w | Firewall( m)Q = out m . m fn(Q)2002-614博士论文答辩 - 鲁棒灰箱演算SA演算通过增加协动作解决强干扰Mobile Safe Ambient (SA):增加协动作，控制强干扰in in, out out, open openSA中的可归约形式：移入： min w . | w in w . 移出： mkout m . | out m . 打开： open m | m open m . 2002-615博士论文答辩 - 鲁棒灰箱演算SA减少了防火墙跨越等价性的条件wormin m . open m . mkQ| in w | F

10、irewall( m)Q = out m . m fn(Q)min m . mopen m . mout m . 2002-616博士论文答辩 - 鲁棒灰箱演算 但是对m的约束依然存在min m . | kin m . open k . in w | Firewall( m , k)min m . 2002-617博士论文答辩 - 鲁棒灰箱演算ROAM修改了SA协动作参数的语义Robust Ambient (ROAM):在协动作基础上，进一步利用其参数提高安全性，减少二义性 SA 中的可归约形式：移入： min w . | w in w . 移出： mkout m . | out m . 打开

11、： open m | m open m . mkROAM2002-618博士论文答辩 - 鲁棒灰箱演算ROAM完全取消了对m的约束min m . | kin m . open k . in w | Firewall( m , k)min m . kk2002-619博士论文答辩 - 鲁棒灰箱演算论文内容的依赖关系研究背景、相关工作、引入ROAM的原因(第一章)ROAM的语法、归约语义(第二章)演化类型系统(第三章)标号转移语义(第四章)等价性判定(第五章)等价性定律(第六章)翻译pi演算(第七章)2002-620博士论文答辩 - 鲁棒灰箱演算内容提要1. 论文的背景2. 灰箱演算，研究ROAM

12、的原因3. 演化类型系统4. ROAM的进程等价性5. 演算的翻译及证明6. 总结论文的创新处2002-621博士论文答辩 - 鲁棒灰箱演算类型系统可以限定进程的属性传统程序语言：数据类型：变量是整数还是指针？函数类型：函数的参数和返回结果类型？灰箱演算：移动性：灰箱会移动吗？安全性：灰箱的活动范围是什么？会进入受保护的禁区吗？会被谁打开？消息传递类型：灰箱中允许广播何种类型的数据？线程数：进程可以激发多少个并发动作？2002-622博士论文答辩 - 鲁棒灰箱演算Fact 1: 灰箱移动性取决于它的顶层动作cs: (非移动)csmailout cs . in lib . open . Body

13、 | out mail mail: (可移动)顶层动作包含out、in顶层动作不包含out、in2002-623博士论文答辩 - 鲁棒灰箱演算Fact 2: 打开动作将引入被打开灰箱的顶层动作mailopen route . Body | route open . out cs . in lib route:顶层动作包含out、inmail:打开route后引入route的顶层动作out、in 2002-624博士论文答辩 - 鲁棒灰箱演算综合上述两点，易得以下结论：使用该规则的文献：Cardelli & Gordon: POPL99, ICALP99Zimmer: FoSSaCS2000传统

14、的open动作类型判定规则： “open n, behave like n” route:open route:mail:2002-625博士论文答辩 - 鲁棒灰箱演算mail: TBody对open动作类型判定规则的细化引入演化思想后的open动作类型判定规则： “open n, behave like ns future type ” Revision of Fact 2: 打开动作将只引入被打开灰箱位于open动作后的顶层动作 csmailout cs . in lib . open . Body | out mail | lib in mail . open maillib: TBod

15、yopen mail: TBodymail的当前类型为可移动mail的未来类型取决于进程Body2002-626博士论文答辩 - 鲁棒灰箱演算论文第三章详细介绍了演化类型系统主要工作描述了进程的移动性和线程数两个性质区分当前类型和未来类型，支持类型演化支持子类型关系给出最小类型推导算法演化类型系统的作用更细致地刻画进程/灰箱特性为研究进程等价性定律打下基础2002-627博士论文答辩 - 鲁棒灰箱演算内容提要1. 论文的背景2. 灰箱演算，研究ROAM的原因3. 演化类型系统4. ROAM的进程等价性5. 演算的翻译及证明6. 总结论文的创新处2002-628博士论文答辩 - 鲁棒灰箱演算并发

16、进程的等价性研究顺序执行程序（函数表达式归约）：Church-Rosser定理: E E E Normal Form并发移动进程： P P1 P2 P11 P12 P21 P22ConfluentReduction P P12002-629博士论文答辩 - 鲁棒灰箱演算不同演算的进程等价性条件不同MA: (v n, m)(nin m . P | m ) | Q (v n, m) m nP | Q SA: (v m)(nin m . P | min m . P ) | Q (v m) m n P | P | QROAM: (v m)(nin m . P | min n . P ) | Q (v

17、m) m n P | P | Q (v n)(nin m . P | min n . P ) | Q (v n) m n P | P | Q无法只约束n进程会使m移动2002-630博士论文答辩 - 鲁棒灰箱演算用单线程性可以得到更一般的结论如果n, m为单线程，那么： (v n)(nin m . P | P1 | min n . P | P1 ) | Q (v n) m n P | P1 | P | P1 | QROAM: (v n)(nin m . P | min n . P ) | Q (v n) m n P | P | Q更进一步，如果外部不存在额外的nin m . 或 min n .

18、 干扰其归约，那么： nin m . P | P1 | min n . P | P1 | Q m n P | P1 | P | P1 | QPage 64, 定理6.17: (ST In)定律2002-631博士论文答辩 - 鲁棒灰箱演算用非移动性可进一步得到定点接收定律ROAM: (v n)(nin m . P | min n . P ) | Q (v n) m n P | P | Q如果n为单线程，m非移动且不能被打开，in n只在m中的复制构造中出现，那么： nin m . P | P1 | m! in n . P | P1 | Q m n P | P1 | ! in n . P | P

19、 | P1 | QPage 68, 定理6.24: (Rec Co-in)定律2002-632博士论文答辩 - 鲁棒灰箱演算定律的证明从标号转移语义开始第四章：标号转移语义第五章：等价性判定的Context Lemma和Activity Lemma第六章：定价性定律及其证明证明关系2002-633博士论文答辩 - 鲁棒灰箱演算内容提要1. 论文的背景2. 灰箱演算，研究ROAM的原因3. 演化类型系统4. ROAM的进程等价性5. 演算的翻译及证明6. 总结论文的创新处2002-634博士论文答辩 - 鲁棒灰箱演算翻译演算体现了ambient的表达能力pi演算的特点channeled communicationname passing and substitution用带通讯的灰箱演算翻译直接利用灰箱演算中