Detail publikace
Pointer Race Freedom
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Meyer Roland (UNIKL)
Wolf Sebastian (UNIKL)
ukazatelový závod
svoboda od ukazatelových závodů
modulární verifikace
Navrhujem pojem ukazatelový závod, analogický známému pojmu datový závod, a studujeme jeho semantické důsledky. Ukazujeme, jak je jej možné použít k zefetktivnění verifikace paralelních programů rozdělením verifikačního úsilí na 1) ověření, že program neobsahuje ukazatelové závody, a 2) ověření původní vlastnosti s pomocí předpokladu z bodu 1.
Navrhujem pojem ukazatelový závod, analogický známému pojmu datový závod, a studujeme jeho semantické důsledky. Ukazujeme, jak je jej možné použít k zefetktivnění verifikace paralelních programů rozdělením verifikačního úsilí na 1) ověření, že program neobsahuje ukazatelové závody, a 2) ověření původní vlastnosti s pomocí předpokladu z bodu 1.
@INPROCEEDINGS{FITPUB11065, author = "Fr\'{e}d\'{e}ric Haziza and Luk\'{a}\v{s} Hol\'{i}k and Roland Meyer and Sebastian Wolf", title = "Pointer Race Freedom", pages = "393--412", booktitle = "Verification, Model Checking, and Abstract Interpretation (VMCAI)", series = "Lecture Notes in Computer Science", volume = 9583, year = 2016, location = "Berlin, DE", publisher = "Springer Verlag", ISBN = "978-3-662-49121-8", doi = "10.1007/978-3-662-49122-5\_19", language = "english", url = "https://www.fit.vut.cz/research/publication/11065" }