Model-checking of correctness conditions for concurrent objects

被引：45

作者：

Alur, R

McMillan, K

Peled, D

机构：

[1] Bell Labs, Murray Hill, NJ 07974 USA

[2] Univ Penn, Dept Comp & Informat Sci, Philadelphia, PA 19003 USA

[3] Cadence Berkeley Labs, Berkeley, CA 94720 USA

[4] Technion Israel Inst Technol, IL-32000 Haifa, Israel

来源：

INFORMATION AND COMPUTATION | 2000年 / 160卷 / 1-2期

关键词：

D O I：

10.1006/inco.1999.2847

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The notions of serializability, linearizability, and sequential consistency are used in the specification of concurrent systems. We show that the model checking problem for each of these properties can be cast in terms of the containment of one regular language in another regular language shuffled using a semicommutative alphabet. The three model checking problems are shown to be, respectively, in PSPACE, in EXPSPACE, and undecidable. (C) 2000 Academic Press.

引用

页码：167 / 188

页数：22

共 11 条

[1] CHARACTERIZATIONS OF THE DECIDABILITY OF SOME PROBLEMS FOR REGULAR TRACE LANGUAGES [J].

AALBERSBERG, IJJ ;

HOOGEBOOM, HJ .

MATHEMATICAL SYSTEMS THEORY, 1989, 22 (01) :1-19

[2]

Bernstein P.A., 1987, Concurrency Control and Recovery in Database Systems

[3] NOTIONS OF CONSISTENCY AND PREDICATE LOCKS IN A DATABASE SYSTEM [J].

ESWARAN, KP ;

GRAY, JN ;

LORIE, RA ;

TRAIGER, IL .

COMMUNICATIONS OF THE ACM, 1976, 19 (11) :624-633

[4] MAXIMAL SERIALIZABILITY OF ITERATED TRANSACTIONS [J].

FLE, MP ;

ROUCAIROL, G .

THEORETICAL COMPUTER SCIENCE, 1985, 38 (01) :1-16

[5]

Gibbons P. B., 1992, Proceedings of the Fourth IEEE Symposium on Parallel and Distributed Processing (Cat. No.92TH0492-9), P317, DOI 10.1109/SPDP.1992.242728

[6] LINEARIZABILITY - A CORRECTNESS CONDITION FOR CONCURRENT OBJECTS [J].

HERLIHY, MP ;

WING, JM .

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1990, 12 (03) :463-492

[7]

LAMPORT L, 1979, IEEE T COMPUT, V28, P690, DOI 10.1109/TC.1979.1675439

[8]

LYNCH N, 1994, ATOMIC T

[9]

MAZURKIEWICZ A, 1987, LECT NOTES COMPUT SC, V255, P279

[10]

OCHMANSKI E, 1995, BOOK TRACES, P67

← 1 2 →