CPA-DA: Formal Methods for Multi-core Shared Memory Protocol Design

职务名称：多核共享内存协议设计的形式化方法研究者：Ganesh GopalakrishnanInst：UtahNSF提案号：0811429摘要：人类社会对计算设备的依赖性很大：从手机中的嵌入式计算机到每秒可以执行100亿次乘法的千万亿级计算系统，以及帮助模拟从车祸到飓风的一切。计算机的性能必须逐年提高，没有计算机的性能，信息化的人类社会将停滞不前。不幸的是，过去的方法来提高计算机的性能？即增加时钟频率和功能单元复杂性--不再有效。这些技术现在只产生微不足道的性能提高，同时导致能源消耗的巨大增加。计算设备已经消耗了全国5%以上的电力！提高计算机性能的唯一节能方法是使用多个中央处理器（CPU）。不幸的是，这样的组织（称为“多核CPU”）要求对中央存储器的访问非常高效-需要使用高度复杂的协议-称为高速缓存一致性协议。 不幸的是，这些协议必须手工制作才能获得高性能，因此非常容易出错。以前的方法来验证高速缓存一致性协议已经在验证工具的能力的限制。随着多核CPU的出现，其复杂性已经超出了所有已发布技术的范围。PI和他的团队是唯一一个已经开发出技术来验证的学术团体，使用数学上合理的计算机算法，分层多核CPU缓存一致性协议。 不幸的是，迄今为止，他们的方法都涉及到专家，而且经常引起相当大的乏味。 本提案中提出的方法预计：（1）减少验证高速缓存一致性协议的负担，以及（2）帮助弥合两个中心抽象差距，从而最大限度地减少微处理器中的错误机会：（i）高级别到低级别的行为建模差距，以及（ii）低行为级别到硬件实现级别差距。 这将有助于培训宝贵的人力资源-包括大学生和代表性不足的群体。这将有助于维持美国的技术势头，因为持续的高性能计算能力的可用性对美国的重要性不亚于其他基本需求，如水，清洁空气和能源。 预计该项目开发的核查工具将是转让给计算机行业的技术。 最后但并非最不重要的是，在这个项目中培养的学生将加入国家和国际高科技劳动力。

Title: Formal Methods for Multi-core Shared Memory Protocol DesignPI: Ganesh GopalakrishnanInst: University of UtahNSF Proposal Number: 0811429 ABSTRACT:The human society crucially depends on computing devices: from embedded computers in phones to peta-scale computing systems that can perform a million billion multiplications every second, and help simulate everything from car crashes to hurricanes. The performance of a computer must increase each year, without which the information-based human society will cease to advance. Unfortunately, past methods to increase the performance of a computer ? namely increasing the clock frequency and the functional unit complexity -- cease to be effective. These techniques now produce only a miniscule performance increase, while causing huge increases in the energy consumption. Already computing equipments consume more than 5% of the nation's electricity! The only available energy-efficient method of increasing computer performance is through the use of multiple central processing units (CPUs). Unfortunately, such organizations (called "multi-core CPUs") require that the accesses to the central memory be extremely efficient - requiring the use of highly complex protocols - called cache coherence protocols. Unfortunately these protocols must be hand-crafted for high performance, and hence are extremely error-prone. Previous methods to verify cache coherence protocols were already at the limits of the capabilities of verification tools. With the advent of multi-core CPUs, the complexity has become out of reach of all published techniques. The PI and his team are the only academic group to have developed techniques to verify, using mathematically sound computer algorithms, hierarchical multi-core CPU cache coherence protocols. Unfortunately, their methods to date have involved expert humans and often cause considerable tedium. The proposed methods in this proposal are expected to: (1) reduce the burden of verifying cache coherence protocols, and (2) help bridge two central abstraction gaps, thus minimizing the chances of errors in microprocessors: (i) high-level to low-level behavioral modeling gap, and (ii) the low behavioral level to hardware implementation level gap. It will help train valuable manpower - including undergraduates and under-represented groups. It will help sustain the technological momentum of the US, as the availability of sustained high performance computing power is no less important to the nation than its other basic needs such as water, clean air, and energy. The verification tools developed in this project are expected to be technology transferred to the computer industry. Last but not least, the students trained in this project will join the national and international high-technology labor force.