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

Displayed 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
25m
Research 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
25m
Research 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
25m
Research paper
Theory and Practice of Coroutines with Snapshots
ECOOP Research Papers
Aleksandar Prokopec Oracle Labs, Fengyun Liu EPFL, Switzerland
DOI
12:15
25m
Research 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