ITR: Protocol Synthesis and Verification

国家重要项目严重依赖于超级计算机，比如部署在劳伦斯利弗莫尔实验室的ASCI白色超级计算机。像这样的超级计算机由数千个微处理器组成，这些微处理器共享tb的主存储器。为了降低这些“共享内存”超级计算机的成本，并确保它们在长时间模拟过程中无错误运行，它们的设计和验证复杂性必须显著降低。这种复杂性很大程度上存在于允许微处理器可靠地共享内存的并发协议中。研究人员研究如何从更容易（因此更快）验证正确的更高级别描述自动合成这些协议。本研究涉及对该领域使用的高性能协议的正式理解，创建指导合成过程，使设计人员能够快速探索协议空间并选择符合性能目标的协议，然后在数学上证明高级协议的正确性以及将其转换为详细的硬件级协议描述。业界可以采用的设计和验证工具正在开发中。分布式共享内存（DSM）是多处理器机器的主要组织范式。DSM机器被用作台式计算机，超级计算机，如劳伦斯利弗莫尔的512节点ASCI怀特，未来作为单芯片多处理器组件出售。众所周知，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.