2026-09-30T11:58:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:9209 2026-09-23T04:20:04Z ddc:004 open_access

A Concurrent Specification of POSIX File Systems Ntzik, Gian da Rocha Pinto, Pedro Sutherland, Julian Gardner, Philippa POSIX concurrency file systems refinement separation logic atomicity POSIX is a standard for operating systems, with a substantial part devoted to specifying file-system operations. File-system operations exhibit complex concurrent behaviour, comprising multiple actions affecting different parts of the state: typically, multiple atomic reads followed by an atomic update. However, the standard's description of concurrent behaviour is unsatisfactory: it is fragmented; contains ambiguities; and is generally under-specified. We provide a formal concurrent specification of POSIX file systems and demonstrate scalable reasoning for clients. Our specification is based on a concurrent specification language, which uses a modern concurrent separation logic for reasoning about abstract atomic operations, and an associated refinement calculus. Our reasoning about clients highlights an important difference between reasoning about modules built over a heap, where the interference on the shared state is restricted to the operations of the module, and modules built over a file system, where the interference cannot be restricted as the file system is a public namespace. We introduce specifications conditional on context invariants used to restrict the interference, and apply our reasoning to the example of lock files. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gian Ntzik and Pedro da Rocha Pinto and Julian Sutherland and Philippa Gardner 2018 Is Part Of LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2018.4 urn:nbn:de:0030-drops-92092 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.4 eng https://creativecommons.org/licenses/by/3.0/legalcode