Indian Journal of Science and Technology

Abstract

Timestamp Ordering (TO) is famous concurrency control method for preserving consistency of database systems with guarantee of generating serializable schedules. Formal correctness of this method is investigated in this paper. A formal hierarchical Coloured Petri Net (CPN) model of TO method is proposed along with a case study that is composed of two transactions. Simulation run of model generates its state space that is investigated for studying correctness of TO method. Transactions of case study are designed such that a bug of this method appears. State space report shows that presented TO method in text books may face with starvation. State space explosion of model shows that TO method falls in infinite loop and therefore has starvation. Cause of this problem is presented using proposed concept of precedence graph. A method for facing with this problem is presented in this paper. Proposing new variations of TO method that inherently eliminates starvation of it is open problem.
Keywords: Coloured Petri Net, Modeling, Serializability, Starvation, Timestamp Ordering