A concurrent specification of POSIX file systems
File(s)Ntzik2018Concurrent.pdf (715.92 KB) Ntzik2018Concurrent-techical-report.pdf (631.75 KB)
Submitted version
Supporting information
Author(s)
Ntzik, G
Da Rocha Pinto, P
Sutherland, JHJ
Gardner, PA
Type
Conference Paper
Abstract
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 nsatisfactory: 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.
Date Issued
2018-07-21
Date Acceptance
2018-04-11
Publisher
ECOOP
Start Page
1
End Page
28
Journal / Book Title
32nd European Conference on Object-Oriented Programming (ECOOP 2018)
Volume
109
Issue
3
Copyright Statement
© Gian Ntzik, Pedro da Rocha Pinto, Julian Sutherland, and Philippa Gardner;
licensed under Creative Commons License (http://creativecommons.org/licenses/by/3.0/) CC-BY
32nd European Conference on Object-Oriented Programming (ECOOP 2018)
licensed under Creative Commons License (http://creativecommons.org/licenses/by/3.0/) CC-BY
32nd European Conference on Object-Oriented Programming (ECOOP 2018)
Source Database
manual-entry
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Identifier
https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16077
Grant Number
EP/K008528/1 - RG65358
EP/K008528/1
Source
32nd European Conference on Object-Oriented Programming (ECOOP 2018)
Publication Status
Published
Start Date
2018-07-19
Finish Date
2018-07-21
Country
Amsterdam, The Netherlands
Date Publish Online
2018-07-21