《气旋的迷人影响(2019)》

2020-10-15 22:31:26

2001年,美国电话电报公司(AT&;T Research)的特雷弗·吉姆(Trevor Jim)和康奈尔大学(Cornell)的格雷格·莫里塞特(Greg Morrisett)启动了一个联合项目,开发一种安全的C编程语言方言,这是早期类型化汇编语言工作的产物。经过五年的努力和一些论文的发表,团队(包括丹·格罗斯曼、迈克尔·希克斯、尼克·斯瓦米和其他人)发布了Cyclone 1.0。然后,开发人员转向了其他事情。

很少有人听说过旋风,也几乎没有人使用过它。然而,当你把合适的石头扔进一个愿意接受的池塘时,影响的浪潮就会向外扩散。旋风是一块巨大的、造型良好的石头;它的时代精神的涟漪,以及它提炼和开创的显著创新,继续以迷人的方式传播。

在讲这个故事之前,我警告你:创新和影响力是一个复杂的社会过程。真空中没有什么新的事情发生。每年都有成千上万的人受到早先扔出的石头的影响,向池塘里扔有趣的石头。没有一篇帖子能公正地处理所有这些混乱的涟漪。

为了保持这个故事的连贯性和易解性,我将重点放在某些主题上:静态安全演化的进展,以及线性在内存管理和并发中的应用,这在几种选定的主流(“命令式”)编程语言中得到了体现。这意味着关于有影响力的学术语言和研究的大量相关和重要的细节将得不到足够的关注。不要让我的编辑缺点误导您对因果的简单理解。相反,要好奇,探索历史记录,欣赏这么多先驱的贡献。

在20世纪末,系统软件通常是用C(或前“现代”C++)构建的。因为它们的语义与CPU的使用方式非常相似,所以这些语言产生了精简、高性能的系统。人们为这种效率付出的代价是安全错误的风险,例如缓冲区溢出,这使得我们的关键系统容易受到恶意行为者的攻击。

Cyclone团队的目标是构建一种与C语言兼容的语言,该语言至少同样快速和精简,但要安全得多。他们的安全概念在当时是激进的:不安全的程序应该很难编写,不可能编译,在运行时遇到安全违规时会惊慌失措。

针对灭绝的漏洞包括:缓冲区溢出、空指针取消引用、释放后使用、悬挂指针、双重释放、格式字符串攻击、未初始化变量使用、不安全强制转换、不确定返回、跨范围GOTO和不加区别的联合。

提高安全性(和多功能性)的主要选择武器来自于通过熟练应用ML,Haskell的现有技术来加强C语言臭名昭著的弱类型系统,并发表了研究报告,特别是:

代数数据类型。虽然C支持带结构的产品类型,但是对SUM类型使用联合可能是不安全的。相反,Cyclone引入了固定大小的标记联合、可变大小的数据类型和模式匹配。Cyclone还支持元组,使函数能够返回多个值。

量化的类型。Cyclone支持函数和类型上的参数多态性(泛型)。尽管被限制为单词大小的类型并且不能单形化,但该功能足以支持类型泛型盒式集合。Cyclone还支持抽象的、存在的类型,具有相似的限制。与特征类似,这些允许跨不同实现的具体类型使用类似方法的函数。

基于区域的内存管理:Cyclone在很大程度上受到了Tofte和Talpin在20世纪90年代中期关于区域推理的开创性工作的启发。正如在ML Kit(与Birkedal和其他人一起)中实现的那样,全程序推理使得使用更快的、作用域嵌套的内存区域(ARENA)取代垃圾收集(GC)内存成为可能。Aiken应用ARENAS和引用计数内存管理到C的相关工作。Cyclone团队对这些技术进行了改进,用显式的区域注释取代了跨功能推理。重要的是,他们丰富了这个方案,以支持前所未有的各种安全的、自动的内存管理策略:Arena区域(包括一级ARENA)、引用计数、跟踪GC(通过Boehm),以及他们所称的唯一区域。

线性/仿射类型。Cyclone的独特区域是Girard从20世纪80年代末开始的线性逻辑的一个有用的应用,后来经过Wadler和Walker的改进,通过保证分配的内存永远只有一个所有者(引用),我们获得了安全的、确定性的内存管理,而不需要运行时GC簿记成本。引用计数的内存管理在使用线性逻辑构建时效率也更高,也就是说,线性逻辑(和区域)在移动语义和量化类型方面增加了语言的复杂性,这是Cyclone团队必须解决的挑战。

