文档结构  
原作者:Joe Duffy    来源:joeduffyblog.com [英文]
中山狼    计算机    2016-12-11    3评/17538阅
翻译进度:65%   参与翻译: solowolf (38), vincentsun (18), 薯片番茄 (6)

在 a Tale of Three Safeties 中,我们讨论了三种安全:类型,内存和并发。 在接下来的这篇文章中,我们将深入到最后一个,也许是最新奇但也是最困难的一个。 第一次引领我进入并发安全的是 Midori 项目,我花了多年的时间在.NET和C ++并发模型上最终进入这个领域。 我们做了一些伟大的事情,在这段时间我感到自豪。 然而,或许更有趣的是,在离开项目几年后对这种经历的反思。

从今年早些时候我大约6次试图写这篇文章,很高兴终于能够把它分享给大家。 我希望它对任何对该领域感兴趣的人都有用,特别是在这一领域积极创新的人。 虽然代码示例和经验教训深深根植于C#,.NET和 Midori 项目,但我已经尝试概括其中的想法以致于它们更容易理解而无关编程语言。 希望你喜欢!

第 1 段(可获 2.16 积分)

背景

2000年的大部分时间,我在微软的 the CLR team 开始从事相对小众的工作,我的工作内容主要是找到让开发人员习惯于并发的方法。

小众起点

当时,很大程度上需要构建更好的经典线程,锁定和同步原语,以及努力巩固最佳实践。 例如,我们向 .NET 1.1 引入了一个线程池,并使用这种经验来提高Windows内核及其调度程序和线程池的可扩展性。 有了这个疯狂的128处理器 NUMA 机器,我们忙于各种各样深奥的性能挑战。 我们制定了正确处理并发的规则 – 锁定等级等等 – 进行了静态分析实验。 我甚至为止写了一本书。

第 2 段(可获 1.63 积分)

为什么把并发放在第一位?

简而言之,从技术上讲,这是非常具有挑战性的,从中可以收获很多乐趣。

我一直专注于语言。 所以,我自然而然地着迷于在学术界几十年的深入工作,包括编程语言和并发运行(特别是 Cilk 和 NESL),高级类型系统,甚至是专门的并行硬件架构(特别是像 the Connection Machine 和 MIMD 这样的超级计算机, 这些创新超越了我们值得信赖的朋友,von Neumann)。

虽然一些非常大的客户实际上在运行 symmetric multiprocessor (SMP)服务器 – 是的,我们曾经这样称呼它 – 但我不会特意说并发是一个非常受欢迎的领域。提到这些酷炫的“研究” 来源的时候,我的同行和经理只会瞥一眼。 然而,我会坚持研究下去。

第 3 段(可获 1.65 积分)

尽管研究有乐趣,但我不会说我们在这段时间内做的工作对临时观察者会有极大的影响。 我们提出了一些抽象概念以便于开发人员可以安排逻辑工作,考虑更高级别的同步等等 – 但游戏规则没有改变。 当时我并不知道,这一时期在技术和社交上为后来的发展奠定了基础。

没有免费的午餐; 进入多核时代

然后有大事发生了。

2004年, Intel 和 AMD向我们介绍了 Moore’s Law,特别是 imminent demisePower wall challenges 将严重削弱该行业已经习惯的逐年提高的时钟速度。

第 4 段(可获 1.51 积分)

突然,管理层开始更加关注并发性。 Herb Sutter 在2005年发表的 “Free Lunch is Over” 一文使并发发展到了极度狂热状态。 如果我们不能使开发人员编写大规模并行软件 – 或者说准入门槛没有显著降低,一些事情会非常困难乃至不可能发生 – Microsoft 和 Intel 的业务和互利的商业模式都会有麻烦。 如果硬件没有变得更快,软件不能自动变得更好,人们没有理由购买新的硬件和软件。 这标志着 Wintel era和 Andy and Bill’s Law 的结束,“ Andy 给我们带来的Bill带走了”。

第 5 段(可获 1.38 积分)

或者说,这种思想过时了。

当 “multicore” 一词成为主流时,我们开始设想一个拥有 1,024个核心处理器的世界,甚至借鉴DSP更具有前瞻性的 “manycore” architectures,将通用核心与能处理加密压缩等繁重任务的特定核心处理器混合在一起。

顺便说一句,10年后的事情并没有完全像我们所想的那样发展。 我们没有运行具有1024个传统内核的PC,尽管我们的GPU已经超过了这个数量,我们看到了更多的异质性,尤其是在数据中心,在那里 FPGA 承载着加密和压缩之类的关键任务。

第 6 段(可获 1.46 积分)

在我看来,真正的失误在于转变。这是明确的,围绕功率曲线,密度和异质性的想法告诉我们在很大程度上转变已经迫在眉睫。这时我们应该注意已有的电脑,而不是去寻找更强大的PC。 相反,自然的本能是坚持过去,即“拯救”PC业务。虽然在当时困难不止一种,但这是一个经典的创新者困境。 当然,电脑没有在一夜之间消失,所以创新没有浪费,只是感觉相对于历史背景不平衡。 无论如何,我跑题了。

第 7 段(可获 1.38 积分)

让并发更容易

作为一个研究并发的极客,这是我期待的时刻。 几乎一夜之间,为创新工作寻找赞助商变得更容易了,因为它现在有真正的非常迫切的业务需求,这是我一直梦想的事情。

简而言之,我们需要:

  • 让并行代码编写起来更容易
  • 更容易避免并发陷阱。
  • 这两种事情只会“偶然发生”。”

我们已经有线程,线程池,锁和基本事件。 下一步该做什么?

在这一点上有三个具体的项目被孵化,得到了兴趣和人员的注入。

第 8 段(可获 1.28 积分)

软件事务存储

讽刺的是,开始的时候我们坚持安全第一。 这预示着后来的故事,因为一般说来,安全占据次要位置,直到我能够在 Midori 的环境中备份它。

开发人员已经有几种引入并发的机制,但仍然很难编写正确的代码。 因此,我们寻求更高层次的抽象概念来纠正偶然的错误。

然后进入了 software transactional memory (STM)时代。 自从 Herlihy 和 Moss 在1993年发表硕士论文以来,许多有希望的研究涌现出来,尽管它不是灵丹妙药,但大多数人对它提高抽象水平的能力表示赞同。

第 9 段(可获 1.41 积分)

STM的写法如下,它可以自动实现安全:

void Transfer(Account from, Account to, int amt) {
    atomic {
        from.Withdraw(amt);
        to.Deposit(amt);
    }
}

看这个例子,没有锁!

STM可以透明地处理所有的决策,比如说明如何使用粗粒度或细粒度同步,围绕同步的竞争策略,死锁检测和预防,以及保证在访问共享数据结构时不会忘记锁定等 。 这些都基于一个诱人的简单的关键字,原子。

STM也有更简单更具说明性的协调机制,如 orElse 。 所以,尽管STM的重点在于消除了手动管理锁定的需要,但它对线程之间同步的演变也是有帮助的。

第 10 段(可获 1.19 积分)

不幸的是,经过几年深度运行时间,操作系统,甚至硬件支持的原型设计,我们放弃了努力。 我的简要总结是,虽然我在这里写了更多简单的架构细节,但比起让它“能工作即可”更重要的是,应该鼓励良好的并发架构。 这种更高层次的架构,正是我们首先应该关注解决的问题,在尘埃落定后,再看看还有什么缺陷。 我甚至不清楚,一旦我们达到这一点,STM 能否成为适合这项工作的工具。 (事后看来,我认为它是工具集中很多合理的工具之一,即使更多的分布式应用程序架构在不断出现,这是一件给人们带来危险的事情。)

第 11 段(可获 1.63 积分)

然而,我们在 STM 上的努力没有完全失败。 正是在这段时间,我开始试验安全并发类型系统。 此外,位和块最终并入 Intel 的 Haswell 处理器作为事务同步扩展(TSX)指令套件,提供了利用推测锁定精度完成最低同步和锁定操作的能力。 再次,这段时间里我和一些了不起的人在一起工作。

并行语言集成查询 (PLINQ)

除了STM之外,利用我们最近在语言集成查询(LINQ)中的工作成果,我在工作日晚上和周末还开发了一个 “skunkworks” 数据并行框架。

第 12 段(可获 1.25 积分)

