Fault-tolerant Resource Reasoning (Extended Version)
File(s)
Supporting information
Author(s)
Ntzik, G
da Rocha Pinto, P
Gardner, P
Type
Report
Abstract
Separation logic has been successful at verifying that programs do not crash due to illegal use of resources. The underlying assumption, however, is that machines do not fail. In practice, machines can fail unpredictably for various reasons, e.g. power loss, corrupting resources. Critical software, e.g. file systems, employ recovery methods to mitigate these effects. We introduce an extension of the Views framework to reason about such methods. We use concurrent separation logic as an instance of the framework to illustrate our reasoning, and explore programs using write-ahead logging, e.g. an ARIES recovery algorithm.
Date Issued
2015-09
Citation
2015
Publisher
Department of Computing, Imperial College London
Copyright Statement
© 2015 The Authors
Place of Publication
London, United Kingdom
Publication Status
Unpublished