ITR: Protocol Synthesis and Verification

ITR：协议合成和验证

• 批准号: 0219805
• 负责人: Ganesh Gopalakrishnan
• 金额: $ 26万
• 依托单位: University of Utah
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-09-01 至 2006-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0219805&HistoricalAwards=false
• 关键词: ITR; Protocol; Synthesis; Verification

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.

一些国家级的重要项目主要依赖于超级计算机，例如部署在劳伦斯利弗莫尔实验室的ASCI白色超级计算机。像这样的超级计算机由数千个微处理器组成，它们共享太字节的主存储器。为了降低这些“共享内存”超级计算机的成本，并确保它们在长时间运行的模拟过程中无差错地运行，必须大大降低它们的设计和验证复杂性。大量的这种复杂性存在于允许微处理器可靠地共享存储器的并发协议中。研究人员研究如何从更高级别的描述中自动合成这些协议，这些描述更容易（因此更快）验证正确。这项研究涉及到一个正式的高性能协议在使用这一领域的理解，创建一个指导的合成过程，使设计人员能够快速探索的协议空间，并选择一个满足性能目标，然后在数学上证明的正确性的高层次的协议，以及它的翻译到一个详细的硬件级协议描述。工业界可以采用的设计和验证工具正在开发中。分布式共享存储器（DSM）是多处理器机器的主要组织范例。 DSM机器被用作台式计算机，超级计算机，如劳伦斯利弗莫尔的512节点ASCI白色，未来作为单芯片多处理器组件出售。 DSM机器的高验证复杂性被认为会延迟微处理器和并行处理软件的出货日期。这种复杂性源于许多DSM协议设计问题，例如：（i）通过乱序处理的侵略性延迟隐藏，这意味着使用复杂的弱存储器一致性模型;（ii）需要缓冲区预留和死锁避免的复杂协议动作。 这项研究涉及到弱内存模型（捕获为定理证明库）的正式理解，以及使用这一领域的高性能协议。它开发了指导合成程序，使设计人员能够快速探索广泛的协议。一旦一个高层次的协议，会议估计的性能目标被选中，模型检查是用来验证所选择的弱内存模型的一致性。 数学证明（使用定理证明）的翻译过程，然后应用，以获得详细的协议描述。分析该描述的性能并迭代直到收敛。从工业多处理器的例子来说明我们的新方法。 正在开发业界可以采用的设计和验证工具。