Testing Multi-Threaded Applications Using Answer Set Programming

Xiaozhen Xue, Sima Siami-Namini, Akbar Siami Namin

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

Abstract

We introduce a technique to formally represent and specify race conditions in multithreaded applications. Answer set programming (ASP) is a logic-based knowledge representation paradigm to formally express belief acquired through reasoning in an application domain. The transparent and expressiveness representation of problems along with powerful non-monotonic reasoning power enable ASP to abstractly represent and solve some certain classes of NP hard problems in polynomial times. We use ASP to formally express race conditions and thus represent potential data races often occurred in multithreaded applications with shared memory models. We then use ASP to generate all possible test inputs and thread interleaving, i.e. scheduling, whose executions would result in deterministically exposing thread interleaving failures. We evaluated the proposed technique with some moderate sized Java programs, and our experimental results confirm that the proposed technique can practically expose common data races in multithreaded programs with low false positive rates. We conjecture that, in addition to generating threads scheduling whose execution order leads to the exposition of data races, ASP has several other applications in constraint-based software testing research and can be utilized to express and solve similar test case generation problems where constraints play a key role in determining the complexity of searches.

Original languageEnglish
Pages (from-to)1151-1175
Number of pages25
JournalInternational Journal of Software Engineering and Knowledge Engineering
Volume28
Issue number8
DOIs
StatePublished - Aug 1 2018

Keywords

  • Answer set programming
  • concurrent programs
  • interleaving

Fingerprint Dive into the research topics of 'Testing Multi-Threaded Applications Using Answer Set Programming'. Together they form a unique fingerprint.

Cite this