ITR: Protocol Synthesis and Verification

具有国家重要性的项目在很大程度上依赖于超级计算机，例如部署在劳伦斯·利弗莫尔实验室的ASCI White超级计算机。像这样的超级计算机是由数千个共享TB主存的微处理器组成的。为了降低这些“共享内存”超级计算机的成本，并确保它们在长期运行的模拟过程中无错误运行，必须显著降低它们的设计和验证复杂性。这种复杂性的很大一部分存在于允许微处理器可靠地共享存储器的并发协议中。研究人员研究如何从更高级别的描述中自动合成这些协议，这些描述更容易(因此也更快)验证正确。这项研究涉及对这一领域中使用的高性能协议的形式化理解，创建指导综合过程，使设计人员能够快速探索协议空间并选择满足性能目标的协议，然后从数学上证明高级协议的正确性以及将其转换为详细的硬件级协议描述。业界可以采用的设计和验证工具正在开发中。分布式共享内存(DSM)是多处理器机器的主导组织模式。DSM机器被用作台式计算机和超级计算机，如劳伦斯·利弗莫尔的512节点ASCI White，未来作为单芯片多处理器组件出售。众所周知，DSM机器的高度验证复杂性会推迟微处理器和并行处理软件的发货日期。这种复杂性源于一系列DSM协议设计问题，例如：(I)通过无序处理的激进延迟隐藏，意味着使用复杂的弱内存一致性模型；(Ii)需要缓冲区预留和避免死锁的复杂协议操作。这项研究涉及对弱内存模型(捕获为定理证明者库)以及使用这一领域的高性能协议的正式理解。它开发了指导性的合成程序，使设计师能够快速探索广泛的协议。一旦选择了满足估计性能目标的高级协议，就使用模型检查来验证与所选择的弱存储器模型的一致性。然后应用数学证明(使用定理证明)转换过程来获得详细的协议描述。对该描述进行性能分析，并迭代直到收敛。文中以工业多处理机为例说明了我们的新方法。目前正在开发业界可以采用的设计和验证工具。

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.