Serialisable multi-level transaction control: A specification and verification

We define a programming language independent controller TACTL for multi-level transactions and an operator TA, which when applied to concurrent programs with multi-level shared locations containing hierarchically structured complex values, turns their behavior with respect to some abstract termination criterion into a transactional behaviour. We prove the correctness property that concurrent runs under the transaction controller are serialisable, assuming an Inverse Operation Postulate to guarantee recoverability. For its applicability to a wide range of programs we specify the transaction controller TACTL and the operator TA in terms of Abstract State Machines (ASMs). This allows us to model concurrent updates at different levels of nested locations in a precise yet simple manner, namely in terms of partial ASM updates. It also provides the possibility to use the controller TACTL and the operator TA as a plug-in when specifying concurrent system components in terms of sequential ASMs.