Isolation-only Transactions by Typing and Versioning
In this paper we design a language and runtime support for isolation-only, multithreaded transactions (called tasks) that are intended for time-critical systems. The key concept of our design is the use of a type system to support rollback-free and safe runtime execution of tasks. We present a first-order type system which can verify information for the concurrency controller. We use an operational semantics to formalize and prove the type soundness result and an isolation property of tasks. The semantics uses a specialized concurrency control algorithm, that is based on access versioning. We give proofs of type soundness and dynamic correctness of the concurrency control algorithm.