Original title:
Instrumentace Java programů, kontrakty pro paralelismus
Translated title:
Parametric Contracts for Concurrency in Java Programs
Authors:
Žárský, Jan ; Křena, Bohuslav (referee) ; Smrčka, Aleš (advisor) Document type: Master’s theses
Year:
2021
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[cze][eng]
Kontrakty pro paralelismus slouží k vyjádření potřebné atomicity sekvencí metod ve vícevláknových programech. Tato práce se zaměřuje na implementaci dynamického analyzátoru, který verifikuje programy napsané v jazyce Java vůči kontraktům. Podporovány jsou parametrické kontrakty se spojlery. Analyzátor je implementován jako rozšíření frameworku RoadRunner. V rámci implementace analyzátoru byla do frameworku RoadRunner přidána podpora pro získávání argumentů metod a jejich návratových hodnot. Analyzátor byl plně implementován a jeho funkčnost byla ověřena na sadě testovacích programů.
Contracts for concurrency describe required atomicity of method sequences in concurrent programs. This work proposes a dynamic analyzer to verify programs written in Java against contracts for concurrency. The analyzer was designed to detect violations of parametric contracts with spoilers. The proposed analyzer was implemented as an extension to the RoadRunner framework. Support for accessing the method arguments and return values was added to RoadRunner as a part of the solution. The analyzer was fully implemented and verified on a set of testing programs.
Keywords:
concurrent programming; contracts for concurrency; dynamic analysis; instrumentation; Java; Java bytecode; RoadRunner; software verification; dynamická analýza; instrumentace; Java; Java bajtkód; kontrakty pro paralelismus; RoadRunner; verifikace softwaru; vícevláknové programování
Institution: Brno University of Technology
(web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library. Original record: http://hdl.handle.net/11012/200113