空指针。Cyclone提供了一个选择,解决了托尼·霍尔所谓的“十亿美元的错误”。你可以将指针定义为不可为空的(例如int@x),并自由安全地使用它们。或者,如果你确实需要一个可为空的指针,编译器不会让你取消引用它,直到你首先证明它不是空的。

胖指针和有界指针。为了防止缓冲区溢出,Cyclone提供了“胖”指针(char?),它将准确的边界数据烘焙到指针旁边。允许使用指针算法,但任何试图访问边界外的元素都会触发运行时错误。绑定指针以稍微不同的方式提供类似的功能。

内存安全指针。为确保指针只能访问有效的实时数据,指针类型可以用其对象从其获取内存的区域进行注释。此注释确保只有当指向该对象的最后一个可用指针过期时才释放对象。使用数据流分析,指向堆栈分配的数据的指针也是安全的。

多态指针。由于指针上有如此多的类型注释,类型安全可能会迫使我们为传递给函数的每个可能的指针变量复制代码(或使用泛型)。Cyclone通过支持多态指针类型克服了这一可用性挑战,它可以安全地容纳各种指针类型。

关于Cyclone的安全扩展(例如,异常处理和明确的赋值)还可以说得更多,但我认为您已经明白了这一点。Cyclone团队在追查和减轻安全漏洞方面非常勤奋和彻底,他们甚至通过使用线程锁和线程本地数据的静态类型策略来确保多线程的安全。

值得注意的是,所有这些安全性和通用性的改进都是为了尽可能保持与C语言的向后兼容性。出于可以理解的原因,他们希望让现有的C程序员尽可能轻松地获得安全。他们的论文给出了将C代码移植到Cyclone的有用示例,给出了基准测试结果,表明安全性不需要大幅降低性能。

在继续讨论之前,我想对比一下Cyclone的安全内存管理历程和C++的内存管理历程。C++的内存管理依赖于1990年前可用的两个关键特性:模板(比典型泛型更通用、更复杂)和资源获取是初始化(RAII)。使用RAII,程序可以获取和使用某个块的某些本地资源,并期望编译器在该块结束时自动销毁该资源。但是,RAII不能处理使用new动态分配的对象。

为了解决因忘记删除而导致泄漏的可能性,1997标准引入了第一个“智能”指针AUTO_PTR。这个模板定义的功能类似于指针,同时仍然授权RAII确保自动删除所拥有的对象。甚至更好的是,AUTO_PTR是线性的-类似于1:只有一个变量拥有指向的资源。赋值将转移所有权。

然而,auto_ptr有一个致命的设计缺陷,限制了它的实用性。2002年,在贝尔实验室Andrew Koenig的启发下,Howard Hinnant撰写了“向C++添加移动语义的建议”。一个关键的动机是性能:非破坏性地复制指针要比任何类型的深度复制便宜得多。标准化过程的结果是,在2005年的技术报告(TR1)中,UNIQUE_PTR取代了AUTO_PTR,最终是C++11。同样的标准还引入了SHARED_PTR,这是一种经过重新计算的智能指针,基于可以追溯到20世纪90年代末的实践。这一标准的结果是在2005年的技术报告(TR1)中取代了AUTO_PTR,并最终在C++11中引入了SHARED_PTR,这是一种经过重新计算的智能指针。

因此,到2006年,不同的影响导致Cyclone和C++都支持相同的两种形式的自动内存管理:单一所有者(线性)和引用计数器。也就是说,Cyclone的基于区域的内存管理更具可逆性(因为它还支持ARENAS和跟踪GC),并且更加安全。

当谈到严格的内存安全时,Cyclone团队有更深的学术研究和先前的实践可以利用。除了我前面提到的影响之外,他们还利用了onalias类型(Smith和Walker,2000,用类型化汇编语言实现)、目标C对引用计数的使用,以及有影响力的分离逻辑(Reynolds,O‘Hain,PYM,2000-2002)。正如Greg Morrisett所说:“Cyclone的贡献是找到了一个公共框架来放入一堆不同的东西。”

对“借来的”引用的处理说明了Cyclone和C++之间的安全鸿沟。在C++智能指针上使用get()会返回一个带别名的指针。由于C++不跟踪以确保指针别名始终可以安全使用,因此在指针指向的对象被释放后使用指针是有问题的。

