# Specifying Transaction Control to Serialize Concurrent Program Executions

## TL;DR

This paper introduces a language-independent transaction controller and operator that transform concurrent program executions into serializable transactions, ensuring correctness and broad applicability through formal specifications in Abstract State Machines.

## Contribution

It defines a formal transaction controller and operator applicable to various programs, guaranteeing serializability and correctness in concurrent executions.

## Key findings

- Proves that concurrent runs under the transaction controller are serializable.
- Provides a formal specification of the transaction controller and operator.
- Applicable as a plug-in for specifying concurrent system components.

## Abstract

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.