Specifying Transaction Control to Serialize Concurrent Program Executions
This work addresses concurrency control for system specification, but it is incremental as it builds on existing Abstract State Machines frameworks.
The authors tackled the problem of ensuring serializable behavior in concurrent programs with shared locations by defining a transaction controller and operator, proving that concurrent runs under this controller are serializable.
We define a programming language independent transaction controller and an operator which when applied to concurrent programs with shared locations 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. We specify the transaction controller TaCtl and the operator TA in terms of Abstract State Machines. This makes TaCtl applicable to a wide range of programs and in particular provides the possibility to use it as a plug-in when specifying concurrent system components in terms of Abstract State Machines.