Accepted author manuscript, 485 KB, PDF document
Available under license: CC BY: Creative Commons Attribution 4.0 International License
Final published version
Licence: CC BY: Creative Commons Attribution 4.0 International License
Research output: Contribution to Journal/Magazine › Journal article › peer-review
Research output: Contribution to Journal/Magazine › Journal article › peer-review
}
TY - JOUR
T1 - Extracting Safe Thread Schedules from Incomplete Model Checking Results
AU - Metzler, Patrick
AU - Suri, Neeraj
AU - Weissenbacher, Georg
PY - 2020/10/31
Y1 - 2020/10/31
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 toward 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 toward 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.
KW - Software verification
KW - Model checking
KW - Concurrency
KW - Nondeterministic scheduling
U2 - 10.1007/s10009-020-00575-y
DO - 10.1007/s10009-020-00575-y
M3 - Journal article
VL - 22
SP - 565
EP - 581
JO - International Journal on Software Tools for Technology Transfer
JF - International Journal on Software Tools for Technology Transfer
SN - 1433-2779
ER -