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.