{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T03:28:27Z","timestamp":1783740507545,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":83,"publisher":"ACM","funder":[{"name":"Microsoft Accelerate Foundation Models Research (AFMR) grant program"},{"name":"NSF CAREER Award","award":["2237295"],"award-info":[{"award-number":["2237295"]}]},{"name":"NSF grants","award":["CNS-2317698"],"award-info":[{"award-number":["CNS-2317698"]}]},{"name":"NSF grants","award":["CNS-2317751"],"award-info":[{"award-number":["CNS-2317751"]}]},{"name":"NSF grants","award":["CCF-2318937"],"award-info":[{"award-number":["CCF-2318937"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3731569.3764850","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:43:24Z","timestamp":1759322604000},"page":"237-253","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["TrainVerify: Equivalence-Based Verification for Distributed LLM Training"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0004-6360-7392","authenticated-orcid":false,"given":"Yunchi","family":"Lu","sequence":"first","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2395-9965","authenticated-orcid":false,"given":"Youshan","family":"Miao","sequence":"additional","affiliation":[{"name":"Microsoft Research, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1420-5125","authenticated-orcid":false,"given":"Cheng","family":"Tan","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6315-0848","authenticated-orcid":false,"given":"Peng","family":"Huang","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7755-6624","authenticated-orcid":false,"given":"Yi","family":"Zhu","sequence":"additional","affiliation":[{"name":"Microsoft Research, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4875-2132","authenticated-orcid":false,"given":"Xian","family":"Zhang","sequence":"additional","affiliation":[{"name":"Microsoft Research, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0378-060X","authenticated-orcid":false,"given":"Fan","family":"Yang","sequence":"additional","affiliation":[{"name":"Microsoft Research, Beijing, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,12]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"CUDA. https:\/\/docs.nvidia.com\/cuda\/."},{"key":"e_1_3_2_2_2_1","unstructured":"CUTLASS: CUDA Templates for Linear Algebra Subroutines. https:\/\/github.com\/NVIDIA\/cutlass."},{"key":"e_1_3_2_2_3_1","unstructured":"DeepSpeed: fix bug where ZeRO2 never uses the reduce method. https:\/\/github.com\/microsoft\/DeepSpeed\/commit\/a85b6e472534d2e0b61fe234fae4f6a2332c95bf."},{"key":"e_1_3_2_2_4_1","unstructured":"DeepSpeed: fix EP grad_scale\/grad_norm fix. https:\/\/github.com\/microsoft\/DeepSpeed\/commit\/e5dd5501c10227ae33dce7d5bdd897741dd3adb7."},{"key":"e_1_3_2_2_5_1","unstructured":"DeepSpeed: partition balanced return wrong result. https:\/\/github.com\/deepspeedai\/DeepSpeed\/commit\/2bdf061f4dc8be70878f032d2e48d2130514f991."},{"key":"e_1_3_2_2_6_1","unstructured":"Distributed Data Parallelism. https:\/\/pytorch.org\/docs\/stable\/notes\/ddp.html."},{"key":"e_1_3_2_2_7_1","unstructured":"A gentle introduction to torch.autograd. https:\/\/pytorch.org\/tutorials\/beginner\/blitz\/autograd_tutorial.html#computational-graph."},{"key":"e_1_3_2_2_8_1","unstructured":"Llama3: Model Details. https:\/\/github.com\/meta-llama\/llama3\/blob\/main\/MODEL_CARD.md."},{"key":"e_1_3_2_2_9_1","unstructured":"Megatron Core. https:\/\/developer.nvidia.com\/megatron-core."},{"key":"e_1_3_2_2_10_1","unstructured":"Megatron: fix cross entropy loss averaging. https:\/\/github.com\/NVIDIA\/Megatron-LM\/commit\/adfa873d965b240962be6539cb5d387c508416b9."},{"key":"e_1_3_2_2_11_1","unstructured":"Megatron: fix distopt allgathers with interleaved pipeline parallelism. https:\/\/github.com\/NVIDIA\/Megatron-LM\/commit\/32bbb76d5767fdbf8dc60d4ef07d103cef8aca02."},{"key":"e_1_3_2_2_12_1","unstructured":"Megatron: fix get_data_parallel_sre_rank. https:\/\/github.com\/NVIDIA\/Megatron-LM\/commit\/9ad1944db1f97000377dc5aee36dcd656b1ae4a2."},{"key":"e_1_3_2_2_13_1","unstructured":"Megatron: fix interleaved schedule with sequence-parallel and overlap-p2p-comm. https:\/\/github.com\/NVIDIA\/Megatron-LM\/commit\/6bd74b0e84577317c06c303f4dae26d249ab55d1#diff-c27f9f2765a43b5c781756ce9fe4b9abcc3618ec96157f5dc67c4a00a7900b73R777."},{"key":"e_1_3_2_2_14_1","unstructured":"Megatron: fix no-interleave pipeline schedule. https:\/\/github.com\/NVIDIA\/Megatron-LM\/commit\/1f387c2cbdb4ce93f0c885862d570efb66dca4a4."},{"key":"e_1_3_2_2_15_1","unstructured":"Megatron: fix scaling down expert grads. https:\/\/github.com\/NVIDIA\/Megatron-LM\/commit\/3373641ff1093073181e219265e8c8ee58d8587c."},{"key":"e_1_3_2_2_16_1","unstructured":"Megatron: fix tiling use correct input size for splits. https:\/\/github.com\/microsoft\/DeepSpeed\/commit\/c543a41b154a991d50cb6cc8c07dbf46b0d2bdf6."},{"key":"e_1_3_2_2_17_1","unstructured":"Megatron issue: Incorrect loss scaling in context parallel code logic. https:\/\/github.com\/NVIDIA\/Megatron-LM\/issues\/673."},{"key":"e_1_3_2_2_18_1","unstructured":"Megatron: LinearWithFrozenWeight backward fix when TP > 1. https:\/\/github.com\/NVIDIA\/Megatron-LM\/commit\/5fffdfc737f14297bc3781dfc9e273199d1df52e."},{"key":"e_1_3_2_2_19_1","unstructured":"Megatron: MoE distributed setup invokes unnecessary all-reduce. https:\/\/github.com\/deepspeedai\/DeepSpeed\/issues\/6714."},{"key":"e_1_3_2_2_20_1","unstructured":"NumPy. https:\/\/numpy.org\/."},{"key":"e_1_3_2_2_21_1","unstructured":"NVIDIA collective communications library. https:\/\/developer.nvidia.com\/nccl."},{"key":"e_1_3_2_2_22_1","unstructured":"PyTorch: Loss Functions. https:\/\/pytorch.org\/docs\/stable\/nn.html#loss-functions."},{"key":"e_1_3_2_2_23_1","unstructured":"StableHLO. https:\/\/github.com\/openxla\/stablehlo."},{"key":"e_1_3_2_2_24_1","unstructured":"Z3 Tactic Online Guide. https:\/\/microsoft.github.io\/z3guide\/docs\/strategies\/tactics\/."},{"key":"e_1_3_2_2_25_1","first-page":"283","volume-title":"Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI '16","author":"Abadi Mart\u00edn","year":"2016","unstructured":"Mart\u00edn Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Geoffrey Irving, Michael Isard, Manjunath Kudlur, Josh Levenberg, Rajat Monga, Sherry Moore, Derek G. Murray, Benoit Steiner, Paul Tucker, Vijay Vasudevan, Pete Warden, Martin Wicke, Yuan Yu, and Xiaoqiang Zheng. TensorFlow: A system for large-scale machine learning. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, OSDI '16, page 265\u2013283, Savannah, GA, USA, 2016. USENIX Association."},{"key":"e_1_3_2_2_26_1","volume-title":"Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. GPT-4 technical report. arXiv preprint arXiv:2303.08774","author":"Achiam Josh","year":"2023","unstructured":"Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, et al. GPT-4 technical report. arXiv preprint arXiv:2303.08774, 2023."},{"key":"e_1_3_2_2_27_1","volume-title":"et al. Gemini: A family of highly capable multimodal models. arXiv preprint arXiv:2312.11805, 1","author":"Anil Rohan","year":"2023","unstructured":"Rohan Anil, Sebastian Borgeaud, Yonghui Wu, Jean-Baptiste Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M Dai, Anja Hauth, Katie Millican, et al. Gemini: A family of highly capable multimodal models. arXiv preprint arXiv:2312.11805, 1, 2023."},{"key":"e_1_3_2_2_28_1","volume-title":"Proc. ACM Program. Lang., 9(POPL)","author":"Arora Jai","year":"2025","unstructured":"Jai Arora, Sirui Lu, Devansh Jain, Tianfan Xu, Farzin Houshmand, Phitchaya Mangpo Phothilimthana, Mohsen Lesani, Praveen Narayanan, Karthik Srinivasa Murthy, Rastislav Bodik, Amit Sabne, and Charith Mendis. TensorRight: Automated verification of tensor graph rewrites. Proc. ACM Program. Lang., 9(POPL), January 2025. 10.1145\/3704865"},{"key":"e_1_3_2_2_29_1","first-page":"132","volume-title":"Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12","author":"Betts Adam","year":"2012","unstructured":"Adam Betts, Nathan Chong, Alastair Donaldson, Shaz Qadeer, and Paul Thomson. GPUVerify: a verifier for GPU kernels. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '12, page 113\u2013132, Tucson, Arizona, USA, 2012. Association for Computing Machinery. 10.1145\/2384616.2384625"},{"key":"e_1_3_2_2_30_1","volume-title":"Maximizing parallelism in distributed training for huge neural networks. arXiv preprint arXiv:2105.14450","author":"Bian Zhengda","year":"2021","unstructured":"Zhengda Bian, Qifan Xu, Boxiang Wang, and Yang You. Maximizing parallelism in distributed training for huge neural networks. arXiv preprint arXiv:2105.14450, 2021."},{"key":"e_1_3_2_2_31_1","first-page":"1901","volume-title":"Advances in Neural Information Processing Systems","author":"Brown Tom","unstructured":"Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 1877\u20131901. Curran Associates, Inc., 2020."},{"key":"e_1_3_2_2_32_1","first-page":"594","volume-title":"Proceedings of the 13th USENIX Conference on Operating Systems Design and Implementation, OSDI '18","author":"Chen Tianqi","year":"2018","unstructured":"Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Meghan Cowan, Haichen Shen, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. TVM: An automated end-to-end optimizing compiler for deep learning. In Proceedings of the 13th USENIX Conference on Operating Systems Design and Implementation, OSDI '18, page 579\u2013594, Carlsbad, CA, USA, 2018. USENIX Association."},{"key":"e_1_3_2_2_33_1","unstructured":"CoreWeave. Weights & Biases. https:\/\/wandb.ai\/site\/."},{"key":"e_1_3_2_2_34_1","volume-title":"The rising costs of training frontier AI models. arXiv preprint arXiv:2405.21015","author":"Cottier Ben","year":"2024","unstructured":"Ben Cottier, Robi Rahman, Loredana Fattorini, Nestor Maslej, Tamay Besiroglu, and David Owen. The rising costs of training frontier AI models. arXiv preprint arXiv:2405.21015, 2024."},{"key":"e_1_3_2_2_35_1","first-page":"340","volume-title":"Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08\/ETAPS'08","author":"Moura Leonardo De","year":"2008","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'08\/ETAPS'08, page 337\u2013340, Budapest, Hungary, 2008. Springer-Verlag."},{"key":"e_1_3_2_2_36_1","volume-title":"DeepSeek-V3 technical report","author":"Aixin Liu AI","year":"2025","unstructured":"DeepSeek-AI, Aixin Liu, Bei Feng, Bing Xue, Bochao Wu, et al. DeepSeek-V3 technical report, 2025. arXiv:2412.19437 [cs.CL] https:\/\/arxiv.org\/abs\/2412.19437."},{"key":"e_1_3_2_2_37_1","first-page":"12","volume-title":"2018 4th International Conference on Green Technology and Sustainable Development (GTSD)","author":"Do Truong-Dong","year":"2018","unstructured":"Truong-Dong Do, Minh-Thien Duong, Quoc-Vu Dang, and My-Ha Le. Real-time self-driving car navigation using deep neural network. In 2018 4th International Conference on Green Technology and Sustainable Development (GTSD), pages 7\u201312, 2018."},{"key":"e_1_3_2_2_38_1","volume-title":"The Llama 3 herd of models. arXiv preprint arXiv:2407.21783","author":"Dubey Abhimanyu","year":"2024","unstructured":"Abhimanyu Dubey, Abhinav Jauhri, Abhinav Pandey, Abhishek Kadian, Ahmad Al-Dahle, Aiesha Letman, Akhil Mathur, Alan Schelten, Amy Yang, Angela Fan, et al. The Llama 3 herd of models. arXiv preprint arXiv:2407.21783, 2024."},{"key":"e_1_3_2_2_39_1","volume-title":"On neural network equivalence checking using SMT solvers","author":"Eleftheriadis Charis","year":"2022","unstructured":"Charis Eleftheriadis, Nikolaos Kekatos, Panagiotis Katsaros, and Stavros Tripakis. On neural network equivalence checking using SMT solvers, 2022. arXiv:2203.11629 [cs.AI] https:\/\/arxiv.org\/abs\/2203.11629."},{"key":"e_1_3_2_2_40_1","first-page":"38","volume-title":"Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering, FSE Companion '25","author":"Gao Yanjie","year":"2025","unstructured":"Yanjie Gao, Jiyu Luo, Haoxiang Lin, Hongyu Zhang, Ming Wu, and Mao Yang. dl2: Detecting communication deadlocks in deep learning jobs. In Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering, FSE Companion '25, page 27\u201338, Clarion Hotel Trondheim, Trondheim, Norway, 2025. Association for Computing Machinery. 10.1145\/3696630.3728529"},{"key":"e_1_3_2_2_41_1","first-page":"112","volume-title":"H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc","author":"Huang Yanping","unstructured":"Yanping Huang, Youlong Cheng, Ankur Bapna, Orhan Firat, Dehao Chen, Mia Chen, HyoukJoong Lee, Jiquan Ngiam, Quoc V Le, Yonghui Wu, and zhifeng Chen. GPipe: Efficient training of giant neural networks using pipeline parallelism. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alch\u00e9-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32, pages 103\u2013112. Curran Associates, Inc., 2019."},{"key":"e_1_3_2_2_42_1","first-page":"395","volume-title":"Proceedings of the 29th Symposium on Operating Systems Principles, SOSP '23","author":"Jang Insu","year":"2023","unstructured":"Insu Jang, Zhenning Yang, Zhen Zhang, Xin Jin, and Mosharaf Chowdhury. Oobleck: Resilient distributed training of large models using pipeline templates. In Proceedings of the 29th Symposium on Operating Systems Principles, SOSP '23, page 382\u2013395, Koblenz, Germany, 2023. Association for Computing Machinery. 10.1145\/3600006.3613152"},{"key":"e_1_3_2_2_43_1","first-page":"62","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19","author":"Jia Zhihao","year":"2019","unstructured":"Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia, and Alex Aiken. TASO: Optimizing deep learning computation with automatic generation of graph substitutions. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19, page 47\u201362, Huntsville, Ontario, Canada, 2019. Association for Computing Machinery. 10.1145\/3341301.3359630"},{"key":"e_1_3_2_2_44_1","volume-title":"Proceedings of the 19th USENIX Symposium on Operating Systems Design and Implementation, OSDI '25","author":"Jiang Yuxuan","year":"2025","unstructured":"Yuxuan Jiang, Ziming Zhou, Boyu Xu, Beijie Liu, Runhui Xu, and Peng Huang. Training with Confidence: Catching silent errors in deep learning training with automated proactive checks. In Proceedings of the 19th USENIX Symposium on Operating Systems Design and Implementation, OSDI '25, Boston, MA, USA, July 2025. USENIX Association."},{"issue":"7873","key":"e_1_3_2_2_45_1","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1038\/s41586-021-03819-2","article-title":"Highly accurate protein structure prediction with AlphaFold","volume":"596","author":"Jumper John","year":"2021","unstructured":"John Jumper, Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnov, Olaf Ronneberger, Kathryn Tunyasuvunakool, Russ Bates, Augustin \u017d\u00eddek, Anna Potapenko, et al. Highly accurate protein structure prediction with AlphaFold. Nature, 596(7873):583\u2013589, 2021.","journal-title":"Nature"},{"key":"e_1_3_2_2_46_1","volume-title":"Scaling laws for neural language models. arXiv preprint arXiv:2001.08361","author":"Kaplan Jared","year":"2020","unstructured":"Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei. Scaling laws for neural language models. arXiv preprint arXiv:2001.08361, 2020."},{"key":"e_1_3_2_2_47_1","first-page":"117","volume-title":"Computer Aided Verification","author":"Katz Guy","year":"2017","unstructured":"Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kun\u010dak, editors, Computer Aided Verification, pages 97\u2013117, Cham, 2017. Springer International Publishing."},{"key":"e_1_3_2_2_48_1","first-page":"353","volume-title":"Proceedings of Machine Learning and Systems","volume":"5","author":"Korthikanti Vijay Anand","unstructured":"Vijay Anand Korthikanti, Jared Casper, Sangkug Lym, Lawrence McAfee, Michael Andersch, Mohammad Shoeybi, and Bryan Catanzaro. Reducing activation recomputation in large transformer models. In D. Song, M. Carbin, and T. Chen, editors, Proceedings of Machine Learning and Systems, volume 5, pages 341\u2013353. Curan, 2023."},{"key":"e_1_3_2_2_49_1","first-page":"14","volume-title":"Proceedings of the 2021 IEEE\/ACM International Symposium on Code Generation and Optimization, CGO '21","author":"Lattner Chris","unstructured":"Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. MLIR: Scaling compiler infrastructure for domain specific computation. In Proceedings of the 2021 IEEE\/ACM International Symposium on Code Generation and Optimization, CGO '21, page 2\u201314. IEEE Press, 2021. 10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_2_2_50_1","first-page":"224","volume-title":"Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '12","author":"Li Guodong","year":"2012","unstructured":"Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, and Sreeranga P. Rajan. GKLEE: Concolic verification and test generation for GPUs. In Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '12, page 215\u2013224, New Orleans, Louisiana, USA, 2012. Association for Computing Machinery. 10.1145\/2145816.2145844"},{"key":"e_1_3_2_2_51_1","volume-title":"Sequence parallelism: Making 4d parallelism possible. arXiv preprint arXiv:2105.13120","author":"Li Shenggui","year":"2021","unstructured":"Shenggui Li, Fuzhao Xue, Yongbin Li, and Yang You. Sequence parallelism: Making 4d parallelism possible. arXiv preprint arXiv:2105.13120, 2021."},{"key":"e_1_3_2_2_52_1","first-page":"363","volume-title":"18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24)","author":"Lin Zhiqi","year":"2024","unstructured":"Zhiqi Lin, Youshan Miao, Quanlu Zhang, Fan Yang, Yi Zhu, Cheng Li, Saeed Maleki, Xu Cao, Ning Shang, Yilei Yang, Weijiang Xu, Mao Yang, Lintao Zhang, and Lidong Zhou. nnScaler: Constraint-guided parallelization plan generation for deep learning training. In 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 24), pages 347\u2013363, Santa Clara, CA, July 2024. USENIX Association. https:\/\/www.usenix.org\/conference\/osdi24\/presentation\/lin-zhiqi."},{"key":"e_1_3_2_2_53_1","volume-title":"Algorithms for verifying deep neural networks. arXiv:1903.06758","author":"Liu Changliu","year":"2019","unstructured":"Changliu Liu, Tomer Arnon, Christopher Lazarus, Clark Barrett, and Mykel J. Kochenderfer. Algorithms for verifying deep neural networks. arXiv:1903.06758, 2019."},{"key":"e_1_3_2_2_54_1","first-page":"181","volume-title":"Proceedings of the Nineteenth European Conference on Computer Systems, EuroSys '24","author":"Liu Guodong","year":"2024","unstructured":"Guodong Liu, Youshan Miao, Zhiqi Lin, Xiaoxiang Shi, Saeed Maleki, Fan Yang, Yungang Bao, and Sa Wang. Aceso: Efficient parallel DNN training through iterative bottleneck alleviation. In Proceedings of the Nineteenth European Conference on Computer Systems, EuroSys '24, page 163\u2013181, Athens, Greece, 2024. Association for Computing Machinery. 10.1145\/3627703.3629554"},{"key":"e_1_3_2_2_55_1","volume-title":"Ring attention with blockwise transformers for near-infinite context. arXiv preprint arXiv:2310.01889","author":"Liu Hao","year":"2023","unstructured":"Hao Liu, Matei Zaharia, and Pieter Abbeel. Ring attention with blockwise transformers for near-infinite context. arXiv preprint arXiv:2310.01889, 2023."},{"key":"e_1_3_2_2_56_1","first-page":"543","volume-title":"Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","volume":"2","author":"Liu Jiawei","year":"2023","unstructured":"Jiawei Liu, Jinkun Lin, Fabian Ruffy, Cheng Tan, Jinyang Li, Aurojit Panda, and Lingming Zhang. NNSmith: Generating diverse and valid test cases for deep learning compilers. In Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, ASPLOS 2023, page 530\u2013543, Vancouver, BC, Canada, 2023. Association for Computing Machinery. 10.1145\/3575693.3575707"},{"key":"e_1_3_2_2_57_1","first-page":"177","volume-title":"Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP '24","author":"Liu Siran","year":"2024","unstructured":"Siran Liu, Chengxiang Qi, Ying Cao, Chao Yang, Weifang Hu, Xuanhua Shi, Fan Yang, and Mao Yang. Uncovering nested data parallelism and data reuse in DNN computation with FractalTensor. In Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles, SOSP '24, page 160\u2013177, Austin, TX, USA, 2024. Association for Computing Machinery. 10.1145\/3694715.3695961"},{"issue":"1","key":"e_1_3_2_2_58_1","first-page":"100","article-title":"Differential testing for software","volume":"10","author":"McKeeman William M","year":"1998","unstructured":"William M McKeeman. Differential testing for software. Digital Technical Journal, 10(1):100\u2013107, 1998.","journal-title":"Digital Technical Journal"},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.103"},{"key":"e_1_3_2_2_60_1","first-page":"364","volume-title":"Proceedings of the 45th International Conference on Software Engineering: Companion Proceedings, ICSE '23","author":"Munakata Satoshi","unstructured":"Satoshi Munakata, Susumu Tokumoto, Koji Yamamoto, and Kazuki Munakata. Towards formal repair and verification of industry-scale deep neural networks. In Proceedings of the 45th International Conference on Software Engineering: Companion Proceedings, ICSE '23, page 360\u2013364. IEEE Press, 2023. 10.1109\/ICSE-Companion58688.2023.00103"},{"key":"e_1_3_2_2_61_1","first-page":"15","volume-title":"Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19","author":"Narayanan Deepak","year":"2019","unstructured":"Deepak Narayanan, Aaron Harlap, Amar Phanishayee, Vivek Seshadri, Nikhil R. Devanur, Gregory R. Ganger, Phillip B. Gibbons, and Matei Zaharia. PipeDream: Generalized pipeline parallelism for DNN training. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP '19, page 1\u201315, Huntsville, Ontario, Canada, 2019. Association for Computing Machinery. 10.1145\/3341301.3359646"},{"key":"e_1_3_2_2_62_1","volume-title":"Automatic differentiation in PyTorch","author":"Paszke Adam","year":"2017","unstructured":"Adam Paszke, Sam Gross, Soumith Chintala, Gregory Chanan, Edward Yang, Zachary DeVito, Zeming Lin, Alban Desmaison, Luca Antiga, and Adam Lerer. Automatic differentiation in PyTorch. 2017."},{"key":"e_1_3_2_2_63_1","unstructured":"PyTorch Team. PyTorch. https:\/\/pytorch.org\/."},{"key":"e_1_3_2_2_64_1","series-title":"Proceedings of Machine Learning Research","first-page":"18346","volume-title":"Ammar Ahmad Awan, Jeff Rasley, and Yuxiong He. DeepSpeed-MoE: Advancing mixture-of-experts inference and training to power next-generation AI scale. In Kamalika Chaudhuri","author":"Rajbhandari Samyam","unstructured":"Samyam Rajbhandari, Conglong Li, Zhewei Yao, Minjia Zhang, Reza Yazdani Aminabadi, Ammar Ahmad Awan, Jeff Rasley, and Yuxiong He. DeepSpeed-MoE: Advancing mixture-of-experts inference and training to power next-generation AI scale. In Kamalika Chaudhuri, Stefanie Jegelka, Le Song, Csaba Szepesvari, Gang Niu, and Sivan Sabato, editors, Proceedings of the 39th International Conference on Machine Learning, volume 162 of Proceedings of Machine Learning Research, pages 18332\u201318346. PMLR, 17\u201323 Jul 2022. https:\/\/proceedings.mlr.press\/v162\/rajbhandari22a.html."},{"key":"e_1_3_2_2_65_1","volume-title":"Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC '20","author":"Rajbhandari Samyam","unstructured":"Samyam Rajbhandari, Jeff Rasley, Olatunji Ruwase, and Yuxiong He. ZeRO: Memory optimizations toward training trillion parameter models. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC '20. IEEE Press."},{"key":"e_1_3_2_2_66_1","first-page":"3506","volume-title":"Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, KDD '20","author":"Rasley Jeff","year":"2020","unstructured":"Jeff Rasley, Samyam Rajbhandari, Olatunji Ruwase, and Yuxiong He. DeepSpeed: System optimizations enable training deep learning models with over 100 billion parameters. In Proceedings of the 26th ACM SIGKDD International Conference on Knowledge Discovery & Data Mining, KDD '20, page 3505\u20133506, Virtual Event, CA, USA, 2020. Association for Computing Machinery. 10.1145\/3394486.3406703"},{"key":"e_1_3_2_2_67_1","volume-title":"Megatron-LM: Training multibillion parameter language models using GPU model parallelism. arXiv preprint arXiv:1909.08053","author":"Shoeybi Mohammad","year":"2019","unstructured":"Mohammad Shoeybi, Mostofa Patwary, Raul Puri, Patrick LeGresley, Jared Casper, and Bryan Catanzaro. Megatron-LM: Training multibillion parameter language models using GPU model parallelism. arXiv preprint arXiv:1909.08053, 2019."},{"key":"e_1_3_2_2_68_1","volume-title":"DeepID3: Face recognition with very deep neural networks","author":"Sun Yi","year":"2015","unstructured":"Yi Sun, Ding Liang, Xiaogang Wang, and Xiaoou Tang. DeepID3: Face recognition with very deep neural networks, 2015. arXiv:1502.00873 [cs.CV] https:\/\/arxiv.org\/abs\/1502.00873."},{"key":"e_1_3_2_2_69_1","first-page":"142","volume-title":"Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA '10","author":"Tang Enyi","year":"2010","unstructured":"Enyi Tang, Earl Barr, Xuandong Li, and Zhendong Su. Perturbing numerical calculations for statistical analysis of floating-point program (in)stability. In Proceedings of the 19th International Symposium on Software Testing and Analysis, ISSTA '10, page 131\u2013142, Trento, Italy, 2010. Association for Computing Machinery. 10.1145\/1831708.1831724"},{"key":"e_1_3_2_2_70_1","unstructured":"PyTorch Team. PyTorch DistributedTensor (DTensor). https:\/\/github.com\/pytorch\/pytorch\/tree\/master\/torch\/distributed\/_tensor."},{"key":"e_1_3_2_2_71_1","unstructured":"PyTorch Team. TorchFX. https:\/\/pytorch.org\/docs\/stable\/fx.html."},{"key":"e_1_3_2_2_72_1","unstructured":"PyTorch Team. TorchScript. https:\/\/pytorch.org\/docs\/stable\/jit.html."},{"key":"e_1_3_2_2_73_1","volume-title":"Revisiting differential verification: Equivalence verification with confidence. arXiv preprint arXiv:2410.20207","author":"Teuber Samuel","year":"2024","unstructured":"Samuel Teuber, Philipp Kern, Marvin Janzen, and Bernhard Beckert. Revisiting differential verification: Equivalence verification with confidence. arXiv preprint arXiv:2410.20207, 2024."},{"key":"e_1_3_2_2_74_1","volume-title":"Llama 2: Open foundation and fine-tuned chat models. arXiv preprint arXiv:2307.09288","author":"Touvron Hugo","year":"2023","unstructured":"Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, et al. Llama 2: Open foundation and fine-tuned chat models. arXiv preprint arXiv:2307.09288, 2023."},{"key":"e_1_3_2_2_75_1","volume-title":"Advances in Neural Information Processing Systems","author":"Vaswani Ashish","unstructured":"Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, \u0141 ukasz Kaiser, and Illia Polosukhin. Attention is all you need. In I. Guyon, U. Von Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 30. Curran Associates, Inc."},{"key":"e_1_3_2_2_76_1","first-page":"54","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Wang Haojie","unstructured":"Haojie Wang, Jidong Zhai, Mingyu Gao, Zixuan Ma, Shizhi Tang, Liyan Zheng, Yuanzhi Li, Kaiyuan Rong, Yuanyong Chen, and Zhihao Jia. PET: Optimizing tensor programs with partially equivalent transformations and automated corrections. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21), pages 37\u201354. USENIX Association, July 2021. https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/wang."},{"key":"e_1_3_2_2_77_1","volume-title":"Proceedings of the 35th International Conference on Neural Information Processing Systems, NIPS '21","author":"Wang Shiqi","year":"2021","unstructured":"Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In Proceedings of the 35th International Conference on Neural Information Processing Systems, NIPS '21, Red Hook, NY, USA, 2021. Curran Associates Inc."},{"key":"e_1_3_2_2_78_1","article-title":"Program slicing","volume":"352","author":"Weiser Mark","year":"1984","unstructured":"Mark Weiser. Program slicing. IEEE Transactions on software engineering, (4):352\u2013357, 1984.","journal-title":"IEEE Transactions on software engineering, (4)"},{"key":"e_1_3_2_2_79_1","volume-title":"Proceedings of the 2025 USENIX Annual Technical Conference (USENIX ATC). USENIX Association","author":"Xie Peichen","year":"2025","unstructured":"Peichen Xie, Yanjie Gao, Yang Wang, and Jilong Xue. Revealing floating-point accumulation orders in software\/hardware implementations. In Proceedings of the 2025 USENIX Annual Technical Conference (USENIX ATC). USENIX Association, 2025."},{"key":"e_1_3_2_2_80_1","unstructured":"XLA and TensorFlow teams. XLA\u2014TensorFlow compiled. https:\/\/developers.googleblog.com\/2017\/03\/xla-tensorflow-compiled.html."},{"key":"e_1_3_2_2_81_1","volume-title":"OneFlow: Redesign the distributed deep learning framework from scratch. arXiv preprint arXiv:2110.15032","author":"Yuan Jinhui","year":"2021","unstructured":"Jinhui Yuan, Xinqi Li, Cheng Cheng, Juncheng Liu, Ran Guo, Shenghang Cai, Chi Yao, Fei Yang, Xiaodong Yi, Chuan Wu, et al. OneFlow: Redesign the distributed deep learning framework from scratch. arXiv preprint arXiv:2110.15032, 2021."},{"key":"e_1_3_2_2_82_1","volume-title":"Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation, OSDI '20, USA","author":"Zheng Lianmin","year":"2020","unstructured":"Lianmin Zheng, Chengfan Jia, Minmin Sun, Zhao Wu, Cody Hao Yu, Ameer Haj-Ali, Yida Wang, Jun Yang, Danyang Zhuo, Koushik Sen, Joseph E. Gonzalez, and Ion Stoica. Ansor: Generating highperformance tensor programs for deep learning. In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation, OSDI '20, USA, 2020. USENIX Association."},{"key":"e_1_3_2_2_83_1","first-page":"578","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22)","author":"Zheng Lianmin","year":"2022","unstructured":"Lianmin Zheng, Zhuohan Li, Hao Zhang, Yonghao Zhuang, Zhifeng Chen, Yanping Huang, Yida Wang, Yuanzhong Xu, Danyang Zhuo, Eric P Xing, et al. Alpa: Automating inter- and intra-operator parallelism for distributed deep learning. In 16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pages 559\u2013578, Carlsbad, CA, July 2022. USENIX Association. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/zheng-lianmin."}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","location":"Lotte Hotel World Seoul Republic of Korea","acronym":"SOSP '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX"]},"container-title":["Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles"],"original-title":[],"deposited":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T12:50:01Z","timestamp":1759323001000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731569.3764850"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,12]]},"references-count":83,"alternative-id":["10.1145\/3731569.3764850","10.1145\/3731569"],"URL":"https:\/\/doi.org\/10.1145\/3731569.3764850","relation":{},"subject":[],"published":{"date-parts":[[2025,10,12]]},"assertion":[{"value":"2025-10-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}