Serialisable Multi-Level Transaction Control: A Specification and Verification

Egon Börger, Klaus-Dieter Schewe, Qing Wang

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 l…