并行 LINQ(PLINQ)背后的想法是从三个研究领域借鉴的一点经验:

  1. 并行数据库,用户执行SQL查询的行为已经实现了并行,用户不需要知道这个概念,但通常结果令人印象深刻。

  2. 声明式和函数式语言,通常使用列表推导来表达可以被积极优化的高级语言操作,包括并行性。 为此,我受到 APL的启发对 Haskell 更加痴迷。

  3. 数据并行性,在学术界有相当长的历史,甚至衍化出一些更主流的学科,最值得注意的是 OpenMP

第 13 段(可获 1.11 积分)

这个想法很简单。 采用现有的LINQ查询并把它们自动并行化 – 这些查询已经包含了映射,过滤器和聚合等操作 – 在语言和数据库中都可以实现并行化。 好吧,副作用是它不是隐式的。 但它只需要 一个 AsParallel 就可以激活:

// Sequential:
var q = (from x in xs
         where p(x)
         select f(x)).Sum();

// Parallel:
var q = (from x in xs.AsParallel()
         where p(x)
         select f(x)).Sum();

上面的例子显现出有关数据并行性的一件伟大的事情。 数据量与针对数据的操作开销两者之一或者同时都可以与输入的大小成比例。 当用足够高级的语言(如LINQ)表达时,开发人员不必担心调度,只需要挑选适当数量的任务或同步即可。

第 14 段(可获 1.31 积分)

这基本上就是 MapReduce ,在一台机器上跨越多个处理器。 事实上,我们后来与 MSR 合作开发了一个名为 DryadLINQ 的项目,它不仅可以在多台处理器上运行这样的查询,还可以将它们分布在许多机器上。 (最终,我们使用 SIMD 和 GPGPU 更好地实现。)这最终导致微软自己的内部系统等同于谷歌的 MapReduce,Cosmos ,到今天在微软仍然有很多大数据创新实验。

开发PLINQ的一段时间,是我职业生涯中一个真正的转折点。 我与一些了不起的人合作并建立了关系。 BillG 对这个想法写了一整页的评论,结束语是“我们必须在这个工作上投入更多的资源”。这种强烈的鼓励措词并没有损害实现这个想法的固定投资。 它也吸引了一些意想不到的人的注意。 例如, Jim Gray 注意到了,我从他那里得到了第一笔慷慨的投资,就在他不幸地消失前两个月。

第 15 段(可获 2.14 积分)

不用说,这是一个激动人心的时刻!

插曲:成立PFX团队

在这段时间,我决定扩大我们的研究范围,不仅仅是数据并行性,同时解决任务并行性和其他并发抽象。 所以我提出组建一个新团队的想法。

令我惊讶的是,开发部门正在创立一个新的并行计算小组以应对不断变化的技术环境,他们想赞助这些项目。 这是一个机会,在顶级的业务主题下,统一进行招聘工作,并进一步采取措施,最终扩展到C ++,GPGPUs 等等。

第 16 段(可获 1.35 积分)

显然,我答应了。

我为团队命名为 “PFX”, 最初简称“并行框架”,到我们感受营销工作的魔力时,又重命名为“.NET并行扩展”。这个团队的初始目标包括 PLINQ,任务并行, 和一个新的研究方向 —— 协调数据结构(CDS),旨在处理诸如 barrier-style synchronization,并发和无锁集合等等衍生自许多伟大研究论文级的高级同步。

任务并行库

这时我开始研究任务并行性。

第 17 段(可获 1.01 积分)

作为 PLINQ 的一部分,我们需要创建自己的并行“任务”概念。还需要一个复杂的调度程序,可以根据机器的可用资源自动扩展。 大多数现有的调度器都是线程池,因为它们要求一个任务在单独的线程上运行,即使这样做不是最好的。尽管多年来我们做了改进,任务到线程的映射仍然是相当初级的。

鉴于我对Cilk的喜爱以及需要安排大量潜在递归的细粒度任务,毫无疑问应该为我们的调度体系结构选择一个 work stealing scheduler

第 18 段(可获 1.28 积分)

起初,我们把目标锁定在PLINQ上,所以没怎么注意抽象。 然后 MSR 开始探索独立的任务并行库将是什么样子。 这是一个完美的合作机会,所以我们开始一起研究。于是Task<T> 抽象诞生了,我们重写了PLINQ来使用它,并创建了一套用于常见模式的并行API,如 fork/join 和并行的for,foreach循环。

在上市之前,我们用新的work-stealing scheduler替代了线程池的核心,在进程内提供统一的资源管理保证多个调度器不会发生冲突。 到这一天,代码几乎与我早期实现 PLINQ 时相同(当然有很多修正和改进)。

第 19 段(可获 1.63 积分)

我们长期以来对于相对较少数量的API的可用性非常痴迷。 虽然我们犯了错误,但事后我很高兴我们这样做了。 我有一个预感Task<T>将成为我们在并行空间中做的所有事情的核心,但我们没有人预测到异步编程的广泛使用,它真正地推广开来是在多年后。 现在,异步和等待都由它来驱动,我不能想象生活中没有 Task<T>。

大声说出:从Java中受到的启发

如果我没有提到Java以及它对我的想法的影响,是我的疏忽。

第 20 段(可获 1.26 积分)

在此之前,受到许多同样的学术资源的启发,由Doug Lea领导,我们在Java社区的邻居也开始做一些创新的工作。 Doug 出版于1999年的书 “Concurrent Programming in Java” 帮助这些想法在主流中普及,最终促成 JSR 166 并入JDK 5.0。 Java的内存模型也在同一时间被正式化为JSR 133,这是无锁数据结构的一个关键支撑,这些结构需要扩展到大量的处理器中。

这是我看到的第一个主流尝试,它将线程,锁和事件之外的抽象层次提升到更平易近人的方式:并发集合, fork/join 等等。 它也使该行业更接近于学术界一些漂亮的并发编程语言。 这些努力对我们有巨大的影响。 我特别钦佩学术界和工业界的密切合作,让学术界数十年的知识积累浮出水面,在之后的几年里我试图效仿这种方法。

第 21 段(可获 2.2 积分)

不用说,从 .NET 和 Java 之间的相似之处以及竞争程度,我们受到了启发。

安全在哪里?

所有这些都有一个大问题。 它们不太安全。 我们几乎完全专注于引入并发机制,但没有任何保证安全使用的措施。

有一个很好的理由:实现这个是困难的。非常难。 特别是对于开发人员来说有许多不同种类的可用的并发。 但幸运的是,学术界在这方面也有几十年的经验,在并行性研究上比主流开发人员研究得更加“深奥”。 我开始不分昼夜地沉迷于此。

第 22 段(可获 1.43 积分)

对我来说,转折点是我在 2008 年发表于 BillG ThinkWeek 的另一篇论文,Taming Side Effects。在其中,我描述了一个新的类型系统,当时我知道的还很少,但这构成我接下来5 年的工作的基础。 也许这是不正确的,因为后续工作可能会被束缚在我关于 STM 的经验里,但它是一个良好的开始。

Bill 再次以“我们需要这样做”结束,所以我开始为此工作!

你好, Midori

但仍然有一个巨大的问题。 我不能想象在现有的语言和运行时间环境中逐步地完成这项工作。 我不是在寻找一个温暖舒适近似安全的东西,而是如果你的程序编译,你可以知道它没有数据竞争。 它需要刀枪不入。

第 23 段(可获 1.75 积分)

事实上,我曾经尝试过。 我使用C#自定义属性和静态分析来原型化系统的一个变体,但很快得出结论,问题在语言深处出现,必须集成到任何想法的类型系统中工作。 并且他们甚至应该可以远程使用。 虽然我们当时有一些有趣的孵化项目(如 Axum),考虑到愿景的范围以及文化和技术的原因,我知道这项工作需要一个新的家。

所以,我加入了 Midori.

一种结构,一个想法

Midori团队还有一些并发大师,直到我加入前的几年间我一直在和他们谈论这一切。 在最高层次上,我们知道现有的基础是错误的赌注。 我们认为共享内存多线程确实不是未来,特别是我以前的工作缺乏解决这个问题的能力。 Midori 团队是为了应对重大挑战而设立的。

第 24 段(可获 2.25 积分)

