Reasoning about the POSIX File System: Local Update and Global Pathnames
We introduce a program logic for specifying a core sequential subset of the POSIX file system and for reasoning abstractly about client programs working with the file system. The challenge is to reason about the combination of local directory update and global pathname traversal (including '..' and symbolic links) which may overlap the directories being updated. Existing reasoning techniques are either based on first-order logic and do not scale, or on separation logic and can only handle linear pathnames (no '..' or symbolic links). We introduce fusion logic for reasoning about local update and global pathname traversal, introducing a novel effect frame rule to propagate the effect of a local update on overlapping pathnames. We apply our reasoning to the standard recursive remove utility (rm -r), discovering bugs in well-known implementations.
Wed 28 OctDisplayed time zone: Eastern Time (US & Canada) change
13:30 - 15:00 | |||
13:30 22mTalk | Conditionally Correct Superoptimization OOPSLA Rahul Sharma Stanford University, Eric Schkufza Stanford University, Berkeley Churchill Stanford University, Alex Aiken Stanford University DOI | ||
13:52 22mTalk | Selective Control-Flow Abstraction via Jumping OOPSLA Sam Blackshear University of Colorado at Boulder, USA, Bor-Yuh Evan Chang University of Colorado at Boulder, USA, Manu Sridharan Samsung Research America Link to publication | ||
14:15 22mTalk | Automating Grammar Comparison OOPSLA Ravichandhran Madhavan EPFL, Switzerland, Mikaël Mayer EPFL, Switzerland, Sumit Gulwani Microsoft Research, USA, Viktor Kunčak EPFL, Switzerland Link to publication | ||
14:37 22mTalk | Reasoning about the POSIX File System: Local Update and Global Pathnames OOPSLA DOI |