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

标题：多核共享内存协议设计的正式方法PI：Ganesh Gopalakrishnan Inst：UtahNSF提议编号：0811429摘要：人类社会关键依赖于计算设备：从手机中的嵌入式计算机到Peta规模的计算系统，每秒可以执行10亿次乘法，并帮助模拟从车祸到飓风的一切。计算机的性能必须每年都在提高，没有它，人类社会的信息化就会停滞不前。不幸的是，过去提高计算机性能的方法呢？即增加时钟频率和功能单元复杂性--不再有效。这些技术现在只产生了很小的性能提升，而导致了能源消耗的巨大增加。计算设备已经消耗了全国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.