Collaborative Research: PPoSS: LARGE: ScaleStuds: Foundations for Correctness Checkability and Performance Predictability of Systems at Scale

合作研究：PPoSS：大型：ScaleStuds：大规模系统正确性可检查性和性能可预测性的基础

• 批准号: 2119184
• 负责人: Haryadi Gunawi
• 金额: $ 312.5万
• 依托单位: University of Chicago
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2119184&HistoricalAwards=false
• 关键词: Collaborative; Research; PPoSS; LARGE; ScaleStuds

In light of the limits of Moore's Law and Dennard scaling and the ever increasing computing demand, the last decade has seen unprecedented deployment scales; Google is known to run clusters with thousands of machines each, Apple deploys a total of 100,000 database machines, and Netflix runs tens of database clusters with 500 nodes each. This era of extreme-scale distributed systems has given birth to a new class of faults, "scalability faults" -- complex latent faults that are scale-dependent, whose symptoms surface in large-scale deployments but not necessarily in small/medium-scale deployments. Many fundamental research questions are not answerable today. On correctness: How to detect bugs that only manifest under large scale through program analysis? How to test and reproduce various dimensions of system scales efficiently on one machine? How to prevent and fix scalability-related faults? On performance: How to reason about software performance on various heterogeneous devices? How to accurately predict performance of fine-grained tasks to reduce inaccuracies at the aggregate level and project performance to future architectures? Finally, in combination: How to answer all these questions for the larger connected ecosystem -- not just the individual software and hardware components -- and to eventually build future-generation systems that are reproducible and verifiable by construction with respect to correctness and performance at scale? The ScaleStuds project involves a team of ten researchers to develop the foundations of correctness checkability (CC) and performance predictability (PP) of systems at scale. The key principle of this project is to "check large with large" -- check large-scale systems with a large fleet of data, analysis, tests, learning, models, and proofs. The vision is to build an ecosystem of distributed "CC+PP-certified" software-software and -hardware interactions. The project is paving the vision one "floor" at a time, creating composable building blocks ("the studs"). The project first builds new mechanisms such as a scale-testing platform and a unified database of software program properties and hardware performance profiles exposing clear APIs. These studs then enable multi-dimensional automated scalability tests and program analysis and performance learning and prediction at various levels of the software/hardware stack. Ultimately all of these experiences are intended to lead to correct and performant cross-layer/service interactions and future design principles including reproducible- and verified-by-construction development methods. The project novelties include the advancement of debugging, testing, learning, and prediction methods to ensure correctness checkability and performance predictability of extreme-scale systems and applications both on classical hardware platforms and emerging ones; a unified data ecosystem of software/hardware properties and profiles that facilitates automated analyses via clear APIs; a multi-dimensional scale-testing framework that empowers the development of new large-scale unit-tests and program analysis; detailed device profiling and observation to enable large-scale performance learning/prediction and deliver lessons for learning/predicting the behavior of other devices and layers in an end-to-end hardware/software stack; and ultimately a clear definition of CC+PP-certifiability for today's systems and future verifiable/reproducible-by-construction development methods.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

考虑到摩尔定律和Dennard扩展的限制以及不断增长的计算需求，过去十年的部署规模达到了前所未有的水平;众所周知，Google运行的集群每个有数千台机器，Apple部署了总共100，000台数据库机器，Netflix运行了数十个数据库集群，每个集群有500个节点。 这个极端规模分布式系统的时代已经产生了一类新的故障，“可扩展性故障”-复杂的潜在故障，是规模相关的，其症状出现在大规模部署，但不一定在小型/中型部署。 许多基本的研究问题在今天是无法回答的。 关于正确性：如何通过程序分析来检测只有在大规模下才会出现的错误？如何在一台机器上有效地测试和再现系统秤的各种尺寸？如何预防和修复与可扩展性相关的故障？ 关于性能：如何在各种异构设备上推理软件性能？如何准确地预测细粒度任务的性能，以减少聚合级别的不准确性，并将性能投射到未来的架构中？ 最后，结合起来：如何为更大的互联生态系统（而不仅仅是单个软件和硬件组件）回答所有这些问题，并最终构建出可复制和可验证的未来一代系统？ScaleStuds项目涉及一个由十名研究人员组成的团队，旨在开发大规模系统的正确性可检查性（CC）和性能可预测性（PP）的基础。这个项目的关键原则是“以大查大”--用大量的数据、分析、测试、学习、模型和证明来检查大规模系统。 我们的愿景是建立一个分布式的“CC+ PP认证”的软件-软件和硬件交互的生态系统。 这个项目是一次铺一层“地板”，创造可组合的积木（“立柱”）。 该项目首先建立了新的机制，例如规模测试平台和软件程序属性和硬件性能配置文件的统一数据库，从而公开明确的API。 然后，这些研究能够在软件/硬件堆栈的各个级别上进行多维自动可扩展性测试和程序分析以及性能学习和预测。 最终，所有这些经验都旨在导致正确和高性能的跨层/服务交互和未来的设计原则，包括可复制和可验证的施工开发方法。 该项目的创新包括调试、测试、学习和预测方法的进步，以确保经典硬件平台和新兴平台上的极端规模系统和应用程序的正确性可检查性和性能可预测性;软件/硬件属性和配置文件的统一数据生态系统，通过清晰的API促进自动化分析;一个多维规模测试框架，使新的大规模单元测试和程序分析的发展;详细的设备分析和观察，以实现大规模的性能学习/预测，并提供学习/预测端到端硬件/软件栈中的其他设备和层的行为;并最终明确定义CC+ PP认证，适用于当今的系统和未来的可验证/可重现系统，该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准。

项目成果

Generating Test Databases for Database-Backed Applications

为数据库支持的应用程序生成测试数据库

• DOI: 10.1109/icse48619.2023.00173
• 发表时间: 2023
• 期刊: 45th International Conference on Software Engineering (ICSE
• 作者: Yan, Cong;Nath, Suman;Lu, Shan
• 通讯作者: Lu, Shan

HotGPT: How to Make Software Documentation More Useful with a Large Language Model?

• DOI: 10.1145/3593856.3595910
• 发表时间: 2023-06
• 期刊: Proceedings of the 19th Workshop on Hot Topics in Operating Systems
• 作者: Yi-An Su;Chengcheng Wan;Utsav Sethi;Shan Lu;M. Musuvathi;Suman Nath

GOAL: Supporting General and Dynamic Adaptation in Computing Systems

• DOI: 10.1145/3563835.3567655
• 发表时间: 2022-11
• 期刊: Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
• 作者: Ahsan Pervaiz;Yao-Hsiang Yang;Adam Duracz;F. Bartha;R. Sai;Connor Imes;Robert Cartwright;K. Palem;Shan Lu;Henry Hoffmann

Towards Continually Learning Application Performance Models

• DOI: 10.48550/arxiv.2310.16996
• 发表时间: 2023-10
• 期刊: ArXiv
• 作者: Ray A. O. Sinurat

Cancellation in Systems: An Empirical Study of Task Cancellation Patterns and Failures

系统中的取消：任务取消模式和失败的实证研究

• 发表时间: 2022
• 期刊: Proceedings of the 16th USENIX Symposium on Operating Systems
• 作者: Sethi, Utsav;Pan, Haochen;Lu, Shan;Musuvathi, Madanlal;Nath, Suman
• 通讯作者: Nath, Suman