Home > Research > Publications & Outputs > Extracting Safe Thread Schedules from Incomplet...

Associated organisational unit

Links

Text available via DOI:

View graph of relations

Extracting Safe Thread Schedules from Incomplete Model Checking Results

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter

Published

Standard

Extracting Safe Thread Schedules from Incomplete Model Checking Results. / Metzler, Patrick; Suri, Neeraj; Weissenbacher, Georg.

Model Checking Software: 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings. Springer, 2019. p. 153-171.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNChapter

Harvard

Metzler, P, Suri, N & Weissenbacher, G 2019, Extracting Safe Thread Schedules from Incomplete Model Checking Results. in Model Checking Software: 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings. Springer, pp. 153-171. https://doi.org/10.1007/978-3-030-30923-7_9

APA

Metzler, P., Suri, N., & Weissenbacher, G. (2019). Extracting Safe Thread Schedules from Incomplete Model Checking Results. In Model Checking Software: 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings (pp. 153-171). Springer. https://doi.org/10.1007/978-3-030-30923-7_9

Vancouver

Metzler P, Suri N, Weissenbacher G. Extracting Safe Thread Schedules from Incomplete Model Checking Results. In Model Checking Software: 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings. Springer. 2019. p. 153-171 https://doi.org/10.1007/978-3-030-30923-7_9

Author

Metzler, Patrick ; Suri, Neeraj ; Weissenbacher, Georg. / Extracting Safe Thread Schedules from Incomplete Model Checking Results. Model Checking Software: 26th International Symposium, SPIN 2019, Beijing, China, July 15–16, 2019, Proceedings. Springer, 2019. pp. 153-171

Bibtex

@inbook{cb88cc3ce18a4f558a1815f568f9f051,
title = "Extracting Safe Thread Schedules from Incomplete Model Checking Results",
abstract = "Model checkers frequently fail to completely verify a concurrent program, even if partial-order reduction is applied. The verification engineer is left in doubt whether the program is safe and the effort towards verifying the program is wasted.We present a technique that uses the results of such incomplete verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This scheduler restricts the execution to schedules that have been proven safe (and prevents executions that were found to be erroneous). We evaluate the performance of our technique and show how it can be improved using partial-order reduction. While constraining the scheduler results in a considerable performance penalty in general, we show that in some cases our approach—somewhat surprisingly—even leads to faster executions.",
author = "Patrick Metzler and Neeraj Suri and Georg Weissenbacher",
year = "2019",
month = "10",
day = "2",
doi = "10.1007/978-3-030-30923-7_9",
language = "English",
isbn = "9783030309220",
pages = "153--171",
booktitle = "Model Checking Software",
publisher = "Springer",

}

RIS

TY - CHAP

T1 - Extracting Safe Thread Schedules from Incomplete Model Checking Results

AU - Metzler, Patrick

AU - Suri, Neeraj

AU - Weissenbacher, Georg

PY - 2019/10/2

Y1 - 2019/10/2

N2 - Model checkers frequently fail to completely verify a concurrent program, even if partial-order reduction is applied. The verification engineer is left in doubt whether the program is safe and the effort towards verifying the program is wasted.We present a technique that uses the results of such incomplete verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This scheduler restricts the execution to schedules that have been proven safe (and prevents executions that were found to be erroneous). We evaluate the performance of our technique and show how it can be improved using partial-order reduction. While constraining the scheduler results in a considerable performance penalty in general, we show that in some cases our approach—somewhat surprisingly—even leads to faster executions.

AB - Model checkers frequently fail to completely verify a concurrent program, even if partial-order reduction is applied. The verification engineer is left in doubt whether the program is safe and the effort towards verifying the program is wasted.We present a technique that uses the results of such incomplete verification attempts to construct a (fair) scheduler that allows the safe execution of the partially verified concurrent program. This scheduler restricts the execution to schedules that have been proven safe (and prevents executions that were found to be erroneous). We evaluate the performance of our technique and show how it can be improved using partial-order reduction. While constraining the scheduler results in a considerable performance penalty in general, we show that in some cases our approach—somewhat surprisingly—even leads to faster executions.

U2 - 10.1007/978-3-030-30923-7_9

DO - 10.1007/978-3-030-30923-7_9

M3 - Chapter

SN - 9783030309220

SP - 153

EP - 171

BT - Model Checking Software

PB - Springer

ER -