Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1576677, author = {Štill, Vladimír and Barnat, Jiří}, address = {Cham}, booktitle = {International Conference on Software Engineering and Formal Methods}, doi = {http://dx.doi.org/10.1007/978-3-030-30446-1_20}, editor = {Ölveczky P., Salaün G.}, keywords = {termination; nontermination; local nontermination; parallel programs; c++; model checking; DIVINE}, howpublished = {tištěná verze "print"}, language = {eng}, location = {Cham}, isbn = {978-3-030-30445-4}, pages = {373-390}, publisher = {Springer}, title = {Local Nontermination Detection for Parallel C++ Programs}, url = {https://divine.fi.muni.cz/2019/lnterm/}, year = {2019} }
TY - JOUR ID - 1576677 AU - Štill, Vladimír - Barnat, Jiří PY - 2019 TI - Local Nontermination Detection for Parallel C++ Programs PB - Springer CY - Cham SN - 9783030304454 KW - termination KW - nontermination KW - local nontermination KW - parallel programs KW - c++ KW - model checking KW - DIVINE UR - https://divine.fi.muni.cz/2019/lnterm/ L2 - https://link.springer.com/chapter/10.1007/978-3-030-30446-1_20 N2 - One of the key problems with parallel programs is ensuring that they do not hang or wait indefinitely – i.e. there are no deadlocks, livelocks and the program proceeds towards its goals. In this work, we present a practical approach to detection of nonterminating sections of programs written in C or C++, and its implementation into the model checker. This complements the existing techniques for finding safety violations such as assertion failures and memory errors. Our approach makes it possible to detect partial deadlocks and livelocks, i.e. those situations in which some of the threads are progressing normally while the others are waiting indefinitely. The approach is also applicable to programs that do not terminate (such as daemons with infinite control loops) as it can be configured to check only for termination of selected sections of the program. The termination criteria can be user-provided, however, comes with the set of built-in termination criteria suited for the analysis of programs with mutexes and other common synchronisation primitives. ER -
ŠTILL, Vladimír a Jiří BARNAT. Local Nontermination Detection for Parallel C++ Programs. In Ölveczky P., Salaün G. \textit{International Conference on Software Engineering and Formal Methods}. Cham: Springer, 2019, s.~373-390. ISBN~978-3-030-30445-4. Dostupné z: https://dx.doi.org/10.1007/978-3-030-30446-1\_{}20.
|