Cyclone还可以创建从任何基于区域的指针借用的多态指针,与C++相比,Cyclone通常隐式地仔细跟踪每个借用指针的作用域生存期。对区域生存期(包括区域子类型)的复杂编译时分析使得任何借用指针的生存期都不可能超过其拥有指针的生存期,因此Cyclone的借用指针总是可以安全使用的。

2006年,就在旋风团队关门的同一年,Graydon Hoare(当时是Mozilla的员工)开始作为私人项目开发Rust编程语言。三年后,公司赞助、资金和人员配备开始发挥作用,最终在2015年发布了1.0稳定版本。

如果你知道Rust,我对Cyclone的安全焦点和特性的总结听起来一定非常熟悉。Rust是一种健壮的、现实世界的系统编程语言,几乎满足了Cyclone的所有目标。

Ruust以Cyclone、C++和SML/OCaml为例,一些核心团队成员,如NikoMatsakis、Aaron Turon和Dave Herman,也为他们的设计选择带来了丰富的学术研究。

铁锈和气旋一样完全安全,方式完全相同,而且经常使用非常相似的技术。这就是说,语言之间的差异很容易被发现:

泛型和特征更灵活,类似于ML系列语言,它们的使用是语言核心功能的核心(例如,选项、结果和智能指针包装器,如RC和Mutex)。

借用的引用功能更多,支持静态可变排除(例如,&;mut)、非词法生存期、使用借用来获得块范围的锁和生存期省略糖。也就是说,有趣的是注意到Cyclone的多态变量‘r(通常用作区域注释)类似于Rust的生存期注释。

内存管理。由于Rust将所有权作为语言的一个定义特性,因此它对多内存管理策略的支持比Cyclone的更有限。与C++一样,单一所有者(Box)和引用计数(RC)是占主导地位的技术。尽管存在用于跟踪GC和竞技场的Rust包,但与Cyclone对这些区域的支持相比,它们是有限的,特别是在安全的一流竞技场方面。

不安全。Rust团队明智地意识到,他们需要提供一个转义舱口,允许程序员编写编译器无法验证为安全的安全、高性能逻辑。许多重要的库都依赖于这一基本功能。

重要的是,Rust在线性方面全力以赴,远远超出了单一所有者的内存管理,他们想要解决因允许共享、可变访问值而产生的问题。

对于大多数主流语言,ProgramScan很容易拥有对同一对象的多个引用,每个引用都可以更改(变异)其状态,这可能会引发问题。当您不知道更改发生在哪里时,调试和维护就明显更加困难,特别是当不变式意外损坏时。不受约束的共享可变性不仅为多线程程序打开了数据竞争的大门,有时在单线程上下文中也是如此。正确使用锁(正如Cyclone预期的那样)可以解决数据竞争,但它们通常会承担巨大的吞吐量成本。

几十年来,语言一直在寻找更好的可变别名解决方案。Ada的有限类型、C的限制、C++的严格别名规则、Fortran的参数非别名限制、灵活的Java别名保护、函数式语言对可变性的限制,以及关于分数权限和(再一次)分离逻辑的学术工作。

事实证明,线性逻辑并不仅仅是一种有价值的内存管理策略。这也是一种有价值的混叠和数据竞赛策略。Clean在1992年引入了独特性类型,用于IO处理和破坏性更新。后来的语言,如ATS、Alms和Mezzo,以不同的方式探索了这一想法。Rust团队与这些团队保持联系,同时了解大量正在进行的研究。

Rust由此产生的基于所有权的模型在很大程度上基于互斥思想,即一个人要么只有一个对对象的可变引用,要么可能有对该对象的多个不可变引用。通过这个限制,消除了前面提到的问题,并使从一个线程到另一个线程无锁地传输可变数据变得安全。Rust对无所畏惧的并发的广泛方法依赖于更多,但这方面是一个重要的贡献者。

而且,如果你真的想要共享的,可变的,这也是可能的,使用基于锁的同步机制(例如,Mutex),甚至是无锁的,但有一定限制的Cell。

Midoria是微软从2007年到2014年的一个研究/孵化项目,其目的是在商业上实现奇点,这是一个建立在比堆积如山的不安全C和C++代码更可靠的基础上的操作系统。

为了实现他们的并发性、安全性和性能目标,该团队创建了一种新的C#编程语言方言,称为M#。后来发布的C#特性,如分片和异步/等待,起源于M#。尽管有一些持久的渴望,但它们在内存管理方面没有追随Cyclone(和Rust)的脚步;M#仍然是一种垃圾收集语言(尽管在那里也进行了广泛的更改)。

