# Serialisable Multi-Level Transaction Control: A Specification and Verification

## TL;DR

This paper introduces a language-independent transaction controller and operator for multi-level transactions, ensuring serializability and recoverability in concurrent programs with complex hierarchical data structures.

## Contribution

It defines TaCtl and $TA$ in terms of Abstract State Machines, enabling precise modeling of multi-level concurrent updates and integration into sequential ASM specifications.

## Key findings

- Proves correctness of serializability under the controller
- Models multi-level transactions with partial ASM updates
- Ensures recoverability with the Inverse Operation Postulate

## Abstract

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 behavior. 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.