Specifying Strict Serializability of Iterated Transactions in Propositional Temporal Logic

Authors: Walter Hussak

Abstract:

We present an operator for a propositional linear temporal logic over infinite schedules of iterated transactions, which, when applied to a formula, asserts that any schedule satisfying the formula is serializable. The resulting logic is suitable for specifying and verifying consistency properties of concurrent transaction management systems, that can be defined in terms of serializability, as well as other general safety and liveness properties. A strict form of serializability is used requiring that, whenever the read and write steps of a transaction occurrence precede the read and write steps of another transaction occurrence in a schedule, the first transaction must precede the second transaction in an equivalent serial schedule. This work improves on previous work in providing a propositional temporal logic with a serializability operator that is of the same PSPACE complete computational complexity as standard propositional linear temporal logic without a serializability operator.

Keywords: Temporal logic, iterated transactions, serializability.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1060591

References:

[1] A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, "NuSMV: a new symbolic model verifier," Lecture Notes in Computer Science, vol. 1633, pp. 495-499, 1999.
[2] E. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 1999.
[3] C.J. Date, An Introduction to Database Systems, Addison Wesley, 2004.
[4] M.P. Fle and G. Roucairol, "On serializability of iterated transactions," Proc, 1st ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pp. 194-200, 1982.
[5] M.P. Fle and G. Roucairol, "Multiserialization of iterated transactions," Information Processing Letters, vol. 18, pp. 243-247, 1984.
[6] G.J. Holzmann, The SPIN model checker. Addison-Wesley, 2004.
[7] W. Hussak, "Serializable Histories in Quantified Propositional Temporal Logic," International Journal of Computer Mathematics, vol. 81(10), pp. 1203-1211, 2004.
[8] W. Hussak and J.A. Keane, "Algebraic Specification of Serializability for Partitioned Transactions," International Journal of Computer Systems Science and Engineering, vol. 1(1), pp. 60-67, 2007.
[9] S. Katz and D. Peled, "Defining conditional independence using collapses," Theoretical Computer Science, vol. 101, pp. 337-359, 1992.
[10] C. Papadimitriou, "The Serializability of Concurrent Database Updates," Journal of ACM, vol. 26(4), pp. 631-653, 1979.
[11] D. Peled and A. Pnueli, "Proving partial order properties," Theoretical Computer Science, vol. 126, pp. 143-182, 1994.
[12] A. Pnueli, "Temporal logic of programs," Proc. 18th IEEE Symp. on Foundations of Computer Science, pp. 46-57, IEEE Computer Society Press, 1977.
[13] L. Sha, J.P. Lehoczky and E.D. Jensen, "Modular Concurrency Control and Failure Recovery," IEEE Transactions on Computers, vol. 37(2), pp. 146-159, 1988.
[14] A.P. Sistla and E.M. Clarke, "The Complexity of Propositional Linear Temporal Logics," Journal of the ACM, vol. 32, pp. 733-49, 1985.
[15] K. Vidyasankar, "Generalized Theory of Serializability," Acta Informatica, vol. 24, pp. 105-119, 1987.