Specifying transaction control to serialize concurrent program executions

E. Börger. Specifying transaction control to serialize concurrent program executions. volume 8477, pages 142-157, DOI 10.1007/978-3-662-43652-3 13, 6, 2014.

Autoren
  • Egon Börger
BuchAbstract State Machines, Alloy, B, TLA, VDM, and Z - Proc. ABZ 2014
TypIn Konferenzband
VerlagSpringer
SerieLecture Notes of Computer Science
Band8477
DOI10.1007/978-3-662-43652-3 13
ISBN978-3-662-43651-6
Monat6
Jahr2014
Seiten142-157
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.