摘要
用带禁止/容许弧的增广Petri网构建一类带封锁机制的数据库并发控制模型,此模型适用于描述多个进程并发访问多个共享资源,采用两段锁协议解决了数据库中并发所引起的数据不一致性,并采用先进先出策略以及一次封锁法避免了由于两段锁协议所引起的死锁和活锁问题。最后,利用S-不变给出此模型的验证。
A model of database concurrency control with locking mechanism is constructed by the extended Petri Nets with inhibitor and permissive arcs. The model is applied to describing the system that has multi-processes accessing to shared resources. The data inconsistency arising as the concurrence in the database is solved by the Two-Phase Locking Protocol. The live-lock and the dead-lock caused by the Two-Phase Locking Protocol are solved by the Fist-In-Fist-Out strategy and the One-Time Locking Method respectively. Finally, the proof of the model is given by S-Invariants.
出处
《系统仿真学报》
CAS
CSCD
北大核心
2007年第A01期164-167,共4页
Journal of System Simulation
基金
国家自然科学基金(60473030)
关键词
PETRI网
禁止弧
容许弧
封锁
S-不变
形式化
Petri nets
inhibitor arcs
permissive arcs
locking
S-Invariants
formalization
