并发事务无死锁的可串行化调度的形式化方法  

Formal Method for Serializable Deadlock-Free Schedules of Concurrent Transactions

作　　者：罗雪梅[1] 王薇[1] 韩耀军[2] 

机构地区：[1]同济大学应用数学系,上海200092 [2]山东科技大学济南校区

出　　处：《计算机工程与应用》2004年第10期181-183,229,共4页Computer Engineering and Applications

基　　金：中国科学院计算机科学实验室开放课题资助(编号:SYSKF0304)

摘　　要：并发控制是多用户数据库管理系统(DBMS)的重要内容之一。该文对其形式化方法进行了研究,建立了符合两段锁协议的扩展有色Petri网模型。利用该模型的可达标识图,给出了判断满足两段锁协议的调度是否死锁的充分必要条件,并由此构造出并发事务的无死锁的可串行化调度。Concurrency control is one of the most important contents in DataBase Management System(DBMS ).A formal method for it is studied in this paper.An Extended Colored Petri net model for transactions concurrently accessing database is established in this paper.The model is correspondent with Two-Phase Locking Protocol(2PL).The paper gives a sufficient and necessary condition for judging if the schedules correspondent with2PL is deadlock by reachable marking graph of the model,and constructs Serializable deadlock-free schedules of concur rent transactions.

关 键 词：并发控制 可串行化 两段锁协议死锁 扩展有色Petri网 可达标识图 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]