Trace-based symbolic analysis for atomicity violations

Chao Wang; Rhishikesh Limaye; Malay Ganai; Aarti Gupta

doi:10.1007/978-3-642-12002-2_27

Trace-based symbolic analysis for atomicity violations

Chao Wang, Rhishikesh Limaye, Malay Ganai, Aarti Gupta

Computer Science

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

53 Scopus citations

Abstract

We propose a symbolic algorithm to accurately predict atomicity violations by analyzing a concrete execution trace of a concurrent program. We use both the execution trace and the program source code to construct a symbolic predictive model, which captures a large set of alternative interleavings of the events of the given trace. We use precise symbolic reasoning with a satisfiability modulo theory (SMT) solver to check the feasible interleavings for atomicity violations. Our algorithm differs from the existing methods in that all reported atomicity violations can appear in the actual program execution; and at the same time the feasible interleavings analyzed by our model are significantly more than other predictive models that guarantee the absence of false alarms.

Original language	English (US)
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.
Pages	328-342
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-642-12002-2_27
State	Published - 2010
Event	16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 - Paphos, Cyprus Duration: Mar 20 2010 → Mar 28 2010

Publication series

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

Other

Other	16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010
Country/Territory	Cyprus
City	Paphos
Period	3/20/10 → 3/28/10

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-12002-2_27

Cite this

Wang, C., Limaye, R., Ganai, M., & Gupta, A. (2010). Trace-based symbolic analysis for atomicity violations. In Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc. (pp. 328-342). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6015 LNCS). https://doi.org/10.1007/978-3-642-12002-2_27

Wang, Chao ; Limaye, Rhishikesh ; Ganai, Malay et al. / Trace-based symbolic analysis for atomicity violations. Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. 2010. pp. 328-342 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{688462c3f873420393001b3314a0c10e,

title = "Trace-based symbolic analysis for atomicity violations",

abstract = "We propose a symbolic algorithm to accurately predict atomicity violations by analyzing a concrete execution trace of a concurrent program. We use both the execution trace and the program source code to construct a symbolic predictive model, which captures a large set of alternative interleavings of the events of the given trace. We use precise symbolic reasoning with a satisfiability modulo theory (SMT) solver to check the feasible interleavings for atomicity violations. Our algorithm differs from the existing methods in that all reported atomicity violations can appear in the actual program execution; and at the same time the feasible interleavings analyzed by our model are significantly more than other predictive models that guarantee the absence of false alarms.",

author = "Chao Wang and Rhishikesh Limaye and Malay Ganai and Aarti Gupta",

year = "2010",

doi = "10.1007/978-3-642-12002-2_27",

language = "English (US)",

isbn = "3642120016",

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

pages = "328--342",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.",

note = "16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 ; Conference date: 20-03-2010 Through 28-03-2010",

}

Wang, C, Limaye, R, Ganai, M & Gupta, A 2010, Trace-based symbolic analysis for atomicity violations. in Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6015 LNCS, pp. 328-342, 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, 3/20/10. https://doi.org/10.1007/978-3-642-12002-2_27

Trace-based symbolic analysis for atomicity violations. / Wang, Chao; Limaye, Rhishikesh; Ganai, Malay et al.
Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. 2010. p. 328-342 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6015 LNCS).

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

TY - GEN

T1 - Trace-based symbolic analysis for atomicity violations

AU - Wang, Chao

AU - Limaye, Rhishikesh

AU - Ganai, Malay

AU - Gupta, Aarti

PY - 2010

Y1 - 2010

N2 - We propose a symbolic algorithm to accurately predict atomicity violations by analyzing a concrete execution trace of a concurrent program. We use both the execution trace and the program source code to construct a symbolic predictive model, which captures a large set of alternative interleavings of the events of the given trace. We use precise symbolic reasoning with a satisfiability modulo theory (SMT) solver to check the feasible interleavings for atomicity violations. Our algorithm differs from the existing methods in that all reported atomicity violations can appear in the actual program execution; and at the same time the feasible interleavings analyzed by our model are significantly more than other predictive models that guarantee the absence of false alarms.

AB - We propose a symbolic algorithm to accurately predict atomicity violations by analyzing a concrete execution trace of a concurrent program. We use both the execution trace and the program source code to construct a symbolic predictive model, which captures a large set of alternative interleavings of the events of the given trace. We use precise symbolic reasoning with a satisfiability modulo theory (SMT) solver to check the feasible interleavings for atomicity violations. Our algorithm differs from the existing methods in that all reported atomicity violations can appear in the actual program execution; and at the same time the feasible interleavings analyzed by our model are significantly more than other predictive models that guarantee the absence of false alarms.

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

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

U2 - 10.1007/978-3-642-12002-2_27

DO - 10.1007/978-3-642-12002-2_27

M3 - Conference contribution

AN - SCOPUS:77951590671

SN - 3642120016

SN - 9783642120015

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

SP - 328

EP - 342

BT - Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.

T2 - 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010

Y2 - 20 March 2010 through 28 March 2010

ER -

Wang C, Limaye R, Ganai M, Gupta A. Trace-based symbolic analysis for atomicity violations. In Tools and Algorithms for the Construction and Analysis of Systems - 16th Int. Conf., TACAS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. 2010. p. 328-342. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-12002-2_27

Trace-based symbolic analysis for atomicity violations

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this