XPS: FULL: Collaborative Research: Rethinking Architecture Support for Memory Consistency

尽管经过了几十年的进步，编写正确的并行软件来实现现代并行计算机硬件的价值仍然是极其困难的。一个关键的问题是，今天的计算机系统并没有给所有的程序提供明确的行为保证；“不同步”的代码，即并行计算不完全或不正确地协调，具有定义不明确的，往往是破坏性的行为。这个问题在几乎所有的并行计算机系统中都是一个关键的理论和实践缺陷。该建议通过提出一类新的并行计算机体系结构来解决这一挑战，该体系结构具有强大的行为保证，即使对于不同步的代码也是如此。其关键思想是让系统在不同步的程序执行引起问题之前安全地终止它们。为了避免降低可用性，该项目包括一些机制，以避免在可能的情况下终止程序执行，通过退回到更宽松、但安全和可预测的行为保证，以及通过解决不同步代码导致的潜在错误。该项目的智力优势在于，它甚至为不同步的并行代码提供了关键的行为保证。该项目淘汰了过时的硬件模型，这些模型不仅提供了不充分的行为保证，而且还复杂且耗电。该项目是该领域中第一个同时直接解决可用性和正确性的项目。该项目更广泛的意义和重要性在于，它将提高所有并行系统的可靠性，这些系统影响到生活的方方面面：医药、能源、交通、健康、国防和商业。该项目提供的更强大的保证避免了代价高昂、危险的失败，并降低了应用程序开发的成本，即使是在成熟的语言中也是如此。该项目将产生与行业相关的成果，并将通过出版影响学术界。该项目将直接影响计算领域的中等和高等教育，培养一支多样化的未来STEM工作队伍。为了为所有代码提供强大的行为保证--即使不正确地同步--建议的体系结构为粗粒度代码区域提供区域原子内存一致性保证。在这些体系结构中，程序的执行要么是代码区域的序列化，要么是以异常终止，该异常指示错误可能已使内存不一致。体系结构为所有程序执行提供了这种强大的内存一致性模型，与一致性和一致性的主流方法不同，这些方法倾向于较弱的保证，而不会在复杂性或性能方面带来明显的好处。在执行不同步代码的系统中，频繁的异常可能会经常终止程序执行，从而降低可用性。提出的体系结构通过使用定义良好的快照隔离语义来容忍一致性违规，从而避免了可用性降低，该语义避免了异常，但不保证代码区域的可串行化。该体系结构进一步通过解决异常来解决可用性，利用代码的可交换性来避免交换操作的不必要异常，以及使用动态符号分析来通过组合符号存储器更新来解决异常。

Despite decades of progress, writing correct parallel software to realize the value of modern parallel computer hardware remains extremely difficult. A key problem is that today's computer systems do not give all programs clear behavioral guarantees; "ill-synchronized" code, in which parallel computations are incompletely or incorrectly coordinated, has ill-defined, often destructive behavior. This problem is a key theoretical and practical flaw in nearly all parallel computer systems. This proposal addresses this challenge, by proposing a new class of parallel computer architectures with strong behavioral guarantees, even for ill-synchronized code. The key idea is to make systems safely terminate ill-synchronized program executions before they can cause problems. To avoid degrading availability, the project includes mechanisms to avoid terminating program executions when possible, by falling back to more permissive, yet safe and predictable behavioral guarantees, and by resolving potential errors caused by ill-synchronized code. The intellectual merits of the project are that it provides crucial behavioral guarantees even to ill-synchronized parallel code. The project eliminates outdated hardware models that not only provide inadequate behavioral guarantees, but are also complex, and power-hungry. The project is the first in this domain to directly address availability and correctness together. The project's broader significance and importance are that it will improve the reliability of all parallel systems, which affects all aspects of life: medicine, energy, transportation, health, defense, and business. The stronger guarantees provided by this project avoid costly, dangerous failures and decrease the cost of application development, even in mature languages. The project will generate results relevant to industry and will influence academia through publication. The project will directly influence secondary and higher education in computing, fostering a diverse, future STEM workforce.To provide strong behavioral guarantees to all code -- even if incorrectly synchronized -- the proposed architectures provide region-atomic memory consistency guarantees for coarse-grained code regions. In these architectures, a program's execution is either a serialization of code regions, or it terminates with an exception that indicates an error could have left memory inconsistent. The architectures provide this strong memory consistency model to all program executions, departing from mainstream approaches to coherence and consistency that favor weaker guarantees without a clear benefit in complexity or performance. In systems executing ill-synchronized code, frequent exceptions may too often terminate program executions, degrading availability. The proposed architectures avoid degrading availability by tolerating consistency violations with a well-defined snapshot isolation semantics that avoids exceptions, but does not guarantee serializability of code regions. The architectures further address availability by resolving exceptions, leveraging commutativity of code to avoid unnecessary exceptions for commutative operations, as well as using dynamic symbolic analysis to resolve exceptions by combining symbolic memory updates.