我们做了一些事情:

  • 隔离是至关重要的,我们将尽可能地拥抱它。

  • 消息传递将通过强类型的RPC接口连接这样的隔离。

  • 也就是说,在进程内部,存在单个消息循环,并且默认情况下没有额外的并行。

  • “promises-like”编程模型是这种模式下的第一个类,所以:

    • 不允许同步阻塞。
    • 系统中的所有异步活动都是显式的。
    • 复杂的协调模式是可能的,但与锁和事件无关。

为了达到这些目标,我们受到了大量的启发,这些启发来自于 Hoare CSPs,Gul Agha和 Carl Hewitt关于 ActorsEπErlang 的工作以及我们自己多年来在构建并发,分布式和各种基于RPC的系统的集体经验。

第 25 段(可获 1.44 积分)

我以前没有这样说过,但是在 PFX 工作中,消息传递显然不存在。 有很多原因。 首先,有许多相互竞争的研究,没有一个人“感觉”是对的。 例如, Concurrency and Coordination Runtime (CCR)非常复杂(但有很多满意的客户); Axum语言是一种新的语言; MSR的  是强大的,但需要语言的变化,有些人对此犹豫(虽然衍生自图书馆的工作有一些保证); 等等。 第二,对于并行的基本概念是什么每个人有不同的想法,而它对此没什么帮助。

第 26 段(可获 1.3 积分)

但它实际上归结为隔离。我们认为对于细粒度隔离 Windows 进程太重了,提供安全的无处不在的消息传递是必要的。 Windows上没有子进程隔离技术真的是为了任务:COM apartments,CLR AppDomains...可以立即想起来许多有缺陷的尝试; 坦率地说,我不想死在那里。

(从那以后,我注意到已经有一些很好的作品,像Orleans  – 部分由一些前 Midori 成员建立 –  TPL Dataflow 和 Akka.NET。今天如果你想用 .NET 做 actors 和 /or 消息传递 ,我建议借鉴他们。)

第 27 段(可获 1.3 积分)

另一方面,从进程本身开始,Midori 拥有许多层次的隔离,由于软件隔离它甚至比Windows进程更便宜。 粗粒度的隔离以域的形式存在,增加了额外的belts-and-suspenders硬件保护来托管不可信或逻辑分离的代码。 早期,我们想要更细的粒度 - 受到 E’s concept of “vats”的启发,早已开始将抽象用于进程消息管理,但没有考虑安全问题。 所以我们在此停滞。 但这恰恰告诉我们一个稳健的,高性能的安全的消息传递机制需要的基础。

第 28 段(可获 1.33 积分)

有关这种架构的讨论重要的是 shared nothing 这个概念, Midori将其作为核心工作原理。 无共享架构对可靠性的意义是巨大的,消除了单点故障,对于并发安全它们也很有用。 如果你不分享任何东西,就没有竞争的机会! (我们会看到,这带有一点谎言的成分,一般不足以说明问题。)

有趣的是,同一时间我们在进行Node.js开发的时候就是这样。 异步,非阻塞,单个进程范围事件循环的核心思想是非常相似的。在2007 - 2009期间,这个领域中有一些很诱人的东西。 事实上,这些特征中大多是事件循环并发的共性。

第 29 段(可获 1.53 积分)

以上构成了在其上绘制整个并发模型的画布。 这一点在 asynchronous everything 一文中已经讨论过。 但还有更多...

为什么不在这里停下?

这是一个合理的问题。 一个非常强大的系统依据上述内容就可以构建,或者我应该说,多年来经历系统上的冲击,上述基础经受住了时间的考验,并经历了比下一步(语法周边)更少的变化 。 我觉得这时可以离开了。 事实上,依据完美的后见之明,我相信停在这里将是一个合理的故事第一个版本。

第 30 段(可获 1.39 积分)

然而,还有很多事情需要我们继续向前:

  • 子进程没有并行性。 值得注意的是现在还缺乏任务和数据的并行性。 这对于构建.NET的任务和 PLINQ编程模型的人来说是痛苦的。 很多场景有潜在的并行性只是等待被发现,例如图像解码,多媒体管道,FRP渲染堆栈,浏览器,最终语音识别等等。 Midori的一个顶级目标是解决并发难题,尽管很多并行化是为了进程的“自由”,没有任务和数据并行性会使之受到损害。

  • 进程之间的所有消息都需要RPC数据调度,因此无法共享对象。 缺少任务并行性的一个解决方案可能是将所有事物抽象为进程。 需要任务? 那就创建一个进程。 在Midori,他们有充足的条件完成这个工作。 然而,这样做需要调度数据。 这不仅是一个成本高昂的操作,而且并不是所有类型都可管理,这会严重限制可并行操作。

  • 事实上,我们为缓冲区开发了一个现有的 “exchange heap”,这是一个松散的基于线性的概念。 为了避免封锁大型缓冲区,我们创建了一个用于在进程之间进行交换的系统,这样就不需要作为RPC协议的一部分进行复制。 这个想法似乎是有用的,足以推广到更高级别的数据结构。

  • 由于上述的单个消息循环模型,尽管缺少数据竞争,但是由于多个异步活动交叉,还存在内部竞争条件。 await 模型的一个好处在于交叉至少在源代码中可见可审计; 但是竞争仍然会触发并发错误。 我们看到了语言和框架可以帮助开发人员解决这个问题的机会。

  • 最后,我们还有一个模糊的愿望,让系统中有更多的不变性。 这样做对并发安全有帮助,当然,我们也认为语言应该帮助开发人员按照正确的构建来获得现有的常见模式。 如果编译器信任不变性,我们还可以看到性能优化的机会。

第 31 段(可获 4.26 积分)

我们回到学术界和ThinkWeek paper寻找灵感。 这些方法如果以一种有趣的方式组合,可以给我们提供必要的工具 —— 不仅可以提供安全的任务和数据并行性,还能提供更细粒度的隔离,不可变性以及可能解决进程内竞争的工具。

所以,我们中一部分人开始继续研究C#编译器。

模型

在这一节,我将重新排列故事,顺序可能有点乱。 (怎么更合适。)经过多年在“教学风格”上的工作经验,首先我将描述我们已经结束的系统,而不是从我们如何结束有点混乱的历史开始。 我希望这能带给你们一个更简洁的欣赏系统的方式。 然后我会提供完整的历史记录,包括以前的数十个系统,这对我们的影响很大。

第 32 段(可获 1.85 积分)

我们从C#的类型系统开始,并添加了两个关键概念:权限和所有权。

许可

第一个关键概念是 permission

任何引用都有一个许可,它控制你可以用引用对象做什么:

  • mutable: 目标对象(图形)可以通过一般方式改变。
  • readonly: 目标对象(图形)可以读取但不能被改变。
  • immutable: 目标对象(图形)可以读取但永远不会改变。

一个 subtyping relationship 意味着你可以隐式地将 mutable 和 immutable 两者之一转化为 readonly. 换句话说, mutable <: readonly , immutable <: readonly.

第 33 段(可获 1.11 积分)

例如:

Foo m = new Foo(); // mutable by default.

immutable Foo i = new Foo(); // cannot ever be mutated.
i.Field++; // error: cannot mutate an immutable object.

readonly Foo r1 = m; // ok; cannot be mutated by this reference.
r1.Field++; // error: cannot mutate a readonly object.

readonly Foo r2 = i; // ok; still cannot be mutated by this reference.
r2.Field++; // error: cannot mutate a readonly object.

这些是保证,由编译器强制执行并经过验证。

如果未声明,默认值对于原始类型如 intstring等是不可变的,对于所有其他类型是可变的。 这保留了几乎所有场景中现有的C#语义。(也就是说,C#编译没有实质上的改变。)这是有争议的,但实际上这是系统一个很酷的方面。 争议来自于最小授权原则会导致你将 readonly作为默认选择。 而很酷的原因在于可以在他们价值提升时通过C#代码递增他的权限。 如果我们决定从C#中彻底地突破——事后看来我们应该这样做—— 打破兼容性选择更安全的默认是正确的; 但是鉴于我们之前所声明的C#兼容性的目标,我认为我们的调用是正确的。

第 34 段(可获 1.78 积分)

这些权限也可以显示在方法上,指示如何使用 this 参数:

class List<T> {
    void Add(T e);
    int IndexOf(T e) readonly;
    T this[int i] { readonly get; set; }
}

调用者需要足够的权限才能调用方法:

readonly List<Foo> foos = ...;
foos[0] = new Foo(); // error: cannot mutate a readonly object.

类似的事情可以使用委托类型和lambda表示。 例如:

