A Concurrent Specification of POSIX File Systems
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.
Thu 19 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:40 | Asynchrony and ConcurrencyECOOP Research Papers at Zurich II Chair(s): Todd Millstein University of California, Los Angeles | ||
11:00 25mResearch paper | Fault-tolerant Distributed Reactive Programming ECOOP Research Papers Ragnar Mogk Technische Universität Darmstadt, Lars Baumgärtner Philipps-Universität Marburg, Guido Salvaneschi TU Darmstadt, Bernd Freisleben Philipps-Universität Marburg, Mira Mezini TU Darmstadt DOI | ||
11:25 25mResearch paper | ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions ECOOP Research Papers Hiroaki Inoue Mitsubishi Electric Corporation, Japan, Tomoyuki Aotani Tokyo Institute of Technology, Atsushi Igarashi Kyoto University, Japan DOI | ||
11:50 25mResearch paper | Theory and Practice of Coroutines with Snapshots ECOOP Research Papers DOI | ||
12:15 25mResearch paper | A Concurrent Specification of POSIX File Systems ECOOP Research Papers Gian Ntzik Imperial College London, Pedro da Rocha Pinto Imperial College London, Julian Sutherland Imperial College London, Philippa Gardner Imperial College London DOI |