ECOOP 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA
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

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