VerifyIO: Verifying Adherence to Parallel I/O Consistency Semantics
- 3 June 2025
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 1-12
Abstract
High-performance computing (HPC) applications generate and consume substantial amounts of data, typically managed by parallel file systems. These applications access file systems either through the POSIX interface or by using highlevel I/O libraries. While the POSIX consistency model remains dominant in HPC, emerging file systems and popular I/O libraries increasingly adopt alternative consistency models that relax semantics in various ways, creating significant challenges for correctness and portability. This paper addresses these challenges by proposing a trace-driven I/O consistency verification workflow, implemented in our open-source tool, VerifyIO, which collects execution traces, detects data conflicts, and verifies proper synchronization against specified consistency models. Our extensive evaluation of 91 test case executions across three widely used I/O libraries with four I/O consistency models reveals critical consistency issues at both application and implementation levels.Keywords
This publication has 28 references indexed in Scilit:
- Reproducible execution of POSIX programs with DiOSSoftware and Systems Modeling, 2020
- Gfarm/BB — Gfarm File System for Node-Local Burst BufferJournal of Computer Science and Technology, 2020
- ECHOFS: A Scheduler-Guided Temporary Filesystem to Leverage Node-Local NVMS2018
- Toward Scalable and Asynchronous Object-Centric Data Management for HPC2018
- Modeling and Verifying Google File System2015
- Checking and Enforcing Robustness against TSO2013
- Runtime Verification of C Memory Safety2009
- POSIX and the Verification Grand Challenge: A Roadmap2008
- Overview of the MPI-IO Parallel I/O Interface1996
- NetCDF: an interface for scientific data accessIEEE Computer Graphics and Applications, 1990