Transactional Forest: A DSL for Managing Concurrent Filestores
Many systems use ad hoc collections of files and directories to store persistent data. For most consumers of this data, the process of properly parsing, using, and updating these filestores using standard APIs is cumbersome and error-prone. Making matters worse, many filestores are too big to fit in memory, so applications must process the data incrementally. They must also correctly manage concurrent accesses by multiple users. This paper presents the design of Transactional Forest (TxForest), which builds on earlier work on Forest and Incremental Forest to provide a simpler, more powerful API for managing filestores and which provides a mechanism for managing concurrent accesses using serializable transactions. Under the hood, TxForest uses Huet’s zippers to track the data associated with filestores and implements an optimistic concurrency control mechanism. We formalize TxForest in a core calculus, develop a formal proof of serializability, describe our OCaml prototype, and present several realistic applications, which serve as case studies.
Tue 3 DecDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
13:30 - 15:00
|Android Multitasking Mechanism: Formal Semantics and Static Analysis of Apps
Taolue Chen Birkbeck, University of London, Jilong He Institute of Software, Chinese Academy of Sciences, Yu-Ping Wang Tsinghua University, China, Zhilin Wu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Jun Yan Institute of Software, Chinese Academy of Sciences
|Conflict Abstractions and Shadow Speculation for Optimistic Transactional Objects
|Transactional Forest: A DSL for Managing Concurrent Filestores