delegate void PureFunc<T>() immutable;

这意味着符合 PureFunc接口的lambda只能在不可变状态上关闭。

第 35 段(可获 0.68 积分)

注意这突然变得多么强大!  PureFunc正是我们想要的并行任务。 我们很快可以看到,这些简单的概念足以使许多 PFX抽象变得安全。

默认情况下,权限是“深”的,它们以传递的方式应用于整个对象中。 然而,明摆着你可以通过其他方式与泛型交互,例如,深权限和浅权限的组合:

readonly List<Foo> foos = ...;             // a readonly list of mutable Foos.
readonly List<readonly Foo> foos = ...;    // a readonly list of readonly Foos.
immutable List<Foo> foos = ...;            // an immutable list of mutable Foos.
immutable List<immutable Foo> foos = ...;  // an immutable list of immutable Foos.
// and so on...
第 36 段(可获 0.95 积分)

尽管样做效果显著,但人是很难满足的!

对于高级用户,我们还有一种写入通用类型的方法 —— 把许可参数化。 这对于通用代码来说是绝对需要的,然而被90%的系统用户忽略:

delegate void PermFunc<T, U, V, permission P>(P T, P U, P V);

// Used elsewhere; expands to `void(immutable Foo, immutable Bar, immutable Baz)`:
PermFunc<Foo, Bar, Baz, immutable> func = ...;

我还想提醒一下,为了方便起见,你可以将一个类型标记为 immutable,这表示“这种类型的所有实例都是不可变的”。实际上这是最受欢迎的特性之一。 在一天结束时,我估计系统中会有 1/4-1/3 的类型被标记为 immutable:

第 37 段(可获 1.41 积分)
immutable class Foo {...}
immutable struct Bar {...}

有一个有趣的转折。 我们将在下面看到, readonly过去常常被称为 readable,而且是完全不同的。 离开 Midori 之后我们努力工作试图把这些概念包含在C#中并尝试统一它们。 这就是我想在这里表达的。 唯一的障碍是 readonly有一个稍微不同的意思。 在字段上, readonly现在表示“值不能更改”; 如果是一个指针,今天的 readonly不影响指示对象。 而在这个新模式中,它会有影响。 由于我们预先选择一个标志 --strict-mutability加入,所以这是可以接受的,同时需要 readonly mutable来获得历史行为,这时一个微小的瑕疵。 对我来说这些无关紧要 – 特别是鉴于C#中的一个非常常见的错误是开发人员假设 readonly是深的(现在是)而明显的相似之处 const

第 38 段(可获 1.91 积分)

所有权

第二个关键概念是 ownership.

一个引用可以被赋予一个所有权注释,正如它可以被赋予一个许可一样:

  • isolated: 目标对象(图)组成了状态的非别名传递性闭环

比如说:

isolated List<int> builder = new List<int>();

与指定了对于给定的引用可以进行哪些操作的许可不同的是,所有权注释告诉我们有关于给定的对象图的别名属性。一个隔离的图有一个“in-reference”指向对象图中的根对象,而没有“our-reference”(除了immutable的对象引用,这种引用是允许的)。

第 39 段(可获 1.08 积分)

下面的可视化材料可以帮助将这个问题概念化:

Isolation Bubbles

给定一个隔离的对象,我们可以原地改变它:

for (int i = 0; i < 42; i++) {
    builder.Add(i);
}

并且/或者销毁原始引用并将所有权迁移到新的引用上面:

isolated List<int> builder2 = consume(builder);

