Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Ntzik:2018,
author = {Ntzik, G and da, Rocha Pinto P and Sutherland, JHJ and Gardner, PA},
pages = {1--28},
publisher = {ECOOP},
title = {A concurrent specification of POSIX file systems},
url = {https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16077},
year = {2018}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Ntzik,G
AU  - da,Rocha Pinto P
AU  - Sutherland,JHJ
AU  - Gardner,PA
EP  - 28
PB  - ECOOP
PY  - 2018///
SP  - 1
TI  - A concurrent specification of POSIX file systems
UR  - https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16077
UR  - http://hdl.handle.net/10044/1/60704
ER  -
Download