Michael Carbin关于近似计算的完整性特性

||对话

迈克尔·卡尔宾肖像迈克尔·卡宾是麻省理工学院电子工程和计算机科学的博士研究生。他的兴趣包括设计编程系统,通过结合近似计算和自修复来提供改进的性能和弹性。金宝博官方

他本科时在斯坦福大学进行的程序分析工作获得了最佳计算机科学本科荣誉论文奖。作为一名研究生,他获得了MIT Lemelson总统和微软研究院研究生奖学金。金宝博娱乐他最近关于验证在不可靠金宝博娱乐硬件上执行的程序的可靠性的研究获得了OOPSLA 2013年最佳论文奖。

路加福音Muehlhauser: 在Carbin等人(2013),您和您的共同作者呈现出一种新的编程语言,即“使开发人员能够理解[程序]在不可靠的硬件上执行时产生正确的结果。”如何与早期的方法不同,以实现可靠的近似计算?


迈克尔·卡宾这是一个好问题。构建使用不可靠组件的应用程序一直是分布式系统社区和其他研究如何构建容错系统的社区的长期目标。金宝博官方容错系统的一个关键目标是,即使在系统的组成组件中存在错误时,也金宝博官方要交付正确的结果。

这一目标与我们在我的工作中有针对性的不可靠的硬件的目标形成鲜明对比。具体而言,硬件设计人员正在考虑新的设计,这些设计将是故意的 - 暴露可能默默地产生不正确结果的组件,以某种不可忽略的概率。这些硬件设计师正在使用广泛称为近似计算的子字段。

The key idea of the approximate computing community is that many large-scale computations (e.g., machine learning, big data analytics, financial analysis, and media processing) have a natural trade-off between the quality of their results and the time and resources required to produce a result. Exploiting this fact, researchers have devised a number of techniques that take an existing application and modify it to trade the quality of its results for increased performance or decreased power consumption.

我的小组工作的一个例子是简单地跳过我们已经证明的计算的部分 - 通过测试 - 可以在没有基本上影响应用程序结果的整体质量的情况下。另一种方法是执行在这些新的不可靠的硬件系统上自然容忍错误的应用程序的部分。金宝博官方

这是一个自然的后续问题是,开发人员先前如何处理近似值?

这些大规模应用自然是近似的,因为确切的解决方案通常是棘手的,或者也许甚至不存在(例如,机器学习)。因此,这些应用程序的开发人员通常从如何计算准确结果的精确模型开始,然后使用该模型作为设计易算法的指南和返回更近似解的相应实现。因此,这些开发人员已经手动向其算法(及其实现)向其近似地应用于其算法的准确性一段时间。这一的主要例子是数值分析领域及其对科学计算的贡献。

新兴的近似计算社区代表了对编程语言,运行时系统,操作系统和硬件架构的实现,不仅可以帮助开发人员在构建这些应用程序时导航所需的近似,而且还可以包含近似值本身。金宝博官方例如,硬件架构本身可能会导出应用程序的开发人员可以用作其许多用于执行近似的工具之一的不可靠的硬件组件。


卢基:你为什么选择开发依赖作为必要而不是功能规划语言?我的理解是,与可靠性,安全性和安全性有关的应用程序通常优先考虑功能规划语言,因为它们通常可以进行机器检查的正确性。


迈克尔:历史上一直是必要和功能语言组之间的热情竞争。传统上,达到广泛使用的语言(例如,C,C,C,C ++,Java,PHP和Python),而功能语言传统上呼吁较小,更加学历的学者倾斜程序员。

迫切和功能性心态之间的划分也适用于编程语言和编译器研究界的研究人员。金宝博娱乐我们使用命令语言的决定主要是由于广泛的公共和研究受众可以访问简单的命令语言。金宝博娱乐

然而,我们对于命令式语言的结果也可以适用于函数式语言。这很重要,因为随着Erlang (WhatsApp)和Scala (Twitter)等语言的流行,公众对函数式语言的兴趣越来越大。结果,随着标准函数式语言特性被主流命令式语言(例如,lambdas c++和Java)所采用,命令式语言和函数式语言阵营之间的界限开始模糊。因此,我金宝博娱乐们的研究能够适应编程范式领域的变化。

需要注意的一件重要的事情是——原则上——对用两种不同的图灵完备语言(命令式或函数式)编写的程序进行推理是同样困难的(即,不可判定)。然而,用函数式语言编写程序通常能更好地暴露计算的结构。

例如,将元素列表映射到功能语言中的另一个元素列表,使得计算的递归性质以及列表的当前头元素与其尾部不相交的事实。

然而,将一个元素列表映射到一个简单的C实现(例如)会立即使用指针,因此使执行验证所需的推理复杂化。随着命令式语言开始公开更好的结构化编程构造,命令式语言和函数式语言之间的推理差距将会缩小。


卢基:对于像Rely这样可以提高近似计算和嵌入式系统应用程序可靠性的方法和工具的研究,有哪金宝博娱乐些有前景的“下一步”?金宝博官方


迈克尔:近似计算社区刚开始拾取蒸汽,所以有很多机会。

在计算机硬件方面,如果我们有意构建硬件,通过无声地返回不正确或近似的结果来打破传统的数字抽象,那么性能/能量增益可能是什么,这仍然是一个悬而未决的问题。例如,社区的研究人员仍然在金宝博娱乐问,我们将看到2倍的增益还是我们希望看到100倍的增益?

关于硬件的另一个主要问题是,每个近似分量的误差模型是什么?它们是由于任意误差而频繁失效,还是由于小的有界误差而很少失效?或者,在这两个极端之间是否存在某种快乐的平衡?

在硬件之上还有各种各样的软件问题。大多数软件的设计和构建都基于硬件是可靠的这一假设。我们和R金宝博娱乐ely一起进行的研究是第一批提出编程模型和工作流程的人,在这些新的近似硬件设计面前提供了可靠性和准确性保证。

然而,仍有许多挑战。例如,编译器传统上依赖于所有指令和存储区域都同样可靠的假设。然而,近似的硬件可能导致某些操作/存储区域比其他区域更可靠的硬件设计。由于这种区别,通过将一个操作序列交换为另一个操作序列来优化程序的标准编译器转换现在可能会改变程序的可靠性。这种新的现实将要求社区重新思考我们如何设计、构建和推理编译器,以平衡优化和可靠性。

近似计算社区还有待探索的另一个机会是,现有的软件实现了一些算法,这些算法本身可能具有灵活性,也可能是许多潜在算法中的一种。展望未来,近似计算社区将需要考虑应用程序的算法灵活性,以实现它希望实现的广泛影响。

具体来说,通过引入算法,近似计算社区将能够结合数值分析、科学计算和理论社区的经验和结果,为精度、稳定性、并利用这些近似的软硬件系统来实现算法的收敛。金宝博官方


卢基:谢谢,迈克尔!