TY - GEN
T1 - Parallel assertions for debugging parallel programs
AU - Schwartz-Narbonne, Daniel
AU - Liu, Feng
AU - Pondicherry, Tarun
AU - August, David
AU - Malik, Sharad
PY - 2011
Y1 - 2011
N2 - A parallel program must execute correctly even in the presence of unpredictable thread interleavings. This interleaving makes it hard to write correct parallel programs, and also makes it hard to find bugs in incorrect parallel programs. A range of tools have been developed to help debug parallel programs, ranging from atomicity-violation and data-race detectors to model-checkers and theorem provers. One technique that has been successful for debugging sequential programs, but less effective for parallel programs, is running the program using assertion predicates provided by the developer. These assertions allow programmers to specify and check their assumptions. In a multi-threaded program, the programmer's assumptions include both the current state, and any actions (e.g. access to shared memory) that other, parallel executing threads might take. We introduce parallel assertions which allow programmers to express these assumptions for parallel programs using simple and intuitive syntax and semantics. We present a proof-of-concept implementation, and demonstrate its value by testing a number of benchmark programs using parallel assertions.
AB - A parallel program must execute correctly even in the presence of unpredictable thread interleavings. This interleaving makes it hard to write correct parallel programs, and also makes it hard to find bugs in incorrect parallel programs. A range of tools have been developed to help debug parallel programs, ranging from atomicity-violation and data-race detectors to model-checkers and theorem provers. One technique that has been successful for debugging sequential programs, but less effective for parallel programs, is running the program using assertion predicates provided by the developer. These assertions allow programmers to specify and check their assumptions. In a multi-threaded program, the programmer's assumptions include both the current state, and any actions (e.g. access to shared memory) that other, parallel executing threads might take. We introduce parallel assertions which allow programmers to express these assumptions for parallel programs using simple and intuitive syntax and semantics. We present a proof-of-concept implementation, and demonstrate its value by testing a number of benchmark programs using parallel assertions.
UR - http://www.scopus.com/inward/record.url?scp=80052105280&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80052105280&partnerID=8YFLogxK
U2 - 10.1109/MEMCOD.2011.5970525
DO - 10.1109/MEMCOD.2011.5970525
M3 - Conference contribution
AN - SCOPUS:80052105280
SN - 9781457701160
T3 - 9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011
SP - 181
EP - 190
BT - 9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011
T2 - 9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011
Y2 - 11 July 2011 through 13 July 2011
ER -