ACM SIGOPS名人堂（第二期）
SIGOPS名人堂奖（Hall of Fame Award, HoF）是SIGOPS组织于2005年设立的奖项，用于评选一批发表10年以上对操作系统领域产生巨大影响力的文章，是系统领域至高无上的荣誉。该奖项每年评选一次，在每年系统领域顶级会议SOSP和OSDI上颁发（两会议隔年交替举办），起初两届奖项（SOSP 2005和OSDI 2006）由当年的SOSP和OSDI的程序委员会成员（Program Committees, PC）投票选出，后为减轻PC们沉重的工作负担，从2007年起成立名人堂奖项委员会，委员会成员由最近4届SOSP和最近4届OSDI的大会主席组成，以此保障奖项的公允性和含金量。
在之前的“SOSP名人堂第一期”中我们介绍了2005年评选出的4篇文章。在本期SOSP名人堂中，作者将向大家介绍2006年以及2007年的部分当选文章，它们分别是：
George C. Necula and Peter Lee “Safe Kernel Extensions Without Run-Time Checking”
Leslie Lamport “Time, Clocks, and the Ordering of Events in a Distributed System”
Andrew D. Birrell and Bruce Jay Nelson “Implementing Remote Procedure Calls”
这三篇文章中，第一篇于2006年被选入SOSP名人堂，发表于1996年第二届OSDI会议。之后的两篇都是2007年入选的，分别发表在1978年的”Communications of the ACM”以及1984年的”ACM Transactions on Computer Systems”。这些工作也都对学术界和工业界产生了巨大而深远的影响，下面我们依次回顾每篇文章。
George C. Necula and Peter Lee
“Safe Kernel Extensions Without Run-Time Checking”
George Necula（左）与Peter Lee（右）
本期介绍的第一篇文章是George C. Necula 与 Peter Lee共同完成的 ”Safe Kernel Extensions Without Run-Time Checking”，该文章也是SOSP名人堂2006年评选出的唯一一篇论文。这篇文章提出了PCC（proof carrying code）的概念，旨在解决“如何在内核中运行不可信代码”这一问题。
在这篇文章提出PCC之前，该问题的主要解决方法是对运行代码进行动态检查。具体来说，就是通过插桩等方法，在运行时检查代码是否违背了内核所制定的一些准则，例如检查所有内存读取是否都在一个特定的范围之内。这种方法无疑会极大地影响代码的执行性能。
George 与 Peter 通过形式化验证的方法，自动化的证明代码的行为符合内核制定的一些准则，并且将证明添加在代码之后从而生成PCC。具体来说，内核作为一个代码执行者首先对外公布一系列的安全性准则，而代码的生成者利用本文提供的编译器对代码进行编译，编译过程中将自动生成对于代码是否符合某些准则的证明。最终代码和相应的证明组合在一起，成为了一份PCC。内核在运行PCC时，首先自动化的验证其中的证明，判断PCC中的代码是否满足事先定义的安全性准则。只有验证通过的PCC才会被执行。而PCC只有在第一次运行时才需要进行证明的验证，而在之后的运行过程中不会产生任何性能影响。
PCC提供了一个通用的方法，将对于一个模块的信任迁移到证明检查器上。模块的执行者无须信任模块的实现者，只要证明检查器工作正确，系统的安全性就能够得到保证。而PCC这种利用高级程序语言的语意，通过编译器自动生成证明的方法，也成为了验证编译的主流方法之一，推动了“language-based security”的发展。
Leslie Lamport
“Time, Clocks, and the Ordering of Events in a Distributed System”
Leslie Lamport
介绍的第二篇文章是 Lesile Lamport 的 ”logical clocks”, 也被人们称为 ”Lamport clocks”。这项工作在2007年被选入SOSP名人堂，被誉为 “第一篇真正的“分布式系统”论文”。Lamport在分布式系统领域无疑是一个家喻户晓的人物，享有“分布式计算原理之父”的美誉，从这篇文章提出的 ”causal ordering" 以及”logical clocks” 到1982年提出的“拜占庭将军问题”, 都对之后分布式系统领域内的研究产生了深远的影响。由于Lamport对分布式系统研究的卓越贡献，他被授予了2013年的图灵奖。
“Time, Clocks, and the Ordering of Events in a Distributed System”这篇曾一度成为计算机科学史上被引用最多的文献，该工作的核心思想最初起始于Paul Johnson 与 Bob Thomas 发表的一篇 “The Maintenance of Duplicate Databases”，当时Lamport正在为这篇论文作序。这篇论文在更新两个完全相同的数据库时，采用了时间戳技术（timestamps）。
看到这篇文章之后，曾经在数学系任教、并且对相对论有着深入了解的Lamport心中灵光一闪。深入了解狭义相对论的Lamport知道“不同的事件在时空是不存在一个不变的全局顺序的，两个事件只有在存在因果影响的情况下，才会有偏序关系”。那么在计算机系统中，如果要确定两个事件之间的顺序，那么他们之间必须要存在因果关系——也就是说传递过消息。利用这一方法，是否就可以为计算机系统中的所有事件进行全局排列？想到这里，Lamport马上记录下了这一巧妙的想法，并且短时间内就完成了算法的设计实现。
完成了算法实现之后，Lamport发现拥有一个能够对事件进行全局排序的算法之后，就能够实现任何分布式系统。他认为一个分布式系统可以被描述为用处理器网络实现的一种状态机，一旦能够对输入请求（也就是事件）进行全局排序之后，就能够给出实现所有这类状态机的方法，也就是说能够实现任意的分布式系统。为此，Lamport完成了这篇论文，希望解决“如何实现一个任意的分布式状态机”这一问题。
理想和现实总是存在差距，虽然这篇文章已经成为了分布式系统领域最著名的著作之一，但是Lamport发现几乎没有人注意到论文中提到的状态机，他们大多认为这篇文章是关于“分布式系统中事件之间的因果关系”或者“分布式互斥算法的”。当然，这些都无法改变这篇文章在分布式计算领域内深远的影响力。
除了“Time, Clocks, and the Ordering of Events in a Distributed System”这篇文章，Lamport也凭借另外两篇文章，先后赢得了2012和2013年的SIGOPS名人堂奖，我们将在之后几期介绍这两项工作。Lamport在进行分布式系统研究之余，也设计开发过许多大家耳熟能详的软件工具。在1984年左右，当时的Lamport使用一款叫做 plain Tex 的排版软件撰写自己的论文，但是写着写着Lamport觉得这个软件不是很好用。然后Lamport就自己开发一套新的论文排版的套件，命名为LaTex，也就是目前被研究者们广泛用于论文撰写的排版工具。
Andrew D. Birrell and Bruce Jay Nelson
“Implementing Remote Procedure Calls”
Andrew D. Birrell（左）与Bruce Jay Nelson（右）
本期介绍的最后一项工作是由Andrew D. Birrell 与 Brue Jay Nelson共同实现的远程通讯方法标准——RPC（Remote Procedure Call的缩写）。普通的过程调用（Procedure Call）提供了一个通用的、标准的程序内控制流与数据传递机制。与之相对应的，RPC（远程过程调用）旨在将普通的过程调用扩展到不同机器之间，从而提供一个标准的、易用的机器间控制流与数据传递机制。该项工作也获得了1994年的ACM软件系统奖（ACM Software System Award）。
在1976年，White, J.E 提出了一个基于网络的资源共享框架，自此学术界也开始了对于RPC的一系列讨论。然而在Andrew和Brue的工作之前，仍然没有通用的、可扩展的RPC实现。Andrew等人发现，一个RPC系统在实现时会遇到以下几个主要的问题：在机器或者通讯出错的情况下，如何保证调用的语意；如何在没有共享地址空间的情况下，传递含地址参数的语意；如何将RPC与现有程序兼容；调用者如何寻找、识别被调用者；如何在调用者与被调用者之间提供一个合适的数据与控制流传递协议；如何在公开网络环境下保证数据的完整性与安全性。
针对这些问题，Andrew等人提出了自己的系统结构、参数打包方法、调用对象之间的绑定策略以及一个新的针对RPC的网络包传输协议。最终实现的RPC使得应用程序可以像调用本地函数一样，直接调用远端机器上的服务。目前，RPC已经成为了跨机器间函数调用的一个通用方法，几乎所有的分布式系统都依赖于这套借口实现不同机器之间的函数调用。毫无疑问的，RPC已经是当下分布式系统的基石之一。
Andrew的另一篇工作Grapevine，也被选入了2008年的SIGOPS名人堂，我们将在近期的“ACM SIGOPS 名人堂”系列进行回顾。令人遗憾的是，本文的第一作者Andrew D. Birrell 于2016年不幸去世，但是他在计算机系统领域作出的贡献，足以被历史所铭记。
总结
与第一期介绍的四篇文章相同，本期介绍的来自2006年与2007年的三篇文章同样在计算机系统领域做出了杰出的贡献，对系统安全以及分布式系统领域之后的发展起到了至关重要的作用。与此同时，这些计算机系统历史上的经典之作，也引领了之后一批批系统工作者，在系统研究的道路上寻找到了自己的方向与研究哲学。在下一期的名人堂中，我们将继续为大家介绍2007年的其他三篇入选文章。
作者
华志超，上海交通大学IPADS实验室，博士生，主要研究方向为操作系统、虚拟化技术、系统安全以及移动设备安全性等。
参考文献
[1] https://www.sigops.org/award-hof.html
[2] http://www.msra.cn/zh-cn/news/features/leslie-lamport-turing-20140327
[3] http://lamport.azurewebsites.net/pubs/p-ubs.html#time-clocks
[4] http://lamport.azurewebsites.net/pubs/ti-meclocks.pdf
[5] https://en.wikipedia.org/wiki/Language-based_security#Techniques
[6]http://static.usenix.org/publications/library
/proceedings/osdi96/full_papers/necula/necula.ps
[7] https://cacm.acm.org/news/210689-in-memoriam-andrew-birrell-1951-2016/fulltext
[8] https://birrell.org/andrew/
[9] http://www.doc4share.com/qurtaba/os-papers/Muhammad%20Sanaullah.pdf
往期回顾
第26届计算机系统原理大会
（Symposium on Operating Systems Principles)
2017年10月28日-10月31日
于上海举办
计算机系统原理大会（SOSP）自1967年以来，每两年举办一次，至今已有50年历史。该会是由ACM组织的、全球最顶级的计算机系统会议之一。在每年的会议上，来自全球各地的学术界、产业界的系统研究者、开发者齐聚一堂，对计算机系统领域的前沿问题进行讨论。今年的第26届计算机系统原理大会将于十月份在中国 上海召开。点击阅读原文了解更多关于SOSP'17。
SOSP会议信息：
SOSP会议注册地址：http://www.regonline.com/sosp2017
资助学生参会的 scholarship，申请截止日期8月21日， 申请方式：https://www.sigops.org/sosp/sosp17/scholarship.html
面向学生的研究竞赛，只需2页的摘要，8月14日截稿，投稿方式：https://www.sigops.org/sosp/sosp17/src.html
面向计算机领域的女性科研人员交流的Ada论坛：https://www.sigops.org/sosp/sosp17/workshop-ada.html