KISS: Keep it simple and sequential

Shaz Qadeer, Dinghao Wu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

162 Citations (Scopus)

Abstract

The design of concurrent programs is error-prone due to the interaction between concurrently executing threads. Traditional automated techniques for finding errors in concurrent programs, such as model checking, explore all possible thread interleavings. Since the number of thread interleavings increases exponentially with the number of threads, such analyses have high computational complexity. In this paper, we present a novel analysis technique for concurrent programs that avoids this exponential complexity. Our analysis transforms a concurrent program into a sequential program that simulates the execution of a large subset of the behaviors of the concurrent program. The sequential program is then analyzed by a tool that only needs to understand the semantics of sequential execution. Our technique never reports false errors but may miss errors. We have implemented the technique in KISS, an automated checker for multithreaded C programs, and obtained promising initial results by using KISS to detect race conditions in Windows device drivers.

Original languageEnglish (US)
Title of host publicationProceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04)
PublisherAssociation for Computing Machinery
Pages14-24
Number of pages11
Volume1
StatePublished - 2004
EventProceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04) - Washington, DC, United States
Duration: Jun 9 2004Jun 11 2004

Other

OtherProceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04)
CountryUnited States
CityWashington, DC
Period6/9/046/11/04

Fingerprint

Hazards and race conditions
Model checking
Computational complexity
Semantics

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Qadeer, S., & Wu, D. (2004). KISS: Keep it simple and sequential. In Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04) (Vol. 1, pp. 14-24). Association for Computing Machinery.
Qadeer, Shaz ; Wu, Dinghao. / KISS : Keep it simple and sequential. Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04). Vol. 1 Association for Computing Machinery, 2004. pp. 14-24
@inproceedings{9eea858d271e4e728d6f2de3a0cd1e3f,
title = "KISS: Keep it simple and sequential",
abstract = "The design of concurrent programs is error-prone due to the interaction between concurrently executing threads. Traditional automated techniques for finding errors in concurrent programs, such as model checking, explore all possible thread interleavings. Since the number of thread interleavings increases exponentially with the number of threads, such analyses have high computational complexity. In this paper, we present a novel analysis technique for concurrent programs that avoids this exponential complexity. Our analysis transforms a concurrent program into a sequential program that simulates the execution of a large subset of the behaviors of the concurrent program. The sequential program is then analyzed by a tool that only needs to understand the semantics of sequential execution. Our technique never reports false errors but may miss errors. We have implemented the technique in KISS, an automated checker for multithreaded C programs, and obtained promising initial results by using KISS to detect race conditions in Windows device drivers.",
author = "Shaz Qadeer and Dinghao Wu",
year = "2004",
language = "English (US)",
volume = "1",
pages = "14--24",
booktitle = "Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04)",
publisher = "Association for Computing Machinery",

}

Qadeer, S & Wu, D 2004, KISS: Keep it simple and sequential. in Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04). vol. 1, Association for Computing Machinery, pp. 14-24, Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'04), Washington, DC, United States, 6/9/04.

KISS : Keep it simple and sequential. / Qadeer, Shaz; Wu, Dinghao.

Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04). Vol. 1 Association for Computing Machinery, 2004. p. 14-24.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - KISS

T2 - Keep it simple and sequential

AU - Qadeer, Shaz

AU - Wu, Dinghao

PY - 2004

Y1 - 2004

N2 - The design of concurrent programs is error-prone due to the interaction between concurrently executing threads. Traditional automated techniques for finding errors in concurrent programs, such as model checking, explore all possible thread interleavings. Since the number of thread interleavings increases exponentially with the number of threads, such analyses have high computational complexity. In this paper, we present a novel analysis technique for concurrent programs that avoids this exponential complexity. Our analysis transforms a concurrent program into a sequential program that simulates the execution of a large subset of the behaviors of the concurrent program. The sequential program is then analyzed by a tool that only needs to understand the semantics of sequential execution. Our technique never reports false errors but may miss errors. We have implemented the technique in KISS, an automated checker for multithreaded C programs, and obtained promising initial results by using KISS to detect race conditions in Windows device drivers.

AB - The design of concurrent programs is error-prone due to the interaction between concurrently executing threads. Traditional automated techniques for finding errors in concurrent programs, such as model checking, explore all possible thread interleavings. Since the number of thread interleavings increases exponentially with the number of threads, such analyses have high computational complexity. In this paper, we present a novel analysis technique for concurrent programs that avoids this exponential complexity. Our analysis transforms a concurrent program into a sequential program that simulates the execution of a large subset of the behaviors of the concurrent program. The sequential program is then analyzed by a tool that only needs to understand the semantics of sequential execution. Our technique never reports false errors but may miss errors. We have implemented the technique in KISS, an automated checker for multithreaded C programs, and obtained promising initial results by using KISS to detect race conditions in Windows device drivers.

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

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

M3 - Conference contribution

AN - SCOPUS:8344288219

VL - 1

SP - 14

EP - 24

BT - Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04)

PB - Association for Computing Machinery

ER -

Qadeer S, Wu D. KISS: Keep it simple and sequential. In Proceedings of the 2004 ACM SIGPLAN Conference on Programming Language Design and Implementaion (PLD'04). Vol. 1. Association for Computing Machinery. 2004. p. 14-24