CPA-DA: Formal Methods for Multi-core Shared Memory Protocol Design
CPA-DA: Formal Methods for Multi-core Shared Memory Protocol Design
批准号:
0811429
负责人:
Ganesh Gopalakrishnan
金额:
$25.0万
依托单位:
依托单位国家:
美国
项目类别:
Continuing Grant
财政年份:
2008
资助国家:
美国
项目状态:
已结题
起止时间:
2008-07-01 至 2013-06-30
中文摘要
摘要:人类社会在很大程度上依赖于计算设备:从手机中的嵌入式计算机到每秒可以执行一百亿亿次乘法的千万亿级计算系统,并帮助模拟从车祸到飓风的一切。计算机的性能必须逐年提高,否则以信息为基础的人类社会将停止进步。不幸的是,过去提高计算机性能的方法?即增加时钟频率和功能单元复杂性——不再有效。这些技术现在只产生微小的性能提高,而导致能源消耗的巨大增加。计算设备已经消耗了全国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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
REU Site: Trust and Reproducibility of Intelligent Computation
-
批准号:2244492
-
项目类别:Standard Grant
-
资助金额:$40.5万
-
财政年份:2023
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
FMiTF: Track-2 : Rigorous and Scalable Formal Floating-Point Error Analysis from LLVM
-
批准号:2319507
-
项目类别:Standard Grant
-
资助金额:$10.0万
-
财政年份:2023
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
Collaborative Research: FMitF: Track-1: Correctness at Both Ends: Rigorous ML Meets Efficient Sparse Implementations
-
批准号:2124100
-
项目类别:Standard Grant
-
资助金额:$45.0万
-
财政年份:2021
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
Collaborative Research: SHF: Medium: Practical and Rigorous Correctness Checking and Correctness Preservation for Irregular Parallel Programs
-
批准号:1956106
-
项目类别:Standard Grant
-
资助金额:$44.76万
-
财政年份:2020
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
FMiTF: Track II: Rigorous and Versatile Float-Point Precision Analysis and Tuning
-
批准号:1918497
-
项目类别:Standard Grant
-
资助金额:$10.0万
-
财政年份:2019
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
SHF: Small: Indy: Toward Safe and Fast Compiler Flags
-
批准号:1817073
-
项目类别:Standard Grant
-
资助金额:$48.14万
-
财政年份:2018
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
SHF: Medium: Hierarchical Tuning of Floating-Point Computations
-
批准号:1704715
-
项目类别:Standard Grant
-
资助金额:$120.0万
-
财政年份:2017
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
2017 Software Infrastructure for Sustained Innovation (SI2) Principal Investigator Workshop
-
批准号:1702722
-
项目类别:Standard Grant
-
资助金额:$9.5万
-
财政年份:2016
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
EAGER: Application-driven Data Precision Selection Methods
-
批准号:1643056
-
项目类别:Standard Grant
-
资助金额:$30.0万
-
财政年份:2016
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
SI2-SSE: Scalable Multifaceted Graphical Processing Unit (GPU) Program Debugging
-
批准号:1535032
-
项目类别:Standard Grant
-
资助金额:$41.75万
-
财政年份:2015
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
XPS: EXPL: CCA: Collaborative Research: Nixing Scale Bugs in HPC Applications
-
批准号:1439002
-
项目类别:Standard Grant
-
资助金额:$15.0万
-
财政年份:2014
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
CSR: SMALL: Design Validation Methods for Reliable and Efficient Floating-Point
-
批准号:1421726
-
项目类别:Standard Grant
-
资助金额:$39.83万
-
财政年份:2014
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
Collaborative Research: Localized, Layered Formal Hardware/Software Resilience Methods
-
批准号:1255776
-
项目类别:Continuing Grant
-
资助金额:$11.55万
-
财政年份:2013
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
CCF: SHF: Medium: Collaborative Research: A Static and Dynamic Verification Framework for Parallel Programming
-
批准号:1302449
-
项目类别:Continuing Grant
-
资助金额:$40.0万
-
财政年份:2013
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
SI2-SSE: Correctness Verification Tools for Extreme Scale Hybrid Concurrency
-
批准号:1148127
-
项目类别:Standard Grant
-
资助金额:$44.43万
-
财政年份:2012
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
EAGER: Formal Reliability Enhancement Methods for Million Core Computational Frameworks
-
批准号:1241849
-
项目类别:Standard Grant
-
资助金额:$20.0万
-
财政年份:2012
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
Travel and Registration Support for Computer Aided Verification 2011
-
批准号:1118485
-
项目类别:Standard Grant
-
资助金额:$0.7万
-
财政年份:2011
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
Collaborative Research: MCDA: Formal Analysis of Multicore Communication APIs and Applications
-
批准号:0903408
-
项目类别:Standard Grant
-
资助金额:$18.83万
-
财政年份:2009
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
CSR-SMA: Toward Reliable and Efficient Message Passing Software Through Formal Analysis
-
批准号:0509379
-
项目类别:Continuing Grant
-
资助金额:$0.0万
-
财政年份:2005
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
ITR: Protocol Synthesis and Verification
-
批准号:0219805
-
项目类别:Continuing Grant
-
资助金额:$26.0万
-
财政年份:2002
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
国内基金
海外基金
登录
查看更多内容
姜黄素衍生物Da0324通过抑制TRIP12介导的FBW7泛素化抑制结直肠癌的化疗耐药
-
批准号:2026JJ82279
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2026
-
负责人:刘亚
-
依托单位:
新型氟化物HFPO-DA和镉对土壤微生物的联合毒性效应
-
批准号:
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2025
-
负责人:秦俊莲
-
依托单位:
LACTB琥珀酰化修饰调控巨噬细胞CCL2-CCR2轴在新型青蒿素衍生物DA抗细菌脓毒症的作用及机制
-
批准号:
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2025
-
负责人:岑彦艳
-
依托单位:
嗜黏蛋白艾克曼菌(AKK)通过肠神经-孤束核-伏隔核DA/5-HT系统对小鼠酒精成瘾行为的预防作用及机制研究
-
批准号:2025JJ50534
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2025
-
负责人:张晓洁
-
依托单位:
CXCR3通路参与调控TSPO-18Da在视神经脊髓炎谱系疾病合并神经性疼痛中的机制研究
-
批准号:2025JJ50684
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2025
-
负责人:周小良
-
依托单位:
OPG-RANKL-RANK轴调控NLRP3炎症小体介导DA神经元变性的分子机制研究
-
批准号:
-
项目类别:省市级项目
-
资助金额:15.0万元
-
批准年份:2024
-
负责人:陈祥
-
依托单位:
基于HIF-1/DA/VEGF途径探讨健脾补肾方介导MAPK调控“成血管-成骨偶联产促进胎骨头环球腹腔机制研究
-
批准号:
-
项目类别:青年科学基金项目
-
资助金额:--
-
批准年份:2024
-
负责人:于湿
-
依托单位:
逆针刺介导DA能系统异常修复运动疲劳后小鼠皮层-纹状体通路突触受损的作用研究
-
批准号:--
-
项目类别:青年科学基金项目
-
资助金额:--
-
批准年份:2024
-
负责人:曹家桢
-
依托单位:
逆针刺介导 DA能系统异常修复运动疲劳后小鼠皮层-纹状体通路突触受损的作用研究
-
批准号:--
-
项目类别:青年科学基金项目
-
资助金额:--
-
批准年份:2024
-
负责人:曹家桢
-
依托单位:
tDCS通过调控星形胶质细胞表型转化对PD鼠中移植DA能神经干细
胞的整合功能的影响及机制研究
-
批准号:
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2024
-
负责人:承欧梅
-
依托单位: