Efficient modeling of concurrent systems in BMC

Malay K. Ganai; Aarti Gupta

doi:10.1007/978-3-540-85114-1_10

Efficient modeling of concurrent systems in BMC

Malay K. Ganai, Aarti Gupta

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

24 Scopus citations

Abstract

We present an efficient method for modeling multi-threaded concurrent systems with shared variables and locks in Bounded Model Checking (BMC), and use it to improve the detection of safety properties such as data races. Previous approaches based on synchronous modeling of interleaving semantics do not scale up well due to the inherent asynchronism in those models. Instead, in our approach, we first create independent (uncoupled) models for each individual thread in the system, then explicitly add additional synchronization variables and constraints, incrementally, and only where such synchronization is needed to guarantee the (chosen) concurrency semantics (based on sequential consistency). We describe our modeling in detail and report verification results to demonstrate the efficacy of our approach on a complex case study.

Original language	English (US)
Title of host publication	Model Checking Software - 15th International SPIN Workshop, Proceedings
Pages	114-133
Number of pages	20
DOIs	https://doi.org/10.1007/978-3-540-85114-1_10
State	Published - 2008
Event	15th International SPIN Workshop on Model Checking of Software, SPIN 2008 - Los Angeles, CA, United States Duration: Aug 10 2008 → Aug 12 2008

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5156 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	15th International SPIN Workshop on Model Checking of Software, SPIN 2008
Country/Territory	United States
City	Los Angeles, CA
Period	8/10/08 → 8/12/08

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-85114-1_10

Cite this

@inproceedings{099068a85680473aa72808505eb80884,

title = "Efficient modeling of concurrent systems in BMC",

abstract = "We present an efficient method for modeling multi-threaded concurrent systems with shared variables and locks in Bounded Model Checking (BMC), and use it to improve the detection of safety properties such as data races. Previous approaches based on synchronous modeling of interleaving semantics do not scale up well due to the inherent asynchronism in those models. Instead, in our approach, we first create independent (uncoupled) models for each individual thread in the system, then explicitly add additional synchronization variables and constraints, incrementally, and only where such synchronization is needed to guarantee the (chosen) concurrency semantics (based on sequential consistency). We describe our modeling in detail and report verification results to demonstrate the efficacy of our approach on a complex case study.",

author = "Ganai, {Malay K.} and Aarti Gupta",

year = "2008",

doi = "10.1007/978-3-540-85114-1_10",

language = "English (US)",

isbn = "3540851135",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "114--133",

booktitle = "Model Checking Software - 15th International SPIN Workshop, Proceedings",

note = "15th International SPIN Workshop on Model Checking of Software, SPIN 2008 ; Conference date: 10-08-2008 Through 12-08-2008",

}

Ganai, MK & Gupta, A 2008, Efficient modeling of concurrent systems in BMC. in Model Checking Software - 15th International SPIN Workshop, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5156 LNCS, pp. 114-133, 15th International SPIN Workshop on Model Checking of Software, SPIN 2008, Los Angeles, CA, United States, 8/10/08. https://doi.org/10.1007/978-3-540-85114-1_10

Efficient modeling of concurrent systems in BMC. / Ganai, Malay K.; Gupta, Aarti.
Model Checking Software - 15th International SPIN Workshop, Proceedings. 2008. p. 114-133 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5156 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Efficient modeling of concurrent systems in BMC

AU - Ganai, Malay K.

AU - Gupta, Aarti

PY - 2008

Y1 - 2008

N2 - We present an efficient method for modeling multi-threaded concurrent systems with shared variables and locks in Bounded Model Checking (BMC), and use it to improve the detection of safety properties such as data races. Previous approaches based on synchronous modeling of interleaving semantics do not scale up well due to the inherent asynchronism in those models. Instead, in our approach, we first create independent (uncoupled) models for each individual thread in the system, then explicitly add additional synchronization variables and constraints, incrementally, and only where such synchronization is needed to guarantee the (chosen) concurrency semantics (based on sequential consistency). We describe our modeling in detail and report verification results to demonstrate the efficacy of our approach on a complex case study.

AB - We present an efficient method for modeling multi-threaded concurrent systems with shared variables and locks in Bounded Model Checking (BMC), and use it to improve the detection of safety properties such as data races. Previous approaches based on synchronous modeling of interleaving semantics do not scale up well due to the inherent asynchronism in those models. Instead, in our approach, we first create independent (uncoupled) models for each individual thread in the system, then explicitly add additional synchronization variables and constraints, incrementally, and only where such synchronization is needed to guarantee the (chosen) concurrency semantics (based on sequential consistency). We describe our modeling in detail and report verification results to demonstrate the efficacy of our approach on a complex case study.

UR - http://www.scopus.com/inward/record.url?scp=54249087637&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=54249087637&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-85114-1_10

DO - 10.1007/978-3-540-85114-1_10

M3 - Conference contribution

AN - SCOPUS:54249087637

SN - 3540851135

SN - 9783540851134

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 114

EP - 133

BT - Model Checking Software - 15th International SPIN Workshop, Proceedings

T2 - 15th International SPIN Workshop on Model Checking of Software, SPIN 2008

Y2 - 10 August 2008 through 12 August 2008

ER -

Efficient modeling of concurrent systems in BMC

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this