HP Labs Technical Reports
Click here for full text:
Modeling Serializability via Process Equivalence in Petri Nets
De Francesco, Nicoletta; Montanari, Ugo; Ristori, Gioia
Abstract: Concurrency control  concerns the monitoring of a set of activities (transactions) concurrently accessing the database in a multiuser database management system. In the paper a transaction system is modeled by a condition/event Petri net, in which the events of the net are the operations of the transactions and the conditions correspond to the objects, while each schedule corresponds to a firing sequence of the net. The net is seen as a program schema, representing the uninterpreted flow of control and data of a program: the conditions correspond to the data values, while the events correspond to the operations. Thus firing sequences may be seen as computations of the program schema and, moreover, the result of a computation can be defined as the value of the conditions holding in the final case. pp In the paper we prove that the semantics of a net, in terms of processes, is isomorphic to the semantics of the net seen as a program schema or, put in another way, two firing sequences compute the same value (for every interpretation of the operations) if, and only if, they are linearizations of the same process. As a result, we generalize concurrency control to any program schema, not necessarily corresponding to a transaction system.
Back to Index