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

摘要：人类社会在很大程度上依赖于计算设备：从手机中的嵌入式计算机到每秒可以执行一百亿亿次乘法的千万亿级计算系统，并帮助模拟从车祸到飓风的一切。计算机的性能必须逐年提高，否则以信息为基础的人类社会将停止进步。不幸的是，过去提高计算机性能的方法？即增加时钟频率和功能单元复杂性——不再有效。这些技术现在只产生微小的性能提高，而导致能源消耗的巨大增加。计算设备已经消耗了全国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.