Logical errors in the input/output subsystems of modern operating systems
Abstract
Modern operating systems use abstraction layers to describe data input/output interfaces. Operating systems based on these principles conform to the POSIX standard, which describes syntax and semantics of system calls. However, use of standards alone does not guarantee the consistency of used software components and correctness of designed algorithms. This article describes several logical errors which are typical for complex systems, different parts of which were developed independently of each other. An analysis of the described errors allows us to state that definition of the detailed models for software components and their subsequent formal verification and application for code testing can significantly improve robustness of the created operating systems and applications.
About the Authors
A. B. BetelinRussian Federation
A. A. Prilipko
Russian Federation
G. A. Prilipko
Russian Federation
S. G. Romanyuk
Russian Federation
D. V. Samborskiy
Russian Federation
References
1. Стандарт POSIX.1-2017. The Open Group Base Specifications Issue 7, 2018 edition IEEE Std 1003.1-2017.
2. Gregg, Brendan. Linux Systems Performance. Portland, OR: USENIX Association, 2019.
3. Сайт "A journal for MD/RAID5", https://lwn.net/Articles/665299
4. Сайт "Partial Parity Log for MD RAID 5", https://lwn.net/Articles/715280
5. J. Gray, et al. The transaction concept: Virtues and limitations, VLDB. – 1981. – Т. 81. – С. 144-154.
6. Сайт "Add 'failfast' support for raid1/raid10", https://lwn.net/Articles/706865
7. Сайт "Timeout Mismatch", https://raid.wiki.kernel.org/index.php/Timeout_Mismatch
8. Сайт "Many (long) HDD default timeouts cause data loss or corruption (silent controller resets)", https://www.smartmontools.org/ticket/658
9. Сайт "PostgreSQL's handling of fsync() errors is unsafe and risks data loss at least on XFS", https://lwn.net/Articles/752093
10. Сайт «Руководство PostgreSQL. Часть III. Администрирование сервера. Глава 29. Надёжность и журнал предзаписи», https://postgrespro.ru/docs/postgresql/13/wal-reliability
11. Klein, Gerwin, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (TOCS) 32, no. 1 (2014): 1-70.
Review
For citations:
Betelin A.B., Prilipko A.A., Prilipko G.A., Romanyuk S.G., Samborskiy D.V. Logical errors in the input/output subsystems of modern operating systems. МАТЕМАТИЧЕСКОЕ И КОМПЬЮТЕРНОЕ МОДЕЛИРОВАНИЕ СЛОЖНЫХ СИСТЕМ: ТЕОРЕТИЧЕСКИЕ И ПРИКЛАДНЫЕ АСПЕКТЫ. 2022;12(4):50-55. (In Russ.)