SHF: Small: Collaborative Research: Hybrid Static-Dynamic Analyses for Region Serializability

点击翻译按钮获取中文摘要

Title: SHF: Small: Collaborative Research: Hybrid Static-Dynamic Analyses for Region SerializabilityComputer systems' performance has grown exponentially for decades, enabling advances in science, health, engineering, and other areas. However, due to power, heat, and wire-length limitations, chip manufacturers are now producing microprocessors that have more, instead of faster, computing cores. To scale with this increasingly parallel hardware, software systems must become more parallel. However, writing correct, scalable shared-memory programs is notoriously difficult. A key challenge is that modern programming languages and software and hardware systems provide virtually no guarantees for programs that have a common, hard-to-eliminate behavior called data races -- because no one knows how to provide better guarantees while retaining high performance. As a result, software is difficult to reason about and fails unexpectedly, leading to high development and testing costs, and imperiling reliability and security of mission- and safety-critical systems. This project provides stronger guarantees for software, achieving reasonable performance on contemporary systems. The intellectual merits are novel program analyses and runtime support that provide strong behavioral guarantees for programs. The project's broader significance and importance are making software systems automatically more reliable; eliminating whole classes of errors; reducing development and testing costs by simplifying programming; and simplifying and reducing costs of program analyses and software system support. Furthermore, the PIs' educational, mentoring, and outreach activities enhance the project by helping educate a diverse workforce of computer scientists trained in the project's work.A key contribution is a novel hybrid static-dynamic analysis that enforces a memory model called statically bounded region serializability (SBRS) entirely in software. This memory model is strictly stronger than sequential consistency (SC) and has the potential to be more efficient than SC to enforce, since it allows compilers and hardware to reorder instructions within regions. The project involves designing, implementing, and evaluating (1) three compiler transformations for enforcing SBRS, (2) enhancements to the static-dynamic analysis for performance and flexibility, (3) a novel asynchronous protocol for overlapping concurrency control with program execution while enforcing SBRS, and (4) enhancements to a software transactional memory (STM) system to use the asynchronous protocol to improve scalability. The work provides, for the first time, support for always-on, end-to-end SBRS that is practical, and it makes further advancements in providing high-performance runtime support for atomicity.