ECOOP 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA 2018
Thu 19 Jul 2018 12:15 - 12:40 at Zurich II - Asynchrony and Concurrency Chair(s): Todd Millstein

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 Jul
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

ecoop-2018-papers
11:00 - 12:40: ECOOP Research Papers - Asynchrony and Concurrency at Zurich II
Chair(s): Todd MillsteinUniversity of California, Los Angeles
ecoop-2018-papers11:00 - 11:25
Research paper
Ragnar MogkTechnische Universität Darmstadt, Lars BaumgärtnerPhilipps-Universität Marburg, Guido SalvaneschiTU Darmstadt, Bernd FreislebenPhilipps-Universität Marburg, Mira MeziniTU Darmstadt
DOI
ecoop-2018-papers11:25 - 11:50
Research paper
Hiroaki InoueMitsubishi Electric Corporation, Japan, Tomoyuki AotaniTokyo Institute of Technology, Atsushi IgarashiKyoto University, Japan
DOI
ecoop-2018-papers11:50 - 12:15
Research paper
Aleksandar ProkopecOracle Labs, Fengyun LiuEPFL, Switzerland
DOI
ecoop-2018-papers12:15 - 12:40
Research paper
Gian NtzikImperial College London, Pedro da Rocha PintoImperial College London, Julian SutherlandImperial College London, Philippa GardnerImperial College London
DOI