A type system for finding upper resource bounds of multi-threaded programs with nested transactions

We present a static, compositional analysis based on a type and effect system to estimate an upper bound for the resource consumption of nested and multi-threaded transactional programs. This work extends our previous type system for Transactional Featherweight Java to allow more liberal use of transactions in the semantics. The new types are also more expressive and structurally simpler using a linear representation instead of a tree representation for capturing static approximation of resource consumption. We prove the soundness of our analysis.