从这里开始,编译器将 builder 标注为未初始化的,尽管它如果被存储在堆中,多个可能的别名会引向它,因此这个分析永远不是无懈可击的。在这种情况下,原始的引用将被标注为 nulled,已防止安全陷阱。(这是众多的做出妥协从而向现存的C#类型系统中更自然地集成的例子之一。)

第 40 段(可获 1.2 积分)

同时我们可以销毁隔离性,并取回一个普通的 List<int>:

List<int> built = consume(builder);

 

这使能了一种线性的形式,可以用于安全并发——从而对象可以被安全地移交,归并了缓存交换堆的特殊情况——同时使能了像builder这样的模式,为强不变性打下了基础。

为了看明白为什么这对不变性很重要,请注意我们跳过了一个immutable对象是如何创建的过程。为了安全性,类型系统需要证明在给定的时间没有其他的 mutable 引用指向那个对象(图)存在,而且永远都不会存在。值得庆幸的是这正是 isolated 能为我们做的事情!

第 41 段(可获 1.41 积分)
immutable List<int> frozen = consume(builder);

或者,更简洁地说,你很容易看到这样的情况:

immutable List<int> frozen = new List<int>(new[] { 0, ..., 9 });

从某种意义上说,我们已经把我们的隔离泡沫(如前所示)完全变绿了:

Immutability from Isolation Bubbles

在幕后,这里驱动类型系统的事情是 isolated 和所有权分析。我们稍后会看到更多的形式可以工作,然而对此有一个简单的看法:所有插入 List<int> 构造函数的输入是 isolated ——也就是说,在这种情况下, new[]生成的向量——从而导致结果的 List<int> 同样是隔离的

第 42 段(可获 0.99 积分)

事实上,任何只消费 isolated 以及/或者 immutable 输入并且仅针对 readonly 类型进行评估的表达式,都可以隐式地升级为 immutable;以及一个类似的评估 mutable 类型的表达式可以被升级为 isolated。这意味着使用普通表达式创建新的 isolated 与 immutable 的事情是很直观的。

这样做的安全性同样依赖于消除环境权限和可导致泄露的构造。

不要使用环境权限(Abmient Authority)

Midori的一个原则是消除 ambient authority。这使能了 基于能力的安全,然而以一种微妙的方式也对于不变性和下面将提到的安全并发抽象是必要的。

第 43 段(可获 1.15 积分)

想知道为什么,我们看看前面提到的 PureFunc 例子。这为我们提供了一种方式来局部推导lambda捕获的状态。实际上,一个我们期待的特性是,只接受 immutable 输入的函数将导致 参考透明(referential transparency),从而解锁一系列创新性的编译器优化,并使得我们更容易溯源代码。

然而,如果可变的静态变量仍存在,PureFunc 函数的调用可能不是单纯的。

比如说:

static int x = 42;

PureFunc<int> func = () => x++;

从类型系统的观点来看,这个 PureFunc 函数没有捕获状态,因此它遵循不可变捕获需求。(这样说可能对我们很有吸引力:我们能“看到” x++,因此能够拒绝lambda,然而这个x++可能深深隐藏在一系列虚拟调用中发生,对我们是不可见的。)

第 44 段(可获 1.65 积分)

所有的副作用需要暴露给类型系统。在过去的几年里,我们探索额外的注释来表明“这个函数对静态变量有可变的访问”;然而,mutable 权限已经是我们这么做的方法了,而且感觉上与Midori采用的对于环境权限整体的立场是一致的。

因此,我们排除了所有环境方面可能带来副作用的操作,转为利用能力对象。这明显覆盖了I/O操作——所有I/O在我们的系统中都是异步的RPC——同时甚至——某种程度是从根本上——意味着即使只是获取当前时间,或者生成一个随机数,都需要一个能力对象。这让我们以类型系统能看到的方式来对副作用进行建模,同时收获能力对象带来的其他好处。

第 45 段(可获 1.53 积分)

这意味着所有的静态变量必须是不变的。 这将 C# 的 const 关键字带给了所有的静态变量:

const Map<string, int> lookupTable = new Map<string, int>(...);

在C#中,const 仅限于原语常量,如 ints,bools,以及 strings。我们的系统扩展了同样的能力至任意类型,如 list,map,…,真正任意的事情。

这正是变得有趣的地方。正如 C# 目前 const 的概念,我们的编译器在编译时评估了所有的对象,并将它们锁定在生成的二进制镜像的只读部分。感谢类型系统保证了不变性得到遵守,这么做会导致没有运行时故障的风险。

第 46 段(可获 1.25 积分)

锁定进行了两项性能改进。首先,我们可以跨多个进程共享页面、降低总体内存使用和 TLB 压力,例如,保存在映射中的查找表可以在使用该二进制的所有程序之间自动共享。其次,我们能避免对所有类构造函数的访问,并用常量偏移量将其代替,在不改变运行速度的情况下将整个系统的代码量减少 10%

可变的静态变量代价高昂!

无泄漏构造

第 47 段(可获 1.06 积分)

现在我们遇到了第二个需要修补的“漏洞”:可导致泄露的构造函数。

泄露构造函数是在构造完成之前共享 this 的构造函数。由于继承和构造函数链式关系,即使它出现在构造函数较末尾的位置,这样做也不能保证是安全的。

为什么说泄露构造不安全呢? 主要是因为他们给第三方提供了未完全构建的对象。 这些对象的不变量是不确定的,特别是在构造过程出错的情况下,其不可变性无法保证。

第 48 段(可获 1.15 积分)

在我们所处的情况中,我们怎么确保在创建一个应是不可变的对象之后,不会有人隐秘地持有一个可变的引用呢?在这种情况下,用 immutable 来标记此对象是一个类型漏洞。

我们可以完全禁用可能导致泄漏的构造函数。关键之处是什么?使用一种特殊权限,init,来表明目标对象正在进行初始化,因此不用遵守常规规则。例如,它意味着字段还不能保证已经被赋值,非空性还未确保,并且对该对象的引用也不能转换为所谓的“顶级”权限, readonly 。任何构造函数默认都有这个权限,并且你不能覆盖它。我们还自动在特定区域使用 init 机制,以保证语言能够更加无缝地工作,比如在对象初始化器中。

第 49 段(可获 1.56 积分)

这会导致一个不好的后果:默认情况下,你不能从构造函数中调用其他实例方法。(说实话,这在我看来是件好事,因为这意味着你不用顾虑还未完全构造的对象,不会意外地从构造函数中调用其他虚函数,等等)。在大多数情况下,这个问题都能变通解决。但是,对于那些真正需要在构造函数中调用实例方法的情形,我们允许将方法标记为 init 来让它们则拥有该权限。

形式及权限格式

第 50 段(可获 1.15 积分)

尽管上文所述在直觉上是合理的,在这些场景背后有一个正式化的类型系统。

作为整个系统的中心,我们与MSR(微软研究院)合作来证明这种方法的可靠性,特别是 isolated,并在 OOPSLA’12 上发表了一篇论文(同样内容参考免费的 MSR技术报告 )。虽然这篇论文是在最终模型固化前几年出现的,但是当时大多数的关键思想已经形成并正在进行中。

然而,作为一个简单的思维模型,我总是从子类型和替代的角度思考问题。

事实上,一旦通过这种方式建模,对于类型系统的大多数启示很自然地“丢掉了”。readonly 是 “最高权限”, mutable 和 immutable 都可以隐式地转换过去。转换到 immutable 是一个精致的过程,需要 isolated 状态来保证遵守不变性需求。从那里,所有的通常的启示开始出现,包括 substitution(替代)variance(变化),以及它们对于对话、覆盖和子类型的各种影响。

第 51 段(可获 1.93 积分)

这形成了一个二维的晶格,其中一个维度是经典意义上的“类型”以及其他的“许可”,从而所有类型都可以转换成 readonly 对象。如下图所示:

Permission Lattice

这个系统明显能够在没有任何这些形式化的情况下被使用。然而,我已经经历过足够的过去几年由于类型系统陷阱,带来的非常可怕但又很细微的安全问题,因此进行形式化不仅帮助我们更好地理解我们的系统,同时帮助我们晚上睡个好觉。

这如何带来安全并发

第 52 段(可获 1.14 积分)

新的类型系统到手后,我们现在回头看看那些PFX抽象,并让他们全部安全起来。

我们必须要建立的必要属性是,当一个 activity(活动)对于一个给定的对象拥有 mutable 权限时,那个对象必须同时对任何其他的 activity 来说都是不可访问的。请注意我是故意使用 activity 这个术语的。现在,想象它等同于“task(任务)”,尽管我们将来会回顾这个微妙的瞬间。同时请注意我说的是“对象”,也是一个总的简化,因为对于某些像向量这样的数据结构,仅仅确保 activity 对于交叉区域没有 mutable 权限就够了。

第 53 段(可获 1.34 积分)

除了不允许的部分外,它其实允许很多有意思的模式。比如说,任意数量的并发的 activity 可能会共享同一个对象的 readonly 访问。(这有点像读写锁,只是没有任何锁以及运行时性能损失。)记住我们能将 mutable 转换为 readonly,这意味着,给定一个具有 mutable 访问权限的activity,我们能够使用fork/join并行化来捕获一个具有 readonly 许可的变量,假设在这个fork/join操作的过程中,变化被临时停止了。

或者,以代码形式描述:

int[] arr = ...;
int[] results = await Parallel.Fork(
    () => await arr.Reduce((x, y) => x+y),
    () => await arr.Reduce((x, y) => x*y)
);
第 54 段(可获 1.05 积分)

仅仅读一下这段代码,我们就能知道它并行计算一个数组的求和以及乘积。这段代码是没有数据竞争的。

这是为什么呢?在下面这个例子中, Fork 使用了许可来执行所需要的安全性:

public static async T[] Fork<T>(params ForkFunc<T>[] funcs);

public async delegate T ForkFunc<T>() readonly;

让我们一点一点看这段代码。 Fork 仅仅以一个 ForkFuncs 数组为输入。由于 Fork 是 static(静态的),我们不必担心它会危险地捕捉状态。但 ForkFunc 是一个委托,并且会因实例方法和 lambda 而得到满足,上述两者都有可能淹没状态。通过将这个位置标记为 readonly,我们限制变量捕获的许可为 readonly;因此,尽管在上述例子中,lambda 能够捕获 arr(数组),它们无法改变它。就是这样。

第 55 段(可获 1.29 积分)

同样需要注意的是内嵌的 Reduce 函数可以并行运行,这多亏了 ForkFunc!很明显所有我们熟悉的 Parallel.ForParallel.ForEach,以及友元函数,都能够在同样安全的情况下享受同样待遇。

实际上我们能保证修改器暂停的大多数的 fork/join 模式都是这样工作的。比如说所有的PLINQ 能够通过这种方式表示,完全没有数据竞争。这是我总能想到的用例。

事实上,我们现在可以引入 automatic parallelism(自动并行)!这有几种方法可以实现。第一种方法是不要提供没有被 readonly 注释保护的 LINQ 操作接口。这也是我倾向的方法,因为让查询接口拥有改变数据的权限是荒谬的。但还有其他办法。其中一种是提供过载——一套 mutable 接口,一套 readonly 接口——编译器的过载决议将选择具有类型检查过的最低权限的接口。

第 56 段(可获 1.88 积分)

如前面提到的,任务可能会比这个更简单:

public static Task<T> Run<T>(PureFunc<T> func);

这采用了我们前面的伙伴,PureFunc,它确保引用透明。由于任务没有像 fork/join 以及前文中的数据平行一样的结构化生命周期,我们甚至不能允许捕获 readonly 状态。要记住,让上述例子工作的一个技巧是修改器被临时暂停了,这是我们在无结构的任务并行中无法保证的。

那么,如果一个任务需要捕获可改变状态呢?

第 57 段(可获 1.01 积分)

对此,我们使用 isolated!有很多方法可以对此编码,但是,我们使用这样的方法:通过标记委托来指明它们可以捕捉 isolated 状态(这样做的副作用是使得委托自身也是 isolated 的)。

public static Task<T> Run<T>(TaskFunc<T> func);

public async delegate T TaskFunc<T>() immutable isolated;

现在我们可以线性地将整个对象图推到一个任务上,永久地或临时地:

isolated int[] data = ...;
Task<int> t = Task.Run([consume data]() => {
    // in here, we own `data`.
});

请注意我们使用 lambda 捕获列表来使得对象的捕捉变得直观。现在有一个 active proposal(活跃的提议) 将像这样的特性添加到未来的C#版本中,但是如果不添加很多Midori其他的特性的话,这个特性自己是否能工作还有待观察。

第 58 段(可获 1.25 积分)

由于 isolation 生产周围的一些规则,任务产生的 mutable 对象可能变成 isolatedreadonly 对象可能会被冻结变成 immutable。这从组合构图的角度来看是非常强大的。

最后,我们创建了更高等级的框架来辅助数据分区、对类似数组的结构进行不均匀数据并行访问,以及其他方面。上述所有都不再面临数据竞争、死锁和相关的并发危害。

尽管我们在GPU上实现了上述功能的一个可运行的子集,我不得不承认我们还没有完全搞清楚要怎么做。我能说的是当在GPU上编程时,了解其 副作用和内存的所有权是非常重要的概念,我们希望上述的构建块能够帮助创造一个更优雅和统一的编程模型。

第 59 段(可获 1.6 积分)

最终,上述带来的主要的编程模型增强是细粒度的“actor”,一种在进程内部的微进程。 我在前面提到了 vat 的概念,但同时说明了我们不知道如何使它安全。最终我们找到了遗漏的线索:一个 vat 实际上只是一个状态的 isolated 气泡。既然我们在类型系统里面有这个概念了, 我们可以允许 immutable 和 isolated 对象的“编组”作为信息传输协议的一部分,这个协议不带有任何混编——他们能够通过引用安全地共享。

我想说,这个系统的主要缺点同样也是其主要的优点。纯粹地排列各种概念是很令人疲惫的。这些概念中大多数都很好地形成了,但是创建底层“安全并发”抽象的糟糕的程序员——包括我自己——几乎在做这件事情的时候失去了理智。或许有一些天才般的统一可以将许可和所有权统一起来,但是线性度的“幽默”是很难检查的。

第 60 段(可获 1.96 积分)

Amazingly, it all worked! All those cases I mentioned earlier – image decoders, the multimedia stack, the browser, etc. – could now use safe intra-process parallelism in addition to being constructed out of many parallel processes. Even more interestingly, our one production workload – taking Speech Recognition traffic for Bing.com – actually saw significant reductions in latency and improvements in throughput as a result. In fact, Cortana’s DNN-based speech recognition algorithms, which delivered a considerable boost to accuracy, could have never reached their latency targets were it not for this overall parallelism model.

第 61 段(可获 1.14 积分)

Sequential Consistency and Tear-Free Code

There was another unanticipated consequence of safe concurrency that I quite liked: sequential consistency (SC).

For free.

After all those years trying to achieve a sane memory model, and ultimately realizing that most of the popular techniques were fundamentally flawed, we had cracked the nut. All developers got SC without the price of barriers everywhere. Given that we had been running on ARM processors where a barrier cost you 160 cycles, this gave us not only a usability edge, but also a performance one. This also gave our optimizing compiler much more leeway on code motion, because it could now freely order what used to be possibly-side- effectful operations visible to multiple threads.

第 62 段(可获 1.48 积分)

To see how we got SC for free, consider how the overall system was layered.

At the bottom of all of the above safe concurrency abstractions, there was indeed unsafecode. This code was responsible for obeying the semantic contract of safe concurrency by decorating APIs with the right permissions and ownership, even if the implementation physically violated them. But it is important to note: this is the only code in the system – plus the 1st party kernel code – that had to deal with concurrency at the threads, locks, events, and lock-free level of abstraction. Everything else built atop the higher-level abstractions, where barriers had already been placed into the instruction stream at all the right places, thanks to the infrastructure.

第 63 段(可获 1.5 积分)

This had another consequence: no struct tearing was visible in the 3rd party programming model. Everything was “atomic”, again for free.

This allowed us to use multi-word slice and interface representations, just like Go does, but without the type-safety- threatening races. It turns out, the risk of struct tearing is one of major factors preventing us from having a great Go-like slice type to C# and .NET. In Midori, slices were safe, efficient, and everywhere.

Message Passing Races

Message passing helps tremendously when building correct, reliable concurrent systems, however it is not a panacea. I had mentioned shared nothing earlier on. It’s a dirty little secret, however, even if you don’t have shared memory, but agents can communicate with one another, you still have shared state encoded in the messaging between those agents, and the opportunity for race conditions due to the generally unpredictable order of arrival of these messages.

第 64 段(可获 1.9 积分)

This is understood, although perhaps not very widely. The most worrisome outcome from these kind of races is time of check time of use (TOCTOU), one of the more common kinds of races that can lead to security vulnerabilities. (Midori’s type- and memory-safety of course helps to avoid this particular symptom, however reliability problems are very real also.)

Although people used to hate it when I compared this situation to COM STAs, for those familiar with them, an analogy is apt. If you need to block a thread inside of a COM STA, you must decide: Do I pump the message loop, or do I not pump the message loop? If you choose to pump the message loop, you can suffer reentrancy, and that reentrancy might be witness to broken invariants, or even mutate state out from underneath the blocking call, must to its dismay after it reawakens. If you choose not to pump the message loop, you can suffer deadlock, as calls pile up, possibly ones that are required to unblock the thread.

第 65 段(可获 2.19 积分)

In Midori’s system, we did not give this choice to the developer. Instead, every await was an opportunity to pump the underlying message loop. Just as with a COM STA, these pumps possibly dispatched work that might interact with shared state. Note that this is not parallelism, mind you, since process event loops did not permit parallelism, however there is possibly a lot of concurrency going on here, and it can definitely screw you:

async bool IsRed(AsyncColor c) {
    return (await c.R > 0 && await c.G == 0 && await c.B == 0);
}

This rather simple (and silly) function checks to see if an AsyncColor is “red”; to do so, it reads the RG, and B properties. For whatever reason, they are asynchronous, so we must await between accesses. If AsyncColor is a mutable object, well, guess what – these values might change after we’ve read them, opening up a possible TOCTOU bug. For instance, imagine a caller’s surprise when IsRed may have lied to it:

第 66 段(可获 1.78 积分)
AsyncColor c = ...;
await IsRed(c);
assert(await c.R > 0);

That assertion can very well fire. Even this callsite has a TOCTOU bug of its own, since c.R might be >0 at the end of IsRed’s return, but not after the assert expression’s own await has completed.

All of this should be familiar territory for concurrency experts. But we sought to eliminate these headaches.

This area of the system was still under active development towards the end of our project, however we had sketched out a very promising approach. It was to essentially apply similar permission annotations to asynchronous activity – hence my choice of the term “activity” earlier – as we did parallel tasks. Although this seriously limited an asynchronous activity’s state purview, combined with a reader/writer-lock like idea, meant that we could use permissions affixed to asynchronous interfaces to automatically ensure state and asynchronous operations were dispatched safely.

第 67 段(可获 1.71 积分)

Evolution

Before moving on, a brief word on the evolution of the system. As I mentioned earlier, I presented the system in its final form. In reality, we went through five major phases of evolution. I won’t bore you with exhaustive details on each one, although I will note the major mistakes and lessons learned in each phase.

In the first phase, I tried to build the system entirely out of annotations that were “outside” of the type system. As I’ve already said, that failed spectacularly. At this point, I hope you can appreciate how deeply integrated into the compiler and its type system these concepts need to be for them to work and for the result to be usable.

第 68 段(可获 1.53 积分)

Next, I tried a variant of this with just readonly. Except I called it readable (a name that would stick until the very tail end of the project), and it was always deep. There was no immutable and there was no isolated. The concept of mutable was called writable, although I was delusional, and thought you’d never need to state it. I was very confused about the role generics played here, and ended up coding myself up into a corner trying to make it work.

After that, I recognized at least that readable and writable were related to one another, and recognized the subtyping relationship of (writable <: readable). And, largely based on conversations with colleagues in MSR, I decided to toss out everything I had done on generics and redo it. It was at that time I recognized that each generic type variable, despite looking like a naked type, actually carried both a permission and a type. That helped.

第 69 段(可获 1.88 积分)

I then came up with immutable, however it wasn’t what you see today. Instead, it had the slightly confusing meaning of being a “view” over just the immutable subset of data in the target object graph. (This was at first limited to only readonly fields (in the classical C# sense) that were of a primitive type.) If you tried reading a non-immutable part from this view, you’d get a compiler error. Bizarrely, this meant you could have an immutable List<T> that wasn’t actually immutable. In hindsight, this was pretty wonky, but it got us thinking about and discussing immutability.

第 70 段(可获 1.23 积分)

Somewhere in here, we recognized the need for generic parameterization over permissions, and so we added that. Unfortunately, I originally picked the % character to indicate that a generic type was a permission, which was quite odd; e.g., G<%P> versus G<T>. We renamed this to permission; e.g., G<permission P> versus G<T>.

There was one problem. Generic permissions were needed in way more places than we expected, like most property getters. We experimented with various “shortcuts” in an attempt to avoid developers needing to know about generic permissions. This hatched the readable+ annotation, which was a shortcut for “flow the this parameter’s permission.” This concept never really left the system, although (as we will see shortly), we fixed generics and eventually this concept became much easier to swallow, syntax-wise (especially with smart defaults like auto-properties).

第 71 段(可获 1.6 积分)

We lived with this system for some time and this was the first version deployed at-scale into Midori.

And then a huge breakthrough happened: we discovered the concepts necessary for isolated and, as a result, an immutable annotation that truly meant that an object (graph) was immutable.

I can’t claim credit for this one. That was the beauty of getting to this stage: after developing and prototyping the initial ideas, and then deploying them at-scale, we suddenly had our best and brightest obsessing over the design of this thing, because it was right under their noses. This was getting an initial idea out in front of “customers” early-and-often at its finest, and, despite some growing pains, worked precisely as designed.

第 72 段(可获 1.49 积分)

We then wallowed in the system for another year and 1/2 and, frankly, I think lost our way a little bit. It turns out deepness was a great default, but sometimes wasn’t what you wanted.List<T> is a perfect example; sometimes you want the List to be readonly but the elements to be mutable. In the above examples, we took this capability for granted, but it wasn’t always the case. The outer readonly would infect the inner Ts.

Our initial whack at this was to come up with shallow variants of all the permissions. This yielded keywords that became a never-ending source of jokes in our hallways: shreadableshimmutable, and – our favorite – shisolated (which sounds like a German swear word when said aloud). Our original justification for such nonsense was that in C#, the signed and unsigned versions of some types used abbreviations (sbyteuint, etc.), and shallow sure would make them quite lengthy, so we were therefore justified in our shortening into a shprefix. How wrong we were.

第 73 段(可获 2.01 积分)

From there, we ditched the special permissions and recognized that objects had “layers”, and that outer and inner layers might have differing permissions. This was the right idea, but like most ideas of this nature, we let the system get inordinately more complex, before recognizing the inner beauty and collapsing it back down to its essence.

At the tail end of our project, we were working to integrate our ideas back into C# and .NET proper. That’s when I was adamant that we unify the concept of readable with readonly, leading to several keyword renames. Ironically, despite me having left .NET to pursue this project several years earlier, I was the most optimistic out of anybody that this could be done tastefully. Sadly, it turned out I was wrong, and the project barely got off the ground before getting axed, however the introductory overview above is my best approximation of what it would have looked like.

第 74 段(可获 1.94 积分)

灵感

现在我们已经看到了系统的最终形态,现在让我们溯源而上看看那些让我们思如泉涌的系统。如图:

Influences

由于涉及范围这么多,在此我只做简单陈述--但如果你想深入了解的话,下面有更多详细论文的链接。这几年我全身心投入在这上面,每周大概会阅读 5-10 篇论文,办公室里这么一大摞资料就是最好的证明:

Concurrency Paper Stack

const

const 的相似之处现在非常明显。 虽然人们对它又爱又恨,但我发现保证 const 正确  值得我们付出比创建一个喜欢的项目更大的努力。(我知道有许多人不同意我的观点。)

第 75 段(可获 1.8 积分)

也就是说,const 有其自身的价值,这要归功于 const_cast 的普遍使用,它通常用在 const 正确的不同库的接口处。由于一些组合的短缺,const 也会出现异常,例如,缺少 const 参数化机制会导致代码重复,面对这种情况,许多开发者宁愿放弃 const 限定。

const 和我们的权限一样,都不是"深层"的,它需要启用激发系统的安全并发机制、隔离机制和不可变性模式。尽管 const 正确用法可以带来许多类似鲁棒性的好处,但这不是它的主要工作动机。

第 76 段(可获 1.54 积分)

Alias Analysis

Although it’s used more as a compiler analysis technique than it is in type systems, alias analysis is obviously a close cousin to all the work we did here. Although the relationship is distant, we looked closely at many uses of aliasing annotations in C(++) code, including__declspec(noalias) in Visual C++ and restrict (__restrict__restrict__, etc.) in GCC and standard C. In fact, some of our ideas around isolated eventually assisted the compiler in performing better alias analysis.

Linear Types

Phillip Wadler’s 1990 “Linear types can change the world!” was immensely influential for me in the early days. I remember a huge lightbulb going off when I first read this paper. Linear types are inspired by the linear logic of J.-Y. Girard, and it is easy to get lost in the mathematics for hours.

第 77 段(可获 1.68 积分)

In a nutshell, a linear type lets you prove that a variable is used exactly once. This is similar to isolated, however due to the aliasing properties of an imperative language like C# (especially for heap structures with possible cycles between them), the simple and elegant model of strict linearity is hard to make work.

Linear types themselves also aren’t very commonly seen in the wild, and are mostly useful for their mathematical and proof properties. If you go looking, you will find examples, however. More than real syntax in real languages, linear types have been hugely influential on subsequent innovations in type systems that also impacted us, such as affine and uniqueness types.

第 78 段(可获 1.43 积分)

Haskell Monads

In the early days, I was pretty obsessed with Haskell, to put it mildly.

I often describe the above system that we built as the inverse of the Haskell state monad. In Haskell, what you had was a purely functional language, with sugar to make certain aspects look imperative. If you wanted side-effects, you needed to enter the beautiful world of monads. In particular, for simple memory side-effects, the state monad let you have traditional mutable data structures, but in a way that the type system very much understood and could restrict for safety where appropriate.

第 79 段(可获 1.23 积分)

Well, the system we built was sort of the opposite: you were in an imperative language, and had a way of marking certain aspects of the program as being purely functional. I am pretty sure I read the classic “State in Haskell” paper at least a dozen times over the years. In fact, as soon as I recognized the similarities, I compared notes with Simon Peyton-Jones, who was immensely gracious and helpful in working through some very difficult type system design challenges.

Effect Types

Effect typing, primarily in the ML community, was also influential in the early days. An effect type propagates information at compile-time describing the dynamic effect(s) executing said code is expected to bring about. This can be useful for checking many properties.

第 80 段(可获 1.58 积分)

For example, I always thought of await and throws annotations as special kinds of effects that indicate a method might block or throw an exception, respectively. Thanks to the additive and subtractive nature of effect types, they propagate naturally, and are even amenable to parametric polymorphism.

It turns out that permissions can be seen as a kind of effect, particularly when annotating an instance method. In a sense, a mutable instance method, when invoked, has the “effect” of mutating the receiving object. This realization was instrumental in pushing me towards leveraging subtyping for modeling the relationship between permissions.

第 81 段(可获 1.19 积分)

Related to this, the various ownership systems over the years were also top-of-mind, particularly given Midori’s heritage with Singularity, which used the Spec# language. This language featured ownership annotations.

Regions

Regions, despite classically being used mostly for deterministic and efficient memory management, were incredibly interesting towards the days of figuring out isolated.

They aren’t identical for several reasons, however.

The first reason is that isolated object graphs in our system weren’t as strictly partitioned as regions, due to immutable in- and out- references. Regions are traditionally used to collect memory efficiently and hence dangling references like this wouldn’t be permitted (and the reachability analysis to detect them would basically devolve into garbage collection).

第 82 段(可获 1.45 积分)

The second reason is that we wanted to avoid the syntactic burden of having regions in the language. A good example of this in action is Deterministic Parallel Java, which requires explicit region annotations on objects using a very generics-like syntax (e.g., Foo<region R>). Some amount of this can be hidden from the developer through more sophisticated compiler analysis – much like Cyclone did – however, we worried that in some very common cases, regions would rear their ugly heads and then the developer would be left confused and dismayed.

All that said, given our challenges with garbage collection, in addition to our sub-process actor model, we often pondered whether some beautiful unification of isolated object graphs and regions awaited our discovery.

第 83 段(可获 1.48 积分)

Separation Logic

Particularly in the search for formalisms to prove the soundness of the system we built, separation logic turned out to be instrumental, especially the concurrent form. This is a formal technique for proving the disjointness of different parts of the heap, which is very much what our system is doing with the safe concurrency abstractions built atop the isolated primitive. In particular, our OOPSLA paper used a novel proof technique, Views, which can be constructed from separation algebras. Caution: this is getting into some very deep mathematical territory; several colleagues far smarter than I am were the go-to guys on all of this. But, it certainly helped all of us sleep better at night.

第 84 段(可获 1.44 积分)

Uniqueness Types

Uniqueness types are a more recent invention, derived from some of the early linear type systems which so fascinated me early on. For a period of time, we actually had a uniquekeyword in the language. Eventually we folded that back into the concept of isolated (it was essentially a “shallow” isolated). But there is no denying that all of this was heavily inspired by what we saw with uniqueness types, especially in languages like Clean, the experimental work to bring uniqueness to Scala, and, now, Rust.

Model Checking

Finally, I would be remiss if I didn’t at least mention model checking. It’s easy to confuse this with static analysis, however, model checking is far more powerful and complete, in that it goes beyond heuristics and therefore statistics. MSR’s Zing and, although we used it to verify the correctness of certain aspects of our implementation, I don’t think we sufficiently considered how model checking might impact the way safety was attained. This was top-of-mind as we faced intra-process interleaving race conditions. Especially as we look to the future with more distributed-style concurrency than intra-process parallelism, where state machine verification is critical, many key ideas in here are relevant.

第 85 段(可获 2.51 积分)

Other Languages

This story spans many years. During those years, we saw several other languages tackling similar challenges, sometimes in similar ways. Because of the complex timeline, it’s hard to trace every single influence to a given point in time, however it’s fair to say that four specific languages had a noteworthy influence on us.

(Note that there are dozens of influential concurrent and parallel languages that inspired our work. I’m sure I haven’t read everything there is to read – there’s always more to learn – however I did my best to survey the field. I will focus here on the most mainstream and relevant to people writing production code in the year 2016.)

第 86 段(可获 1.48 积分)

(Modern) C++

I already mentioned const and its influence.

It is also interesting to note the similarities between isolated and C++11’s std::unique_ptr. Although born in different times, and in very different worlds, they both clearly deliver a similar perspective on ownership. Noted difference include deepness – C++’s approach is “deep” insofar as you leverage RAII faithfully in your data structures – and motivations – C++’s motivation being primarily memory management, and neither safe concurrency nor immutability.

The concept of constexpr has obvious similarities to both isolated and immutable, particularly the compile-time evaluation and freezing of the results. The continued evolution of constexpr in C++13 and C++17 is taking the basic building blocks to new frontiers that I had always wanted to do with our system, but never had time, like arbitrary compile-time evaluation of expressions, and freezing/memoization of the results.

第 87 段(可获 1.71 积分)

Thankfully, because I was leading the C++ group at Microsoft for some time after Midori, I was able to bring many of our lessons learned to the discussion, and I like to think it has had a positive impact on evolving C++ even further.

D

The system we came up with has obvious comparisons to D’s take on const and immutable; just as D’s const is a view over mutable or immutable data, so too is our readonly. And just as D added deepness to the concept of const, so did we in our permissions model generally. This is perhaps the closest analogy in any existing systems. I am frankly surprised it doesn’t get used an order of magnitude more than it does, although Andrei, one of its chief developers, has some thoughts on that topic.

第 88 段(可获 1.68 积分)

Go

Although I personally love programming in Go, it didn’t have as much influence on our system as you might expect. Go lists concurrency as one of its primary features. Although concurrency is easy to generate thanks to goroutines, and best practices encourage wonderful things like “Share Memory by Communicating”, the basic set of primitives doesn’t go much beyond the threads, thread-pools, locks, and events that I mention us beginning with in the early days of this journey.

On one hand, I see that Go has brought its usual approach to bear here; namely, eschewing needless complexity, and exposing just the bare essentials. I compare this to the system we built, with its handful of keywords and associated concept count, and admire the simplicity of Go’s approach. It even has nice built-in deadlock detection. And yet, on the other hand, when I find myself debugging classical data races, and torn structs or interfaces, I clamor for more. I have remarked before that simply running with GOMAXPROCS=1, coupled with a simple RPC system – ideally integrated in such a way where you needn’t step outside of Go’s native type system – can get you close to the simple “no intra-process parallelism” Midori model that we began with. And perhaps the best sweet spot of all.

第 89 段(可获 2.7 积分)

Rust

Out of the bunch, Rust has impressed me the most. They have delivered on much of what we set out to deliver with Midori, but actually shipped it (whereas we did not). My hat goes off to that team, seriously, because I know first hand what hard, hard, hard work this level of type system hacking is.

I haven’t yet described our “borrowed references” system, or the idea of auto-destructible types, however when you add those into the mix, the underlying type system concepts are remarkably similar. Rust is slightly less opinionated on the overall architecture of your system than Midori was, which means it is easier to adopt piecemeal, however the application of these concepts to traditional concurrency mechanisms like locks is actually fascinating to see.

第 90 段(可获 1.61 积分)

This article gives a great whirlwind tour of safe concurrency in Rust. Poking through to some of the references reveals APIs designed with similar principles in mind. For example, simple_parallel looks a whole lot like the PFX Parallel API described earlier with safety annotations applied to it. I trust their system more than ours, because they have shipped and had thousands of eyes and real-world experience applied to it.

Epilogue and Conclusion

Although I’ve glossed over many details, I hope you enjoyed the journey, and that the basic ideas were clear. And, most importantly, that you learned something new. If you want to understand anything in greater detail, please see our OOPSLA paper, or just ask.

第 91 段(可获 1.44 积分)

It’s been a couple years since I’ve been away from this. As most of you know, Midori happened before the OSS renaissance at Microsoft, and so it never saw the light of day. In that time, I’ve pondered what lessons we learned on this journey, and whether any of it is relevant beyond the hallways of our old building 34. I believe it is, otherwise I’d not have taken the time to write up this article.

I’m thrilled that the world has adopted tasks in a big way, although it was for a different reason than we expected (asynchrony and not parallelism). In many ways this was inevitable, however I have to think that doing tasks a half-decade ahead of the curve at least had a minor influence, including the async and await ideas built atop it.

第 92 段(可获 1.75 积分)

Data parallelism has taken off…sort of. Far fewer people leverage CPUs in the way we imagined, but that’s for good reason: GPUs are architected for extremely wide SIMD operations over floating points, which is essentially the killer scenario for this sort of parallelism. It doesn’t cover all of the cases, but man does it scream.

Safe concurrency is still critically important, yet lacking, and the world still needs it. I think we collectively underestimated how long it would take for the industry to move to type- and memory-safe programming models. Despite the increasing popularity of safe systems languages like Go and Rust, it pains me to say it, but I still believe we are a decade away from our fundamental technology stacks – like the operating systems themselves – being safe to the core. But our industry desperately needs this to happen, given that buffer errors remain the #1 attack type for critical security vulnerabilities in our software.

第 93 段(可获 1.99 积分)

I do think that concurrency-safety will be our next frontier after type- and memory-safety have arrived. TOCTOU, and race conditions generally, are an underexploited yet readily attackable vector. (Thankfully, just as writing correct concurrent code is hard, so too is provoking a latent concurrency error through the delicate orchestration of race conditions). As more systems become concurrent (distributed) systems this will become an increasing problem for us. It’s not clear the exact formulation of techniques I demonstrated above is the answer – in fact, given our focus on parallelism over asynchrony, surely it is not – however we will need someanswer. It’s just too damn hard to build robust, secure, and safe concurrent programs, still, to this day, 15 years later.

第 94 段(可获 1.51 积分)

In particular, I’m still conflicted about whether all those type system extensions were warranted. Certainly immutability helped with things far beyond safe concurrency. And so did the side-effect annotations, as they commonly helped to root out bugs caused by unintended side-effects. The future for our industry is a massively distributed one, however, where you want simple individual components composed into a larger fabric. In this world, individual nodes are less “precious”, and arguably the correctness of the overall orchestration will become far more important. I do think this points to a more Go-like approach, with a focus on the RPC mechanisms connecting disparate pieces.

第 95 段(可获 1.31 积分)

The model of leveraging decades of prior research was fascinating and I’m so happy we took this approach. I literally tried not to invent anything new. I used to joke that our job was to sift through decades of research and attempt to combine them in new and novel ways. Although it sounds less glamorous, the reality is that this is how a lot of our industry’s innovation takes place; very seldom does it happen by inventing new ideas out of thin air.

Anyway, there you have it. Next up in the series, we will talk about Battling the GC.

第 96 段(可获 1.28 积分)

文章评论

访客
没翻译完的文章就给推荐到了开源中国的邮件列表里,谁干的?
班纳睿
呃,什么情况?
solowolf
开源中国的发布的这篇文章早于本站,请看清楚时间再评论!请对比一下两篇翻译的风格再评论!