ITR: Protocol Synthesis and Verification
ITR: Protocol Synthesis and Verification
批准号:
0219805
负责人:
Ganesh Gopalakrishnan
金额:
$26.0万
依托单位:
依托单位国家:
美国
项目类别:
Continuing Grant
财政年份:
2002
资助国家:
美国
项目状态:
已结题
起止时间:
2002-09-01 至 2006-10-31
中文摘要
点击翻译按钮获取中文摘要
英文摘要
Projects of national importance critically depend on supercomputers, such as the ASCI White supercomputer deployed at Lawrence Livermore Laboratories. Supercomputers such as these are comprised of thousands of microprocessors that share terabytes of main memory. In order to bring down the cost of these `shared memory' supercomputers and to ensure their error-free operation during long-running simulations, their design and verification complexity must be significantly reduced. A significant amount of this complexity exists in the concurrent protocols that allow the microprocessors to reliably share memory. The investigators study how to automatically synthesize these protocols from higher level descriptions that are easier (and hence quicker) to verify correct. This research involves a formal understanding of high performance protocols in use this area, the creation of a guided synthesis procedure that allows designers to quickly explore the space of protocols and select one that meets the performance goals, and then mathematically prove the correctness of the high level protocol as well as its translation to a detailed hardware-level protocol description. Design and verification tools that the industry can adopt are being developed.The distributed shared memory (DSM) is a dominant organizational paradigm for multiprocessor machines. DSM machines are used as desktop computers, supercomputers such as the 512-node ASCI White of Lawrence Livermore, and in future sold as single-chip multiprocessor components. The high verification complexity of DSM machines is known to delay the shipping dates of microprocessors and parallel processing software. This complexity stems from a host of DSM protocol design issues, such as: (i) aggressive latency hiding through out-of-order processing, implying the use of complex weak memory consistency models; (ii) complex protocol actions that require buffer reservation and deadlock avoidance. This research involves a formal understanding of weak memory models (captured as a theorem-prover library), and high performance protocols in use this area. It develops guided synthesis procedures that allow designers to quickly explore a wide spectrum of protocols. Once a high-level protocol meeting estimated performance goals is selected, model checking is employed to verify conformance against the chosen weak memory model. A mathematically proven (using theorem proving) translation procedure is then applied to obtain a detailed protocol description. This description is analyzed for performance and iterated till convergence. Examples drawn from industrial multiprocessors are used to illustrate our new methods. Design and verification tools that the industry can adopt are being developed.
期刊论文(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
-
依托单位:
CPA-DA: Formal Methods for Multi-core Shared Memory Protocol Design
-
批准号:0811429
-
项目类别:Continuing Grant
-
资助金额:$25.0万
-
财政年份:2008
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
CSR-SMA: Toward Reliable and Efficient Message Passing Software Through Formal Analysis
-
批准号:0509379
-
项目类别:Continuing Grant
-
资助金额:$0.0万
-
财政年份:2005
-
负责人:Ganesh Gopalakrishnan
-
依托单位:
海外基金