就像“气旋与锈”一样,有关“气旋”和“M#”的工作充分受到了现有技术和研究的启发:C++常量、别名分析、线性类型、单体、效果类型、区域、分离逻辑、唯一性类型、模型检查、现代C++、D、GO和Rust。Midori团队中的几个人都知道气旋。科林·戈登知道丹·格罗斯曼在气旋方面的工作,他在华盛顿大学读研究生/博士生时跟随他来到华盛顿大学,在那里他作为Midori团队的实习生做出了重要贡献。曼努埃尔·法恩德里奇(Manuel Fähndrich),他早先曾研究过气旋的借款,是Singulicity项目的关键贡献者。David Tarditi,Colin Gordon,他是华盛顿大学的研究生/博士生,在那里他作为Midori团队的实习生做出了重要贡献。Manuel Fähndrich,他早期曾为Cyclone的借款工作,是Singulicity项目的关键贡献者。David Tarditi,奇点/Midori的另一位贡献者,现在正在与Michael Hicks(Cyclone团队)和其他微软的Checked C合作,他们的目标与Cyclone的目标产生了共鸣。

Midori团队完全像Cyclone和Rust一样专注于“三个安全”,他们使用了类似的安全机制,如切片(用于解决边界安全)、歧视联合和借用引用,他们还经过了战斗测试的附加机制,包括软件隔离进程、对象功能、合同、异常处理和引用功能。

M#的引用功能丰富了唯一引用的有用性。M#用四种无锁引用功能(权限限定符)中的一种标记了所有引用:隔离的、可写的、不可变的和可读的。即使所有引用都是数据竞争安全的,但每个引用都以不同的方式启用(和约束)其引用的功能。隔离施加的约束是线性的:只能有一个。

唯一(线性)引用有很大的局限性。只使用唯一引用,只能构建层次(树)数据结构。几乎所有有循环的数据结构都需要允许对同一对象的多个引用,而唯一引用不能这样做。当吹捧单一所有者内存管理和唯一引用的优点时,这个限制以及移动语义的破坏性约束应该一直放在首位。

考虑到这一限制,想象一下,我们有一个对某些循环数据结构的隔离(唯一)引用,该结构在内部使用可别名引用实现。将整个数据结构从一个线程移动到另一个线程是否安全?如果别名引用指向不可变值,则肯定是安全的。但是,如果别名引用是可变的(可写的),我们必须更加小心。只有当对该数据结构中每个对象的所有可写引用实质上一起移动时,移动才是安全的。如果我们不能保证可移动数据结构是“外部隔离的”,我们就会将数据竞争安全置于危险之中,因为多个线程可能会以对相同对象的可变引用结束。

通过使用两种引用能力机制,M#能够在编译时保证外部隔离,第一种是一种视点自适应形式,其中可以根据用于访问该字段的引用的许可来降低对该字段的引用的许可。例如,不可变引用不能用于更改其字段引用所指向的值,即使该字段的引用告诉您可以这样做。

第二种机制是M#强制然后“恢复”能力的能力。恢复使得隔离引用可以在一定范围内被临时强制为可写(或不可变),之后我们可以安全地恢复其原始隔离状态。当它是可写的时,我们可以用额外的对象来改变和丰富指向数据结构。为了保持外部隔离,恢复范围内的逻辑被约束,使得它只能使用来自作用域之外的不可变的或隔离的引用(并且不可写或只读)。

除了可以跨线程移动可变的循环数据结构外,M#的强制和恢复机制还提供了其他好处。它还可以用于安全(和可变地)构建最终过渡到不可变的循环数据结构。最终结果是Midori的引用功能使多线程程序能够通过使用唯一引用安全地提取额外的性能和数据结构的多功能性优势。

在2014-2005年度,Sylvan Clebsch和他的团队为基于演员的Pony语言设计并构建了一个编译器。这里带来了太多相关的影响,包括Erlang之前在演员流程方面的工作。设计选择再次证明,性能和能力-安全-安全不一定是敌人。

Pony充满了引人入胜的特性和体系结构决策,例如:参与者和行为、隐式消息传递、接口与特征,以及使用引用计数和跟踪的不同寻常的混合垃圾收集方法。与M#一样,Pony支持对象和引用功能。Pony对其引用功能集进行了改进、丰富和重命名,进一步明确了允许和拒绝的内容。Pony还使使用唯一引用实例化泛型成为可能。

虽然到目前为止我所讲的故事中没有我的角色,但它们具有很大的个人趣味性。

.