Type-theoretic Semantics for Transactional Concurrency

Abstract

We propose a dependent type theory that combines programming, specifications and reasoning about higher-order concurrent programs with shared higher-order transactional memory. We build on our previous work on Hoare Type Theory (HTT), which is extended here with types that correspond to Hoare-style specifications for transactions. The new types have the form CMD {I}{P} x:A{Q}, and classify concurrent programs that may execute in a shared state with invariant I, and local state precondition P. Upon termination, such programs return a result of type A, and local state changed according to the postcondition Q. Throughout the execution, shared state always satisfies the invariant I, except at specific critical sections which are executed atomically; that is, sequentially, without interference from other processes. Atomic sections may violate the invariant, but must restore it upon exit. We follow the idea of Separation Logic, and adopt “small footprint” specifications, whereby each process is associated with a precondition that tightly describes its state requirement. HTT is a program logic and a dependently typed programming language at the same time. To consider it as a logic, we prove that it is sound and compositional. To consider it as a programming language, we define its operational semantics, and show adequacy with respect to the specifications.